Правильность определения функции проверки в Isabelle

Question

Я хочу доказать правильность определения функции, используя определение ключевого слова function. Вот определение функции сложения по обычному индуктивному определению натуральных чисел:

theory FunctionDefinition 
imports Main 

begin 

datatype natural = Zero | Succ natural 

function add :: "natural => natural => natural" 
where 
    "add Zero  m = m" 
| "add (Succ n) m = Succ (add n m)" 

Isabelle/JEdit показывает мне следующие подзадачи:

goal (4 subgoals): 
1. ⋀P x. (⋀m. x = (Zero, m) ⟹ P) ⟹ (⋀n m. x = (Succ n, m) ⟹ P) ⟹ P 
2. ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma 
3. ⋀m n ma. (Zero, m) = (Succ n, ma) ⟹ m = Succ (add_sumC (n, ma)) 
4. ⋀n m na ma. (Succ n, m) = (Succ na, ma) ⟹ Succ (add_sumC (n, m)) = Succ (add_sumC (na, ma)) 
Auto solve_direct: ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma can be solved directly with 
    Product_Type.Pair_inject: (?a, ?b) = (?a', ?b') ⟹ (?a = ?a' ⟹ ?b = ?b' ⟹ ?R) ⟹ ?R 

с использованием

apply (auto simp add: Product_Type.Pair_inject) 

Я получаю

goal (1 subgoal): 
1. ⋀P a b. (⋀m. a = Zero ∧ b = m ⟹ P) ⟹ (⋀n m. a = Succ n ∧ b = m ⟹ P) ⟹ P 

Непонятно, как действовать. На самом деле, это правильный способ решить эту проблему?

Я знаю, что Изабель сделает это автоматически, если я использую определение fun - я хочу узнать, как это сделать вручную.

Answer 1

tutorial on the function package упоминается в разделе 3, fun f where ...

сокращает

function (sequential) f where ... 
by pat_completeness auto 
termination by lexicographic_order 

Здесь pat_completeness является методом доказательства от function пакета, который автоматизирует доказательство полноты для моделей типа данных конструкторов. Это первый подзаголовок, который вам нужно доказать. Рекомендуется применять pat_completeness до auto, потому что auto изменяет синтаксическую структуру цели, а pat_completeness может не работать после авто.

Если вы хотите доказать полноту рисунка без pat_completeness, вы должны попытаться проанализировать все параметры функции, т. Е. case_tac a в вашем примере.

Answer 2

Manuel уже упомянул об этом в своем комментарии, но я подумал, что более подробный пример может быть полезен в любом случае. Вот что вы можете сделать вручную:

Сначала вы определяете вашу функцию как обычно

function add :: "natural => natural => natural" 
where 
    "add Zero  m = m" | 
    "add (Succ n) m = Succ (add n m)" 

а затем доказать, что данные модели охватывают все случаи по

by (pat_completeness) auto 

Затем вы заботитесь о прекращение. Например, каждый datatype поставляется с функцией size, и вы можете заметить, что первый аргумент add строго уменьшается в размере для каждого рекурсивного вызова. По умолчанию function будет объединять все аргументы функции в кортеж для прекращения доказательства, то есть, вместо того, чтобы два аргументов n и m, в прекращении доказательства вы работаете с одного парой (n, m).Таким образом, если вы хотите, чтобы сообщить системе, что он должен использовать размер аргумента первый вы можете сделать это следующим образом:

termination add 
    apply (relation "measure (size o fst)") 

Это даст оставшиеся цели:

goal (2 subgoals): 
1. wf (measure (size o fst)) 
2. !!n m. ((n, m), Succ n, m) : measure (size o fst) 

То есть , вы должны показать, что данное соотношение является обоснованным (что является тривиальным для measure s, которые всегда являются обоснованными, поскольку они построены путем сопоставления аргументов натуральным числам, а затем используют меньше, чем на naturals как отношение) и, что для каждого рекурсивного вызова t аргументы на самом деле находятся в данном соотношении. Оба гола легко отправляются simp.

apply simp 
    apply simp 
done