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, false.

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.


Cheers,

Manuel


On 03/02/16 11:50, Buday Gergely wrote:
Hi Lars,

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
use meta-implication:

   <https://stackoverflow.com/a/25442787/4776939>
Thanks. Re-formulating my goal I wrote

lemma
  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?

- Gergely





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