renamed Lattice_Locales to Lattices
authorhaftmann
Wed Nov 08 19:48:34 2006 +0100 (2006-11-08)
changeset 21249d594c58e24ed
parent 21248 3fd22b0939ff
child 21250 a268f6288fb6
renamed Lattice_Locales to Lattices
src/HOL/Finite_Set.thy
src/HOL/IsaMakefile
src/HOL/LOrder.thy
src/HOL/Lattice_Locales.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Nov 08 19:46:10 2006 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Nov 08 19:48:34 2006 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Power Inductive Lattice_Locales
     1.8 +imports Power Inductive Lattices
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}
     2.1 --- a/src/HOL/IsaMakefile	Wed Nov 08 19:46:10 2006 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Nov 08 19:48:34 2006 +0100
     2.3 @@ -94,7 +94,7 @@
     2.4    Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
     2.5    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
     2.6    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
     2.7 -  Lattice_Locales.thy List.ML List.thy Main.thy Map.thy			\
     2.8 +  Lattices.thy List.ML List.thy Main.thy Map.thy			\
     2.9    Nat.ML Nat.thy OrderedGroup.ML OrderedGroup.thy	\
    2.10    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    2.11    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
     3.1 --- a/src/HOL/LOrder.thy	Wed Nov 08 19:46:10 2006 +0100
     3.2 +++ b/src/HOL/LOrder.thy	Wed Nov 08 19:48:34 2006 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Lattice Orders *}
     3.5  
     3.6  theory LOrder
     3.7 -imports Lattice_Locales
     3.8 +imports Lattices
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Lattice_Locales.thy	Wed Nov 08 19:46:10 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,336 +0,0 @@
     4.4 -(*  Title:      HOL/Lattices.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow
     4.7 -*)
     4.8 -
     4.9 -header {* Lattices via Locales *}
    4.10 -
    4.11 -theory Lattice_Locales
    4.12 -imports Orderings
    4.13 -begin
    4.14 -
    4.15 -subsection{* Lattices *}
    4.16 -
    4.17 -text{* This theory of lattice locales only defines binary sup and inf
    4.18 -operations. The extension to finite sets is done in theory @{text
    4.19 -Finite_Set}. In the longer term it may be better to define arbitrary
    4.20 -sups and infs via @{text THE}. *}
    4.21 -
    4.22 -locale lower_semilattice = partial_order +
    4.23 -  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    4.24 -  assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
    4.25 -  and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    4.26 -
    4.27 -locale upper_semilattice = partial_order +
    4.28 -  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    4.29 -  assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
    4.30 -  and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    4.31 -
    4.32 -locale lattice = lower_semilattice + upper_semilattice
    4.33 -
    4.34 -lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    4.35 -by(blast intro: antisym inf_le1 inf_le2 inf_least)
    4.36 -
    4.37 -lemma (in upper_semilattice) sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    4.38 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
    4.39 -
    4.40 -lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    4.41 -by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl)
    4.42 -
    4.43 -lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    4.44 -by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl)
    4.45 -
    4.46 -lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x"
    4.47 -by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
    4.48 -
    4.49 -lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
    4.50 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
    4.51 -
    4.52 -lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.53 -by (simp add: inf_assoc[symmetric])
    4.54 -
    4.55 -lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.56 -by (simp add: sup_assoc[symmetric])
    4.57 -
    4.58 -lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    4.59 -by(blast intro: antisym inf_le1 inf_least sup_ge1)
    4.60 -
    4.61 -lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    4.62 -by(blast intro: antisym sup_ge1 sup_greatest inf_le1)
    4.63 -
    4.64 -lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    4.65 -by(blast intro: antisym inf_le1 inf_least refl)
    4.66 -
    4.67 -lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    4.68 -by(blast intro: antisym sup_ge2 sup_greatest refl)
    4.69 -
    4.70 -
    4.71 -lemma (in lower_semilattice) less_eq_inf_conv [simp]:
    4.72 - "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    4.73 -by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
    4.74 -
    4.75 -lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv
    4.76 -  -- {* a duplicate for backward compatibility *}
    4.77 -
    4.78 -lemma (in upper_semilattice) above_sup_conv[simp]:
    4.79 - "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    4.80 -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
    4.81 -
    4.82 -
    4.83 -text{* Towards distributivity: if you have one of them, you have them all. *}
    4.84 -
    4.85 -lemma (in lattice) distrib_imp1:
    4.86 -assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    4.87 -shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    4.88 -proof-
    4.89 -  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    4.90 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    4.91 -  also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    4.92 -    by(simp add:inf_sup_absorb inf_commute)
    4.93 -  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    4.94 -  finally show ?thesis .
    4.95 -qed
    4.96 -
    4.97 -lemma (in lattice) distrib_imp2:
    4.98 -assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    4.99 -shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   4.100 -proof-
   4.101 -  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
   4.102 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
   4.103 -  also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   4.104 -    by(simp add:sup_inf_absorb sup_commute)
   4.105 -  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   4.106 -  finally show ?thesis .
   4.107 -qed
   4.108 -
   4.109 -text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
   4.110 -
   4.111 -lemma (in lower_semilattice) inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   4.112 -proof -
   4.113 -  have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
   4.114 -  also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
   4.115 -  also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
   4.116 -  finally(back_subst) show ?thesis .
   4.117 -qed
   4.118 -
   4.119 -lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   4.120 -proof -
   4.121 -  have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
   4.122 -  also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
   4.123 -  also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
   4.124 -  finally(back_subst) show ?thesis .
   4.125 -qed
   4.126 -
   4.127 -lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   4.128 -proof -
   4.129 -  have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc)
   4.130 -  also have "\<dots> = x \<sqinter> y" by(simp)
   4.131 -  finally show ?thesis .
   4.132 -qed
   4.133 -
   4.134 -lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   4.135 -proof -
   4.136 -  have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc)
   4.137 -  also have "\<dots> = x \<squnion> y" by(simp)
   4.138 -  finally show ?thesis .
   4.139 -qed
   4.140 -
   4.141 -
   4.142 -lemmas (in lower_semilattice) inf_ACI =
   4.143 - inf_commute inf_assoc inf_left_commute inf_left_idem
   4.144 -
   4.145 -lemmas (in upper_semilattice) sup_ACI =
   4.146 - sup_commute sup_assoc sup_left_commute sup_left_idem
   4.147 -
   4.148 -lemmas (in lattice) ACI = inf_ACI sup_ACI
   4.149 -
   4.150 -
   4.151 -subsection{* Distributive lattices *}
   4.152 -
   4.153 -locale distrib_lattice = lattice +
   4.154 -  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   4.155 -
   4.156 -lemma (in distrib_lattice) sup_inf_distrib2:
   4.157 - "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   4.158 -by(simp add:ACI sup_inf_distrib1)
   4.159 -
   4.160 -lemma (in distrib_lattice) inf_sup_distrib1:
   4.161 - "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   4.162 -by(rule distrib_imp2[OF sup_inf_distrib1])
   4.163 -
   4.164 -lemma (in distrib_lattice) inf_sup_distrib2:
   4.165 - "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   4.166 -by(simp add:ACI inf_sup_distrib1)
   4.167 -
   4.168 -lemmas (in distrib_lattice) distrib =
   4.169 -  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   4.170 -
   4.171 -
   4.172 -subsection {* Least value operator and min/max -- properties *}
   4.173 - 
   4.174 -(*FIXME: derive more of the min/max laws generically via semilattices*)
   4.175 -
   4.176 -lemma LeastI2_order:
   4.177 -  "[| P (x::'a::order);
   4.178 -      !!y. P y ==> x <= y;
   4.179 -      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   4.180 -   ==> Q (Least P)"
   4.181 -  apply (unfold Least_def)
   4.182 -  apply (rule theI2)
   4.183 -    apply (blast intro: order_antisym)+
   4.184 -  done
   4.185 -
   4.186 -lemma Least_equality:
   4.187 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   4.188 -  apply (simp add: Least_def)
   4.189 -  apply (rule the_equality)
   4.190 -  apply (auto intro!: order_antisym)
   4.191 -  done
   4.192 -
   4.193 -lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   4.194 -  by (simp add: min_def)
   4.195 -
   4.196 -lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
   4.197 -  by (simp add: max_def)
   4.198 -
   4.199 -lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
   4.200 -  apply (simp add: min_def)
   4.201 -  apply (blast intro: order_antisym)
   4.202 -  done
   4.203 -
   4.204 -lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
   4.205 -  apply (simp add: max_def)
   4.206 -  apply (blast intro: order_antisym)
   4.207 -  done
   4.208 -
   4.209 -lemma min_of_mono:
   4.210 -    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
   4.211 -  by (simp add: min_def)
   4.212 -
   4.213 -lemma max_of_mono:
   4.214 -    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   4.215 -  by (simp add: max_def)
   4.216 -
   4.217 -text{* Instantiate locales: *}
   4.218 -
   4.219 -interpretation min_max:
   4.220 -  lower_semilattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   4.221 -apply unfold_locales
   4.222 -apply(simp add:min_def linorder_not_le order_less_imp_le)
   4.223 -apply(simp add:min_def linorder_not_le order_less_imp_le)
   4.224 -apply(simp add:min_def linorder_not_le order_less_imp_le)
   4.225 -done
   4.226 -
   4.227 -interpretation min_max:
   4.228 -  upper_semilattice["op \<le>" "op <" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   4.229 -apply unfold_locales
   4.230 -apply(simp add: max_def linorder_not_le order_less_imp_le)
   4.231 -apply(simp add: max_def linorder_not_le order_less_imp_le)
   4.232 -apply(simp add: max_def linorder_not_le order_less_imp_le)
   4.233 -done
   4.234 -
   4.235 -interpretation min_max:
   4.236 -  lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   4.237 -  by unfold_locales
   4.238 -
   4.239 -interpretation min_max:
   4.240 -  distrib_lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   4.241 -apply unfold_locales
   4.242 -apply(rule_tac x=x and y=y in linorder_le_cases)
   4.243 -apply(rule_tac x=x and y=z in linorder_le_cases)
   4.244 -apply(rule_tac x=y and y=z in linorder_le_cases)
   4.245 -apply(simp add:min_def max_def)
   4.246 -apply(simp add:min_def max_def)
   4.247 -apply(rule_tac x=y and y=z in linorder_le_cases)
   4.248 -apply(simp add:min_def max_def)
   4.249 -apply(simp add:min_def max_def)
   4.250 -apply(rule_tac x=x and y=z in linorder_le_cases)
   4.251 -apply(rule_tac x=y and y=z in linorder_le_cases)
   4.252 -apply(simp add:min_def max_def)
   4.253 -apply(simp add:min_def max_def)
   4.254 -apply(rule_tac x=y and y=z in linorder_le_cases)
   4.255 -apply(simp add:min_def max_def)
   4.256 -apply(simp add:min_def max_def)
   4.257 -done
   4.258 -
   4.259 -lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   4.260 -  apply(simp add:max_def)
   4.261 -  apply (insert linorder_linear)
   4.262 -  apply (blast intro: order_trans)
   4.263 -  done
   4.264 -
   4.265 -lemmas le_maxI1 = min_max.sup_ge1
   4.266 -lemmas le_maxI2 = min_max.sup_ge2
   4.267 -
   4.268 -lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   4.269 -  apply (simp add: max_def order_le_less)
   4.270 -  apply (insert linorder_less_linear)
   4.271 -  apply (blast intro: order_less_trans)
   4.272 -  done
   4.273 -
   4.274 -lemma max_less_iff_conj [simp]:
   4.275 -    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   4.276 -  apply (simp add: order_le_less max_def)
   4.277 -  apply (insert linorder_less_linear)
   4.278 -  apply (blast intro: order_less_trans)
   4.279 -  done
   4.280 -
   4.281 -lemma min_less_iff_conj [simp]:
   4.282 -    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   4.283 -  apply (simp add: order_le_less min_def)
   4.284 -  apply (insert linorder_less_linear)
   4.285 -  apply (blast intro: order_less_trans)
   4.286 -  done
   4.287 -
   4.288 -lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   4.289 -  apply (simp add: min_def)
   4.290 -  apply (insert linorder_linear)
   4.291 -  apply (blast intro: order_trans)
   4.292 -  done
   4.293 -
   4.294 -lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   4.295 -  apply (simp add: min_def order_le_less)
   4.296 -  apply (insert linorder_less_linear)
   4.297 -  apply (blast intro: order_less_trans)
   4.298 -  done
   4.299 -
   4.300 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   4.301 -               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   4.302 -
   4.303 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   4.304 -               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   4.305 -
   4.306 -lemma split_min:
   4.307 -    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   4.308 -  by (simp add: min_def)
   4.309 -
   4.310 -lemma split_max:
   4.311 -    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   4.312 -  by (simp add: max_def)
   4.313 -
   4.314 -text {* ML legacy bindings *}
   4.315 -
   4.316 -ML {*
   4.317 -val Least_def = thm "Least_def";
   4.318 -val Least_equality = thm "Least_equality";
   4.319 -val min_def = thm "min_def";
   4.320 -val min_of_mono = thm "min_of_mono";
   4.321 -val max_def = thm "max_def";
   4.322 -val max_of_mono = thm "max_of_mono";
   4.323 -val min_leastL = thm "min_leastL";
   4.324 -val max_leastL = thm "max_leastL";
   4.325 -val min_leastR = thm "min_leastR";
   4.326 -val max_leastR = thm "max_leastR";
   4.327 -val le_max_iff_disj = thm "le_max_iff_disj";
   4.328 -val le_maxI1 = thm "le_maxI1";
   4.329 -val le_maxI2 = thm "le_maxI2";
   4.330 -val less_max_iff_disj = thm "less_max_iff_disj";
   4.331 -val max_less_iff_conj = thm "max_less_iff_conj";
   4.332 -val min_less_iff_conj = thm "min_less_iff_conj";
   4.333 -val min_le_iff_disj = thm "min_le_iff_disj";
   4.334 -val min_less_iff_disj = thm "min_less_iff_disj";
   4.335 -val split_min = thm "split_min";
   4.336 -val split_max = thm "split_max";
   4.337 -*}
   4.338 -
   4.339 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lattices.thy	Wed Nov 08 19:48:34 2006 +0100
     5.3 @@ -0,0 +1,336 @@
     5.4 +(*  Title:      HOL/Lattices.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow
     5.7 +*)
     5.8 +
     5.9 +header {* Lattices via Locales *}
    5.10 +
    5.11 +theory Lattices
    5.12 +imports Orderings
    5.13 +begin
    5.14 +
    5.15 +subsection{* Lattices *}
    5.16 +
    5.17 +text{* This theory of lattice locales only defines binary sup and inf
    5.18 +operations. The extension to finite sets is done in theory @{text
    5.19 +Finite_Set}. In the longer term it may be better to define arbitrary
    5.20 +sups and infs via @{text THE}. *}
    5.21 +
    5.22 +locale lower_semilattice = partial_order +
    5.23 +  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    5.24 +  assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
    5.25 +  and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    5.26 +
    5.27 +locale upper_semilattice = partial_order +
    5.28 +  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    5.29 +  assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
    5.30 +  and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    5.31 +
    5.32 +locale lattice = lower_semilattice + upper_semilattice
    5.33 +
    5.34 +lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
    5.35 +by(blast intro: antisym inf_le1 inf_le2 inf_least)
    5.36 +
    5.37 +lemma (in upper_semilattice) sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
    5.38 +by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
    5.39 +
    5.40 +lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    5.41 +by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl)
    5.42 +
    5.43 +lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    5.44 +by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl)
    5.45 +
    5.46 +lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x"
    5.47 +by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
    5.48 +
    5.49 +lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
    5.50 +by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
    5.51 +
    5.52 +lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    5.53 +by (simp add: inf_assoc[symmetric])
    5.54 +
    5.55 +lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    5.56 +by (simp add: sup_assoc[symmetric])
    5.57 +
    5.58 +lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    5.59 +by(blast intro: antisym inf_le1 inf_least sup_ge1)
    5.60 +
    5.61 +lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    5.62 +by(blast intro: antisym sup_ge1 sup_greatest inf_le1)
    5.63 +
    5.64 +lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    5.65 +by(blast intro: antisym inf_le1 inf_least refl)
    5.66 +
    5.67 +lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    5.68 +by(blast intro: antisym sup_ge2 sup_greatest refl)
    5.69 +
    5.70 +
    5.71 +lemma (in lower_semilattice) less_eq_inf_conv [simp]:
    5.72 + "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    5.73 +by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
    5.74 +
    5.75 +lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv
    5.76 +  -- {* a duplicate for backward compatibility *}
    5.77 +
    5.78 +lemma (in upper_semilattice) above_sup_conv[simp]:
    5.79 + "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    5.80 +by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
    5.81 +
    5.82 +
    5.83 +text{* Towards distributivity: if you have one of them, you have them all. *}
    5.84 +
    5.85 +lemma (in lattice) distrib_imp1:
    5.86 +assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    5.87 +shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    5.88 +proof-
    5.89 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    5.90 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    5.91 +  also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    5.92 +    by(simp add:inf_sup_absorb inf_commute)
    5.93 +  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    5.94 +  finally show ?thesis .
    5.95 +qed
    5.96 +
    5.97 +lemma (in lattice) distrib_imp2:
    5.98 +assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    5.99 +shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   5.100 +proof-
   5.101 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
   5.102 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
   5.103 +  also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   5.104 +    by(simp add:sup_inf_absorb sup_commute)
   5.105 +  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   5.106 +  finally show ?thesis .
   5.107 +qed
   5.108 +
   5.109 +text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
   5.110 +
   5.111 +lemma (in lower_semilattice) inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   5.112 +proof -
   5.113 +  have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
   5.114 +  also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
   5.115 +  also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
   5.116 +  finally(back_subst) show ?thesis .
   5.117 +qed
   5.118 +
   5.119 +lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   5.120 +proof -
   5.121 +  have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
   5.122 +  also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
   5.123 +  also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
   5.124 +  finally(back_subst) show ?thesis .
   5.125 +qed
   5.126 +
   5.127 +lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   5.128 +proof -
   5.129 +  have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc)
   5.130 +  also have "\<dots> = x \<sqinter> y" by(simp)
   5.131 +  finally show ?thesis .
   5.132 +qed
   5.133 +
   5.134 +lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   5.135 +proof -
   5.136 +  have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc)
   5.137 +  also have "\<dots> = x \<squnion> y" by(simp)
   5.138 +  finally show ?thesis .
   5.139 +qed
   5.140 +
   5.141 +
   5.142 +lemmas (in lower_semilattice) inf_ACI =
   5.143 + inf_commute inf_assoc inf_left_commute inf_left_idem
   5.144 +
   5.145 +lemmas (in upper_semilattice) sup_ACI =
   5.146 + sup_commute sup_assoc sup_left_commute sup_left_idem
   5.147 +
   5.148 +lemmas (in lattice) ACI = inf_ACI sup_ACI
   5.149 +
   5.150 +
   5.151 +subsection{* Distributive lattices *}
   5.152 +
   5.153 +locale distrib_lattice = lattice +
   5.154 +  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   5.155 +
   5.156 +lemma (in distrib_lattice) sup_inf_distrib2:
   5.157 + "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   5.158 +by(simp add:ACI sup_inf_distrib1)
   5.159 +
   5.160 +lemma (in distrib_lattice) inf_sup_distrib1:
   5.161 + "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   5.162 +by(rule distrib_imp2[OF sup_inf_distrib1])
   5.163 +
   5.164 +lemma (in distrib_lattice) inf_sup_distrib2:
   5.165 + "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   5.166 +by(simp add:ACI inf_sup_distrib1)
   5.167 +
   5.168 +lemmas (in distrib_lattice) distrib =
   5.169 +  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   5.170 +
   5.171 +
   5.172 +subsection {* Least value operator and min/max -- properties *}
   5.173 + 
   5.174 +(*FIXME: derive more of the min/max laws generically via semilattices*)
   5.175 +
   5.176 +lemma LeastI2_order:
   5.177 +  "[| P (x::'a::order);
   5.178 +      !!y. P y ==> x <= y;
   5.179 +      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   5.180 +   ==> Q (Least P)"
   5.181 +  apply (unfold Least_def)
   5.182 +  apply (rule theI2)
   5.183 +    apply (blast intro: order_antisym)+
   5.184 +  done
   5.185 +
   5.186 +lemma Least_equality:
   5.187 +    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   5.188 +  apply (simp add: Least_def)
   5.189 +  apply (rule the_equality)
   5.190 +  apply (auto intro!: order_antisym)
   5.191 +  done
   5.192 +
   5.193 +lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   5.194 +  by (simp add: min_def)
   5.195 +
   5.196 +lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
   5.197 +  by (simp add: max_def)
   5.198 +
   5.199 +lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
   5.200 +  apply (simp add: min_def)
   5.201 +  apply (blast intro: order_antisym)
   5.202 +  done
   5.203 +
   5.204 +lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
   5.205 +  apply (simp add: max_def)
   5.206 +  apply (blast intro: order_antisym)
   5.207 +  done
   5.208 +
   5.209 +lemma min_of_mono:
   5.210 +    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
   5.211 +  by (simp add: min_def)
   5.212 +
   5.213 +lemma max_of_mono:
   5.214 +    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   5.215 +  by (simp add: max_def)
   5.216 +
   5.217 +text{* Instantiate locales: *}
   5.218 +
   5.219 +interpretation min_max:
   5.220 +  lower_semilattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   5.221 +apply unfold_locales
   5.222 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   5.223 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   5.224 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   5.225 +done
   5.226 +
   5.227 +interpretation min_max:
   5.228 +  upper_semilattice["op \<le>" "op <" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   5.229 +apply unfold_locales
   5.230 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   5.231 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   5.232 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   5.233 +done
   5.234 +
   5.235 +interpretation min_max:
   5.236 +  lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   5.237 +  by unfold_locales
   5.238 +
   5.239 +interpretation min_max:
   5.240 +  distrib_lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   5.241 +apply unfold_locales
   5.242 +apply(rule_tac x=x and y=y in linorder_le_cases)
   5.243 +apply(rule_tac x=x and y=z in linorder_le_cases)
   5.244 +apply(rule_tac x=y and y=z in linorder_le_cases)
   5.245 +apply(simp add:min_def max_def)
   5.246 +apply(simp add:min_def max_def)
   5.247 +apply(rule_tac x=y and y=z in linorder_le_cases)
   5.248 +apply(simp add:min_def max_def)
   5.249 +apply(simp add:min_def max_def)
   5.250 +apply(rule_tac x=x and y=z in linorder_le_cases)
   5.251 +apply(rule_tac x=y and y=z in linorder_le_cases)
   5.252 +apply(simp add:min_def max_def)
   5.253 +apply(simp add:min_def max_def)
   5.254 +apply(rule_tac x=y and y=z in linorder_le_cases)
   5.255 +apply(simp add:min_def max_def)
   5.256 +apply(simp add:min_def max_def)
   5.257 +done
   5.258 +
   5.259 +lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   5.260 +  apply(simp add:max_def)
   5.261 +  apply (insert linorder_linear)
   5.262 +  apply (blast intro: order_trans)
   5.263 +  done
   5.264 +
   5.265 +lemmas le_maxI1 = min_max.sup_ge1
   5.266 +lemmas le_maxI2 = min_max.sup_ge2
   5.267 +
   5.268 +lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   5.269 +  apply (simp add: max_def order_le_less)
   5.270 +  apply (insert linorder_less_linear)
   5.271 +  apply (blast intro: order_less_trans)
   5.272 +  done
   5.273 +
   5.274 +lemma max_less_iff_conj [simp]:
   5.275 +    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   5.276 +  apply (simp add: order_le_less max_def)
   5.277 +  apply (insert linorder_less_linear)
   5.278 +  apply (blast intro: order_less_trans)
   5.279 +  done
   5.280 +
   5.281 +lemma min_less_iff_conj [simp]:
   5.282 +    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   5.283 +  apply (simp add: order_le_less min_def)
   5.284 +  apply (insert linorder_less_linear)
   5.285 +  apply (blast intro: order_less_trans)
   5.286 +  done
   5.287 +
   5.288 +lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   5.289 +  apply (simp add: min_def)
   5.290 +  apply (insert linorder_linear)
   5.291 +  apply (blast intro: order_trans)
   5.292 +  done
   5.293 +
   5.294 +lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   5.295 +  apply (simp add: min_def order_le_less)
   5.296 +  apply (insert linorder_less_linear)
   5.297 +  apply (blast intro: order_less_trans)
   5.298 +  done
   5.299 +
   5.300 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   5.301 +               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   5.302 +
   5.303 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   5.304 +               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   5.305 +
   5.306 +lemma split_min:
   5.307 +    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   5.308 +  by (simp add: min_def)
   5.309 +
   5.310 +lemma split_max:
   5.311 +    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   5.312 +  by (simp add: max_def)
   5.313 +
   5.314 +text {* ML legacy bindings *}
   5.315 +
   5.316 +ML {*
   5.317 +val Least_def = thm "Least_def";
   5.318 +val Least_equality = thm "Least_equality";
   5.319 +val min_def = thm "min_def";
   5.320 +val min_of_mono = thm "min_of_mono";
   5.321 +val max_def = thm "max_def";
   5.322 +val max_of_mono = thm "max_of_mono";
   5.323 +val min_leastL = thm "min_leastL";
   5.324 +val max_leastL = thm "max_leastL";
   5.325 +val min_leastR = thm "min_leastR";
   5.326 +val max_leastR = thm "max_leastR";
   5.327 +val le_max_iff_disj = thm "le_max_iff_disj";
   5.328 +val le_maxI1 = thm "le_maxI1";
   5.329 +val le_maxI2 = thm "le_maxI2";
   5.330 +val less_max_iff_disj = thm "less_max_iff_disj";
   5.331 +val max_less_iff_conj = thm "max_less_iff_conj";
   5.332 +val min_less_iff_conj = thm "min_less_iff_conj";
   5.333 +val min_le_iff_disj = thm "min_le_iff_disj";
   5.334 +val min_less_iff_disj = thm "min_less_iff_disj";
   5.335 +val split_min = thm "split_min";
   5.336 +val split_max = thm "split_max";
   5.337 +*}
   5.338 +
   5.339 +end