# HG changeset patch
# User haftmann
# Date 1364327397 -3600
# Node ID eea5c4ca4a0ee533b319d6414cf6a965b66abbef
# Parent  625d2ec0bbff41dac9e55f2c314c8ce6dd7c9f31
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts

diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -1694,6 +1694,21 @@
 where
   "Max = semilattice_set.F max"
 
+sublocale linorder < Min!: semilattice_order_set min less_eq less
+  + Max!: semilattice_order_set max greater_eq greater
+where
+  "semilattice_set.F min = Min"
+  and "semilattice_set.F max = Max"
+proof -
+  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
+  then interpret Min!: semilattice_order_set min less_eq less.
+  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
+  then interpret Max!: semilattice_order_set max greater_eq greater .
+  from Min_def show "semilattice_set.F min = Min" by rule
+  from Max_def show "semilattice_set.F max = Max" by rule
+qed
+
+
 text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
 
 sublocale linorder < min_max!: distrib_lattice min less_eq less max
@@ -1714,20 +1729,14 @@
     by (simp only: min_max.Sup_fin_def Max_def)
 qed
 
-lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
-  by (rule ext)+ (auto intro: antisym)
-
-lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
-  by (rule ext)+ (auto intro: antisym)
-
 lemmas le_maxI1 = min_max.sup_ge1
 lemmas le_maxI2 = min_max.sup_ge2
  
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
-  min_max.inf.left_commute
+  min.left_commute
 
 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
-  min_max.sup.left_commute
+  max.left_commute
 
 
 text {* Lattice operations proper *}
@@ -1753,6 +1762,18 @@
 qed
 
 
+text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
+
+lemma Inf_fin_Min:
+  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
+  by (simp add: Inf_fin_def Min_def inf_min)
+
+lemma Sup_fin_Max:
+  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
+  by (simp add: Sup_fin_def Max_def sup_max)
+
+
+
 subsection {* Infimum and Supremum over non-empty sets *}
 
 text {*
@@ -1920,34 +1941,34 @@
   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
 qed
 
-lemmas Min_singleton = min_max.Inf_fin.singleton
-lemmas Max_singleton = min_max.Sup_fin.singleton
-lemmas Min_insert = min_max.Inf_fin.insert
-lemmas Max_insert = min_max.Sup_fin.insert
-lemmas Min_Un = min_max.Inf_fin.union
-lemmas Max_Un = min_max.Sup_fin.union
-lemmas hom_Min_commute = min_max.Inf_fin.hom_commute
-lemmas hom_Max_commute = min_max.Sup_fin.hom_commute
+lemmas Min_singleton = Min.singleton
+lemmas Max_singleton = Max.singleton
+lemmas Min_insert = Min.insert
+lemmas Max_insert = Max.insert
+lemmas Min_Un = Min.union
+lemmas Max_Un = Max.union
+lemmas hom_Min_commute = Min.hom_commute
+lemmas hom_Max_commute = Max.hom_commute
 
 lemma Min_in [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
-  using assms by (auto simp add: min_def min_max.Inf_fin.closed)
+  using assms by (auto simp add: min_def Min.closed)
 
 lemma Max_in [simp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<in> A"
-  using assms by (auto simp add: max_def min_max.Sup_fin.closed)
+  using assms by (auto simp add: max_def Max.closed)
 
 lemma Min_le [simp]:
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
-  using assms by (fact min_max.Inf_fin.coboundedI)
+  using assms by (fact Min.coboundedI)
 
 lemma Max_ge [simp]:
   assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
-  using assms by (fact min_max.Sup_fin.coboundedI)
+  using assms by (fact Max.coboundedI)
 
 lemma Min_eqI:
   assumes "finite A"
@@ -1976,12 +1997,12 @@
 lemma Min_ge_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
-  using assms by (fact min_max.Inf_fin.bounded_iff)
+  using assms by (fact Min.bounded_iff)
 
 lemma Max_le_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
-  using assms by (fact min_max.Sup_fin.bounded_iff)
+  using assms by (fact Max.bounded_iff)
 
 lemma Min_gr_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
@@ -2016,12 +2037,12 @@
 lemma Min_antimono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"
-  using assms by (fact min_max.Inf_fin.antimono)
+  using assms by (fact Min.antimono)
 
 lemma Max_mono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Max M \<le> Max N"
-  using assms by (fact min_max.Sup_fin.antimono)
+  using assms by (fact Max.antimono)
 
 lemma mono_Min_commute:
   assumes "mono f"
@@ -2133,5 +2154,28 @@
 
 end
 
+context complete_linorder
+begin
+
+lemma Min_Inf:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min A = Inf A"
+proof -
+  from assms obtain b B where "A = insert b B" and "finite B" by auto
+  then show ?thesis
+    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
+qed
+
+lemma Max_Sup:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max A = Sup A"
+proof -
+  from assms obtain b B where "A = insert b B" and "finite B" by auto
+  then show ?thesis
+    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
+qed
+
 end
 
+end
+
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -514,10 +514,10 @@
   by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
 
 lemma complete_linorder_inf_min: "inf = min"
-  by (rule ext)+ (auto intro: antisym simp add: min_def)
+  by (auto intro: antisym simp add: min_def fun_eq_iff)
 
 lemma complete_linorder_sup_max: "sup = max"
-  by (rule ext)+ (auto intro: antisym simp add: max_def)
+  by (auto intro: antisym simp add: max_def fun_eq_iff)
 
 lemma Inf_less_iff:
   "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -233,7 +233,7 @@
 apply(induction rule: sec_type2.induct)
 apply (metis Skip')
 apply (metis Assign' eq_imp_le)
-apply (metis Seq' anti_mono' min_max.inf.commute min_max.inf_le2)
+apply (metis Seq' anti_mono' min_max.inf_le1 min_max.inf_le2)
 apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
 by (metis While')
 
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Lattices.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -689,6 +689,19 @@
 end
 
 
+subsection {* @{text "min/max"} as special case of lattice *}
+
+sublocale linorder < min!: semilattice_order min less_eq less
+  + max!: semilattice_order max greater_eq greater
+  by default (auto simp add: min_def max_def)
+
+lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+  by (auto intro: antisym simp add: min_def fun_eq_iff)
+
+lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+  by (auto intro: antisym simp add: max_def fun_eq_iff)
+
+
 subsection {* Uniqueness of inf and sup *}
 
 lemma (in semilattice_inf) inf_unique:
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -319,7 +319,7 @@
   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   with assms show ?thesis
     by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
-      min_max.Inf_fin.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
+      Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
 qed
 
 (* maximum *)
@@ -336,7 +336,7 @@
   fixes xs :: "('a :: linorder) list"
   assumes "xs \<noteq> []"
   shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
-  using assms by (simp add: min_max.Sup_fin.set_eq_fold [symmetric])
+  using assms by (simp add: Max.set_eq_fold [symmetric])
 
 lemma rbt_max_simps:
   assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
@@ -413,7 +413,7 @@
   from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
   with assms show ?thesis
     by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
-      min_max.Sup_fin.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
+      Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
 qed
 
 
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Library/Saturated.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -45,7 +45,7 @@
 
 lemma min_nat_of_len_of [simp]:
   "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
-  by (subst min_max.inf.commute) simp
+  by (subst min.commute) simp
 
 lemma Abs_sat'_nat_of [simp]:
   "Abs_sat' (nat_of n) = n"
diff -r 625d2ec0bbff -r eea5c4ca4a0e src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/List.thy	Tue Mar 26 20:49:57 2013 +0100
@@ -2783,8 +2783,8 @@
 
 declare Inf_fin.set_eq_fold [code]
 declare Sup_fin.set_eq_fold [code]
-declare min_max.Inf_fin.set_eq_fold [code]
-declare min_max.Sup_fin.set_eq_fold [code]
+declare Min.set_eq_fold [code]
+declare Max.set_eq_fold [code]
 
 lemma (in complete_lattice) Inf_set_fold:
   "Inf (set xs) = fold inf xs top"