Re: [isabelle] residual subgoals
You are not using your assumption at all, so effectively, you're trying
to show that /every/ number n is structurally even, which is, of course,
Chain in the assumption by putting a "using assms" in front of your
"proof". Then you will have the additional assumption
"computational_even (Suc 0)" in the second case, and that should be
false, which means the second case is trivially provable.
On 03/02/16 11:50, Buday Gergely wrote:
Is it standard practice not to bother these but postpone solving them via
the final qed?
I'd say it's not standard practice. Most Isabelle users prefer not using meta-
implications and meta-quantification in Isar proofs if it can be avoided. See
Lars Noschinski's answer here for a case where it actually doesn't work if you
Thanks. Re-formulating my goal I wrote
fixes n :: "nat"
assumes "computational_even n"
shows "structural_even n"
proof (induct n rule:computational_even.induct)
which results in
goal (3 subgoals):
1. structural_even 0
2. structural_even (Suc 0)
3. ân. structural_even n â structural_even (Suc (Suc n))
where the 2nd subgoal is simply not true.
What is wrong with that lemma expression?
This archive was generated by a fusion of
Pipermail (Mailman edition) and