*To*: Amarin Phaosawasdi <phaosaw2 at illinois.edu>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] reasoning with even and odd numbers*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sun, 19 Oct 2014 20:47:19 +0200*In-reply-to*: <54440117.3010909@illinois.edu>*References*: <543DEC15.1020302@illinois.edu> <543E0F72.70108@in.tum.de> <54440117.3010909@illinois.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2

Hallo, On 19.10.2014 20:21, Amarin Phaosawasdi wrote: > How did evE[elim!] help me with, for example, "¬ev (Suc 0)"? The typical way of proving negations is by assuming the statement holds and deriving False. You can do this with the rule notI: lemma "¬ev (Suc 0)" apply (rule notI) This leaves you with goal (1 subgoal): 1. ev (Suc 0) ⟹ False Now you can use evE to perform a case distinction on ‘ev (Suc 0)’: if ‘ev (Suc 0)’ holds, it was either derived by ev0 (in which case ‘Suc 0’ would have to be ‘0’) or it was derived by evSS (in which case ‘Suc 0’ would have to be ‘Suc (Suc n)’ for some n). Both are trivially false and can be discharged by ‘simp_all’. lemma "¬ev (Suc 0)" apply (rule notI) apply (erule evE) apply simp_all done It should be mentioned that your evE is the same as the automatically-proved ev.cases. inductive_cases is for deriving more specialised elimination rules, i.e. ones where you don't have ‘ev n’, but something more restricted, such as ‘ev 0’ or ‘ev (Suc n)’ or ‘ev (Suc (Suc n))’. inductive_cases simply uses the ev.cases rule and performs some simplification on it. In your case, you could do the following: inductive_cases evS: "ev (Suc n)" Then, in the above proof of ‘¬ev (Suc 0)’, you applying the elimination rule would leave you with the goal ‘Suc 0 = 0’. In this case, it doesn't make much difference though – you might as well just use ev.cases. Also, I would like to say that declaring rules as elimination rules ([elim]), especially safe ones ([elim!]) should be done with care. The evE rule you defined is probably not a good choice for an automatic elimination rule, since it doesn't always make the goal ‘simpler’ and can be applied infinitely often, blowing the goal up indefinitely. In these examples, it all works out, but in more complicated ones, auto (and force, blast, etc.) might loop because of it, applying the rule infinitely often. Cheers, Manuel

**References**:**[isabelle] reasoning with even and odd numbers***From:*Amarin Phaosawasdi

**Re: [isabelle] reasoning with even and odd numbers***From:*Manuel Eberl

**Re: [isabelle] reasoning with even and odd numbers***From:*Amarin Phaosawasdi

- Previous by Date: Re: [isabelle] reasoning with even and odd numbers
- Next by Date: Re: [isabelle] Raw proof blocks
- Previous by Thread: Re: [isabelle] reasoning with even and odd numbers
- Next by Thread: Re: [isabelle] reasoning with even and odd numbers
- Cl-isabelle-users October 2014 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