Re: [isabelle] reasoning with even and odd numbers


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

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

    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.


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