*To*: 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*: Wed, 15 Oct 2014 08:08:50 +0200*In-reply-to*: <543DEC15.1020302@illinois.edu>*References*: <543DEC15.1020302@illinois.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Hallo, On 15/10/14 05:37, Amarin Phaosawasdi wrote: > Q1: Is there anyway to simplify "evSS[OF evSS[OF ev0]]" on the fly > such that I don't need the lemma "four_is_even"? By ‘simplify’, you probably mean ‘derive automatically’. evSS[OF evSS[OF ev0]] is basically a ‘hand-crafted proof’ where you put together the existing lemmas by hand to derive a new lemma. Isabelle proof methods like simp and auto basically do the same thing automatically in the background. You have correctly deduced that the problem here is that in order to apply the introduction rules for ev (ev0 and evSS), the goal must be in the shape ‘ev 0’ or ‘ev (n + 2)’. This is what your subgoal_tac achieves. When the goal /is/ in that shape, you can simply apply the introduction rules for ev to solve it: > apply (rule evSS) > apply (rule evSS) > apply (rule ev0) Or shorter: > apply (rule evSS ev0)+ Or even shorter: > apply (intro evSS ev0) Or this: > apply (intro ev.intros) The entire proof: > lemma "ev 4" > proof- > have "(4::nat) = 0 + 2 + 2" by simp > also have "ev (0 + 2 + 2)" by (intro ev.intros) > finally show ?thesis . > qed Now, as for the matter of getting from ‘4’ to ‘Suc (Suc (Suc (Suc 0)))’: the representation of numeral constants (such as 4) in Isabelle is a bit tricky for technical reasons. There is a collection of rewrite rules to convert something like ‘4’ into its ‘Suc’ notation. It is called eval_nat_numeral. If you write > lemma "ev 4" > apply (simp only: eval_nat_numeral) you get the new goal "ev (Suc (Suc (Suc (Suc 0))))". You can usually also use ‘simp add: eval_nat_numeral’, the ‘only’ just means that /only/ the given rules will be applied, which can be useful sometimes. The problem is that evSS cannot be applied then, because they want the form ‘ev (n + 2)’. Therefore, I would recommend to define the inductive differently: > inductive ev :: "nat ⇒ bool" where > ev0: "ev 0" | > evSS: "ev n ⟹ ev (Suc (Suc n))" Then you can simply prove even ‘ev 1000’ easily: > lemma "ev 1000" > by (auto simp: eval_nat_numeral intro!: ev.intros) Alternatively, if you don't want to define the inductive differently, you could just prove a derived introduction rule: > lemma evSS': "ev n ⟹ ev (Suc (Suc n))" > using evSS by simp And then you can prove your lemmas with that. On 15/10/14 05:37, Amarin Phaosawasdi wrote: > Isabelle told me that proof failed for the goal. > mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n)) As far as I know: inductive definitions require the properties to be monotonic, i.e. among other things you can't have something like ‘¬ev n’ anywhere in it. This is not an inductive property anymore, you could otherwise define something silly like ‘¬ev n ⟹ ev n’. Regardless, you don't need this rule anyway. First of all, it is already subsumed by the other rules and secondly, it does not help you at all in proving ‘¬ev 1’. For that, ‘¬ev _’ would have to be on the right-hand side of the implication. The way to prove ‘¬ev 1’ is by case distinction: if ‘ev 1’ were to hold, then either 1 = 0, which is obviously false, or 1 = Suc (Suc n), which is also obviously false. The idea here is that ev is the ‘smallest’ predicate that fulfils the introduction rules given in its definition, so if ‘ev n’ cannot be derived by ev0 and evSS, it is false. A simple way to do this case distinction is by using the simplification rules for ev, ev.simps: > lemma "¬ev 1" > by (subst ev.simps) auto Using ev.simps with the ‘simp’ method is not a good idea because it will probably cause the simplifier to loop. For more complicated examples, you can prove the following (intuitively obvious) lemma: > lemma ev_imp_not_ev_Suc: "ev n ⟹ ¬ev (Suc n)" I will not give you the proof – it can be proven by induction over the inductive definition of ‘ev’ and I think it makes a nice exercise. You may also want to look up the ev.cases rule and the ‘inductive_cases’ command. With that lemma, if you want to prove that something is not even, you can just rewrite it to ‘Suc’ notation with ‘eval_nat_numeral’, apply ev_imp_not_ev_Suc, and thus reduce the problem to proving that the predecessor of the number is even – which you have already done. As a side note: with the command ‘code_pred ev .’, you can generate executable code for the predicate ‘ev’. Then you can check evenness with ‘value "ev 3"’ and even prove or disprove it by using the ‘eval’ method. > lemma "ev 4" by eval > lemma "¬ev 3" by eval Note that, for technical reasons, a proof involving ‘eval’ is arguably not as nice as a ‘normal’ proof. Cheers, Manuel > > Q2: I am not able to prove "ev 4". The closest that I got is this. > > lemma "ev 4" > apply (subgoal_tac "ev (0 + 2 + 2)") > sorry > > Simplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4". > > How can I prove "ev 4"? > > Q3: I also wanted to prove that "¬ev 1", so I tried modifying the > inductive definition as follows. > > inductive ev :: "nat ⇒ bool" where > ev0: "ev 0" | > evS: "¬ev n ⟹ ev (n + 1)" | > evSS: "ev n ⟹ ev (n + 2)" > > Isabelle told me that proof failed for the goal. > mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n)) > > What's going on? If I can't define ev this way, what's the best way to > prove "¬ev 1" > > Maybe the questions weren't that short, sorry about that. > > Any help on any of the questions are much appreciated. > > Thank you, > Amarin >

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

**References**:**[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] reasoning with even and odd numbers
- 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