# HG changeset patch
# User nipkow
# Date 1114096937 -7200
# Node ID 446ec11266be9aefcb9b6e8981b4fe4559c96809
# Parent  e68dab670fc54b19627e8238dd5d7d0c96f17451
tuning locales

diff -r e68dab670fc5 -r 446ec11266be src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 21 17:22:17 2005 +0200
@@ -2227,45 +2227,45 @@
 text{* Before we can do anything, we need to show that @{text min} and
 @{text max} are ACI and the ordering is linear: *}
 
-interpretation AC_min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACf.intro)
 apply(auto simp:min_def)
 done
 
-interpretation AC_min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACIf_axioms.intro)
 apply(auto simp:min_def)
 done
 
-interpretation AC_max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACf.intro)
 apply(auto simp:max_def)
 done
 
-interpretation AC_max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACIf_axioms.intro)
 apply(auto simp:max_def)
 done
 
-interpretation AC_min [rule del]:
+interpretation min [rule del]:
   ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:min_def)
 done
 
-interpretation AC_min [rule del]:
+interpretation min [rule del]:
   ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:min_def)
 done
 
-interpretation AC_max [rule del]:
+interpretation max [rule del]:
   ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:max_def)
 done
 
-interpretation AC_max [rule del]:
+interpretation max [rule del]:
   ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:max_def)
@@ -2295,42 +2295,42 @@
 
 declare
   fold1_singleton_def[OF Min_def, simp]
-  AC_min.fold1_insert_idem_def[OF Min_def, simp]
+  min.fold1_insert_idem_def[OF Min_def, simp]
   fold1_singleton_def[OF Max_def, simp]
-  AC_max.fold1_insert_idem_def[OF Max_def, simp]
+  max.fold1_insert_idem_def[OF Max_def, simp]
 
 text{* Now we instantiate some @{text fold1} properties: *}
 
 lemma Min_in [simp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
-using AC_min.fold1_in
+using min.fold1_in
 by(fastsimp simp: Min_def min_def)
 
 lemma Max_in [simp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
-using AC_max.fold1_in
+using max.fold1_in
 by(fastsimp simp: Max_def max_def)
 
 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
-by(simp add: Min_def AC_min.fold1_belowI)
+by(simp add: Min_def min.fold1_belowI)
 
 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
-by(simp add: Max_def AC_max.fold1_belowI)
+by(simp add: Max_def max.fold1_belowI)
 
 lemma Min_ge_iff[simp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
-by(simp add: Min_def AC_min.below_fold1_iff)
+by(simp add: Min_def min.below_fold1_iff)
 
 lemma Max_le_iff[simp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
-by(simp add: Max_def AC_max.below_fold1_iff)
+by(simp add: Max_def max.below_fold1_iff)
 
 lemma Min_le_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
-by(simp add: Min_def AC_min.fold1_below_iff)
+by(simp add: Min_def min.fold1_below_iff)
 
 lemma Max_ge_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
-by(simp add: Max_def AC_max.fold1_below_iff)
+by(simp add: Max_def max.fold1_below_iff)
 
 end
diff -r e68dab670fc5 -r 446ec11266be src/HOL/Lattice_Locales.thy
--- a/src/HOL/Lattice_Locales.thy	Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Lattice_Locales.thy	Thu Apr 21 17:22:17 2005 +0200
@@ -52,6 +52,12 @@
 lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
 by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
 
+lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+by (simp add: inf_assoc[symmetric])
+
+lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+by (simp add: sup_assoc[symmetric])
+
 lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
 by(blast intro: antisym inf_le1 inf_least sup_ge1)
 
diff -r e68dab670fc5 -r 446ec11266be src/HOL/Orderings.ML
--- a/src/HOL/Orderings.ML	Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Orderings.ML	Thu Apr 21 17:22:17 2005 +0200
@@ -33,8 +33,10 @@
 val linorder_not_le = thm "linorder_not_le";
 val linorder_neq_iff = thm "linorder_neq_iff";
 val linorder_neqE = thm "linorder_neqE";
+(*
 val min_same = thm "min_same";
 val max_same = thm "max_same";
+*)
 val le_max_iff_disj = thm "le_max_iff_disj";
 val le_maxI1 = thm "le_maxI1";
 val le_maxI2 = thm "le_maxI2";
diff -r e68dab670fc5 -r 446ec11266be src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 21 17:22:17 2005 +0200
@@ -390,12 +390,6 @@
 
 subsection "Min and max on (linear) orders"
 
-lemma min_same [simp]: "min (x::'a::order) x = x"
-  by (simp add: min_def)
-
-lemma max_same [simp]: "max (x::'a::order) x = x"
-  by (simp add: max_def)
-
 text{* Instantiate locales: *}
 
 interpretation min_max [rule del]:
@@ -461,12 +455,7 @@
   apply (insert linorder_less_linear)
   apply (blast intro: order_less_trans)
   done
-(*
-lemma le_min_iff_conj [simp]:
-    "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
-    -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
-by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
-*)
+
 lemma min_less_iff_conj [simp]:
     "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   apply (simp add: order_le_less min_def)
@@ -485,22 +474,10 @@
   apply (insert linorder_less_linear)
   apply (blast intro: order_less_trans)
   done
-(*
-lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
-by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
 
-lemma max_commute: "!!x::'a::linorder. max x y = max y x"
-by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
-*)
 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
                mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
-(*
-lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
-by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
 
-lemma min_commute: "!!x::'a::linorder. min x y = min y x"
-by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
-*)
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
                mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]