# HG changeset patch
# User haftmann
# Date 1387116616 -3600
# Node ID 46e441e61ff52cb875913b92ca88b91ea1e89d9c
# Parent  1e7f2d296e19cb524d42a6409901ce89c5cfa08e
disambiguation of interpretation prefixes

diff -r 1e7f2d296e19 -r 46e441e61ff5 NEWS
--- a/NEWS	Sun Dec 15 15:10:14 2013 +0100
+++ b/NEWS	Sun Dec 15 15:10:16 2013 +0100
@@ -28,6 +28,9 @@
 
 *** HOL ***
 
+* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
+INCOMPATBILITY.
+
 * Code generations are provided for make, fields, extend and truncate
 operations on records.
 
diff -r 1e7f2d296e19 -r 46e441e61ff5 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:14 2013 +0100
+++ b/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:16 2013 +0100
@@ -20,8 +20,8 @@
 interpretation comp_fun_commute f
   by default (simp add: fun_eq_iff left_commute)
 
-interpretation comp_fun_commute "f \<circ> g"
-  by (rule comp_comp_fun_commute)
+interpretation comp?: comp_fun_commute "f \<circ> g"
+  by (fact comp_comp_fun_commute)
 
 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
 where
diff -r 1e7f2d296e19 -r 46e441e61ff5 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:14 2013 +0100
+++ b/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:16 2013 +0100
@@ -127,7 +127,7 @@
 
 end
 
-locale semilattice_order_set = semilattice_order + semilattice_set
+locale semilattice_order_set = binary?: semilattice_order + semilattice_set
 begin
 
 lemma bounded_iff:
@@ -251,7 +251,7 @@
 
 end
 
-locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
+locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
 begin
 
 lemma bounded_iff:
@@ -425,24 +425,23 @@
 context lattice
 begin
 
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
-apply(subgoal_tac "EX a. a:A")
-prefer 2 apply blast
-apply(erule exE)
-apply(rule order_trans)
-apply(erule (1) Inf_fin.coboundedI)
-apply(erule (1) Sup_fin.coboundedI)
-done
+lemma Inf_fin_le_Sup_fin [simp]: 
+  assumes "finite A" and "A \<noteq> {}"
+  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
+proof -
+  from `A \<noteq> {}` obtain a where "a \<in> A" by blast
+  with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
+  moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
+  ultimately show ?thesis by (rule order_trans)
+qed
 
 lemma sup_Inf_absorb [simp]:
-  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
-apply(subst sup_commute)
-apply(simp add: sup_absorb2 Inf_fin.coboundedI)
-done
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
+  by (rule sup_absorb2) (rule Inf_fin.coboundedI)
 
 lemma inf_Sup_absorb [simp]:
-  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
-by (simp add: inf_absorb1 Sup_fin.coboundedI)
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
+  by (rule inf_absorb1) (rule Sup_fin.coboundedI)
 
 end