# HG changeset patch # User haftmann # Date 1383216260 -3600 # Node ID 229282d5378133ba1604ca60a4bf0f0fcf6dd251 # Parent 63b441f4964586de1442ab07eb59e6af78321aa8 purely algebraic foundation for even/odd diff -r 63b441f49645 -r 229282d53781 NEWS --- a/NEWS Thu Oct 31 11:44:20 2013 +0100 +++ b/NEWS Thu Oct 31 11:44:20 2013 +0100 @@ -6,9 +6,14 @@ *** HOL *** -* Fact name generalization and consolidation: - neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 - +* Fact generalization and consolidation: + neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 +INCOMPATIBILITY. + +* Purely algebraic definition of even. Fact generalization and consolidation: + nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd + even_zero_(nat|int) ~> even_zero +INCOMPATIBILITY. New in Isabelle2013-1 (November 2013) diff -r 63b441f49645 -r 229282d53781 src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy --- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy Thu Oct 31 11:44:20 2013 +0100 @@ -16,6 +16,20 @@ by a corresponding @{text export_code} command. *} -export_code _ checking SML OCaml? Haskell? Scala +text {* Formal joining of hierarchy of implicit definitions in Scala *} + +class semiring_numeral_even_odd = semiring_numeral_div + even_odd + +instance nat :: semiring_numeral_even_odd .. + +definition semiring_numeral_even_odd :: "'a itself \ 'a::semiring_numeral_even_odd" +where + "semiring_numeral_even_odd TYPE('a) = undefined" + +definition semiring_numeral_even_odd_nat :: "nat itself \ nat" +where + "semiring_numeral_even_odd_nat = semiring_numeral_even_odd" + +export_code _ checking SML OCaml? Haskell? Scala end diff -r 63b441f49645 -r 229282d53781 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Number_Theory/Primes.thy Thu Oct 31 11:44:20 2013 +0100 @@ -74,8 +74,9 @@ subsection {* Primes *} lemma prime_odd_nat: "prime (p::nat) \ p > 2 \ odd p" - unfolding prime_nat_def - by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat) + apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0) + apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral) + done lemma prime_odd_int: "prime (p::int) \ p > 2 \ odd p" unfolding prime_int_def diff -r 63b441f49645 -r 229282d53781 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Parity.thy Thu Oct 31 11:44:20 2013 +0100 @@ -9,29 +9,52 @@ imports Main begin -class even_odd = - fixes even :: "'a \ bool" +class even_odd = semiring_div_parity begin +definition even :: "'a \ bool" +where + even_def [presburger]: "even a \ a mod 2 = 0" + +lemma even_iff_2_dvd [algebra]: + "even a \ 2 dvd a" + by (simp add: even_def dvd_eq_mod_eq_0) + +lemma even_zero [simp]: + "even 0" + by (simp add: even_def) + +lemma even_times_anything: + "even a \ even (a * b)" + by (simp add: even_iff_2_dvd) + +lemma anything_times_even: + "even a \ even (b * a)" + by (simp add: even_iff_2_dvd) + abbreviation odd :: "'a \ bool" where - "odd x \ \ even x" + "odd a \ \ even a" + +lemma odd_times_odd: + "odd a \ odd b \ odd (a * b)" + by (auto simp add: even_def mod_mult_left_eq) + +lemma even_product [simp, presburger]: + "even (a * b) \ even a \ even b" + apply (auto simp add: even_times_anything anything_times_even) + apply (rule ccontr) + apply (auto simp add: odd_times_odd) + done end -instantiation nat and int :: even_odd -begin - -definition - even_def [presburger]: "even x \ (x\int) mod 2 = 0" +instance nat and int :: even_odd .. -definition - even_nat_def [presburger]: "even x \ even (int x)" - -instance .. - -end - +lemma even_nat_def [presburger]: + "even x \ even (int x)" + by (auto simp add: even_def int_eq_iff int_mult nat_mult_distrib) + lemma transfer_int_nat_relations: "even (int x) \ even x" by (simp add: even_nat_def) @@ -40,13 +63,13 @@ transfer_int_nat_relations ] -lemma even_zero_int[simp]: "even (0::int)" by presburger - -lemma odd_one_int[simp]: "odd (1::int)" by presburger +lemma odd_one_int [simp]: + "odd (1::int)" + by presburger -lemma even_zero_nat[simp]: "even (0::nat)" by presburger - -lemma odd_1_nat [simp]: "odd (1::nat)" by presburger +lemma odd_1_nat [simp]: + "odd (1::nat)" + by presburger lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)" unfolding even_def by simp @@ -67,25 +90,6 @@ subsection {* Behavior under integer arithmetic operations *} -declare dvd_def[algebra] -lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \ 2 dvd x" - by presburger -lemma int_even_iff_2_dvd[algebra]: "even (x::int) \ 2 dvd x" - by presburger - -lemma even_times_anything: "even (x::int) ==> even (x * y)" - by algebra - -lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra - -lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" - by (simp add: even_def mod_mult_right_eq) - -lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)" - apply (auto simp add: even_times_anything anything_times_even) - apply (rule ccontr) - apply (auto simp add: odd_times_odd) - done lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)" by presburger @@ -181,45 +185,19 @@ subsection {* Parity and powers *} -lemma minus_one_even_odd_power: - "(even x --> (- 1::'a::{comm_ring_1})^x = 1) & - (odd x --> (- 1::'a)^x = - 1)" - apply (induct x) - apply (rule conjI) - apply simp - apply (insert even_zero_nat, blast) - apply simp - done - -lemma minus_one_even_power [simp]: - "even x ==> (- 1::'a::{comm_ring_1})^x = 1" - using minus_one_even_odd_power by blast - -lemma minus_one_odd_power [simp]: - "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1" - using minus_one_even_odd_power by blast +lemma (in comm_ring_1) neg_power_if: + "(- a) ^ n = (if even n then (a ^ n) else - (a ^ n))" + by (induct n) simp_all -lemma neg_one_even_odd_power: - "(even x --> (-1::'a::{comm_ring_1})^x = 1) & - (odd x --> (-1::'a)^x = -1)" - apply (induct x) - apply (simp, simp) - done - -lemma neg_one_even_power [simp]: - "even x ==> (-1::'a::{comm_ring_1})^x = 1" - using neg_one_even_odd_power by blast +lemma (in comm_ring_1) + shows minus_one_even_power [simp]: "even n \ (- 1) ^ n = 1" + and minus_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" + by (simp_all add: neg_power_if del: minus_one) -lemma neg_one_odd_power [simp]: - "odd x ==> (-1::'a::{comm_ring_1})^x = -1" - using neg_one_even_odd_power by blast - -lemma neg_power_if: - "(-x::'a::{comm_ring_1}) ^ n = - (if even n then (x ^ n) else -(x ^ n))" - apply (induct n) - apply simp_all - done +lemma (in comm_ring_1) + shows neg_one_even_power [simp]: "even n \ (-1) ^ n = 1" + and neg_one_odd_power [simp]: "odd n \ (-1) ^ n = - 1" + by (simp_all add: minus_one [symmetric] del: minus_one) lemma zero_le_even_power: "even n ==> 0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"