证明伊莎贝尔自然递归"less than"定义的基本性质

Question

为了学习，我试图重新创建自然数的简化版本(因为它涉及归纳定义、递归函数等(。然而，在这个过程中，我遇到了一些我认为非常琐碎的事情。

基本上，我有一个自然数"natt"的定义和一个"<"关系的定义：

datatype natt = Zero | Succ natt
primrec natt_less :: "natt ⇒ natt ⇒ bool" (infixl "<" 75) where
"natt_less n Zero = False"
| "natt_less n (Succ m') = (case n of Zero ⇒ True | Succ n' ⇒ natt_less n' m')"

由此，我试图证明<关系的3个基本性质：

1. 非自反性：~ (a < a)
2. 非对称：a < b ⟹ ~ (b < a)
3. 传递性：a < b ⟹ b < c ⟹ a < c

我能够证明第一个，但不能证明其他。更让我惊讶的是，有一些子引理可以帮助解决这些问题，比如Succ a < b ⟹ a < b、a < b ⟹ a < Succ b或a < b ∨ a = b ∨ b < a，它们看起来更微不足道，但尽管如此，即使在多次尝试之后，我也无法证明。似乎只有其中一个(包括2.和3.(足以证明其余的，但我无法证明其中的任何。

我主要尝试使用归纳法。再加上我自己定义的事实，有两种可能性——要么我的定义是错误的，没有所需的属性，要么我缺少一些方法/参数。所以，我有两个问题：

1. 我的定义是错误的吗(即，它不能准确地表示<，并且缺乏所需的属性(？如果是，我该如何修复
2. 如果不是，我该如何证明这些看似微不足道的性质

---

就上下文而言，我目前的尝试是通过归纳法进行的，我可以证明基本情况，但总是被困在归纳法中，不知道该如何处理假设，例如在本例中：

lemma less_Succ_1: "Succ a < b ⟹ a < b"
proof (induction b)
case Zero
assume "Succ a < Zero"
then have "False" by simp
then show ?case by simp
next 
case (Succ b)
assume "(Succ a < b ⟹ a < b)" "Succ a < Succ b"
then show "a < Succ b" oops

Answer 1

经过user9716869的一些提示，很明显，我的主要问题是对induction中的arbitrary选项缺乏了解。使用(induction _ arbitrary: _)和(cases _)(详见参考手册(，证明是非常直接的。

既然这些都是为了教育目的，下面的证明并不是为了简洁，而是为了让每一步都非常清楚。如果需要更多的自动化，其中大多数可以大大减少，有些可以在一行中完成(我在引理下面留下了一条评论(。

---

注意：在这些证明中，我们使用了一个关于归纳类型的隐引理，它们的内射性(暗示(Succ a = Succ b) ≡ (a = b)和Zero ≠ Succ a(。此外，定义为(Succ a < Succ b) ≡ (a < b)

首先，我们证明了两个有用的引理：

• a < b ⟹ b ≠ Zero
• b ≠ Zero ⟷ (∃ b'. b = Succ b')

lemma greater_not_Zero [simp]: "a < b ⟹ b ≠ Zero"
(*by clarsimp*)
proof
assume "a < b" "b = Zero"
then have "a < Zero" by simp
then show "False" by simp
qed
lemma not_Zero_is_Succ: "b ≠ Zero ⟷ (∃ b'. b = Succ b')"
(*by (standard, cases b) auto*)
proof
show "b ≠ Zero ⟹ ∃ b'. b = Succ b'"
proof (cases b)
case Zero
assume ‹b ≠ Zero› 
moreover note ‹b = Zero›
ultimately show "∃b'. b = Succ b'" by contradiction
next
case (Succ b')
assume ‹b ≠ Zero› 
note ‹b = Succ b'› 
then show "∃b'. b = Succ b'" by simp
qed
next
assume "∃ b'. b = Succ b'"
then obtain b'::natt where "b = Succ b'" by clarsimp
then show "b ≠ Zero" by simp
qed

有了这些，我们可以证明三个主要的陈述：

• 非自反性：~ (a < a)
• 非对称：a < b ⟹ ~ (b < a)
• 传递性：a < b ⟹ b < c ⟹ a < c

lemma less_not_refl [simp]: "¬ a < a"
(*by (induction a) auto*)
proof (induction a)
case Zero
show "¬ Zero < Zero" by simp
next
case (Succ a)
note IH = ‹¬ a < a›
show "¬ Succ a < Succ a" 
proof
assume "Succ a < Succ a"
then have "a < a" by simp
then show "False" using IH by contradiction
qed
qed
lemma less_not_sym: "a < b ⟹ ¬ b < a"
proof (induction a arbitrary: b)
case Zero
then show "¬ b < Zero" by simp
next
case (Succ a)
note IH = ‹⋀b. a < b ⟹ ¬ b < a› 
and IH_prems = ‹Succ a < b›
show "¬ b < Succ a"
proof
assume asm:"b < Succ a"
have "b ≠ Zero" using IH_prems by simp
then obtain b'::natt where eq: "b = Succ (b')" 
using not_Zero_is_Succ by clarsimp
then have "b' < a" using asm by simp
then have "¬ a < b'" using IH by clarsimp
moreover have "a < b'" using IH_prems eq by simp
ultimately show "False" by contradiction
qed
qed
lemma less_trans [trans]: "a < b ⟹ b < c ⟹ a < c"
proof (induction c arbitrary: a b)
case Zero
note ‹b < Zero›
then have "False" by simp
then show ?case by simp
next 
case (Succ c)
note IH = ‹⋀a b. a < b ⟹ b < c ⟹ a < c› 
and IH_prems = ‹a < b› ‹b < Succ c›
show "a < Succ c"
proof (cases a)
case Zero
note ‹a = Zero›
then show "a < Succ c" by simp 
next 
case (Succ a')
note cs_prem = ‹a = Succ a'›
have "b ≠ Zero" using IH_prems by simp
then obtain b' where b_eq: "b = Succ b'" 
using not_Zero_is_Succ by clarsimp
then have "a' < b'" using IH_prems cs_prem b_eq by simp
moreover have "b' < c" using IH_prems b_eq by simp
ultimately have "a' < c" using IH by simp
then show "a < Succ c" using cs_prem by simp
qed
qed