# HG changeset patch
# User wenzelm
# Date 1530212756 -7200
# Node ID e14848001c4c41132dc343145c9a157e5b73b274
# Parent  ccacc84e02518a177b0db087bab0526071f43313
avoid pending shyps in global theory facts;

diff -r ccacc84e0251 -r e14848001c4c src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/FOL/ex/Miniscope.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -17,14 +17,19 @@
 
 subsubsection \<open>de Morgan laws\<close>
 
-lemma demorgans:
+lemma demorgans1:
   "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
   "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
   "\<not> \<not> P \<longleftrightarrow> P"
+  by blast+
+
+lemma demorgans2:
   "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
   "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
   by blast+
 
+lemmas demorgans = demorgans1 demorgans2
+
 (*** Removal of --> and <-> (positive and negative occurrences) ***)
 (*Last one is important for computing a compact CNF*)
 lemma nnf_simps:
diff -r ccacc84e0251 -r e14848001c4c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Euclidean_Division.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -1638,7 +1638,7 @@
       by (simp only: *, simp only: l q divide_int_unfold)
         (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
   qed
-qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
 
 end
 
diff -r ccacc84e0251 -r e14848001c4c src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Fields.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -863,10 +863,6 @@
 of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
 explosions.\<close>
 
-lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
-lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-
 (* Only works once linear arithmetic is installed:
 text{*An example:*}
 lemma fixes a b c d e f :: "'a::linordered_field"
diff -r ccacc84e0251 -r e14848001c4c src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -457,7 +457,7 @@
   hence "\<exists>(v::'a) (u::'a) SKF\<^sub>7::'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
     by (metis mult_left_mono)
   then show "\<exists>ca::'a. \<forall>x::'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
-    using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
+    using A2 F4 by (metis F1 \<open>0 < \<bar>inverse c\<bar>\<close> mult.assoc mult_le_cancel_left_pos)
 qed
 
 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
diff -r ccacc84e0251 -r e14848001c4c src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Num.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -1282,14 +1282,20 @@
   numeral for 1 reduces the number of special cases.
 \<close>
 
-lemma mult_1s:
+lemma mult_1s_semiring_numeral:
   "Numeral1 * a = a"
   "a * Numeral1 = a"
+  for a :: "'a::semiring_numeral"
+  by simp_all
+
+lemma mult_1s_ring_1:
   "- Numeral1 * b = - b"
   "b * - Numeral1 = - b"
-  for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
+  for b :: "'a::ring_1"
   by simp_all
 
+lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1
+
 setup \<open>
   Reorient_Proc.add
     (fn Const (@{const_name numeral}, _) $ _ => true
@@ -1385,13 +1391,20 @@
   "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
   by (simp_all add: add.assoc [symmetric])
 
-lemma mult_numeral_left [simp]:
+lemma mult_numeral_left_semiring_numeral:
   "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
-  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
-  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
-  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
+  by (simp add: mult.assoc [symmetric])
+
+lemma mult_numeral_left_ring_1:
+  "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+  "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)"
+  "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)"
   by (simp_all add: mult.assoc [symmetric])
 
+lemmas mult_numeral_left [simp] =
+  mult_numeral_left_semiring_numeral
+  mult_numeral_left_ring_1
+
 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
 
 
diff -r ccacc84e0251 -r e14848001c4c src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Rat.thy	Thu Jun 28 21:05:56 2018 +0200
@@ -529,6 +529,10 @@
 
 end
 
+lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+
+
 instantiation rat :: distrib_lattice
 begin