Email Gateway (Aug 22 2022 at 18:24): Email Gateway (Aug 22 2022 at 18:24):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Consider the following inductive definition and a simple lemma about it:
inductive ev' :: "nat ⇒ bool" where
ev'_0: "ev' 0" |
ev'_2: "ev' 2" |
ev'_sum: "ev' n ⟹ ev' m ⟹ ev' (n+m)"
lemma test1: "ev' n ⟹ ev' (n + 2)"
apply (rule ev'_sum)
by (simp_all add: ev'_2)
But when I tried to prove the lemma using simp:
by (simp add: ev'_sum ev'_2)
Isabelle seems to try to turn the (n+2) into (Suc (Suc n)) and then get
stuck:
Failed to finish proof⌂:
goal (1 subgoal):
Is there a way to tell Isabelle not to do that?
Thanks!
Last updated: Apr 25 2024 at 01:08 UTC