2

我试图证明如果n > 0那么g n b = True（见下文）的定理。情况就是这样，因为g (Suc n) b只有调用g 0 True. 不幸的是，当我试图证明时，我的归纳中没有这个事实g 0 b。我怎样才能完成证明（我必须用什么代替sorry）？

fun g :: "nat ⇒ bool ⇒ bool" where
  "g (Suc n) b = g n True" |
  "g 0 b = b"

theorem 
    fixes n::nat and b::bool
    assumes "n > 0"
    shows "g n b"
proof (induct n b rule: g.induct)
    fix n 
    fix b
    assume "g n True"
    thus "g (Suc n) b" by (metis g.simps(1))
next
    fix b
    show "g 0 b" sorry
qed
4

1 回答 1

6

n > 0你忘了在你的归纳中使用这个假设。

例如，你可以写

theorem 
  fixes n::nat and b::bool
  assumes "n > 0"
  shows "g n b"
using assms (* this is important *)
proof (induct n b rule: g.induct)
  case (1 n b)
  thus ?case by (cases n) auto
next
  case (2 b)
  thus ?case by auto
qed

或者，您可以立即像这样开始您的定理并进一步缩短它：

theorem "n > 0 ==> g n b"
proof (induct n b rule: g.induct)
  case (1 n b)
  thus ?case by (cases n) auto
qed auto
于 2013-09-25T17:45:04.650 回答