Re: [isabelle] residual subgoals



Am Mittwoch, den 03.02.2016, 11:50 +0100 schrieb Buday Gergely:
> 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)

You need to add the assumption with "using":

    assumes "computational_even n"
    shows "structural_even n"
>>  using assms
  proof (induct n rule:computational_even.induct)

Then your 2. goal should state:

  computational_even (Suc 0) ==> structural_even (Suc 0)

Which is true as "computational_even (Suc 0) = False"

 - Johannes

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