--- 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:
--- 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
--- 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"
--- 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)"
--- 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
--- 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