function - 证明 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

尚不清楚如何继续。到底，这是解决这个问题的正确方法吗？

我知道如果我使用有趣定义，Isabelle 会自动执行此操作 - 我想学习如何手动执行此操作。

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包中的一个证明方法，它可以自动证明数据类型构造函数模式的完整性。这是您必须证明的第一个子目标。建议在 auto 之前应用 pat_completeness，因为 auto 会更改目标的语法结构，而 pat_completeness 可能不会自动后工作。

如果您想在没有 pat_completeness 的情况下证明模式完整性，您应该尝试对所有函数参数进行案例分析，即示例中的 case_tac a。