merged;
authorwenzelm
Fri, 24 Oct 2014 20:49:23 +0200
changeset 58781 c385da5c665e
parent 58778 e29cae8eab1f (diff)
parent 58780 1f8c0da85664 (current diff)
child 58782 7305bad408b5
merged;
--- a/NEWS	Fri Oct 24 11:30:39 2014 +0200
+++ b/NEWS	Fri Oct 24 20:49:23 2014 +0200
@@ -49,6 +49,8 @@
 
 *** HOL ***
 
+* Add NO_MATCH-simproc, allows to check for syntactic non-equality
+
 * Generalized and consolidated some theorems concerning divsibility:
   dvd_reduce ~> dvd_add_triv_right_iff
   dvd_plus_eq_right ~> dvd_add_right_iff
@@ -63,6 +65,12 @@
 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
 Minor INCOMPATIBILITY.
 
+* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
+  non-termination in case of distributing a division. With this change
+  field_simps is in some cases slightly less powerful, if it fails try
+  to add algebra_simps, or use divide_simps.
+Minor INCOMPATIBILITY.
+
 * Bootstrap of listsum as special case of abstract product over lists.
 Fact rename:
     listsum_def ~> listsum.eq_foldr
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -375,7 +375,7 @@
 
 lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
   by (induct p q rule: polyadd.induct)
-    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
+     (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
 
 lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
--- a/src/HOL/Divides.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -6,7 +6,7 @@
 header {* The division operators div and mod *}
 
 theory Divides
-imports Nat_Transfer
+imports Parity
 begin
 
 subsection {* Syntactic division operations *}
@@ -504,6 +504,9 @@
 
 end
 
+
+subsubsection {* Parity and division *}
+
 class semiring_div_parity = semiring_div + semiring_numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   assumes one_mod_two_eq_one: "1 mod 2 = 1"
@@ -524,6 +527,76 @@
   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   by (cases a rule: parity_cases) simp_all
 
+lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
+  "1 div 2 = 0"
+proof (cases "2 = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
+  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
+  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
+  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
+  with False show ?thesis by auto
+qed
+
+subclass semiring_parity
+proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
+  fix a b c
+  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
+    by simp
+next
+  fix a b c
+  assume "(b + c) mod a = 0"
+  with mod_add_eq [of b c a]
+  have "(b mod a + c mod a) mod a = 0"
+    by simp
+  moreover assume "b mod a = 0"
+  ultimately show "c mod a = 0"
+    by simp
+next
+  show "1 mod 2 = 1"
+    by (fact one_mod_two_eq_one)
+next
+  fix a b
+  assume "a mod 2 = 1"
+  moreover assume "b mod 2 = 1"
+  ultimately show "(a + b) mod 2 = 0"
+    using mod_add_eq [of a b 2] by simp
+next
+  fix a b
+  assume "(a * b) mod 2 = 0"
+  then have "(a mod 2) * (b mod 2) = 0"
+    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
+  then show "a mod 2 = 0 \<or> b mod 2 = 0"
+    by (rule divisors_zero)
+next
+  fix a
+  assume "a mod 2 = 1"
+  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
+  then show "\<exists>b. a = b + 1" ..
+qed
+
+lemma even_iff_mod_2_eq_zero:
+  "even a \<longleftrightarrow> a mod 2 = 0"
+  by (fact dvd_eq_mod_eq_0)
+
+lemma even_succ_div_two [simp]:
+  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ:
+  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+
 end
 
 
@@ -1451,6 +1524,44 @@
 instance nat :: semiring_numeral_div
   by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
 
+lemma even_Suc_div_two [simp]:
+  "even n \<Longrightarrow> Suc n div 2 = n div 2"
+  using even_succ_div_two [of n] by simp
+  
+lemma odd_Suc_div_two [simp]:
+  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
+  using odd_succ_div_two [of n] by simp
+
+lemma odd_two_times_div_two_Suc:
+  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
+  using odd_two_times_div_two_succ [of n] by simp
+
+lemma parity_induct [case_names zero even odd]:
+  assumes zero: "P 0"
+  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
+  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+  shows "P n"
+proof (induct n rule: less_induct)
+  case (less n)
+  show "P n"
+  proof (cases "n = 0")
+    case True with zero show ?thesis by simp
+  next
+    case False
+    with less have hyp: "P (n div 2)" by simp
+    show ?thesis
+    proof (cases "even n")
+      case True
+      with hyp even [of "n div 2"] show ?thesis
+        by (simp add: dvd_mult_div_cancel)
+    next
+      case False
+      with hyp odd [of "n div 2"] show ?thesis 
+        by (simp add: odd_two_times_div_two_Suc)
+    qed
+  qed
+qed
+
 
 subsection {* Division on @{typ int} *}
 
--- a/src/HOL/Fields.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Fields.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -23,11 +23,37 @@
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
 
+setup {* Sign.add_const_constraint
+  (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+
+context semiring
+begin
+
+lemma [field_simps]:
+  shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
+  by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
+  by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint
+  (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
 
 named_theorems divide_simps "rewrite rules to eliminate divisions"
 
-
 class division_ring = ring_1 + inverse +
   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
--- a/src/HOL/GCD.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/GCD.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -1049,7 +1049,7 @@
       apply (subst mod_div_equality [of m n, symmetric])
       (* applying simp here undoes the last substitution!
          what is procedure cancel_div_mod? *)
-      apply (simp only: field_simps of_nat_add of_nat_mult)
+      apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
       done
 qed
 
--- a/src/HOL/Groebner_Basis.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -5,7 +5,7 @@
 header {* Groebner bases *}
 
 theory Groebner_Basis
-imports Semiring_Normalization
+imports Semiring_Normalization Parity
 keywords "try0" :: diag
 begin
 
@@ -77,4 +77,22 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
+context semiring_parity
+begin
+
+declare even_times_iff [algebra]
+declare even_power [algebra]
+
 end
+
+context ring_parity
+begin
+
+declare even_minus [algebra]
+
+end
+
+declare even_Suc [algebra]
+declare even_diff_nat [algebra]
+
+end
--- a/src/HOL/HOL.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -1701,6 +1701,29 @@
 ML_file "Tools/cnf.ML"
 
 
+section {* @{text NO_MATCH} simproc *}
+
+text {*
+ The simplification procedure can be used to avoid simplification of terms of a certain form
+*}
+
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
+
+simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
+    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
+  in if m then NONE else SOME @{thm NO_MATCH_def} end
+*}
+
+text {*
+  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
+  is only applied, if the pattern @{term pat} does not match the value @{term val}.
+*}
+
+
 subsection {* Code generator setup *}
 
 subsubsection {* Generic code generator preprocessor setup *}
--- a/src/HOL/Main.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Main.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -2,7 +2,7 @@
 
 theory Main
 imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
-  BNF_Greatest_Fixpoint Parity
+  BNF_Greatest_Fixpoint
 begin
 
 text {*
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -5915,29 +5915,10 @@
   proof -
     fix y
     assume as: "y\<in>cbox (x - ?d) (x + ?d)"
-    {
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
-        using as[unfolded mem_box, THEN bspec[where x=i]] i
-        by (auto simp: inner_simps)
-      then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
-        apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
-        unfolding mult.assoc[symmetric]
-        using assms
-        by (auto simp add: field_simps)
-      then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
-        "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
-        using `0<d` by (auto simp add: field_simps) }
     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
-      unfolding mem_box using assms
-      by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
-    then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
-      apply -
-      apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
-      using assms
-      apply auto
-      done
+      using assms by (simp add: mem_box field_simps inner_simps)
+    with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
+      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
   next
     fix y z
     assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
@@ -6076,7 +6057,7 @@
           using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
           by (auto simp add:field_simps)
         also have "\<dots> = (f w + t * f y) / (1 + t)"
-          using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
+          using `t > 0` by (auto simp add: divide_simps)
         also have "\<dots> < e + f y"
           using `t > 0` * `e > 0` by (auto simp add: field_simps)
         finally have "f x - f y < e" by auto
--- a/src/HOL/Parity.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Parity.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -6,7 +6,7 @@
 header {* Even and Odd for int and nat *}
 
 theory Parity
-imports Presburger
+imports Nat_Transfer
 begin
 
 subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
@@ -36,7 +36,7 @@
 lemma two_dvd_diff_iff:
   fixes k l :: int
   shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
-  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
+  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
 
 lemma two_dvd_abs_add_iff:
   fixes k l :: int
@@ -139,48 +139,6 @@
   then show "\<exists>l. k = l + 1" ..
 qed
 
-context semiring_div_parity
-begin
-
-subclass semiring_parity
-proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
-  fix a b c
-  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
-    by simp
-next
-  fix a b c
-  assume "(b + c) mod a = 0"
-  with mod_add_eq [of b c a]
-  have "(b mod a + c mod a) mod a = 0"
-    by simp
-  moreover assume "b mod a = 0"
-  ultimately show "c mod a = 0"
-    by simp
-next
-  show "1 mod 2 = 1"
-    by (fact one_mod_two_eq_one)
-next
-  fix a b
-  assume "a mod 2 = 1"
-  moreover assume "b mod 2 = 1"
-  ultimately show "(a + b) mod 2 = 0"
-    using mod_add_eq [of a b 2] by simp
-next
-  fix a b
-  assume "(a * b) mod 2 = 0"
-  then have "(a mod 2) * (b mod 2) = 0"
-    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
-  then show "a mod 2 = 0 \<or> b mod 2 = 0"
-    by (rule divisors_zero)
-next
-  fix a
-  assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
-  then show "\<exists>b. a = b + 1" ..
-qed
-
-end
-
 
 subsection {* Dedicated @{text even}/@{text odd} predicate *}
 
@@ -274,47 +232,6 @@
 end
 
 
-subsubsection {* Parity and division *}
-
-context semiring_div_parity
-begin
-
-lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
-  "1 div 2 = 0"
-proof (cases "2 = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
-  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
-  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
-  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
-  with False show ?thesis by auto
-qed
-
-lemma even_iff_mod_2_eq_zero:
-  "even a \<longleftrightarrow> a mod 2 = 0"
-  by (fact dvd_eq_mod_eq_0)
-
-lemma even_succ_div_two [simp]:
-  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
-  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
-  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
-  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
-
-lemma even_two_times_div_two:
-  "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ:
-  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
-  
-end
-
-
 subsubsection {* Particularities for @{typ nat} and @{typ int} *}
 
 lemma even_Suc [simp]:
@@ -342,44 +259,6 @@
   "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
   by simp
 
-lemma even_Suc_div_two [simp]:
-  "even n \<Longrightarrow> Suc n div 2 = n div 2"
-  using even_succ_div_two [of n] by simp
-  
-lemma odd_Suc_div_two [simp]:
-  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
-  using odd_succ_div_two [of n] by simp
-
-lemma odd_two_times_div_two_Suc:
-  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
-  using odd_two_times_div_two_succ [of n] by simp
-
-lemma parity_induct [case_names zero even odd]:
-  assumes zero: "P 0"
-  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
-  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
-  shows "P n"
-proof (induct n rule: less_induct)
-  case (less n)
-  show "P n"
-  proof (cases "n = 0")
-    case True with zero show ?thesis by simp
-  next
-    case False
-    with less have hyp: "P (n div 2)" by simp
-    show ?thesis
-    proof (cases "even n")
-      case True
-      with hyp even [of "n div 2"] show ?thesis
-        by (simp add: dvd_mult_div_cancel)
-    next
-      case False
-      with hyp odd [of "n div 2"] show ?thesis 
-        by (simp add: odd_two_times_div_two_Suc)
-    qed
-  qed
-qed
-  
 text {* Parity and powers *}
 
 context comm_ring_1
@@ -546,77 +425,5 @@
   even_int_iff
 ]
 
-context semiring_parity
-begin
-
-declare even_times_iff [presburger, algebra]
-
-declare even_power [presburger, algebra]
-
-lemma [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
-
-declare even_diff_nat [presburger, algebra]
-
-lemma [presburger]:
-  fixes k :: int
-  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
-  by presburger
-
-lemma [presburger]:
-  fixes k :: int
-  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
-  by presburger
-
-lemma [presburger]:
-  "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
-
--- a/src/HOL/Presburger.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Presburger.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -434,6 +434,78 @@
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
+context semiring_parity
+begin
+
+declare even_times_iff [presburger]
+
+declare even_power [presburger]
+
+lemma [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]
+
+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]
+
+lemma [presburger]:
+  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+  by presburger
+
+declare even_diff_nat [presburger]
+
+lemma [presburger]:
+  fixes k :: int
+  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
+  by presburger
+
+lemma [presburger]:
+  fixes k :: int
+  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
+  by presburger
+
+lemma [presburger]:
+  "even n \<longleftrightarrow> even (int n)"
+  using even_int_iff [of n] by simp
+  
+
+subsection {* 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
+
 
 subsection {* Try0 *}
 
--- a/src/HOL/Rings.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Rings.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -14,8 +14,8 @@
 begin
 
 class semiring = ab_semigroup_add + semigroup_mult +
-  assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
-  assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
+  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
+  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
 begin
 
 text{*For the @{text combine_numerals} simproc*}
@@ -299,11 +299,11 @@
 lemma minus_mult_commute: "- a * b = a * - b"
 by simp
 
-lemma right_diff_distrib [algebra_simps, field_simps]:
+lemma right_diff_distrib [algebra_simps]:
   "a * (b - c) = a * b - a * c"
   using distrib_left [of a b "-c "] by simp
 
-lemma left_diff_distrib [algebra_simps, field_simps]:
+lemma left_diff_distrib [algebra_simps]:
   "(a - b) * c = a * c - b * c"
   using distrib_right [of a "- b" c] by simp
 
--- a/src/HOL/SMT.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/SMT.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -322,6 +322,7 @@
   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
   if_True if_False not_not
+  NO_MATCH_def
 
 lemma [z3_rule]:
   "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))"
--- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 20:49:23 2014 +0200
@@ -121,7 +121,7 @@
   val basic_simpset =
     simpset_of (put_simpset HOL_ss @{context}
       addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
-        arith_simps rel_simps array_rules z3div_def z3mod_def}
+        arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
       addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
         Simplifier.simproc_global @{theory} "fast_int_arith" [
           "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
--- a/src/HOL/ex/Lagrange.thy	Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/ex/Lagrange.thy	Fri Oct 24 20:49:23 2014 +0200
@@ -28,7 +28,7 @@
    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
-by (simp only: sq_def field_simps)
+by (simp only: sq_def algebra_simps)
 
 
 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
@@ -44,6 +44,6 @@
       sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
       sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-by (simp only: sq_def field_simps)
+by (simp only: sq_def algebra_simps)
 
 end