equal
deleted
inserted
replaced
72 by algebra |
72 by algebra |
73 |
73 |
74 lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra |
74 lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra |
75 |
75 |
76 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" |
76 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" |
77 by (simp add: even_def zmod_zmult1_eq) |
77 by (simp add: even_def mod_mult_right_eq) |
78 |
78 |
79 lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)" |
79 lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)" |
80 apply (auto simp add: even_times_anything anything_times_even) |
80 apply (auto simp add: even_times_anything anything_times_even) |
81 apply (rule ccontr) |
81 apply (rule ccontr) |
82 apply (auto simp add: odd_times_odd) |
82 apply (auto simp add: odd_times_odd) |