Re: [isabelle] reasoning with even and odd numbers



Other people have answered your questions in detail, but I just wanted to stress one point about inductive definitions. They give you rules for building up the elements of a set (equivalently, for constructing elements were a predicate is true), but the negative cases are implicit. Therefore, once you have defined the notion of even, you have also defined the notion of odd. And inductive references in the rules can only be positive. You should regard the rules as stating “0 is even”; “if N is even then so is N 2”; "there are no other even numbers”. A statement such as “if N is odd then N+1 is even” should be provable.

Larry Paulson


On 15 Oct 2014, at 04:37, Amarin Phaosawasdi <phaosaw2 at illinois.edu> wrote:

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





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