On 15/10/2014 05:37, Amarin Phaosawasdi wrote:
Hello, 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)") sorry 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 Tobias
Maybe the questions weren't that short, sorry about that. Any help on any of the questions are much appreciated. Thank you, Amarin
Description: S/MIME Cryptographic Signature