[isabelle] residual subgoals



Hi,

following

http://stackoverflow.com/questions/35156803/sledgehammer-gives-insufficient-proof-tactic

I created

theory Even
imports Main

begin

inductive
  structural_even :: "nat â bool"
where
  "structural_even 0"
| "structural_even n â structural_even (Suc(Suc n))"

fun
  computational_even :: "nat â bool"
where
  "computational_even 0 = True"
| "computational_even (Suc 0) = False"
| "computational_even (Suc(Suc n)) = computational_even n"

lemma "computational_even n â structural_even n"
proof (induct n rule: computational_even.induct)
show "computational_even 0 â structural_even 0"
  by (metis structural_even.intros(1))
next
show "computational_even (Suc 0) â structural_even (Suc 0)"
  by (metis computational_even.simps(2))
next
show "ân. (computational_even n â structural_even n) â computational_even (Suc (Suc n)) â structural_even (Suc (Suc n))"
  proof
   fix n
   assume "computational_even n â structural_even n"
   from this show "computational_even (Suc (Suc n)) â structural_even n"
    by (simp only: computational_even.simps(3))
  qed
qed

end

--

before the last qed, the Output window says

goal (4 subgoals):
1. computational_even 0 â computational_even 0
2. computational_even (Suc 0) â computational_even (Suc 0)
3. ân. (computational_even n â structural_even n) â
         computational_even (Suc (Suc n)) â computational_even n â structural_even n
4. ân. (computational_even n â structural_even n) â
         computational_even (Suc (Suc n)) â computational_even (Suc (Suc n))

These all seem trivial and qed does overcome them.

Is it standard practice not to bother these but postpone solving them via the final qed?

- Gergely












This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.