further downshift of theory Parity in the hierarchy
authorhaftmann
Thu Oct 23 19:40:39 2014 +0200 (2014-10-23)
changeset 587776ba2f1fa243b
parent 58776 95e58e04e534
child 58778 e29cae8eab1f
further downshift of theory Parity in the hierarchy
src/HOL/Groebner_Basis.thy
src/HOL/Main.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Oct 24 15:07:51 2014 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Oct 23 19:40:39 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Groebner bases *}
     1.5  
     1.6  theory Groebner_Basis
     1.7 -imports Semiring_Normalization
     1.8 +imports Semiring_Normalization Parity
     1.9  keywords "try0" :: diag
    1.10  begin
    1.11  
    1.12 @@ -77,4 +77,22 @@
    1.13  declare zmod_eq_dvd_iff[algebra]
    1.14  declare nat_mod_eq_iff[algebra]
    1.15  
    1.16 +context semiring_parity
    1.17 +begin
    1.18 +
    1.19 +declare even_times_iff [algebra]
    1.20 +declare even_power [algebra]
    1.21 +
    1.22  end
    1.23 +
    1.24 +context ring_parity
    1.25 +begin
    1.26 +
    1.27 +declare even_minus [algebra]
    1.28 +
    1.29 +end
    1.30 +
    1.31 +declare even_Suc [algebra]
    1.32 +declare even_diff_nat [algebra]
    1.33 +
    1.34 +end
     2.1 --- a/src/HOL/Main.thy	Fri Oct 24 15:07:51 2014 +0200
     2.2 +++ b/src/HOL/Main.thy	Thu Oct 23 19:40:39 2014 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  
     2.5  theory Main
     2.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     2.7 -  BNF_Greatest_Fixpoint Parity
     2.8 +  BNF_Greatest_Fixpoint
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Parity.thy	Fri Oct 24 15:07:51 2014 +0200
     3.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 19:40:39 2014 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Even and Odd for int and nat *}
     3.5  
     3.6  theory Parity
     3.7 -imports Presburger
     3.8 +imports Divides
     3.9  begin
    3.10  
    3.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
    3.12 @@ -36,7 +36,7 @@
    3.13  lemma two_dvd_diff_iff:
    3.14    fixes k l :: int
    3.15    shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    3.16 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
    3.17 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    3.18  
    3.19  lemma two_dvd_abs_add_iff:
    3.20    fixes k l :: int
    3.21 @@ -546,77 +546,5 @@
    3.22    even_int_iff
    3.23  ]
    3.24  
    3.25 -context semiring_parity
    3.26 -begin
    3.27 -
    3.28 -declare even_times_iff [presburger, algebra]
    3.29 -
    3.30 -declare even_power [presburger, algebra]
    3.31 -
    3.32 -lemma [presburger]:
    3.33 -  "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    3.34 -  by auto
    3.35 -
    3.36 -end
    3.37 -
    3.38 -context ring_parity
    3.39 -begin
    3.40 -
    3.41 -declare even_minus [presburger, algebra]
    3.42 -
    3.43 -end
    3.44 -
    3.45 -context linordered_idom
    3.46 -begin
    3.47 -
    3.48 -declare zero_le_power_iff [presburger]
    3.49 -
    3.50 -declare zero_le_power_eq [presburger]
    3.51 -
    3.52 -declare zero_less_power_eq [presburger]
    3.53 -
    3.54 -declare power_less_zero_eq [presburger]
    3.55 -  
    3.56 -declare power_le_zero_eq [presburger]
    3.57 -
    3.58  end
    3.59  
    3.60 -declare even_Suc [presburger, algebra]
    3.61 -
    3.62 -lemma [presburger]:
    3.63 -  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    3.64 -  by presburger
    3.65 -
    3.66 -declare even_diff_nat [presburger, algebra]
    3.67 -
    3.68 -lemma [presburger]:
    3.69 -  fixes k :: int
    3.70 -  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
    3.71 -  by presburger
    3.72 -
    3.73 -lemma [presburger]:
    3.74 -  fixes k :: int
    3.75 -  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
    3.76 -  by presburger
    3.77 -
    3.78 -lemma [presburger]:
    3.79 -  "even n \<longleftrightarrow> even (int n)"
    3.80 -  using even_int_iff [of n] by simp
    3.81 -  
    3.82 -
    3.83 -subsubsection {* Nice facts about division by @{term 4} *}  
    3.84 -
    3.85 -lemma even_even_mod_4_iff:
    3.86 -  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    3.87 -  by presburger
    3.88 -
    3.89 -lemma odd_mod_4_div_2:
    3.90 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    3.91 -  by presburger
    3.92 -
    3.93 -lemma even_mod_4_div_2:
    3.94 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    3.95 -  by presburger
    3.96 -  
    3.97 -end
    3.98 -
     4.1 --- a/src/HOL/Presburger.thy	Fri Oct 24 15:07:51 2014 +0200
     4.2 +++ b/src/HOL/Presburger.thy	Thu Oct 23 19:40:39 2014 +0200
     4.3 @@ -434,6 +434,78 @@
     4.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     4.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     4.6  
     4.7 +context semiring_parity
     4.8 +begin
     4.9 +
    4.10 +declare even_times_iff [presburger]
    4.11 +
    4.12 +declare even_power [presburger]
    4.13 +
    4.14 +lemma [presburger]:
    4.15 +  "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    4.16 +  by auto
    4.17 +
    4.18 +end
    4.19 +
    4.20 +context ring_parity
    4.21 +begin
    4.22 +
    4.23 +declare even_minus [presburger]
    4.24 +
    4.25 +end
    4.26 +
    4.27 +context linordered_idom
    4.28 +begin
    4.29 +
    4.30 +declare zero_le_power_iff [presburger]
    4.31 +
    4.32 +declare zero_le_power_eq [presburger]
    4.33 +
    4.34 +declare zero_less_power_eq [presburger]
    4.35 +
    4.36 +declare power_less_zero_eq [presburger]
    4.37 +  
    4.38 +declare power_le_zero_eq [presburger]
    4.39 +
    4.40 +end
    4.41 +
    4.42 +declare even_Suc [presburger]
    4.43 +
    4.44 +lemma [presburger]:
    4.45 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    4.46 +  by presburger
    4.47 +
    4.48 +declare even_diff_nat [presburger]
    4.49 +
    4.50 +lemma [presburger]:
    4.51 +  fixes k :: int
    4.52 +  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
    4.53 +  by presburger
    4.54 +
    4.55 +lemma [presburger]:
    4.56 +  fixes k :: int
    4.57 +  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
    4.58 +  by presburger
    4.59 +
    4.60 +lemma [presburger]:
    4.61 +  "even n \<longleftrightarrow> even (int n)"
    4.62 +  using even_int_iff [of n] by simp
    4.63 +  
    4.64 +
    4.65 +subsection {* Nice facts about division by @{term 4} *}  
    4.66 +
    4.67 +lemma even_even_mod_4_iff:
    4.68 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    4.69 +  by presburger
    4.70 +
    4.71 +lemma odd_mod_4_div_2:
    4.72 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    4.73 +  by presburger
    4.74 +
    4.75 +lemma even_mod_4_div_2:
    4.76 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    4.77 +  by presburger
    4.78 +
    4.79  
    4.80  subsection {* Try0 *}
    4.81