# HG changeset patch
# User haftmann
# Date 1592296899 0
# Node ID e1b262e7480ceb20d9a8de7410015cf80d8203af
# Parent  92de7d74b8f81be766e0650b2c09a2a85d7ae917
interpretations for boolean operators

diff -r 92de7d74b8f8 -r e1b262e7480c src/HOL/Algebra/Cycles.thy
--- a/src/HOL/Algebra/Cycles.thy	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Algebra/Cycles.thy	Tue Jun 16 08:41:39 2020 +0000
@@ -160,7 +160,7 @@
       using aui_lemma[OF assms] by simp
   next
     case 2 thus ?thesis
-      using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps(8))
+      using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps)
   next
     case 3 thus ?thesis
       by (simp add: id_outside_supp)
diff -r 92de7d74b8f8 -r e1b262e7480c src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jun 16 08:41:39 2020 +0000
@@ -2015,8 +2015,8 @@
           "min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
           "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
         using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
-      with False show ?thesis using a_le_b
-        unfolding * by (auto simp: le_divide_eq divide_le_eq ac_simps)
+      with False show ?thesis using a_le_b *
+        by (simp add: le_divide_eq divide_le_eq) (simp add: ac_simps)
     qed
   qed
 qed simp
diff -r 92de7d74b8f8 -r e1b262e7480c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jun 16 08:41:39 2020 +0000
@@ -2545,8 +2545,7 @@
 
 lemma comm_monoid_set_F_and: "comm_monoid_set.F (\<and>) True f s \<longleftrightarrow> (finite s \<longrightarrow> (\<forall>x\<in>s. f x))"
 proof -
-  interpret bool: comm_monoid_set "(\<and>)" True
-    proof qed auto
+  interpret bool: comm_monoid_set \<open>(\<and>)\<close> True ..
   show ?thesis
     by (induction s rule: infinite_finite_induct) auto
 qed
diff -r 92de7d74b8f8 -r e1b262e7480c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Lattices.thy	Tue Jun 16 08:41:39 2020 +0000
@@ -145,16 +145,16 @@
 
 end
 
-text \<open>Passive interpretations for boolean operators\<close>
+text \<open>Interpretations for boolean operators\<close>
 
-lemma semilattice_neutr_and:
-  "semilattice_neutr HOL.conj True"
+interpretation conj: semilattice_neutr \<open>(\<and>)\<close> True
   by standard auto
 
-lemma semilattice_neutr_or:
-  "semilattice_neutr HOL.disj False"
+interpretation disj: semilattice_neutr \<open>(\<or>)\<close> False
   by standard auto
 
+declare conj_assoc [ac_simps del] disj_assoc [ac_simps del] \<comment> \<open>already simp by default\<close>
+
 
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
diff -r 92de7d74b8f8 -r e1b262e7480c src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jun 16 08:41:39 2020 +0000
@@ -353,7 +353,7 @@
     using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
   also have "\<dots> = (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j))"
     by (rule prod.reindex_cong [of "\<lambda>x. x - i"])
-       (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
+      (auto simp: image_iff ac_simps nat_eq_diff_eq cong: conj_cong intro!: inj_onI)
   also have "emeasure S ?E = (\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j))"
     using J by (intro emeasure_PiM_emb) simp_all
   also have "(\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j)) * (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
@@ -384,7 +384,7 @@
     using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
   also have "\<dots> = (\<Prod>j\<in>J - {0}. emeasure M (E j))"
     by (rule prod.reindex_cong [of "\<lambda>x. x - 1"])
-       (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
+      (auto simp: image_iff nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
   also have "emeasure M ?E * (\<Prod>j\<in>J - {0}. emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
     by (auto simp: M.emeasure_space_1 prod.remove J)
   finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .