在 Isabelle 中使用归纳法证明 ~pvq 形式的定理

Question

我有一个称为反馈的函数，它计算 3 的幂（即）

反馈（t）= 3^t

primrec feedback :: "nat ⇒ nat" where
"feedback 0 = Suc(0)"|
"feedback (Suc t) = (feedback t)*3"

我想证明

if t > 5 then feedback(t) > 200

使用归纳法

lemma th2: "¬(t>5) ∨ ((feedback t) > 200)" (is "?H(t)" is "?P(t)∨?Q(t)" is "(?P(t))∨(?F(t) > 200)")  
proof(induct t) 
   case 0 show "?P 0 ∨ ?Q 0" by simp
next 
   assume a:" ?F(t) > 200"
   assume d: "?P(t) = False"
   have b: "?F (Suc(t)) ≥ ?F(t)" by simp
   from b and a have c: "?F(Suc(t)) > 200" by simp
   from c have e: "?Q(Suc(t))" by simp
   from d have f:"?P(Suc(t)) = False" by simp
   from f and e have g: "?P(Suc(t))∨?Q(Suc(t))" by simp
   from a and d and g have h: "?P(t)∨?Q(t) ⟹ ?P(Suc(t))∨?Q(Suc(t))" by simp 
   from a and d have "?H(Suc(t))" by simp
qed

首先我证明

反馈(t+1) >=反馈(t)
然后假设反馈(t) > 200，所以反馈(t+1)>200
假设 t>5
这意味着 (t+1) > 5
另外~((t+1)>5)V(反馈(t+1)>200)为真
因此如果 P(t) 为真则 P(t+1) 为真

但这不起作用。我不知道问题是什么

Answer 1

嗯，首先，你不能简单地假设 Isar 中的任意事情。或者更确切地说，你可以那样做，但你做完之后将无法显示你的目标。 Isar 允许您假设的事情非常严格；在你的情况下，它是 ¬ 5 < t ∨ 200 < feedback t.

我建议使用 case 命令，它会为您假设正确的事情。然后你可以对这个析取做一个案例区分，然后另一个关于是否 t = 5:

lemma th2: "¬(t>5) ∨ ((feedback t) > 200)"  
proof (induct t) 
  case 0
  show ?case by simp
next
  case (Suc t)
  thus ?case
  proof
    assume "¬t > 5"
    moreover have "feedback 6 = 729" by code_simp 
      -- ‹"simp add: eval_nat_numeral" would also work›
    ultimately show ?thesis
      by (cases "t = 5") auto
  next
    assume "feedback t > 200"
    thus ?thesis by simp
  qed
qed

或者，更简洁：

lemma th2: "¬(t>5) ∨ ((feedback t) > 200)"  
proof (induct t) 
  case (Suc t)
  moreover have "feedback 6 = 729" by code_simp
  ultimately show ?case by (cases "t = 5") auto
qed simp_all

如果你的反馈函数实际上是单调的，我会建议先证明这一点，然后证明会变得不那么乏味。

在 Isabelle 中使用归纳法证明 ~pvq 形式的定理

Proving theorem of the form ~pvq using Induction in Isabelle

isabelle