Re: [isabelle] reasoning with even and odd numbers

On 15/10/2014 05:37, Amarin Phaosawasdi wrote:

I have a series of short, related questions regarding reasoning with even and
odd numbers.

There are a lot of examples on the inductive definitions of even numbers, such
as the following from the book Concrete Semantics.

inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (n + 2)"

For a start, note that a bit further down, in the section "In Isabelle", the "+2" is replaced by "Suc(Suc". The "+2" version was just an intuitive starter.

Proving that 4 is even can be done like this.

lemmas four_is_even = evSS[OF evSS[OF ev0]]

lemma "ev (Suc(Suc(Suc(Suc 0))))"
by (rule four_is_even[simplified])

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"?

Yes, you can combine attributes with ",":
evSS[OF evSS[OF ev0], simplified]

Q2: I am not able to prove "ev 4". The closest that I got is this.

Numerals are distinct from Suc terms.

lemma "ev 4"
apply (subgoal_tac "ev (0 + 2 + 2)")

Simplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4".

How can I prove "ev 4"?

One possibility:

lemma "ev 4"
using evSS[OF evSS[OF ev0]]
by(simp add: numeral_eq_Suc)

where numeral_eq_Suc expands numerals to Sc terms. There may also exist a set of rules that performs the opposite conversion.

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)"

Rule evS violates the format for inductive definitions (see 4.5.3).

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"

You have to rephrase it such that you can apply induction, eg

ev n ==> n ~= 1


Maybe the questions weren't that short, sorry about that.

Any help on any of the questions are much appreciated.

Thank you,

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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