use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
authorhoelzl
Fri Oct 24 15:07:51 2014 +0200 (2014-10-24)
changeset 5877695e58e04e534
parent 58775 9cd64a66a765
child 58777 6ba2f1fa243b
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
NEWS
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Rings.thy
src/HOL/SMT.thy
src/HOL/Tools/SMT/z3_replay_util.ML
src/HOL/ex/Lagrange.thy
     1.1 --- a/NEWS	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/NEWS	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -65,6 +65,12 @@
     1.4  * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
     1.8 +  non-termination in case of distributing a division. With this change
     1.9 +  field_simps is in some cases slightly less powerful, if it fails try
    1.10 +  to add algebra_simps, or use divide_simps.
    1.11 +Minor INCOMPATIBILITY.
    1.12 +
    1.13  * Bootstrap of listsum as special case of abstract product over lists.
    1.14  Fact rename:
    1.15      listsum_def ~> listsum.eq_foldr
     2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:49 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:51 2014 +0200
     2.3 @@ -375,7 +375,7 @@
     2.4  
     2.5  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
     2.6    by (induct p q rule: polyadd.induct)
     2.7 -    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
     2.8 +     (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
     2.9  
    2.10  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
    2.11    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
     3.1 --- a/src/HOL/Fields.thy	Fri Oct 24 15:07:49 2014 +0200
     3.2 +++ b/src/HOL/Fields.thy	Fri Oct 24 15:07:51 2014 +0200
     3.3 @@ -23,11 +23,37 @@
     3.4    fixes inverse :: "'a \<Rightarrow> 'a"
     3.5      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
     3.6  
     3.7 +setup {* Sign.add_const_constraint
     3.8 +  (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
     3.9 +
    3.10 +
    3.11 +context semiring
    3.12 +begin
    3.13 +
    3.14 +lemma [field_simps]:
    3.15 +  shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
    3.16 +    and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
    3.17 +  by (rule distrib_left distrib_right)+
    3.18 +
    3.19 +end
    3.20 +
    3.21 +context ring
    3.22 +begin
    3.23 +
    3.24 +lemma [field_simps]:
    3.25 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
    3.26 +    and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
    3.27 +  by (rule left_diff_distrib right_diff_distrib)+
    3.28 +
    3.29 +end
    3.30 +
    3.31 +setup {* Sign.add_const_constraint
    3.32 +  (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    3.33 +
    3.34  text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
    3.35  
    3.36  named_theorems divide_simps "rewrite rules to eliminate divisions"
    3.37  
    3.38 -
    3.39  class division_ring = ring_1 + inverse +
    3.40    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    3.41    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
     4.1 --- a/src/HOL/GCD.thy	Fri Oct 24 15:07:49 2014 +0200
     4.2 +++ b/src/HOL/GCD.thy	Fri Oct 24 15:07:51 2014 +0200
     4.3 @@ -1049,7 +1049,7 @@
     4.4        apply (subst mod_div_equality [of m n, symmetric])
     4.5        (* applying simp here undoes the last substitution!
     4.6           what is procedure cancel_div_mod? *)
     4.7 -      apply (simp only: field_simps of_nat_add of_nat_mult)
     4.8 +      apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
     4.9        done
    4.10  qed
    4.11  
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:49 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:51 2014 +0200
     5.3 @@ -5915,29 +5915,10 @@
     5.4    proof -
     5.5      fix y
     5.6      assume as: "y\<in>cbox (x - ?d) (x + ?d)"
     5.7 -    {
     5.8 -      fix i :: 'a
     5.9 -      assume i: "i \<in> Basis"
    5.10 -      have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
    5.11 -        using as[unfolded mem_box, THEN bspec[where x=i]] i
    5.12 -        by (auto simp: inner_simps)
    5.13 -      then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
    5.14 -        apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
    5.15 -        unfolding mult.assoc[symmetric]
    5.16 -        using assms
    5.17 -        by (auto simp add: field_simps)
    5.18 -      then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
    5.19 -        "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
    5.20 -        using `0<d` by (auto simp add: field_simps) }
    5.21      then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
    5.22 -      unfolding mem_box using assms
    5.23 -      by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
    5.24 -    then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
    5.25 -      apply -
    5.26 -      apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
    5.27 -      using assms
    5.28 -      apply auto
    5.29 -      done
    5.30 +      using assms by (simp add: mem_box field_simps inner_simps)
    5.31 +    with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
    5.32 +      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
    5.33    next
    5.34      fix y z
    5.35      assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
    5.36 @@ -6076,7 +6057,7 @@
    5.37            using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
    5.38            by (auto simp add:field_simps)
    5.39          also have "\<dots> = (f w + t * f y) / (1 + t)"
    5.40 -          using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
    5.41 +          using `t > 0` by (auto simp add: divide_simps)
    5.42          also have "\<dots> < e + f y"
    5.43            using `t > 0` * `e > 0` by (auto simp add: field_simps)
    5.44          finally have "f x - f y < e" by auto
     6.1 --- a/src/HOL/Rings.thy	Fri Oct 24 15:07:49 2014 +0200
     6.2 +++ b/src/HOL/Rings.thy	Fri Oct 24 15:07:51 2014 +0200
     6.3 @@ -14,8 +14,8 @@
     6.4  begin
     6.5  
     6.6  class semiring = ab_semigroup_add + semigroup_mult +
     6.7 -  assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
     6.8 -  assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
     6.9 +  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
    6.10 +  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
    6.11  begin
    6.12  
    6.13  text{*For the @{text combine_numerals} simproc*}
    6.14 @@ -299,11 +299,11 @@
    6.15  lemma minus_mult_commute: "- a * b = a * - b"
    6.16  by simp
    6.17  
    6.18 -lemma right_diff_distrib [algebra_simps, field_simps]:
    6.19 +lemma right_diff_distrib [algebra_simps]:
    6.20    "a * (b - c) = a * b - a * c"
    6.21    using distrib_left [of a b "-c "] by simp
    6.22  
    6.23 -lemma left_diff_distrib [algebra_simps, field_simps]:
    6.24 +lemma left_diff_distrib [algebra_simps]:
    6.25    "(a - b) * c = a * c - b * c"
    6.26    using distrib_right [of a "- b" c] by simp
    6.27  
     7.1 --- a/src/HOL/SMT.thy	Fri Oct 24 15:07:49 2014 +0200
     7.2 +++ b/src/HOL/SMT.thy	Fri Oct 24 15:07:51 2014 +0200
     7.3 @@ -322,6 +322,7 @@
     7.4    refl eq_commute conj_commute disj_commute simp_thms nnf_simps
     7.5    ring_distribs field_simps times_divide_eq_right times_divide_eq_left
     7.6    if_True if_False not_not
     7.7 +  NO_MATCH_def
     7.8  
     7.9  lemma [z3_rule]:
    7.10    "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))"
     8.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:49 2014 +0200
     8.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:51 2014 +0200
     8.3 @@ -121,7 +121,7 @@
     8.4    val basic_simpset =
     8.5      simpset_of (put_simpset HOL_ss @{context}
     8.6        addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
     8.7 -        arith_simps rel_simps array_rules z3div_def z3mod_def}
     8.8 +        arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
     8.9        addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
    8.10          Simplifier.simproc_global @{theory} "fast_int_arith" [
    8.11            "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
     9.1 --- a/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:49 2014 +0200
     9.2 +++ b/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:51 2014 +0200
     9.3 @@ -28,7 +28,7 @@
     9.4     sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
     9.5     sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
     9.6     sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
     9.7 -by (simp only: sq_def field_simps)
     9.8 +by (simp only: sq_def algebra_simps)
     9.9  
    9.10  
    9.11  text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    9.12 @@ -44,6 +44,6 @@
    9.13        sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    9.14        sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    9.15        sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    9.16 -by (simp only: sq_def field_simps)
    9.17 +by (simp only: sq_def algebra_simps)
    9.18  
    9.19  end