*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] residual subgoals*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 3 Feb 2016 12:23:55 +0100*In-reply-to*: <C32D3449D568C445AB18C60817FABFE10144E5188658@ingrid.foiskola.krf>*References*: <C32D3449D568C445AB18C60817FABFE10144E5188657@ingrid.foiskola.krf> <56B1CC57.2050707@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144E5188658@ingrid.foiskola.krf>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

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

**References**:**[isabelle] residual subgoals***From:*Buday Gergely

**Re: [isabelle] residual subgoals***From:*Lars Hupel

**Re: [isabelle] residual subgoals***From:*Buday Gergely

- Previous by Date: Re: [isabelle] residual subgoals
- Next by Date: Re: [isabelle] residual subgoals
- Previous by Thread: Re: [isabelle] residual subgoals
- Next by Thread: Re: [isabelle] residual subgoals
- Cl-isabelle-users February 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list