downshift of theory Parity in the hierarchy
authorhaftmann
Thu Oct 23 14:04:05 2014 +0200 (2014-10-23)
changeset 58770ae5e9b4f8daf
parent 58769 70fff47875cd
child 58771 0997ea62e868
downshift of theory Parity in the hierarchy
NEWS
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/GCD.thy
src/HOL/IMPP/EvenOdd.thy
src/HOL/Import/Import_Setup.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Permutations.thy
src/HOL/Main.thy
src/HOL/NthRoot.thy
src/HOL/Parity.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word_Miscellaneous.thy
src/HOL/ex/Fundefs.thy
src/HOL/ex/NatSum.thy
     1.1 --- a/NEWS	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/NEWS	Thu Oct 23 14:04:05 2014 +0200
     1.3 @@ -55,7 +55,8 @@
     1.4    dvd_plus_eq_left ~> dvd_add_left_iff
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 -* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
     1.8 +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
     1.9 +and part of HOL-Main.
    1.10    even_def ~> even_iff_mod_2_eq_zero
    1.11  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 23 14:04:05 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 23 14:04:05 2014 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Proving equalities in commutative rings *}
     2.5  
     2.6  theory Commutative_Ring
     2.7 -imports Parity
     2.8 +imports Main
     2.9  begin
    2.10  
    2.11  text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
     3.1 --- a/src/HOL/GCD.thy	Thu Oct 23 14:04:05 2014 +0200
     3.2 +++ b/src/HOL/GCD.thy	Thu Oct 23 14:04:05 2014 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4  header {* Greatest common divisor and least common multiple *}
     3.5  
     3.6  theory GCD
     3.7 -imports Fact Parity
     3.8 +imports Fact
     3.9  begin
    3.10  
    3.11  declare One_nat_def [simp del]
     4.1 --- a/src/HOL/IMPP/EvenOdd.thy	Thu Oct 23 14:04:05 2014 +0200
     4.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Thu Oct 23 14:04:05 2014 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Example of mutually recursive procedures verified with Hoare logic *}
     4.5  
     4.6  theory EvenOdd
     4.7 -imports Misc "~~/src/HOL/Parity"
     4.8 +imports Main Misc
     4.9  begin
    4.10  
    4.11  axiomatization
     5.1 --- a/src/HOL/Import/Import_Setup.thy	Thu Oct 23 14:04:05 2014 +0200
     5.2 +++ b/src/HOL/Import/Import_Setup.thy	Thu Oct 23 14:04:05 2014 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Importer machinery and required theorems *}
     5.5  
     5.6  theory Import_Setup
     5.7 -imports "~~/src/HOL/Parity" "~~/src/HOL/Fact"
     5.8 +imports Main "~~/src/HOL/Fact"
     5.9  keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Library/Nat_Bijection.thy	Thu Oct 23 14:04:05 2014 +0200
     6.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Thu Oct 23 14:04:05 2014 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  header {* Bijections between natural numbers and other types *}
     6.5  
     6.6  theory Nat_Bijection
     6.7 -imports Main Parity
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  subsection {* Type @{typ "nat \<times> nat"} *}
     7.1 --- a/src/HOL/Library/Permutations.thy	Thu Oct 23 14:04:05 2014 +0200
     7.2 +++ b/src/HOL/Library/Permutations.thy	Thu Oct 23 14:04:05 2014 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Permutations, both general and specifically on finite sets.*}
     7.5  
     7.6  theory Permutations
     7.7 -imports Parity Fact
     7.8 +imports Fact
     7.9  begin
    7.10  
    7.11  subsection {* Transpositions *}
     8.1 --- a/src/HOL/Main.thy	Thu Oct 23 14:04:05 2014 +0200
     8.2 +++ b/src/HOL/Main.thy	Thu Oct 23 14:04:05 2014 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4  
     8.5  theory Main
     8.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     8.7 -  BNF_Greatest_Fixpoint
     8.8 +  BNF_Greatest_Fixpoint Parity
     8.9  begin
    8.10  
    8.11  text {*
     9.1 --- a/src/HOL/NthRoot.thy	Thu Oct 23 14:04:05 2014 +0200
     9.2 +++ b/src/HOL/NthRoot.thy	Thu Oct 23 14:04:05 2014 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  header {* Nth Roots of Real Numbers *}
     9.5  
     9.6  theory NthRoot
     9.7 -imports Parity Deriv
     9.8 +imports Deriv
     9.9  begin
    9.10  
    9.11  lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
    10.1 --- a/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
    10.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Even and Odd for int and nat *}
    10.5  
    10.6  theory Parity
    10.7 -imports Main
    10.8 +imports Presburger
    10.9  begin
   10.10  
   10.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
   10.12 @@ -24,7 +24,7 @@
   10.13    shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
   10.14  proof (cases "n \<le> m")
   10.15    case True
   10.16 -  then have "m - n + n * 2 = m + n" by simp
   10.17 +  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
   10.18    moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
   10.19    ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
   10.20    then show ?thesis by auto
   10.21 @@ -103,7 +103,7 @@
   10.22      then obtain r where "Suc n = 2 * r" ..
   10.23      moreover from * obtain s where "m * n = 2 * s" ..
   10.24      then have "2 * s + m = m * Suc n" by simp
   10.25 -    ultimately have " 2 * s + m = 2 * (m * r)" by simp
   10.26 +    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
   10.27      then have "m = 2 * (m * r - s)" by simp
   10.28      then show "2 dvd m" ..
   10.29    qed
   10.30 @@ -207,7 +207,7 @@
   10.31    obtains b where "a = 2 * b + 1"
   10.32    using assms by (rule not_two_dvdE)
   10.33    
   10.34 -lemma even_times_iff [simp, presburger, algebra]:
   10.35 +lemma even_times_iff [simp]:
   10.36    "even (a * b) \<longleftrightarrow> even a \<or> even b"
   10.37    by (auto simp add: dest: two_is_prime)
   10.38  
   10.39 @@ -254,7 +254,7 @@
   10.40    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
   10.41    by simp
   10.42  
   10.43 -lemma even_power [simp, presburger]:
   10.44 +lemma even_power [simp]:
   10.45    "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
   10.46    by (induct n) auto
   10.47  
   10.48 @@ -263,7 +263,7 @@
   10.49  context ring_parity
   10.50  begin
   10.51  
   10.52 -lemma even_minus [simp, presburger, algebra]:
   10.53 +lemma even_minus [simp]:
   10.54    "even (- a) \<longleftrightarrow> even a"
   10.55    by (fact dvd_minus_iff)
   10.56  
   10.57 @@ -317,7 +317,7 @@
   10.58  
   10.59  subsubsection {* Particularities for @{typ nat} and @{typ int} *}
   10.60  
   10.61 -lemma even_Suc [simp, presburger, algebra]:
   10.62 +lemma even_Suc [simp]:
   10.63    "even (Suc n) = odd n"
   10.64    by (fact two_dvd_Suc_iff)
   10.65  
   10.66 @@ -380,20 +380,6 @@
   10.67    qed
   10.68  qed
   10.69    
   10.70 -text {* Nice facts about division by @{term 4} *}  
   10.71 -
   10.72 -lemma even_even_mod_4_iff:
   10.73 -  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
   10.74 -  by presburger
   10.75 -
   10.76 -lemma odd_mod_4_div_2:
   10.77 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
   10.78 -  by presburger
   10.79 -
   10.80 -lemma even_mod_4_div_2:
   10.81 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
   10.82 -  by presburger
   10.83 -  
   10.84  text {* Parity and powers *}
   10.85  
   10.86  context comm_ring_1
   10.87 @@ -451,7 +437,7 @@
   10.88    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   10.89    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
   10.90  
   10.91 -lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
   10.92 +lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
   10.93    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
   10.94  proof (cases "even n")
   10.95    case True
   10.96 @@ -466,11 +452,11 @@
   10.97      by (auto simp add: zero_le_mult_iff zero_le_even_power)
   10.98  qed
   10.99  
  10.100 -lemma zero_le_power_eq [presburger]:
  10.101 +lemma zero_le_power_eq:
  10.102    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
  10.103    using zero_le_power_iff [of a n] by auto
  10.104  
  10.105 -lemma zero_less_power_eq [presburger]:
  10.106 +lemma zero_less_power_eq:
  10.107    "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
  10.108  proof -
  10.109    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
  10.110 @@ -479,11 +465,11 @@
  10.111    unfolding less_le zero_le_power_eq by auto
  10.112  qed
  10.113  
  10.114 -lemma power_less_zero_eq [presburger]:
  10.115 +lemma power_less_zero_eq:
  10.116    "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
  10.117    unfolding not_le [symmetric] zero_le_power_eq by auto
  10.118    
  10.119 -lemma power_le_zero_eq [presburger]:
  10.120 +lemma power_le_zero_eq:
  10.121    "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
  10.122    unfolding not_less [symmetric] zero_less_power_eq by auto 
  10.123  
  10.124 @@ -560,14 +546,47 @@
  10.125    even_int_iff
  10.126  ]
  10.127  
  10.128 +context semiring_parity
  10.129 +begin
  10.130 +
  10.131 +declare even_times_iff [presburger, algebra]
  10.132 +
  10.133 +declare even_power [presburger]
  10.134 +
  10.135  lemma [presburger]:
  10.136 -  "even n \<longleftrightarrow> even (int n)"
  10.137 -  using even_int_iff [of n] by simp
  10.138 -
  10.139 -lemma (in semiring_parity) [presburger]:
  10.140    "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
  10.141    by auto
  10.142  
  10.143 +end
  10.144 +
  10.145 +context ring_parity
  10.146 +begin
  10.147 +
  10.148 +declare even_minus [presburger, algebra]
  10.149 +
  10.150 +end
  10.151 +
  10.152 +context linordered_idom
  10.153 +begin
  10.154 +
  10.155 +declare zero_le_power_iff [presburger]
  10.156 +
  10.157 +declare zero_le_power_eq [presburger]
  10.158 +
  10.159 +declare zero_less_power_eq [presburger]
  10.160 +
  10.161 +declare power_less_zero_eq [presburger]
  10.162 +  
  10.163 +declare power_le_zero_eq [presburger]
  10.164 +
  10.165 +end
  10.166 +
  10.167 +declare even_Suc [presburger, algebra]
  10.168 +
  10.169 +lemma [presburger]:
  10.170 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
  10.171 +  by presburger
  10.172 +
  10.173  lemma [presburger, algebra]:
  10.174    fixes m n :: nat
  10.175    shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
  10.176 @@ -587,10 +606,25 @@
  10.177    fixes k :: int
  10.178    shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
  10.179    by presburger
  10.180 -  
  10.181 +
  10.182  lemma [presburger]:
  10.183 -  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
  10.184 +  "even n \<longleftrightarrow> even (int n)"
  10.185 +  using even_int_iff [of n] by simp
  10.186 +  
  10.187 +
  10.188 +subsubsection {* Nice facts about division by @{term 4} *}  
  10.189 +
  10.190 +lemma even_even_mod_4_iff:
  10.191 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
  10.192    by presburger
  10.193  
  10.194 +lemma odd_mod_4_div_2:
  10.195 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
  10.196 +  by presburger
  10.197 +
  10.198 +lemma even_mod_4_div_2:
  10.199 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
  10.200 +  by presburger
  10.201 +  
  10.202  end
  10.203  
    11.1 --- a/src/HOL/Word/Misc_Numeric.thy	Thu Oct 23 14:04:05 2014 +0200
    11.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Thu Oct 23 14:04:05 2014 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* Useful Numerical Lemmas *}
    11.5  
    11.6  theory Misc_Numeric
    11.7 -imports Main Parity
    11.8 +imports Main
    11.9  begin
   11.10  
   11.11  lemma mod_2_neq_1_eq_eq_0:
    12.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Thu Oct 23 14:04:05 2014 +0200
    12.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Thu Oct 23 14:04:05 2014 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  header {* Miscellaneous lemmas, of at least doubtful value *}
    12.5  
    12.6  theory Word_Miscellaneous
    12.7 -imports Main Parity "~~/src/HOL/Library/Bit" Misc_Numeric
    12.8 +imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
    12.9  begin
   12.10  
   12.11  lemma power_minus_simp:
    13.1 --- a/src/HOL/ex/Fundefs.thy	Thu Oct 23 14:04:05 2014 +0200
    13.2 +++ b/src/HOL/ex/Fundefs.thy	Thu Oct 23 14:04:05 2014 +0200
    13.3 @@ -5,7 +5,7 @@
    13.4  header {* Examples of function definitions *}
    13.5  
    13.6  theory Fundefs 
    13.7 -imports Parity "~~/src/HOL/Library/Monad_Syntax"
    13.8 +imports Main "~~/src/HOL/Library/Monad_Syntax"
    13.9  begin
   13.10  
   13.11  subsection {* Very basic *}
    14.1 --- a/src/HOL/ex/NatSum.thy	Thu Oct 23 14:04:05 2014 +0200
    14.2 +++ b/src/HOL/ex/NatSum.thy	Thu Oct 23 14:04:05 2014 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4  
    14.5  header {* Summing natural numbers *}
    14.6  
    14.7 -theory NatSum imports Main Parity begin
    14.8 +theory NatSum imports Main begin
    14.9  
   14.10  text {*
   14.11    Summing natural numbers, squares, cubes, etc.