# HG changeset patch
# User hoelzl
# Date 1414156071 -7200
# Node ID 95e58e04e534ea4c2b05dffe38e827432a6c3dc4
# Parent  9cd64a66a76534969ebf9f65806f24515ee3311f
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating

diff -r 9cd64a66a765 -r 95e58e04e534 NEWS
--- a/NEWS	Fri Oct 24 15:07:49 2014 +0200
+++ b/NEWS	Fri Oct 24 15:07:51 2014 +0200
@@ -65,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
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:51 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
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Fields.thy	Fri Oct 24 15:07:51 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"
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/GCD.thy	Fri Oct 24 15:07:51 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
 
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:51 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
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Rings.thy	Fri Oct 24 15:07:51 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
 
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/SMT.thy	Fri Oct 24 15:07:51 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))"
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/Tools/SMT/z3_replay_util.ML
--- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:51 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,
diff -r 9cd64a66a765 -r 95e58e04e534 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:49 2014 +0200
+++ b/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:51 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