# HG changeset patch # User haftmann # Date 1414065845 -7200 # Node ID ae5e9b4f8daffb0e2a4c5d932212fb459a2965a5 # Parent 70fff47875cd71d5a347399852977c130c464e23 downshift of theory Parity in the hierarchy diff -r 70fff47875cd -r ae5e9b4f8daf NEWS --- a/NEWS Thu Oct 23 14:04:05 2014 +0200 +++ b/NEWS Thu Oct 23 14:04:05 2014 +0200 @@ -55,7 +55,8 @@ dvd_plus_eq_left ~> dvd_add_left_iff Minor INCOMPATIBILITY. -* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _". +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" +and part of HOL-Main. even_def ~> even_iff_mod_2_eq_zero INCOMPATIBILITY. diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 23 14:04:05 2014 +0200 @@ -6,7 +6,7 @@ header {* Proving equalities in commutative rings *} theory Commutative_Ring -imports Parity +imports Main begin text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *} diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/GCD.thy Thu Oct 23 14:04:05 2014 +0200 @@ -28,7 +28,7 @@ header {* Greatest common divisor and least common multiple *} theory GCD -imports Fact Parity +imports Fact begin declare One_nat_def [simp del] diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/IMPP/EvenOdd.thy --- a/src/HOL/IMPP/EvenOdd.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/IMPP/EvenOdd.thy Thu Oct 23 14:04:05 2014 +0200 @@ -5,7 +5,7 @@ header {* Example of mutually recursive procedures verified with Hoare logic *} theory EvenOdd -imports Misc "~~/src/HOL/Parity" +imports Main Misc begin axiomatization diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Import/Import_Setup.thy --- a/src/HOL/Import/Import_Setup.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Import/Import_Setup.thy Thu Oct 23 14:04:05 2014 +0200 @@ -6,7 +6,7 @@ header {* Importer machinery and required theorems *} theory Import_Setup -imports "~~/src/HOL/Parity" "~~/src/HOL/Fact" +imports Main "~~/src/HOL/Fact" keywords "import_type_map" "import_const_map" "import_file" :: thy_decl begin diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Library/Nat_Bijection.thy --- a/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200 @@ -9,7 +9,7 @@ header {* Bijections between natural numbers and other types *} theory Nat_Bijection -imports Main Parity +imports Main begin subsection {* Type @{typ "nat \ nat"} *} diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Library/Permutations.thy Thu Oct 23 14:04:05 2014 +0200 @@ -5,7 +5,7 @@ header {* Permutations, both general and specifically on finite sets.*} theory Permutations -imports Parity Fact +imports Fact begin subsection {* Transpositions *} diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Main.thy --- a/src/HOL/Main.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Main.thy Thu Oct 23 14:04:05 2014 +0200 @@ -2,7 +2,7 @@ theory Main imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick - BNF_Greatest_Fixpoint + BNF_Greatest_Fixpoint Parity begin text {* diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/NthRoot.thy Thu Oct 23 14:04:05 2014 +0200 @@ -7,7 +7,7 @@ header {* Nth Roots of Real Numbers *} theory NthRoot -imports Parity Deriv +imports Deriv begin lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)" diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Parity.thy Thu Oct 23 14:04:05 2014 +0200 @@ -6,7 +6,7 @@ header {* Even and Odd for int and nat *} theory Parity -imports Main +imports Presburger begin subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *} @@ -24,7 +24,7 @@ shows "2 dvd m - n \ m < n \ 2 dvd m + n" proof (cases "n \ m") case True - then have "m - n + n * 2 = m + n" by simp + then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) moreover have "2 dvd m - n \ 2 dvd m - n + n * 2" by simp ultimately have "2 dvd m - n \ 2 dvd m + n" by (simp only:) then show ?thesis by auto @@ -103,7 +103,7 @@ then obtain r where "Suc n = 2 * r" .. moreover from * obtain s where "m * n = 2 * s" .. then have "2 * s + m = m * Suc n" by simp - ultimately have " 2 * s + m = 2 * (m * r)" by simp + ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps) then have "m = 2 * (m * r - s)" by simp then show "2 dvd m" .. qed @@ -207,7 +207,7 @@ obtains b where "a = 2 * b + 1" using assms by (rule not_two_dvdE) -lemma even_times_iff [simp, presburger, algebra]: +lemma even_times_iff [simp]: "even (a * b) \ even a \ even b" by (auto simp add: dest: two_is_prime) @@ -254,7 +254,7 @@ "odd (a + b) \ (\ (odd a \ odd b))" by simp -lemma even_power [simp, presburger]: +lemma even_power [simp]: "even (a ^ n) \ even a \ n \ 0" by (induct n) auto @@ -263,7 +263,7 @@ context ring_parity begin -lemma even_minus [simp, presburger, algebra]: +lemma even_minus [simp]: "even (- a) \ even a" by (fact dvd_minus_iff) @@ -317,7 +317,7 @@ subsubsection {* Particularities for @{typ nat} and @{typ int} *} -lemma even_Suc [simp, presburger, algebra]: +lemma even_Suc [simp]: "even (Suc n) = odd n" by (fact two_dvd_Suc_iff) @@ -380,20 +380,6 @@ qed qed -text {* Nice facts about division by @{term 4} *} - -lemma even_even_mod_4_iff: - "even (n::nat) \ even (n mod 4)" - by presburger - -lemma odd_mod_4_div_2: - "n mod 4 = (3::nat) \ odd ((n - 1) div 2)" - by presburger - -lemma even_mod_4_div_2: - "n mod 4 = (1::nat) \ even ((n - 1) div 2)" - by presburger - text {* Parity and powers *} context comm_ring_1 @@ -451,7 +437,7 @@ "odd n \ 0 \ a ^ n \ 0 \ a" by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) -lemma zero_le_power_iff [presburger]: -- \FIXME cf. @{text zero_le_power_eq}\ +lemma zero_le_power_iff: -- \FIXME cf. @{text zero_le_power_eq}\ "0 \ a ^ n \ 0 \ a \ even n" proof (cases "even n") case True @@ -466,11 +452,11 @@ by (auto simp add: zero_le_mult_iff zero_le_even_power) qed -lemma zero_le_power_eq [presburger]: +lemma zero_le_power_eq: "0 \ a ^ n \ even n \ odd n \ 0 \ a" using zero_le_power_iff [of a n] by auto -lemma zero_less_power_eq [presburger]: +lemma zero_less_power_eq: "0 < a ^ n \ n = 0 \ even n \ a \ 0 \ odd n \ 0 < a" proof - have [simp]: "0 = a ^ n \ a = 0 \ n > 0" @@ -479,11 +465,11 @@ unfolding less_le zero_le_power_eq by auto qed -lemma power_less_zero_eq [presburger]: +lemma power_less_zero_eq: "a ^ n < 0 \ odd n \ a < 0" unfolding not_le [symmetric] zero_le_power_eq by auto -lemma power_le_zero_eq [presburger]: +lemma power_le_zero_eq: "a ^ n \ 0 \ n > 0 \ (odd n \ a \ 0 \ even n \ a = 0)" unfolding not_less [symmetric] zero_less_power_eq by auto @@ -560,14 +546,47 @@ even_int_iff ] +context semiring_parity +begin + +declare even_times_iff [presburger, algebra] + +declare even_power [presburger] + lemma [presburger]: - "even n \ even (int n)" - using even_int_iff [of n] by simp - -lemma (in semiring_parity) [presburger]: "even (a + b) \ even a \ even b \ odd a \ odd b" by auto +end + +context ring_parity +begin + +declare even_minus [presburger, algebra] + +end + +context linordered_idom +begin + +declare zero_le_power_iff [presburger] + +declare zero_le_power_eq [presburger] + +declare zero_less_power_eq [presburger] + +declare power_less_zero_eq [presburger] + +declare power_le_zero_eq [presburger] + +end + +declare even_Suc [presburger, algebra] + +lemma [presburger]: + "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \ even n" + by presburger + lemma [presburger, algebra]: fixes m n :: nat shows "even (m - n) \ m < n \ even m \ even n \ odd m \ odd n" @@ -587,10 +606,25 @@ fixes k :: int shows "(k + 1) div 2 = k div 2 + 1 \ odd k" by presburger - + lemma [presburger]: - "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \ even n" + "even n \ even (int n)" + using even_int_iff [of n] by simp + + +subsubsection {* Nice facts about division by @{term 4} *} + +lemma even_even_mod_4_iff: + "even (n::nat) \ even (n mod 4)" by presburger +lemma odd_mod_4_div_2: + "n mod 4 = (3::nat) \ odd ((n - 1) div 2)" + by presburger + +lemma even_mod_4_div_2: + "n mod 4 = (1::nat) \ even ((n - 1) div 2)" + by presburger + end diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Word/Misc_Numeric.thy --- a/src/HOL/Word/Misc_Numeric.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Word/Misc_Numeric.thy Thu Oct 23 14:04:05 2014 +0200 @@ -5,7 +5,7 @@ header {* Useful Numerical Lemmas *} theory Misc_Numeric -imports Main Parity +imports Main begin lemma mod_2_neq_1_eq_eq_0: diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/Word/Word_Miscellaneous.thy --- a/src/HOL/Word/Word_Miscellaneous.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Word/Word_Miscellaneous.thy Thu Oct 23 14:04:05 2014 +0200 @@ -5,7 +5,7 @@ header {* Miscellaneous lemmas, of at least doubtful value *} theory Word_Miscellaneous -imports Main Parity "~~/src/HOL/Library/Bit" Misc_Numeric +imports Main "~~/src/HOL/Library/Bit" Misc_Numeric begin lemma power_minus_simp: diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/ex/Fundefs.thy Thu Oct 23 14:04:05 2014 +0200 @@ -5,7 +5,7 @@ header {* Examples of function definitions *} theory Fundefs -imports Parity "~~/src/HOL/Library/Monad_Syntax" +imports Main "~~/src/HOL/Library/Monad_Syntax" begin subsection {* Very basic *} diff -r 70fff47875cd -r ae5e9b4f8daf src/HOL/ex/NatSum.thy --- a/src/HOL/ex/NatSum.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/ex/NatSum.thy Thu Oct 23 14:04:05 2014 +0200 @@ -4,7 +4,7 @@ header {* Summing natural numbers *} -theory NatSum imports Main Parity begin +theory NatSum imports Main begin text {* Summing natural numbers, squares, cubes, etc.