explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
authorhaftmann
Tue Mar 26 20:49:57 2013 +0100 (2013-03-26)
changeset 51540eea5c4ca4a0e
parent 51539 625d2ec0bbff
child 51545 6f6012f430fc
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/Lattices.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Saturated.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Mar 26 15:10:28 2013 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Mar 26 20:49:57 2013 +0100
     1.3 @@ -1694,6 +1694,21 @@
     1.4  where
     1.5    "Max = semilattice_set.F max"
     1.6  
     1.7 +sublocale linorder < Min!: semilattice_order_set min less_eq less
     1.8 +  + Max!: semilattice_order_set max greater_eq greater
     1.9 +where
    1.10 +  "semilattice_set.F min = Min"
    1.11 +  and "semilattice_set.F max = Max"
    1.12 +proof -
    1.13 +  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
    1.14 +  then interpret Min!: semilattice_order_set min less_eq less.
    1.15 +  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
    1.16 +  then interpret Max!: semilattice_order_set max greater_eq greater .
    1.17 +  from Min_def show "semilattice_set.F min = Min" by rule
    1.18 +  from Max_def show "semilattice_set.F max = Max" by rule
    1.19 +qed
    1.20 +
    1.21 +
    1.22  text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
    1.23  
    1.24  sublocale linorder < min_max!: distrib_lattice min less_eq less max
    1.25 @@ -1714,20 +1729,14 @@
    1.26      by (simp only: min_max.Sup_fin_def Max_def)
    1.27  qed
    1.28  
    1.29 -lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.30 -  by (rule ext)+ (auto intro: antisym)
    1.31 -
    1.32 -lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.33 -  by (rule ext)+ (auto intro: antisym)
    1.34 -
    1.35  lemmas le_maxI1 = min_max.sup_ge1
    1.36  lemmas le_maxI2 = min_max.sup_ge2
    1.37   
    1.38  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
    1.39 -  min_max.inf.left_commute
    1.40 +  min.left_commute
    1.41  
    1.42  lemmas max_ac = min_max.sup_assoc min_max.sup_commute
    1.43 -  min_max.sup.left_commute
    1.44 +  max.left_commute
    1.45  
    1.46  
    1.47  text {* Lattice operations proper *}
    1.48 @@ -1753,6 +1762,18 @@
    1.49  qed
    1.50  
    1.51  
    1.52 +text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
    1.53 +
    1.54 +lemma Inf_fin_Min:
    1.55 +  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
    1.56 +  by (simp add: Inf_fin_def Min_def inf_min)
    1.57 +
    1.58 +lemma Sup_fin_Max:
    1.59 +  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
    1.60 +  by (simp add: Sup_fin_def Max_def sup_max)
    1.61 +
    1.62 +
    1.63 +
    1.64  subsection {* Infimum and Supremum over non-empty sets *}
    1.65  
    1.66  text {*
    1.67 @@ -1920,34 +1941,34 @@
    1.68    show ?thesis by (simp add: dual.Max_def dual_max Min_def)
    1.69  qed
    1.70  
    1.71 -lemmas Min_singleton = min_max.Inf_fin.singleton
    1.72 -lemmas Max_singleton = min_max.Sup_fin.singleton
    1.73 -lemmas Min_insert = min_max.Inf_fin.insert
    1.74 -lemmas Max_insert = min_max.Sup_fin.insert
    1.75 -lemmas Min_Un = min_max.Inf_fin.union
    1.76 -lemmas Max_Un = min_max.Sup_fin.union
    1.77 -lemmas hom_Min_commute = min_max.Inf_fin.hom_commute
    1.78 -lemmas hom_Max_commute = min_max.Sup_fin.hom_commute
    1.79 +lemmas Min_singleton = Min.singleton
    1.80 +lemmas Max_singleton = Max.singleton
    1.81 +lemmas Min_insert = Min.insert
    1.82 +lemmas Max_insert = Max.insert
    1.83 +lemmas Min_Un = Min.union
    1.84 +lemmas Max_Un = Max.union
    1.85 +lemmas hom_Min_commute = Min.hom_commute
    1.86 +lemmas hom_Max_commute = Max.hom_commute
    1.87  
    1.88  lemma Min_in [simp]:
    1.89    assumes "finite A" and "A \<noteq> {}"
    1.90    shows "Min A \<in> A"
    1.91 -  using assms by (auto simp add: min_def min_max.Inf_fin.closed)
    1.92 +  using assms by (auto simp add: min_def Min.closed)
    1.93  
    1.94  lemma Max_in [simp]:
    1.95    assumes "finite A" and "A \<noteq> {}"
    1.96    shows "Max A \<in> A"
    1.97 -  using assms by (auto simp add: max_def min_max.Sup_fin.closed)
    1.98 +  using assms by (auto simp add: max_def Max.closed)
    1.99  
   1.100  lemma Min_le [simp]:
   1.101    assumes "finite A" and "x \<in> A"
   1.102    shows "Min A \<le> x"
   1.103 -  using assms by (fact min_max.Inf_fin.coboundedI)
   1.104 +  using assms by (fact Min.coboundedI)
   1.105  
   1.106  lemma Max_ge [simp]:
   1.107    assumes "finite A" and "x \<in> A"
   1.108    shows "x \<le> Max A"
   1.109 -  using assms by (fact min_max.Sup_fin.coboundedI)
   1.110 +  using assms by (fact Max.coboundedI)
   1.111  
   1.112  lemma Min_eqI:
   1.113    assumes "finite A"
   1.114 @@ -1976,12 +1997,12 @@
   1.115  lemma Min_ge_iff [simp, no_atp]:
   1.116    assumes "finite A" and "A \<noteq> {}"
   1.117    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.118 -  using assms by (fact min_max.Inf_fin.bounded_iff)
   1.119 +  using assms by (fact Min.bounded_iff)
   1.120  
   1.121  lemma Max_le_iff [simp, no_atp]:
   1.122    assumes "finite A" and "A \<noteq> {}"
   1.123    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   1.124 -  using assms by (fact min_max.Sup_fin.bounded_iff)
   1.125 +  using assms by (fact Max.bounded_iff)
   1.126  
   1.127  lemma Min_gr_iff [simp, no_atp]:
   1.128    assumes "finite A" and "A \<noteq> {}"
   1.129 @@ -2016,12 +2037,12 @@
   1.130  lemma Min_antimono:
   1.131    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   1.132    shows "Min N \<le> Min M"
   1.133 -  using assms by (fact min_max.Inf_fin.antimono)
   1.134 +  using assms by (fact Min.antimono)
   1.135  
   1.136  lemma Max_mono:
   1.137    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   1.138    shows "Max M \<le> Max N"
   1.139 -  using assms by (fact min_max.Sup_fin.antimono)
   1.140 +  using assms by (fact Max.antimono)
   1.141  
   1.142  lemma mono_Min_commute:
   1.143    assumes "mono f"
   1.144 @@ -2133,5 +2154,28 @@
   1.145  
   1.146  end
   1.147  
   1.148 +context complete_linorder
   1.149 +begin
   1.150 +
   1.151 +lemma Min_Inf:
   1.152 +  assumes "finite A" and "A \<noteq> {}"
   1.153 +  shows "Min A = Inf A"
   1.154 +proof -
   1.155 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.156 +  then show ?thesis
   1.157 +    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   1.158 +qed
   1.159 +
   1.160 +lemma Max_Sup:
   1.161 +  assumes "finite A" and "A \<noteq> {}"
   1.162 +  shows "Max A = Sup A"
   1.163 +proof -
   1.164 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.165 +  then show ?thesis
   1.166 +    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   1.167 +qed
   1.168 +
   1.169  end
   1.170  
   1.171 +end
   1.172 +
     2.1 --- a/src/HOL/Complete_Lattices.thy	Tue Mar 26 15:10:28 2013 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Mar 26 20:49:57 2013 +0100
     2.3 @@ -514,10 +514,10 @@
     2.4    by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
     2.5  
     2.6  lemma complete_linorder_inf_min: "inf = min"
     2.7 -  by (rule ext)+ (auto intro: antisym simp add: min_def)
     2.8 +  by (auto intro: antisym simp add: min_def fun_eq_iff)
     2.9  
    2.10  lemma complete_linorder_sup_max: "sup = max"
    2.11 -  by (rule ext)+ (auto intro: antisym simp add: max_def)
    2.12 +  by (auto intro: antisym simp add: max_def fun_eq_iff)
    2.13  
    2.14  lemma Inf_less_iff:
    2.15    "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
     3.1 --- a/src/HOL/IMP/Sec_Typing.thy	Tue Mar 26 15:10:28 2013 +0100
     3.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Tue Mar 26 20:49:57 2013 +0100
     3.3 @@ -233,7 +233,7 @@
     3.4  apply(induction rule: sec_type2.induct)
     3.5  apply (metis Skip')
     3.6  apply (metis Assign' eq_imp_le)
     3.7 -apply (metis Seq' anti_mono' min_max.inf.commute min_max.inf_le2)
     3.8 +apply (metis Seq' anti_mono' min_max.inf_le1 min_max.inf_le2)
     3.9  apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
    3.10  by (metis While')
    3.11  
     4.1 --- a/src/HOL/Lattices.thy	Tue Mar 26 15:10:28 2013 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Tue Mar 26 20:49:57 2013 +0100
     4.3 @@ -689,6 +689,19 @@
     4.4  end
     4.5  
     4.6  
     4.7 +subsection {* @{text "min/max"} as special case of lattice *}
     4.8 +
     4.9 +sublocale linorder < min!: semilattice_order min less_eq less
    4.10 +  + max!: semilattice_order max greater_eq greater
    4.11 +  by default (auto simp add: min_def max_def)
    4.12 +
    4.13 +lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    4.14 +  by (auto intro: antisym simp add: min_def fun_eq_iff)
    4.15 +
    4.16 +lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    4.17 +  by (auto intro: antisym simp add: max_def fun_eq_iff)
    4.18 +
    4.19 +
    4.20  subsection {* Uniqueness of inf and sup *}
    4.21  
    4.22  lemma (in semilattice_inf) inf_unique:
     5.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Mar 26 15:10:28 2013 +0100
     5.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Mar 26 20:49:57 2013 +0100
     5.3 @@ -319,7 +319,7 @@
     5.4    from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
     5.5    with assms show ?thesis
     5.6      by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
     5.7 -      min_max.Inf_fin.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
     5.8 +      Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
     5.9  qed
    5.10  
    5.11  (* maximum *)
    5.12 @@ -336,7 +336,7 @@
    5.13    fixes xs :: "('a :: linorder) list"
    5.14    assumes "xs \<noteq> []"
    5.15    shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
    5.16 -  using assms by (simp add: min_max.Sup_fin.set_eq_fold [symmetric])
    5.17 +  using assms by (simp add: Max.set_eq_fold [symmetric])
    5.18  
    5.19  lemma rbt_max_simps:
    5.20    assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
    5.21 @@ -413,7 +413,7 @@
    5.22    from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
    5.23    with assms show ?thesis
    5.24      by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
    5.25 -      min_max.Sup_fin.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
    5.26 +      Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
    5.27  qed
    5.28  
    5.29  
     6.1 --- a/src/HOL/Library/Saturated.thy	Tue Mar 26 15:10:28 2013 +0100
     6.2 +++ b/src/HOL/Library/Saturated.thy	Tue Mar 26 20:49:57 2013 +0100
     6.3 @@ -45,7 +45,7 @@
     6.4  
     6.5  lemma min_nat_of_len_of [simp]:
     6.6    "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
     6.7 -  by (subst min_max.inf.commute) simp
     6.8 +  by (subst min.commute) simp
     6.9  
    6.10  lemma Abs_sat'_nat_of [simp]:
    6.11    "Abs_sat' (nat_of n) = n"
     7.1 --- a/src/HOL/List.thy	Tue Mar 26 15:10:28 2013 +0100
     7.2 +++ b/src/HOL/List.thy	Tue Mar 26 20:49:57 2013 +0100
     7.3 @@ -2783,8 +2783,8 @@
     7.4  
     7.5  declare Inf_fin.set_eq_fold [code]
     7.6  declare Sup_fin.set_eq_fold [code]
     7.7 -declare min_max.Inf_fin.set_eq_fold [code]
     7.8 -declare min_max.Sup_fin.set_eq_fold [code]
     7.9 +declare Min.set_eq_fold [code]
    7.10 +declare Max.set_eq_fold [code]
    7.11  
    7.12  lemma (in complete_lattice) Inf_set_fold:
    7.13    "Inf (set xs) = fold inf xs top"