# 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 \<times> 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 \<longleftrightarrow> m < n \<or> 2 dvd m + n"
 proof (cases "n \<le> 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 \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
   ultimately have "2 dvd m - n \<longleftrightarrow> 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) \<longleftrightarrow> even a \<or> even b"
   by (auto simp add: dest: two_is_prime)
 
@@ -254,7 +254,7 @@
   "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
   by simp
 
-lemma even_power [simp, presburger]:
+lemma even_power [simp]:
   "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 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) \<longleftrightarrow> 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) \<longleftrightarrow> even (n mod 4)"
-  by presburger
-
-lemma odd_mod_4_div_2:
-  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
-  by presburger
-
-lemma even_mod_4_div_2:
-  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
-  by presburger
-  
 text {* Parity and powers *}
 
 context comm_ring_1
@@ -451,7 +437,7 @@
   "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
 
-lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
+lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
   "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> 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 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> 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 \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
 proof -
   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> 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 \<longleftrightarrow> odd n \<and> 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 \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> 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 \<longleftrightarrow> even (int n)"
-  using even_int_iff [of n] by simp
-
-lemma (in semiring_parity) [presburger]:
   "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> 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) \<longleftrightarrow> even n"
+  by presburger
+
 lemma [presburger, algebra]:
   fixes m n :: nat
   shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
@@ -587,10 +606,25 @@
   fixes k :: int
   shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
   by presburger
-  
+
 lemma [presburger]:
-  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+  "even n \<longleftrightarrow> 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) \<longleftrightarrow> even (n mod 4)"
   by presburger
 
+lemma odd_mod_4_div_2:
+  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
+  by presburger
+
+lemma even_mod_4_div_2:
+  "n mod 4 = (1::nat) \<Longrightarrow> 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.