伊莎贝尔中~pvq形式的归纳法证明定理

Question

我有一个叫做反馈的函数，它计算3的幂(即)

反馈(T)= 3^t

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

我想证明

如果t>5，则反馈(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

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