src/HOL/Lattices.thy
changeset 21381 79e065f2be95
parent 21312 1d39091a3208
child 21619 dea0914773f7
     1.1 --- a/src/HOL/Lattices.thy	Wed Nov 15 17:05:39 2006 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Nov 15 17:05:40 2006 +0100
     1.3 @@ -166,148 +166,27 @@
     1.4    sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
     1.5  
     1.6  
     1.7 -subsection {* Least value operator and min/max -- properties *}
     1.8 - 
     1.9 -(*FIXME: derive more of the min/max laws generically via semilattices*)
    1.10 -
    1.11 -lemma LeastI2_order:
    1.12 -  "[| P (x::'a::order);
    1.13 -      !!y. P y ==> x <= y;
    1.14 -      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
    1.15 -   ==> Q (Least P)"
    1.16 -  apply (unfold Least_def)
    1.17 -  apply (rule theI2)
    1.18 -    apply (blast intro: order_antisym)+
    1.19 -  done
    1.20 -
    1.21 -lemma Least_equality:
    1.22 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
    1.23 -  apply (simp add: Least_def)
    1.24 -  apply (rule the_equality)
    1.25 -  apply (auto intro!: order_antisym)
    1.26 -  done
    1.27 -
    1.28 -lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    1.29 -  by (simp add: min_def)
    1.30 -
    1.31 -lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    1.32 -  by (simp add: max_def)
    1.33 -
    1.34 -lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
    1.35 -  apply (simp add: min_def)
    1.36 -  apply (blast intro: order_antisym)
    1.37 -  done
    1.38 -
    1.39 -lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
    1.40 -  apply (simp add: max_def)
    1.41 -  apply (blast intro: order_antisym)
    1.42 -  done
    1.43 -
    1.44 -lemma min_of_mono:
    1.45 -    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
    1.46 -  by (simp add: min_def)
    1.47 -
    1.48 -lemma max_of_mono:
    1.49 -    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
    1.50 -  by (simp add: max_def)
    1.51 -
    1.52 -text{* Instantiate locales: *}
    1.53 +subsection {* min/max on linear orders as special case of inf/sup *}
    1.54  
    1.55  interpretation min_max:
    1.56 -  lower_semilattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    1.57 -apply unfold_locales
    1.58 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.59 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.60 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.61 -done
    1.62 -
    1.63 -interpretation min_max:
    1.64 -  upper_semilattice["op \<le>" "op <" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    1.65 -apply unfold_locales
    1.66 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.67 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.68 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.69 -done
    1.70 -
    1.71 -interpretation min_max:
    1.72 -  lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.73 -  by unfold_locales
    1.74 -
    1.75 -interpretation min_max:
    1.76 -  distrib_lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.77 +  distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.78  apply unfold_locales
    1.79 -apply(rule_tac x=x and y=y in linorder_le_cases)
    1.80 -apply(rule_tac x=x and y=z in linorder_le_cases)
    1.81 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.82 -apply(simp add:min_def max_def)
    1.83 -apply(simp add:min_def max_def)
    1.84 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.85 -apply(simp add:min_def max_def)
    1.86 -apply(simp add:min_def max_def)
    1.87 -apply(rule_tac x=x and y=z in linorder_le_cases)
    1.88 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.89 -apply(simp add:min_def max_def)
    1.90 -apply(simp add:min_def max_def)
    1.91 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.92 -apply(simp add:min_def max_def)
    1.93 -apply(simp add:min_def max_def)
    1.94 -done
    1.95 -
    1.96 -lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
    1.97 -  apply(simp add:max_def)
    1.98 -  apply (insert linorder_linear)
    1.99 -  apply (blast intro: order_trans)
   1.100 -  done
   1.101 +apply (simp add: min_def linorder_not_le order_less_imp_le)
   1.102 +apply (simp add: min_def linorder_not_le order_less_imp_le)
   1.103 +apply (simp add: min_def linorder_not_le order_less_imp_le)
   1.104 +apply (simp add: max_def linorder_not_le order_less_imp_le)
   1.105 +apply (simp add: max_def linorder_not_le order_less_imp_le)
   1.106 +unfolding min_def max_def by auto
   1.107  
   1.108  lemmas le_maxI1 = min_max.sup_ge1
   1.109  lemmas le_maxI2 = min_max.sup_ge2
   1.110 -
   1.111 -lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   1.112 -  apply (simp add: max_def order_le_less)
   1.113 -  apply (insert linorder_less_linear)
   1.114 -  apply (blast intro: order_less_trans)
   1.115 -  done
   1.116 -
   1.117 -lemma max_less_iff_conj [simp]:
   1.118 -    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   1.119 -  apply (simp add: order_le_less max_def)
   1.120 -  apply (insert linorder_less_linear)
   1.121 -  apply (blast intro: order_less_trans)
   1.122 -  done
   1.123 -
   1.124 -lemma min_less_iff_conj [simp]:
   1.125 -    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   1.126 -  apply (simp add: order_le_less min_def)
   1.127 -  apply (insert linorder_less_linear)
   1.128 -  apply (blast intro: order_less_trans)
   1.129 -  done
   1.130 -
   1.131 -lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   1.132 -  apply (simp add: min_def)
   1.133 -  apply (insert linorder_linear)
   1.134 -  apply (blast intro: order_trans)
   1.135 -  done
   1.136 -
   1.137 -lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   1.138 -  apply (simp add: min_def order_le_less)
   1.139 -  apply (insert linorder_less_linear)
   1.140 -  apply (blast intro: order_less_trans)
   1.141 -  done
   1.142 -
   1.143 + 
   1.144  lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.145                 mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   1.146  
   1.147  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.148                 mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   1.149  
   1.150 -lemma split_min:
   1.151 -    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   1.152 -  by (simp add: min_def)
   1.153 -
   1.154 -lemma split_max:
   1.155 -    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   1.156 -  by (simp add: max_def)
   1.157 -
   1.158  text {* ML legacy bindings *}
   1.159  
   1.160  ML {*