* HOL/Lattice: fundamental concepts of lattice theory and order structures;
authorwenzelm
Fri Oct 06 01:04:56 2000 +0200 (2000-10-06)
changeset 101576d3987f3aad9
parent 10156 9d4d5852eb47
child 10158 00fdd5c330ea
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
NEWS
src/HOL/IsaMakefile
src/HOL/Lattice/Bounds.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Lattice/ROOT.ML
src/HOL/Lattice/document/root.bib
src/HOL/Lattice/document/root.tex
     1.1 --- a/NEWS	Thu Oct 05 14:04:56 2000 +0200
     1.2 +++ b/NEWS	Fri Oct 06 01:04:56 2000 +0200
     1.3 @@ -243,10 +243,17 @@
     1.4  * HOL/Algebra: new theory of rings and univariate polynomials, by
     1.5  Clemens Ballarin;
     1.6  
     1.7 -* HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese
     1.8 +* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese
     1.9  Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
    1.10  Rasmussen;
    1.11  
    1.12 +* HOL/Lattice: fundamental concepts of lattice theory and order
    1.13 +structures, including duals, properties of bounds versus algebraic
    1.14 +laws, lattice operations versus set-theoretic ones, the Knaster-Tarski
    1.15 +Theorem for complete lattices etc.; may also serve as a demonstration
    1.16 +for abstract algebraic reasoning using axiomatic type classes, and
    1.17 +mathematics-style proof in Isabelle/Isar; by Markus Wenzel;
    1.18 +
    1.19  * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
    1.20  von Oheimb;
    1.21  
     2.1 --- a/src/HOL/IsaMakefile	Thu Oct 05 14:04:56 2000 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 06 01:04:56 2000 +0200
     2.3 @@ -9,13 +9,38 @@
     2.4  default: HOL
     2.5  images: HOL HOL-Real TLA
     2.6  
     2.7 -test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-AxClasses HOL-ex HOL-Subst HOL-IMP \
     2.8 -  HOL-IMPP HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth \
     2.9 -  HOL-UNITY HOL-Modelcheck HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV \
    2.10 -  HOL-MicroJava HOL-IOA HOL-Real-ex HOL-Real-HahnBanach \
    2.11 -  TLA-Inc TLA-Buffer TLA-Memory
    2.12 -
    2.13 -all: images test
    2.14 +#Note: keep targets sorted!
    2.15 +test: \
    2.16 +  HOL-Algebra \
    2.17 +  HOL-Auth \
    2.18 +  HOL-AxClasses \
    2.19 +  HOL-BCV \
    2.20 +      HOL-Real-HahnBanach \
    2.21 +      HOL-Real-ex \
    2.22 +  HOL-Hoare \
    2.23 +  HOL-IMP \
    2.24 +  HOL-IMPP \
    2.25 +  HOL-IOA \
    2.26 +  HOL-Induct \
    2.27 +  HOL-Isar_examples \
    2.28 +  HOL-Lambda \
    2.29 +  HOL-Lattice \
    2.30 +  HOL-Lex \
    2.31 +  HOL-MicroJava \
    2.32 +  HOL-MiniML \
    2.33 +  HOL-Modelcheck \
    2.34 +  HOL-NumberTheory \
    2.35 +  HOL-Prolog \
    2.36 +  HOL-Subst \
    2.37 +      TLA-Buffer \
    2.38 +      TLA-Inc \
    2.39 +      TLA-Memory \
    2.40 +  HOL-UNITY \
    2.41 +  HOL-W0 \
    2.42 +  HOL-ex
    2.43 +    # ^ this is the sort position
    2.44 +  
    2.45 +all: test images
    2.46  
    2.47  
    2.48  ## global settings
    2.49 @@ -406,6 +431,16 @@
    2.50  	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
    2.51  
    2.52  
    2.53 +## HOL-Lattice
    2.54 +
    2.55 +HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
    2.56 +
    2.57 +$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
    2.58 +  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
    2.59 +  Lattice/ROOT.ML Lattice/document/root.tex
    2.60 +	@$(ISATOOL) usedir $(OUT)/HOL Lattice
    2.61 +
    2.62 +
    2.63  ## HOL-ex
    2.64  
    2.65  HOL-ex: HOL $(LOG)/HOL-ex.gz
    2.66 @@ -502,6 +537,6 @@
    2.67  		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    2.68  		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
    2.69  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    2.70 -		$(LOG)/HOL-Real-ex.gz \
    2.71 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
    2.72  		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
    2.73  		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Lattice/Bounds.thy	Fri Oct 06 01:04:56 2000 +0200
     3.3 @@ -0,0 +1,325 @@
     3.4 +(*  Title:      HOL/Lattice/Bounds.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +*)
     3.8 +
     3.9 +header {* Bounds *}
    3.10 +
    3.11 +theory Bounds = Orders:
    3.12 +
    3.13 +subsection {* Infimum and supremum *}
    3.14 +
    3.15 +text {*
    3.16 +  Given a partial order, we define infimum (greatest lower bound) and
    3.17 +  supremum (least upper bound) wrt.\ @{text \<sqsubseteq>} for two and for any
    3.18 +  number of elements.
    3.19 +*}
    3.20 +
    3.21 +constdefs
    3.22 +  is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.23 +  "is_inf x y inf \<equiv> inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf)"
    3.24 +
    3.25 +  is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.26 +  "is_sup x y sup \<equiv> x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z)"
    3.27 +
    3.28 +  is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
    3.29 +  "is_Inf A inf \<equiv> (\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf)"
    3.30 +
    3.31 +  is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
    3.32 +  "is_Sup A sup \<equiv> (\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z)"
    3.33 +
    3.34 +text {*
    3.35 +  These definitions entail the following basic properties of boundary
    3.36 +  elements.
    3.37 +*}
    3.38 +
    3.39 +lemma is_infI [intro?]: "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow>
    3.40 +    (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_inf x y inf"
    3.41 +  by (unfold is_inf_def) blast
    3.42 +
    3.43 +lemma is_inf_greatest [elim?]:
    3.44 +    "is_inf x y inf \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf"
    3.45 +  by (unfold is_inf_def) blast
    3.46 +
    3.47 +lemma is_inf_lower [elim?]:
    3.48 +    "is_inf x y inf \<Longrightarrow> (inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
    3.49 +  by (unfold is_inf_def) blast
    3.50 +
    3.51 +
    3.52 +lemma is_supI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
    3.53 +    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_sup x y sup"
    3.54 +  by (unfold is_sup_def) blast
    3.55 +
    3.56 +lemma is_sup_least [elim?]:
    3.57 +    "is_sup x y sup \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z"
    3.58 +  by (unfold is_sup_def) blast
    3.59 +
    3.60 +lemma is_sup_upper [elim?]:
    3.61 +    "is_sup x y sup \<Longrightarrow> (x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow> C) \<Longrightarrow> C"
    3.62 +  by (unfold is_sup_def) blast
    3.63 +
    3.64 +
    3.65 +lemma is_InfI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> inf \<sqsubseteq> x) \<Longrightarrow>
    3.66 +    (\<And>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_Inf A inf"
    3.67 +  by (unfold is_Inf_def) blast
    3.68 +
    3.69 +lemma is_Inf_greatest [elim?]:
    3.70 +    "is_Inf A inf \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf"
    3.71 +  by (unfold is_Inf_def) blast
    3.72 +
    3.73 +lemma is_Inf_lower [dest?]:
    3.74 +    "is_Inf A inf \<Longrightarrow> x \<in> A \<Longrightarrow> inf \<sqsubseteq> x"
    3.75 +  by (unfold is_Inf_def) blast
    3.76 +
    3.77 +
    3.78 +lemma is_SupI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> sup) \<Longrightarrow>
    3.79 +    (\<And>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_Sup A sup"
    3.80 +  by (unfold is_Sup_def) blast
    3.81 +
    3.82 +lemma is_Sup_least [elim?]:
    3.83 +    "is_Sup A sup \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z"
    3.84 +  by (unfold is_Sup_def) blast
    3.85 +
    3.86 +lemma is_Sup_upper [dest?]:
    3.87 +    "is_Sup A sup \<Longrightarrow> x \<in> A \<Longrightarrow> x \<sqsubseteq> sup"
    3.88 +  by (unfold is_Sup_def) blast
    3.89 +
    3.90 +
    3.91 +subsection {* Duality *}
    3.92 +
    3.93 +text {*
    3.94 +  Infimum and supremum are dual to each other.
    3.95 +*}
    3.96 +
    3.97 +theorem dual_inf [iff?]:
    3.98 +    "is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"
    3.99 +  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
   3.100 +
   3.101 +theorem dual_sup [iff?]:
   3.102 +    "is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"
   3.103 +  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
   3.104 +
   3.105 +theorem dual_Inf [iff?]:
   3.106 +    "is_Inf (dual `` A) (dual sup) = is_Sup A sup"
   3.107 +  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
   3.108 +
   3.109 +theorem dual_Sup [iff?]:
   3.110 +    "is_Sup (dual `` A) (dual inf) = is_Inf A inf"
   3.111 +  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
   3.112 +
   3.113 +
   3.114 +subsection {* Uniqueness *}
   3.115 +
   3.116 +text {*
   3.117 +  Infima and suprema on partial orders are unique; this is mainly due
   3.118 +  to anti-symmetry of the underlying relation.
   3.119 +*}
   3.120 +
   3.121 +theorem is_inf_uniq: "is_inf x y inf \<Longrightarrow> is_inf x y inf' \<Longrightarrow> inf = inf'"
   3.122 +proof -
   3.123 +  assume inf: "is_inf x y inf"
   3.124 +  assume inf': "is_inf x y inf'"
   3.125 +  show ?thesis
   3.126 +  proof (rule leq_antisym)
   3.127 +    from inf' show "inf \<sqsubseteq> inf'"
   3.128 +    proof (rule is_inf_greatest)
   3.129 +      from inf show "inf \<sqsubseteq> x" ..
   3.130 +      from inf show "inf \<sqsubseteq> y" ..
   3.131 +    qed
   3.132 +    from inf show "inf' \<sqsubseteq> inf"
   3.133 +    proof (rule is_inf_greatest)
   3.134 +      from inf' show "inf' \<sqsubseteq> x" ..
   3.135 +      from inf' show "inf' \<sqsubseteq> y" ..
   3.136 +    qed
   3.137 +  qed
   3.138 +qed
   3.139 +
   3.140 +theorem is_sup_uniq: "is_sup x y sup \<Longrightarrow> is_sup x y sup' \<Longrightarrow> sup = sup'"
   3.141 +proof -
   3.142 +  assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"
   3.143 +  have "dual sup = dual sup'"
   3.144 +  proof (rule is_inf_uniq)
   3.145 +    from sup show "is_inf (dual x) (dual y) (dual sup)" ..
   3.146 +    from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
   3.147 +  qed
   3.148 +  thus "sup = sup'" ..
   3.149 +qed
   3.150 +
   3.151 +theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
   3.152 +proof -
   3.153 +  assume inf: "is_Inf A inf"
   3.154 +  assume inf': "is_Inf A inf'"
   3.155 +  show ?thesis
   3.156 +  proof (rule leq_antisym)
   3.157 +    from inf' show "inf \<sqsubseteq> inf'"
   3.158 +    proof (rule is_Inf_greatest)
   3.159 +      fix x assume "x \<in> A"
   3.160 +      from inf show "inf \<sqsubseteq> x" ..
   3.161 +    qed
   3.162 +    from inf show "inf' \<sqsubseteq> inf"
   3.163 +    proof (rule is_Inf_greatest)
   3.164 +      fix x assume "x \<in> A"
   3.165 +      from inf' show "inf' \<sqsubseteq> x" ..
   3.166 +    qed
   3.167 +  qed
   3.168 +qed
   3.169 +
   3.170 +theorem is_Sup_uniq: "is_Sup A sup \<Longrightarrow> is_Sup A sup' \<Longrightarrow> sup = sup'"
   3.171 +proof -
   3.172 +  assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
   3.173 +  have "dual sup = dual sup'"
   3.174 +  proof (rule is_Inf_uniq)
   3.175 +    from sup show "is_Inf (dual `` A) (dual sup)" ..
   3.176 +    from sup' show "is_Inf (dual `` A) (dual sup')" ..
   3.177 +  qed
   3.178 +  thus "sup = sup'" ..
   3.179 +qed
   3.180 +
   3.181 +
   3.182 +subsection {* Related elements *}
   3.183 +
   3.184 +text {*
   3.185 +  The binary bound of related elements is either one of the argument.
   3.186 +*}
   3.187 +
   3.188 +theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
   3.189 +proof -
   3.190 +  assume "x \<sqsubseteq> y"
   3.191 +  show ?thesis
   3.192 +  proof
   3.193 +    show "x \<sqsubseteq> x" ..
   3.194 +    show "x \<sqsubseteq> y" .
   3.195 +    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
   3.196 +  qed
   3.197 +qed
   3.198 +
   3.199 +theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
   3.200 +proof -
   3.201 +  assume "x \<sqsubseteq> y"
   3.202 +  show ?thesis
   3.203 +  proof
   3.204 +    show "x \<sqsubseteq> y" .
   3.205 +    show "y \<sqsubseteq> y" ..
   3.206 +    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   3.207 +    show "y \<sqsubseteq> z" .
   3.208 +  qed
   3.209 +qed
   3.210 +
   3.211 +
   3.212 +subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *}
   3.213 +
   3.214 +text {*
   3.215 +  General bounds of two-element sets coincide with binary bounds.
   3.216 +*}
   3.217 +
   3.218 +theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"
   3.219 +proof -
   3.220 +  let ?A = "{x, y}"
   3.221 +  show ?thesis
   3.222 +  proof
   3.223 +    assume is_Inf: "is_Inf ?A inf"
   3.224 +    show "is_inf x y inf"
   3.225 +    proof
   3.226 +      have "x \<in> ?A" by simp
   3.227 +      with is_Inf show "inf \<sqsubseteq> x" ..
   3.228 +      have "y \<in> ?A" by simp
   3.229 +      with is_Inf show "inf \<sqsubseteq> y" ..
   3.230 +      fix z assume zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y"
   3.231 +      from is_Inf show "z \<sqsubseteq> inf"
   3.232 +      proof (rule is_Inf_greatest)
   3.233 +        fix a assume "a \<in> ?A"
   3.234 +        hence "a = x \<or> a = y" by blast
   3.235 +        thus "z \<sqsubseteq> a"
   3.236 +        proof
   3.237 +          assume "a = x"
   3.238 +          with zx show ?thesis by simp
   3.239 +        next
   3.240 +          assume "a = y"
   3.241 +          with zy show ?thesis by simp
   3.242 +        qed
   3.243 +      qed
   3.244 +    qed
   3.245 +  next
   3.246 +    assume is_inf: "is_inf x y inf"
   3.247 +    show "is_Inf {x, y} inf"
   3.248 +    proof
   3.249 +      fix a assume "a \<in> ?A"
   3.250 +      hence "a = x \<or> a = y" by blast
   3.251 +      thus "inf \<sqsubseteq> a"
   3.252 +      proof
   3.253 +        assume "a = x"
   3.254 +        also from is_inf have "inf \<sqsubseteq> x" ..
   3.255 +        finally show ?thesis .
   3.256 +      next
   3.257 +        assume "a = y"
   3.258 +        also from is_inf have "inf \<sqsubseteq> y" ..
   3.259 +        finally show ?thesis .
   3.260 +      qed
   3.261 +    next
   3.262 +      fix z assume z: "\<forall>a \<in> ?A. z \<sqsubseteq> a"
   3.263 +      from is_inf show "z \<sqsubseteq> inf"
   3.264 +      proof (rule is_inf_greatest)
   3.265 +        from z show "z \<sqsubseteq> x" by blast
   3.266 +        from z show "z \<sqsubseteq> y" by blast
   3.267 +      qed
   3.268 +    qed
   3.269 +  qed
   3.270 +qed
   3.271 +
   3.272 +theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
   3.273 +proof -
   3.274 +  have "is_Sup {x, y} sup = is_Inf (dual `` {x, y}) (dual sup)"
   3.275 +    by (simp only: dual_Inf)
   3.276 +  also have "dual `` {x, y} = {dual x, dual y}"
   3.277 +    by simp
   3.278 +  also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
   3.279 +    by (rule is_Inf_binary)
   3.280 +  also have "\<dots> = is_sup x y sup"
   3.281 +    by (simp only: dual_inf)
   3.282 +  finally show ?thesis .
   3.283 +qed
   3.284 +
   3.285 +
   3.286 +subsection {* Connecting general bounds \label{sec:connect-bounds} *}
   3.287 +
   3.288 +text {*
   3.289 +  Either kind of general bounds is sufficient to express the other.
   3.290 +  The least upper bound (supremum) is the same as the the greatest
   3.291 +  lower bound of the set of all upper bounds; the dual statements
   3.292 +  holds as well; the dual statement holds as well.
   3.293 +*}
   3.294 +
   3.295 +theorem Inf_Sup: "is_Inf {b. \<forall>a \<in> A. a \<sqsubseteq> b} sup \<Longrightarrow> is_Sup A sup"
   3.296 +proof -
   3.297 +  let ?B = "{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
   3.298 +  assume is_Inf: "is_Inf ?B sup"
   3.299 +  show "is_Sup A sup"
   3.300 +  proof
   3.301 +    fix x assume x: "x \<in> A"
   3.302 +    from is_Inf show "x \<sqsubseteq> sup"
   3.303 +    proof (rule is_Inf_greatest)
   3.304 +      fix y assume "y \<in> ?B"
   3.305 +      hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
   3.306 +      from this x show "x \<sqsubseteq> y" ..
   3.307 +    qed
   3.308 +  next
   3.309 +    fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
   3.310 +    hence "z \<in> ?B" ..
   3.311 +    with is_Inf show "sup \<sqsubseteq> z" ..
   3.312 +  qed
   3.313 +qed
   3.314 +
   3.315 +theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
   3.316 +proof -
   3.317 +  assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
   3.318 +  hence "is_Inf (dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
   3.319 +    by (simp only: dual_Inf dual_leq)
   3.320 +  also have "dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual `` A. a' \<sqsubseteq> b'}"
   3.321 +    by (auto iff: dual_ball dual_Collect)  (* FIXME !? *)
   3.322 +  finally have "is_Inf \<dots> (dual inf)" .
   3.323 +  hence "is_Sup (dual `` A) (dual inf)"
   3.324 +    by (rule Inf_Sup)
   3.325 +  thus ?thesis ..
   3.326 +qed
   3.327 +
   3.328 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Fri Oct 06 01:04:56 2000 +0200
     4.3 @@ -0,0 +1,409 @@
     4.4 +(*  Title:      HOL/Lattice/CompleteLattice.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Markus Wenzel, TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +header {* Complete lattices *}
    4.10 +
    4.11 +theory CompleteLattice = Lattice:
    4.12 +
    4.13 +subsection {* Complete lattice operations *}
    4.14 +
    4.15 +text {*
    4.16 +  A \emph{complete lattice} is a partial order with general
    4.17 +  (infinitary) infimum of any set of elements.  General supremum
    4.18 +  exists as well, as a consequence of the connection of infinitary
    4.19 +  bounds (see \S\ref{sec:connect-bounds}).
    4.20 +*}
    4.21 +
    4.22 +axclass complete_lattice < partial_order
    4.23 +  ex_Inf: "\<exists>inf. is_Inf A inf"
    4.24 +
    4.25 +theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
    4.26 +proof -
    4.27 +  from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
    4.28 +  hence "is_Sup A sup" by (rule Inf_Sup)
    4.29 +  thus ?thesis ..
    4.30 +qed
    4.31 +
    4.32 +text {*
    4.33 +  The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
    4.34 +  such infimum and supremum elements.
    4.35 +*}
    4.36 +
    4.37 +consts
    4.38 +  Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
    4.39 +  Join :: "'a::complete_lattice set \<Rightarrow> 'a"
    4.40 +syntax (symbols)
    4.41 +  Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_" [90] 90)
    4.42 +  Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
    4.43 +defs
    4.44 +  Meet_def: "\<Sqinter>A \<equiv> SOME inf. is_Inf A inf"
    4.45 +  Join_def: "\<Squnion>A \<equiv> SOME sup. is_Sup A sup"
    4.46 +
    4.47 +text {*
    4.48 +  Due to unique existence of bounds, the complete lattice operations
    4.49 +  may be exhibited as follows.
    4.50 +*}
    4.51 +
    4.52 +lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
    4.53 +proof (unfold Meet_def)
    4.54 +  assume "is_Inf A inf"
    4.55 +  thus "(SOME inf. is_Inf A inf) = inf"
    4.56 +    by (rule some_equality) (rule is_Inf_uniq)
    4.57 +qed
    4.58 +
    4.59 +lemma MeetI [intro?]:
    4.60 +  "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>
    4.61 +    (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
    4.62 +    \<Sqinter>A = inf"
    4.63 +  by (rule Meet_equality, rule is_InfI) blast+
    4.64 +
    4.65 +lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
    4.66 +proof (unfold Join_def)
    4.67 +  assume "is_Sup A sup"
    4.68 +  thus "(SOME sup. is_Sup A sup) = sup"
    4.69 +    by (rule some_equality) (rule is_Sup_uniq)
    4.70 +qed
    4.71 +
    4.72 +lemma JoinI [intro?]:
    4.73 +  "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>
    4.74 +    (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
    4.75 +    \<Squnion>A = sup"
    4.76 +  by (rule Join_equality, rule is_SupI) blast+
    4.77 +
    4.78 +
    4.79 +text {*
    4.80 +  \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
    4.81 +  bounds on a complete lattice structure.
    4.82 +*}
    4.83 +
    4.84 +lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
    4.85 +proof (unfold Meet_def)
    4.86 +  from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)"
    4.87 +    by (rule ex_someI)
    4.88 +qed
    4.89 +
    4.90 +lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
    4.91 +  by (rule is_Inf_greatest, rule is_Inf_Meet) blast
    4.92 +
    4.93 +lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"
    4.94 +  by (rule is_Inf_lower) (rule is_Inf_Meet)
    4.95 +
    4.96 +
    4.97 +lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
    4.98 +proof (unfold Join_def)
    4.99 +  from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)"
   4.100 +    by (rule ex_someI)
   4.101 +qed
   4.102 +
   4.103 +lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
   4.104 +  by (rule is_Sup_least, rule is_Sup_Join) blast
   4.105 +lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"
   4.106 +  by (rule is_Sup_upper) (rule is_Sup_Join)
   4.107 +
   4.108 +
   4.109 +subsection {* The Knaster-Tarski Theorem *}
   4.110 +
   4.111 +text {*
   4.112 +  The Knaster-Tarski Theorem (in its simplest formulation) states that
   4.113 +  any monotone function on a complete lattice has a least fixed-point
   4.114 +  (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
   4.115 +  is a consequence of the basic boundary properties of the complete
   4.116 +  lattice operations.
   4.117 +*}
   4.118 +
   4.119 +theorem Knaster_Tarski:
   4.120 +  "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
   4.121 +proof
   4.122 +  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   4.123 +  let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
   4.124 +  have ge: "f ?a \<sqsubseteq> ?a"
   4.125 +  proof
   4.126 +    fix x assume x: "x \<in> ?H"
   4.127 +    hence "?a \<sqsubseteq> x" ..
   4.128 +    hence "f ?a \<sqsubseteq> f x" by (rule mono)
   4.129 +    also from x have "... \<sqsubseteq> x" ..
   4.130 +    finally show "f ?a \<sqsubseteq> x" .
   4.131 +  qed
   4.132 +  also have "?a \<sqsubseteq> f ?a"
   4.133 +  proof
   4.134 +    from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
   4.135 +    thus "f ?a : ?H" ..
   4.136 +  qed
   4.137 +  finally show "f ?a = ?a" .
   4.138 +qed
   4.139 +
   4.140 +
   4.141 +subsection {* Bottom and top elements *}
   4.142 +
   4.143 +text {*
   4.144 +  With general bounds available, complete lattices also have least and
   4.145 +  greatest elements.
   4.146 +*}
   4.147 +
   4.148 +constdefs
   4.149 +  bottom :: "'a::complete_lattice"    ("\<bottom>")
   4.150 +  "\<bottom> \<equiv> \<Sqinter>UNIV"
   4.151 +  top :: "'a::complete_lattice"    ("\<top>")
   4.152 +  "\<top> \<equiv> \<Squnion>UNIV"
   4.153 +
   4.154 +lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
   4.155 +proof (unfold bottom_def)
   4.156 +  have "x \<in> UNIV" ..
   4.157 +  thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
   4.158 +qed
   4.159 +
   4.160 +lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
   4.161 +proof (unfold bottom_def)
   4.162 +  assume "\<And>a. x \<sqsubseteq> a"
   4.163 +  show "\<Sqinter>UNIV = x"
   4.164 +  proof
   4.165 +    fix a show "x \<sqsubseteq> a" .
   4.166 +  next
   4.167 +    fix b :: "'a::complete_lattice"
   4.168 +    assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
   4.169 +    have "x \<in> UNIV" ..
   4.170 +    with b show "b \<sqsubseteq> x" ..
   4.171 +  qed
   4.172 +qed
   4.173 +
   4.174 +lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
   4.175 +proof (unfold top_def)
   4.176 +  have "x \<in> UNIV" ..
   4.177 +  thus "x \<sqsubseteq> \<Squnion>UNIV" ..
   4.178 +qed
   4.179 +
   4.180 +lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
   4.181 +proof (unfold top_def)
   4.182 +  assume "\<And>a. a \<sqsubseteq> x"
   4.183 +  show "\<Squnion>UNIV = x"
   4.184 +  proof
   4.185 +    fix a show "a \<sqsubseteq> x" .
   4.186 +  next
   4.187 +    fix b :: "'a::complete_lattice"
   4.188 +    assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
   4.189 +    have "x \<in> UNIV" ..
   4.190 +    with b show "x \<sqsubseteq> b" ..
   4.191 +  qed
   4.192 +qed
   4.193 +
   4.194 +
   4.195 +subsection {* Duality *}
   4.196 +
   4.197 +text {*
   4.198 +  The class of complete lattices is closed under formation of dual
   4.199 +  structures.
   4.200 +*}
   4.201 +
   4.202 +instance dual :: (complete_lattice) complete_lattice
   4.203 +proof intro_classes
   4.204 +  fix A' :: "'a::complete_lattice dual set"
   4.205 +  show "\<exists>inf'. is_Inf A' inf'"
   4.206 +  proof -
   4.207 +    have "\<exists>sup. is_Sup (undual `` A') sup" by (rule ex_Sup)
   4.208 +    hence "\<exists>sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf)
   4.209 +    thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
   4.210 +  qed
   4.211 +qed
   4.212 +
   4.213 +text {*
   4.214 +  Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
   4.215 +  other.
   4.216 +*}
   4.217 +
   4.218 +theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual `` A)"
   4.219 +proof -
   4.220 +  from is_Inf_Meet have "is_Sup (dual `` A) (dual (\<Sqinter>A))" ..
   4.221 +  hence "\<Squnion>(dual `` A) = dual (\<Sqinter>A)" ..
   4.222 +  thus ?thesis ..
   4.223 +qed
   4.224 +
   4.225 +theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual `` A)"
   4.226 +proof -
   4.227 +  from is_Sup_Join have "is_Inf (dual `` A) (dual (\<Squnion>A))" ..
   4.228 +  hence "\<Sqinter>(dual `` A) = dual (\<Squnion>A)" ..
   4.229 +  thus ?thesis ..
   4.230 +qed
   4.231 +
   4.232 +text {*
   4.233 +  Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
   4.234 +*}
   4.235 +
   4.236 +theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
   4.237 +proof -
   4.238 +  have "\<top> = dual \<bottom>"
   4.239 +  proof
   4.240 +    fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
   4.241 +    hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
   4.242 +    thus "a' \<sqsubseteq> dual \<bottom>" by simp
   4.243 +  qed
   4.244 +  thus ?thesis ..
   4.245 +qed
   4.246 +
   4.247 +theorem dual_top [intro?]: "dual \<top> = \<bottom>"
   4.248 +proof -
   4.249 +  have "\<bottom> = dual \<top>"
   4.250 +  proof
   4.251 +    fix a' have "undual a' \<sqsubseteq> \<top>" ..
   4.252 +    hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
   4.253 +    thus "dual \<top> \<sqsubseteq> a'" by simp
   4.254 +  qed
   4.255 +  thus ?thesis ..
   4.256 +qed
   4.257 +
   4.258 +
   4.259 +subsection {* Complete lattices are lattices *}
   4.260 +
   4.261 +text {*
   4.262 +  Complete lattices (with general bounds) available are indeed plain
   4.263 +  lattices as well.  This holds due to the connection of general
   4.264 +  versus binary bounds that has been formally established in
   4.265 +  \S\ref{sec:gen-bin-bounds}.
   4.266 +*}
   4.267 +
   4.268 +lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
   4.269 +proof -
   4.270 +  have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
   4.271 +  thus ?thesis by (simp only: is_Inf_binary)
   4.272 +qed
   4.273 +
   4.274 +lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
   4.275 +proof -
   4.276 +  have "is_Sup {x, y} (\<Squnion>{x, y})" ..
   4.277 +  thus ?thesis by (simp only: is_Sup_binary)
   4.278 +qed
   4.279 +
   4.280 +instance complete_lattice < lattice
   4.281 +proof intro_classes
   4.282 +  fix x y :: "'a::complete_lattice"
   4.283 +  from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
   4.284 +  from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
   4.285 +qed
   4.286 +
   4.287 +theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
   4.288 +  by (rule meet_equality) (rule is_inf_binary)
   4.289 +
   4.290 +theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"
   4.291 +  by (rule join_equality) (rule is_sup_binary)
   4.292 +
   4.293 +
   4.294 +subsection {* Complete lattices and set-theory operations *}
   4.295 +
   4.296 +text {*
   4.297 +  The complete lattice operations are (anti) monotone wrt.\ set
   4.298 +  inclusion.
   4.299 +*}
   4.300 +
   4.301 +theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
   4.302 +proof (rule Meet_greatest)
   4.303 +  fix a assume "a \<in> A"
   4.304 +  also assume "A \<subseteq> B"
   4.305 +  finally have "a \<in> B" .
   4.306 +  thus "\<Sqinter>B \<sqsubseteq> a" ..
   4.307 +qed
   4.308 +
   4.309 +theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
   4.310 +proof -
   4.311 +  assume "A \<subseteq> B"
   4.312 +  hence "dual `` A \<subseteq> dual `` B" by blast
   4.313 +  hence "\<Sqinter>(dual `` B) \<sqsubseteq> \<Sqinter>(dual `` A)" by (rule Meet_subset_antimono)
   4.314 +  hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
   4.315 +  thus ?thesis by (simp only: dual_leq)
   4.316 +qed
   4.317 +
   4.318 +text {*
   4.319 +  Bounds over unions of sets may be obtained separately.
   4.320 +*}
   4.321 +
   4.322 +theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   4.323 +proof
   4.324 +  fix a assume "a \<in> A \<union> B"
   4.325 +  thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
   4.326 +  proof
   4.327 +    assume a: "a \<in> A"
   4.328 +    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
   4.329 +    also from a have "\<dots> \<sqsubseteq> a" ..
   4.330 +    finally show ?thesis .
   4.331 +  next
   4.332 +    assume a: "a \<in> B"
   4.333 +    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
   4.334 +    also from a have "\<dots> \<sqsubseteq> a" ..
   4.335 +    finally show ?thesis .
   4.336 +  qed
   4.337 +next
   4.338 +  fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
   4.339 +  show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
   4.340 +  proof
   4.341 +    show "b \<sqsubseteq> \<Sqinter>A"
   4.342 +    proof
   4.343 +      fix a assume "a \<in> A"
   4.344 +      hence "a \<in>  A \<union> B" ..
   4.345 +      with b show "b \<sqsubseteq> a" ..
   4.346 +    qed
   4.347 +    show "b \<sqsubseteq> \<Sqinter>B"
   4.348 +    proof
   4.349 +      fix a assume "a \<in> B"
   4.350 +      hence "a \<in>  A \<union> B" ..
   4.351 +      with b show "b \<sqsubseteq> a" ..
   4.352 +    qed
   4.353 +  qed
   4.354 +qed
   4.355 +
   4.356 +theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   4.357 +proof -
   4.358 +  have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual `` A \<union> dual `` B)"
   4.359 +    by (simp only: dual_Join image_Un)
   4.360 +  also have "\<dots> = \<Sqinter>(dual `` A) \<sqinter> \<Sqinter>(dual `` B)"
   4.361 +    by (rule Meet_Un)
   4.362 +  also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
   4.363 +    by (simp only: dual_join dual_Join)
   4.364 +  finally show ?thesis ..
   4.365 +qed
   4.366 +
   4.367 +text {*
   4.368 +  Bounds over singleton sets are trivial.
   4.369 +*}
   4.370 +
   4.371 +theorem Meet_singleton: "\<Sqinter>{x} = x"
   4.372 +proof
   4.373 +  fix a assume "a \<in> {x}"
   4.374 +  hence "a = x" by simp
   4.375 +  thus "x \<sqsubseteq> a" by (simp only: leq_refl)
   4.376 +next
   4.377 +  fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
   4.378 +  thus "b \<sqsubseteq> x" by simp
   4.379 +qed
   4.380 +
   4.381 +theorem Join_singleton: "\<Squnion>{x} = x"
   4.382 +proof -
   4.383 +  have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
   4.384 +  also have "\<dots> = dual x" by (rule Meet_singleton)
   4.385 +  finally show ?thesis ..
   4.386 +qed
   4.387 +
   4.388 +text {*
   4.389 +  Bounds over the empty and universal set correspond to each other.
   4.390 +*}
   4.391 +
   4.392 +theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
   4.393 +proof
   4.394 +  fix a :: "'a::complete_lattice"
   4.395 +  assume "a \<in> {}"
   4.396 +  hence False by simp
   4.397 +  thus "\<Squnion>UNIV \<sqsubseteq> a" ..
   4.398 +next
   4.399 +  fix b :: "'a::complete_lattice"
   4.400 +  have "b \<in> UNIV" ..
   4.401 +  thus "b \<sqsubseteq> \<Squnion>UNIV" ..
   4.402 +qed
   4.403 +
   4.404 +theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
   4.405 +proof -
   4.406 +  have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
   4.407 +  also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
   4.408 +  also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
   4.409 +  finally show ?thesis ..
   4.410 +qed
   4.411 +
   4.412 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Lattice/Lattice.thy	Fri Oct 06 01:04:56 2000 +0200
     5.3 @@ -0,0 +1,609 @@
     5.4 +(*  Title:      HOL/Lattice/Lattice.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Markus Wenzel, TU Muenchen
     5.7 +*)
     5.8 +
     5.9 +header {* Lattices *}
    5.10 +
    5.11 +theory Lattice = Bounds:
    5.12 +
    5.13 +subsection {* Lattice operations *}
    5.14 +
    5.15 +text {*
    5.16 +  A \emph{lattice} is a partial order with infimum and supremum of any
    5.17 +  two elements (thus any \emph{finite} number of elements have bounds
    5.18 +  as well).
    5.19 +*}
    5.20 +
    5.21 +axclass lattice < partial_order
    5.22 +  ex_inf: "\<exists>inf. is_inf x y inf"
    5.23 +  ex_sup: "\<exists>sup. is_sup x y sup"
    5.24 +
    5.25 +text {*
    5.26 +  The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
    5.27 +  infimum and supremum elements.
    5.28 +*}
    5.29 +
    5.30 +consts
    5.31 +  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70)
    5.32 +  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65)
    5.33 +syntax (symbols)
    5.34 +  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70)
    5.35 +  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65)
    5.36 +defs
    5.37 +  meet_def: "x && y \<equiv> SOME inf. is_inf x y inf"
    5.38 +  join_def: "x || y \<equiv> SOME sup. is_sup x y sup"
    5.39 +
    5.40 +text {*
    5.41 +  Due to unique existence of bounds, the lattice operations may be
    5.42 +  exhibited as follows.
    5.43 +*}
    5.44 +
    5.45 +lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
    5.46 +proof (unfold meet_def)
    5.47 +  assume "is_inf x y inf"
    5.48 +  thus "(SOME inf. is_inf x y inf) = inf"
    5.49 +    by (rule some_equality) (rule is_inf_uniq)
    5.50 +qed
    5.51 +
    5.52 +lemma meetI [intro?]:
    5.53 +    "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"
    5.54 +  by (rule meet_equality, rule is_infI) blast+
    5.55 +
    5.56 +lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
    5.57 +proof (unfold join_def)
    5.58 +  assume "is_sup x y sup"
    5.59 +  thus "(SOME sup. is_sup x y sup) = sup"
    5.60 +    by (rule some_equality) (rule is_sup_uniq)
    5.61 +qed
    5.62 +
    5.63 +lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
    5.64 +    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"
    5.65 +  by (rule join_equality, rule is_supI) blast+
    5.66 +
    5.67 +
    5.68 +text {*
    5.69 +  \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine
    5.70 +  bounds on a lattice structure.
    5.71 +*}
    5.72 +
    5.73 +lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
    5.74 +proof (unfold meet_def)
    5.75 +  from ex_inf show "is_inf x y (SOME inf. is_inf x y inf)"
    5.76 +    by (rule ex_someI)
    5.77 +qed
    5.78 +
    5.79 +lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
    5.80 +  by (rule is_inf_greatest) (rule is_inf_meet)
    5.81 +
    5.82 +lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"
    5.83 +  by (rule is_inf_lower) (rule is_inf_meet)
    5.84 +
    5.85 +lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"
    5.86 +  by (rule is_inf_lower) (rule is_inf_meet)
    5.87 +
    5.88 +
    5.89 +lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
    5.90 +proof (unfold join_def)
    5.91 +  from ex_sup show "is_sup x y (SOME sup. is_sup x y sup)"
    5.92 +    by (rule ex_someI)
    5.93 +qed
    5.94 +
    5.95 +lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    5.96 +  by (rule is_sup_least) (rule is_sup_join)
    5.97 +
    5.98 +lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"
    5.99 +  by (rule is_sup_upper) (rule is_sup_join)
   5.100 +
   5.101 +lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"
   5.102 +  by (rule is_sup_upper) (rule is_sup_join)
   5.103 +
   5.104 +
   5.105 +subsection {* Duality *}
   5.106 +
   5.107 +text {*
   5.108 +  The class of lattices is closed under formation of dual structures.
   5.109 +  This means that for any theorem of lattice theory, the dualized
   5.110 +  statement holds as well; this important fact simplifies many proofs
   5.111 +  of lattice theory.
   5.112 +*}
   5.113 +
   5.114 +instance dual :: (lattice) lattice
   5.115 +proof intro_classes
   5.116 +  fix x' y' :: "'a::lattice dual"
   5.117 +  show "\<exists>inf'. is_inf x' y' inf'"
   5.118 +  proof -
   5.119 +    have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
   5.120 +    hence "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
   5.121 +      by (simp only: dual_inf)
   5.122 +    thus ?thesis by (simp add: dual_ex [symmetric])
   5.123 +  qed
   5.124 +  show "\<exists>sup'. is_sup x' y' sup'"
   5.125 +  proof -
   5.126 +    have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
   5.127 +    hence "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
   5.128 +      by (simp only: dual_sup)
   5.129 +    thus ?thesis by (simp add: dual_ex [symmetric])
   5.130 +  qed
   5.131 +qed
   5.132 +
   5.133 +text {*
   5.134 +  Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each
   5.135 +  other.
   5.136 +*}
   5.137 +
   5.138 +theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
   5.139 +proof -
   5.140 +  from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
   5.141 +  hence "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
   5.142 +  thus ?thesis ..
   5.143 +qed
   5.144 +
   5.145 +theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
   5.146 +proof -
   5.147 +  from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
   5.148 +  hence "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
   5.149 +  thus ?thesis ..
   5.150 +qed
   5.151 +
   5.152 +
   5.153 +subsection {* Algebraic properties \label{sec:lattice-algebra} *}
   5.154 +
   5.155 +text {*
   5.156 +  The @{text \<sqinter>} and @{text \<squnion>} operations have to following
   5.157 +  characteristic algebraic properties: associative (A), commutative
   5.158 +  (C), and absorptive (AB).
   5.159 +*}
   5.160 +
   5.161 +theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   5.162 +proof
   5.163 +  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
   5.164 +  proof
   5.165 +    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
   5.166 +    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
   5.167 +    proof -
   5.168 +      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   5.169 +      also have "\<dots> \<sqsubseteq> y" ..
   5.170 +      finally show ?thesis .
   5.171 +    qed
   5.172 +  qed
   5.173 +  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
   5.174 +  proof -
   5.175 +    have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   5.176 +    also have "\<dots> \<sqsubseteq> z" ..
   5.177 +    finally show ?thesis .
   5.178 +  qed
   5.179 +  fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
   5.180 +  show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   5.181 +  proof
   5.182 +    show "w \<sqsubseteq> x"
   5.183 +    proof -
   5.184 +      have "w \<sqsubseteq> x \<sqinter> y" .
   5.185 +      also have "\<dots> \<sqsubseteq> x" ..
   5.186 +      finally show ?thesis .
   5.187 +    qed
   5.188 +    show "w \<sqsubseteq> y \<sqinter> z"
   5.189 +    proof
   5.190 +      show "w \<sqsubseteq> y"
   5.191 +      proof -
   5.192 +        have "w \<sqsubseteq> x \<sqinter> y" .
   5.193 +        also have "\<dots> \<sqsubseteq> y" ..
   5.194 +        finally show ?thesis .
   5.195 +      qed
   5.196 +      show "w \<sqsubseteq> z" .
   5.197 +    qed
   5.198 +  qed
   5.199 +qed
   5.200 +
   5.201 +theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   5.202 +proof -
   5.203 +  have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"
   5.204 +    by (simp only: dual_join)
   5.205 +  also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"
   5.206 +    by (rule meet_assoc)
   5.207 +  also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"
   5.208 +    by (simp only: dual_join)
   5.209 +  finally show ?thesis ..
   5.210 +qed
   5.211 +
   5.212 +theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
   5.213 +proof
   5.214 +  show "y \<sqinter> x \<sqsubseteq> x" ..
   5.215 +  show "y \<sqinter> x \<sqsubseteq> y" ..
   5.216 +  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
   5.217 +  show "z \<sqsubseteq> y \<sqinter> x" ..
   5.218 +qed
   5.219 +
   5.220 +theorem join_commute: "x \<squnion> y = y \<squnion> x"
   5.221 +proof -
   5.222 +  have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..
   5.223 +  also have "\<dots> = dual y \<sqinter> dual x"
   5.224 +    by (rule meet_commute)
   5.225 +  also have "\<dots> = dual (y \<squnion> x)"
   5.226 +    by (simp only: dual_join)
   5.227 +  finally show ?thesis ..
   5.228 +qed
   5.229 +
   5.230 +theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
   5.231 +proof
   5.232 +  show "x \<sqsubseteq> x" ..
   5.233 +  show "x \<sqsubseteq> x \<squnion> y" ..
   5.234 +  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
   5.235 +  show "z \<sqsubseteq> x" .
   5.236 +qed
   5.237 +
   5.238 +theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
   5.239 +proof -
   5.240 +  have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
   5.241 +    by (rule meet_join_absorb)
   5.242 +  hence "dual (x \<squnion> (x \<sqinter> y)) = dual x"
   5.243 +    by (simp only: dual_meet dual_join)
   5.244 +  thus ?thesis ..
   5.245 +qed
   5.246 +
   5.247 +text {*
   5.248 +  \medskip Some further algebraic properties hold as well.  The
   5.249 +  property idempotent (I) is a basic algebraic consequence of (AB).
   5.250 +*}
   5.251 +
   5.252 +theorem meet_idem: "x \<sqinter> x = x"
   5.253 +proof -
   5.254 +  have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
   5.255 +  also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
   5.256 +  finally show ?thesis .
   5.257 +qed
   5.258 +
   5.259 +theorem join_idem: "x \<squnion> x = x"
   5.260 +proof -
   5.261 +  have "dual x \<sqinter> dual x = dual x"
   5.262 +    by (rule meet_idem)
   5.263 +  hence "dual (x \<squnion> x) = dual x"
   5.264 +    by (simp only: dual_join)
   5.265 +  thus ?thesis ..
   5.266 +qed
   5.267 +
   5.268 +text {*
   5.269 +  Meet and join are trivial for related elements.
   5.270 +*}
   5.271 +
   5.272 +theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   5.273 +proof
   5.274 +  assume "x \<sqsubseteq> y"
   5.275 +  show "x \<sqsubseteq> x" ..
   5.276 +  show "x \<sqsubseteq> y" .
   5.277 +  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
   5.278 +qed
   5.279 +
   5.280 +theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   5.281 +proof -
   5.282 +  assume "x \<sqsubseteq> y" hence "dual y \<sqsubseteq> dual x" ..
   5.283 +  hence "dual y \<sqinter> dual x = dual y" by (rule meet_related)
   5.284 +  also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
   5.285 +  also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
   5.286 +  finally show ?thesis ..
   5.287 +qed
   5.288 +
   5.289 +
   5.290 +subsection {* Order versus algebraic structure *}
   5.291 +
   5.292 +text {*
   5.293 +  The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the
   5.294 +  underlying @{text \<sqsubseteq>} relation in a canonical manner.
   5.295 +*}
   5.296 +
   5.297 +theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
   5.298 +proof
   5.299 +  assume "x \<sqsubseteq> y"
   5.300 +  hence "is_inf x y x" ..
   5.301 +  thus "x \<sqinter> y = x" ..
   5.302 +next
   5.303 +  have "x \<sqinter> y \<sqsubseteq> y" ..
   5.304 +  also assume "x \<sqinter> y = x"
   5.305 +  finally show "x \<sqsubseteq> y" .
   5.306 +qed
   5.307 +
   5.308 +theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
   5.309 +proof
   5.310 +  assume "x \<sqsubseteq> y"
   5.311 +  hence "is_sup x y y" ..
   5.312 +  thus "x \<squnion> y = y" ..
   5.313 +next
   5.314 +  have "x \<sqsubseteq> x \<squnion> y" ..
   5.315 +  also assume "x \<squnion> y = y"
   5.316 +  finally show "x \<sqsubseteq> y" .
   5.317 +qed
   5.318 +
   5.319 +text {*
   5.320 +  \medskip The most fundamental result of the meta-theory of lattices
   5.321 +  is as follows (we do not prove it here).
   5.322 +
   5.323 +  Given a structure with binary operations @{text \<sqinter>} and @{text \<squnion>}
   5.324 +  such that (A), (C), and (AB) hold (cf.\
   5.325 +  \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
   5.326 +  if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
   5.327 +  (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and
   5.328 +  supremum with respect to this ordering coincide with the original
   5.329 +  @{text \<sqinter>} and @{text \<squnion>} operations.
   5.330 +*}
   5.331 +
   5.332 +
   5.333 +subsection {* Example instances *}
   5.334 +
   5.335 +subsubsection {* Linear orders *}
   5.336 +
   5.337 +text {*
   5.338 +  Linear orders with @{term minimum} and @{term minimum} operations
   5.339 +  are a (degenerate) example of lattice structures.
   5.340 +*}
   5.341 +
   5.342 +constdefs
   5.343 +  minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
   5.344 +  "minimum x y \<equiv> (if x \<sqsubseteq> y then x else y)"
   5.345 +  maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
   5.346 +  "maximum x y \<equiv> (if x \<sqsubseteq> y then y else x)"
   5.347 +
   5.348 +lemma is_inf_minimum: "is_inf x y (minimum x y)"
   5.349 +proof
   5.350 +  let ?min = "minimum x y"
   5.351 +  from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)
   5.352 +  from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)
   5.353 +  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
   5.354 +  with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)
   5.355 +qed
   5.356 +
   5.357 +lemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)
   5.358 +proof
   5.359 +  let ?max = "maximum x y"
   5.360 +  from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)
   5.361 +  from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)
   5.362 +  fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   5.363 +  with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
   5.364 +qed
   5.365 +
   5.366 +instance linear_order < lattice
   5.367 +proof intro_classes
   5.368 +  fix x y :: "'a::linear_order"
   5.369 +  from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
   5.370 +  from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
   5.371 +qed
   5.372 +
   5.373 +text {*
   5.374 +  The lattice operations on linear orders indeed coincide with @{term
   5.375 +  minimum} and @{term maximum}.
   5.376 +*}
   5.377 +
   5.378 +theorem meet_mimimum: "x \<sqinter> y = minimum x y"
   5.379 +  by (rule meet_equality) (rule is_inf_minimum)
   5.380 +
   5.381 +theorem meet_maximum: "x \<squnion> y = maximum x y"
   5.382 +  by (rule join_equality) (rule is_sup_maximum)
   5.383 +
   5.384 +
   5.385 +
   5.386 +subsubsection {* Binary products *}
   5.387 +
   5.388 +text {*
   5.389 +  The class of lattices is closed under direct binary products (cf.\
   5.390 +  also \S\ref{sec:prod-order}).
   5.391 +*}
   5.392 +
   5.393 +lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   5.394 +proof
   5.395 +  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"
   5.396 +  proof -
   5.397 +    have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..
   5.398 +    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..
   5.399 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.400 +  qed
   5.401 +  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"
   5.402 +  proof -
   5.403 +    have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..
   5.404 +    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..
   5.405 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.406 +  qed
   5.407 +  fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"
   5.408 +  show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   5.409 +  proof -
   5.410 +    have "fst r \<sqsubseteq> fst p \<sqinter> fst q"
   5.411 +    proof
   5.412 +      from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)
   5.413 +      from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)
   5.414 +    qed
   5.415 +    moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"
   5.416 +    proof
   5.417 +      from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)
   5.418 +      from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)
   5.419 +    qed
   5.420 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.421 +  qed
   5.422 +qed
   5.423 +
   5.424 +lemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)
   5.425 +proof
   5.426 +  show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   5.427 +  proof -
   5.428 +    have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..
   5.429 +    moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..
   5.430 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.431 +  qed
   5.432 +  show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   5.433 +  proof -
   5.434 +    have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..
   5.435 +    moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..
   5.436 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.437 +  qed
   5.438 +  fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"
   5.439 +  show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"
   5.440 +  proof -
   5.441 +    have "fst p \<squnion> fst q \<sqsubseteq> fst r"
   5.442 +    proof
   5.443 +      from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)
   5.444 +      from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)
   5.445 +    qed
   5.446 +    moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"
   5.447 +    proof
   5.448 +      from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)
   5.449 +      from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)
   5.450 +    qed
   5.451 +    ultimately show ?thesis by (simp add: leq_prod_def)
   5.452 +  qed
   5.453 +qed
   5.454 +
   5.455 +instance * :: (lattice, lattice) lattice
   5.456 +proof intro_classes
   5.457 +  fix p q :: "'a::lattice \<times> 'b::lattice"
   5.458 +  from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
   5.459 +  from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
   5.460 +qed
   5.461 +
   5.462 +text {*
   5.463 +  The lattice operations on a binary product structure indeed coincide
   5.464 +  with the products of the original ones.
   5.465 +*}
   5.466 +
   5.467 +theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   5.468 +  by (rule meet_equality) (rule is_inf_prod)
   5.469 +
   5.470 +theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   5.471 +  by (rule join_equality) (rule is_sup_prod)
   5.472 +
   5.473 +
   5.474 +subsubsection {* General products *}
   5.475 +
   5.476 +text {*
   5.477 +  The class of lattices is closed under general products (function
   5.478 +  spaces) as well (cf.\ also \S\ref{sec:fun-order}).
   5.479 +*}
   5.480 +
   5.481 +lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
   5.482 +proof
   5.483 +  show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"
   5.484 +  proof
   5.485 +    fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..
   5.486 +  qed
   5.487 +  show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"
   5.488 +  proof
   5.489 +    fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..
   5.490 +  qed
   5.491 +  fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"
   5.492 +  show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"
   5.493 +  proof
   5.494 +    fix x
   5.495 +    show "h x \<sqsubseteq> f x \<sqinter> g x"
   5.496 +    proof
   5.497 +      from hf show "h x \<sqsubseteq> f x" ..
   5.498 +      from hg show "h x \<sqsubseteq> g x" ..
   5.499 +    qed
   5.500 +  qed
   5.501 +qed
   5.502 +
   5.503 +lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)"   (* FIXME dualize!? *)
   5.504 +proof
   5.505 +  show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
   5.506 +  proof
   5.507 +    fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..
   5.508 +  qed
   5.509 +  show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
   5.510 +  proof
   5.511 +    fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..
   5.512 +  qed
   5.513 +  fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"
   5.514 +  show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"
   5.515 +  proof
   5.516 +    fix x
   5.517 +    show "f x \<squnion> g x \<sqsubseteq> h x"
   5.518 +    proof
   5.519 +      from fh show "f x \<sqsubseteq> h x" ..
   5.520 +      from gh show "g x \<sqsubseteq> h x" ..
   5.521 +    qed
   5.522 +  qed
   5.523 +qed
   5.524 +
   5.525 +instance fun :: ("term", lattice) lattice
   5.526 +proof intro_classes
   5.527 +  fix f g :: "'a \<Rightarrow> 'b::lattice"
   5.528 +  show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
   5.529 +  show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
   5.530 +qed
   5.531 +
   5.532 +text {*
   5.533 +  The lattice operations on a general product structure (function
   5.534 +  space) indeed emerge by point-wise lifting of the original ones.
   5.535 +*}
   5.536 +
   5.537 +theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   5.538 +  by (rule meet_equality) (rule is_inf_fun)
   5.539 +
   5.540 +theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   5.541 +  by (rule join_equality) (rule is_sup_fun)
   5.542 +
   5.543 +
   5.544 +subsection {* Monotonicity and semi-morphisms *}
   5.545 +
   5.546 +text {*
   5.547 +  The lattice operations are monotone in both argument positions.  In
   5.548 +  fact, monotonicity of the second position is trivial due to
   5.549 +  commutativity.
   5.550 +*}
   5.551 +
   5.552 +theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
   5.553 +proof -
   5.554 +  {
   5.555 +    fix a b c :: "'a::lattice"
   5.556 +    assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
   5.557 +    proof
   5.558 +      have "a \<sqinter> b \<sqsubseteq> a" ..
   5.559 +      also have "\<dots> \<sqsubseteq> c" .
   5.560 +      finally show "a \<sqinter> b \<sqsubseteq> c" .
   5.561 +      show "a \<sqinter> b \<sqsubseteq> b" ..
   5.562 +    qed
   5.563 +  } note this [elim?]
   5.564 +  assume "x \<sqsubseteq> z" hence "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
   5.565 +  also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
   5.566 +  also assume "y \<sqsubseteq> w" hence "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
   5.567 +  also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
   5.568 +  finally show ?thesis .
   5.569 +qed
   5.570 +
   5.571 +theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
   5.572 +proof -
   5.573 +  assume "x \<sqsubseteq> z" hence "dual z \<sqsubseteq> dual x" ..
   5.574 +  moreover assume "y \<sqsubseteq> w" hence "dual w \<sqsubseteq> dual y" ..
   5.575 +  ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
   5.576 +    by (rule meet_mono)
   5.577 +  hence "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
   5.578 +    by (simp only: dual_join)
   5.579 +  thus ?thesis ..
   5.580 +qed
   5.581 +
   5.582 +text {*
   5.583 +  \medskip A semi-morphisms is a function $f$ that preserves the
   5.584 +  lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
   5.585 +  \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of
   5.586 +  these properties is equivalent with monotonicity.
   5.587 +*}  (* FIXME dual version !? *)
   5.588 +
   5.589 +theorem meet_semimorph:
   5.590 +  "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
   5.591 +proof
   5.592 +  assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   5.593 +  fix x y :: "'a::lattice"
   5.594 +  assume "x \<sqsubseteq> y" hence "x \<sqinter> y = x" ..
   5.595 +  hence "x = x \<sqinter> y" ..
   5.596 +  also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
   5.597 +  also have "\<dots> \<sqsubseteq> f y" ..
   5.598 +  finally show "f x \<sqsubseteq> f y" .
   5.599 +next
   5.600 +  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   5.601 +  show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   5.602 +  proof -
   5.603 +    fix x y
   5.604 +    show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   5.605 +    proof
   5.606 +      have "x \<sqinter> y \<sqsubseteq> x" .. thus "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
   5.607 +      have "x \<sqinter> y \<sqsubseteq> y" .. thus "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
   5.608 +    qed
   5.609 +  qed
   5.610 +qed
   5.611 +
   5.612 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lattice/Orders.thy	Fri Oct 06 01:04:56 2000 +0200
     6.3 @@ -0,0 +1,294 @@
     6.4 +(*  Title:      HOL/Lattice/Orders.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Markus Wenzel, TU Muenchen
     6.7 +*)
     6.8 +
     6.9 +header {* Orders *}
    6.10 +
    6.11 +theory Orders = Main:
    6.12 +
    6.13 +subsection {* Ordered structures *}
    6.14 +
    6.15 +text {*
    6.16 +  We define several classes of ordered structures over some type @{typ
    6.17 +  'a} with relation @{text "\<sqsubseteq> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.  For a
    6.18 +  \emph{quasi-order} that relation is required to be reflexive and
    6.19 +  transitive, for a \emph{partial order} it also has to be
    6.20 +  anti-symmetric, while for a \emph{linear order} all elements are
    6.21 +  required to be related (in either direction).
    6.22 +*}
    6.23 +
    6.24 +axclass leq < "term"
    6.25 +consts
    6.26 +  leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
    6.27 +syntax (symbols)
    6.28 +  leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sqsubseteq>" 50)
    6.29 +
    6.30 +axclass quasi_order < leq
    6.31 +  leq_refl [intro?]: "x \<sqsubseteq> x"
    6.32 +  leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    6.33 +
    6.34 +axclass partial_order < quasi_order
    6.35 +  leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    6.36 +
    6.37 +axclass linear_order < partial_order
    6.38 +  leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    6.39 +
    6.40 +lemma linear_order_cases:
    6.41 +    "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
    6.42 +  by (insert leq_linear) blast
    6.43 +
    6.44 +
    6.45 +subsection {* Duality *}
    6.46 +
    6.47 +text {*
    6.48 +  The \emph{dual} of an ordered structure is an isomorphic copy of the
    6.49 +  underlying type, with the @{text \<sqsubseteq>} relation defined as the inverse
    6.50 +  of the original one.
    6.51 +*}
    6.52 +
    6.53 +datatype 'a dual = dual 'a
    6.54 +
    6.55 +consts
    6.56 +  undual :: "'a dual \<Rightarrow> 'a"
    6.57 +primrec
    6.58 +  undual_dual: "undual (dual x) = x"
    6.59 +
    6.60 +instance dual :: (leq) leq
    6.61 +  by intro_classes
    6.62 +
    6.63 +defs (overloaded)
    6.64 +  leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
    6.65 +
    6.66 +lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
    6.67 +  by (simp add: leq_dual_def)
    6.68 +
    6.69 +lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"
    6.70 +  by (simp add: leq_dual_def)
    6.71 +
    6.72 +text {*
    6.73 +  \medskip Functions @{term dual} and @{term undual} are inverse to
    6.74 +  each other; this entails the following fundamental properties.
    6.75 +*}
    6.76 +
    6.77 +lemma dual_undual [simp]: "dual (undual x') = x'"
    6.78 +  by (cases x') simp
    6.79 +
    6.80 +lemma undual_dual_id [simp]: "undual o dual = id"
    6.81 +  by (rule ext) simp
    6.82 +
    6.83 +lemma dual_undual_id [simp]: "dual o undual = id"
    6.84 +  by (rule ext) simp
    6.85 +
    6.86 +text {*
    6.87 +  \medskip Since @{term dual} (and @{term undual}) are both injective
    6.88 +  and surjective, the basic logical connectives (equality,
    6.89 +  quantification etc.) are transferred as follows.
    6.90 +*}
    6.91 +
    6.92 +lemma undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"
    6.93 +  by (cases x', cases y') simp
    6.94 +
    6.95 +lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"
    6.96 +  by simp
    6.97 +
    6.98 +lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual `` A. P x')"
    6.99 +proof
   6.100 +  assume a: "\<forall>x \<in> A. P (dual x)"
   6.101 +  show "\<forall>x' \<in> dual `` A. P x'"
   6.102 +  proof
   6.103 +    fix x' assume x': "x' \<in> dual `` A"
   6.104 +    have "undual x' \<in> A"
   6.105 +    proof -
   6.106 +      from x' have "undual x' \<in> undual `` dual `` A" by simp
   6.107 +      thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
   6.108 +    qed
   6.109 +    with a have "P (dual (undual x'))" ..
   6.110 +    also have "\<dots> = x'" by simp
   6.111 +    finally show "P x'" .
   6.112 +  qed
   6.113 +next
   6.114 +  assume a: "\<forall>x' \<in> dual `` A. P x'"
   6.115 +  show "\<forall>x \<in> A. P (dual x)"
   6.116 +  proof
   6.117 +    fix x assume "x \<in> A"
   6.118 +    hence "dual x \<in> dual `` A" by simp
   6.119 +    with a show "P (dual x)" ..
   6.120 +  qed
   6.121 +qed
   6.122 +
   6.123 +lemma range_dual [simp]: "dual `` UNIV = UNIV"
   6.124 +proof (rule surj_range)
   6.125 +  have "\<And>x'. dual (undual x') = x'" by simp
   6.126 +  thus "surj dual" by (rule surjI)
   6.127 +qed
   6.128 +
   6.129 +lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
   6.130 +proof -
   6.131 +  have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual `` UNIV. P x')"
   6.132 +    by (rule dual_ball)
   6.133 +  thus ?thesis by simp
   6.134 +qed
   6.135 +
   6.136 +lemma dual_ex: "(\<exists>x. P (dual x)) = (\<exists>x'. P x')"
   6.137 +proof -
   6.138 +  have "(\<forall>x. \<not> P (dual x)) = (\<forall>x'. \<not> P x')"
   6.139 +    by (rule dual_all)
   6.140 +  thus ?thesis by blast
   6.141 +qed
   6.142 +
   6.143 +lemma dual_Collect: "{dual x| x. P (dual x)} = {x'. P x'}"
   6.144 +proof -
   6.145 +  have "{dual x| x. P (dual x)} = {x'. \<exists>x''. x' = x'' \<and> P x''}"
   6.146 +    by (simp only: dual_ex [symmetric])
   6.147 +  thus ?thesis by blast
   6.148 +qed
   6.149 +
   6.150 +
   6.151 +subsection {* Transforming orders *}
   6.152 +
   6.153 +subsubsection {* Duals *}
   6.154 +
   6.155 +text {*
   6.156 +  The classes of quasi, partial, and linear orders are all closed
   6.157 +  under formation of dual structures.
   6.158 +*}
   6.159 +
   6.160 +instance dual :: (quasi_order) quasi_order
   6.161 +proof intro_classes
   6.162 +  fix x' y' z' :: "'a::quasi_order dual"
   6.163 +  have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
   6.164 +  assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
   6.165 +  also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
   6.166 +  finally show "x' \<sqsubseteq> z'" ..
   6.167 +qed
   6.168 +
   6.169 +instance dual :: (partial_order) partial_order
   6.170 +proof intro_classes
   6.171 +  fix x' y' :: "'a::partial_order dual"
   6.172 +  assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
   6.173 +  also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
   6.174 +  finally show "x' = y'" ..
   6.175 +qed
   6.176 +
   6.177 +instance dual :: (linear_order) linear_order
   6.178 +proof intro_classes
   6.179 +  fix x' y' :: "'a::linear_order dual"
   6.180 +  show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
   6.181 +  proof (rule linear_order_cases)
   6.182 +    assume "undual y' \<sqsubseteq> undual x'"
   6.183 +    hence "x' \<sqsubseteq> y'" .. thus ?thesis ..
   6.184 +  next
   6.185 +    assume "undual x' \<sqsubseteq> undual y'"
   6.186 +    hence "y' \<sqsubseteq> x'" .. thus ?thesis ..
   6.187 +  qed
   6.188 +qed
   6.189 +
   6.190 +
   6.191 +subsubsection {* Binary products \label{sec:prod-order} *}
   6.192 +
   6.193 +text {*
   6.194 +  The classes of quasi and partial orders are closed under binary
   6.195 +  products.  Note that the direct product of linear orders need
   6.196 +  \emph{not} be linear in general.
   6.197 +*}
   6.198 +
   6.199 +instance * :: (leq, leq) leq
   6.200 +  by intro_classes
   6.201 +
   6.202 +defs (overloaded)
   6.203 +  leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
   6.204 +
   6.205 +lemma leq_prodI [intro?]:
   6.206 +    "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
   6.207 +  by (unfold leq_prod_def) blast
   6.208 +
   6.209 +lemma leq_prodE [elim?]:
   6.210 +    "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
   6.211 +  by (unfold leq_prod_def) blast
   6.212 +
   6.213 +instance * :: (quasi_order, quasi_order) quasi_order
   6.214 +proof intro_classes
   6.215 +  fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
   6.216 +  show "p \<sqsubseteq> p"
   6.217 +  proof
   6.218 +    show "fst p \<sqsubseteq> fst p" ..
   6.219 +    show "snd p \<sqsubseteq> snd p" ..
   6.220 +  qed
   6.221 +  assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"
   6.222 +  show "p \<sqsubseteq> r"
   6.223 +  proof
   6.224 +    from pq have "fst p \<sqsubseteq> fst q" ..
   6.225 +    also from qr have "\<dots> \<sqsubseteq> fst r" ..
   6.226 +    finally show "fst p \<sqsubseteq> fst r" .
   6.227 +    from pq have "snd p \<sqsubseteq> snd q" ..
   6.228 +    also from qr have "\<dots> \<sqsubseteq> snd r" ..
   6.229 +    finally show "snd p \<sqsubseteq> snd r" .
   6.230 +  qed
   6.231 +qed
   6.232 +
   6.233 +instance * :: (partial_order, partial_order) partial_order
   6.234 +proof intro_classes
   6.235 +  fix p q :: "'a::partial_order \<times> 'b::partial_order"
   6.236 +  assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
   6.237 +  show "p = q"
   6.238 +  proof
   6.239 +    from pq have "fst p \<sqsubseteq> fst q" ..
   6.240 +    also from qp have "\<dots> \<sqsubseteq> fst p" ..
   6.241 +    finally show "fst p = fst q" .
   6.242 +    from pq have "snd p \<sqsubseteq> snd q" ..
   6.243 +    also from qp have "\<dots> \<sqsubseteq> snd p" ..
   6.244 +    finally show "snd p = snd q" .
   6.245 +  qed
   6.246 +qed
   6.247 +
   6.248 +
   6.249 +subsubsection {* General products \label{sec:fun-order} *}
   6.250 +
   6.251 +text {*
   6.252 +  The classes of quasi and partial orders are closed under general
   6.253 +  products (function spaces).  Note that the direct product of linear
   6.254 +  orders need \emph{not} be linear in general.
   6.255 +*}
   6.256 +
   6.257 +instance fun :: ("term", leq) leq
   6.258 +  by intro_classes
   6.259 +
   6.260 +defs (overloaded)
   6.261 +  leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
   6.262 +
   6.263 +lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
   6.264 +  by (unfold leq_fun_def) blast
   6.265 +
   6.266 +lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   6.267 +  by (unfold leq_fun_def) blast
   6.268 +
   6.269 +instance fun :: ("term", quasi_order) quasi_order
   6.270 +proof intro_classes
   6.271 +  fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
   6.272 +  show "f \<sqsubseteq> f"
   6.273 +  proof
   6.274 +    fix x show "f x \<sqsubseteq> f x" ..
   6.275 +  qed
   6.276 +  assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"
   6.277 +  show "f \<sqsubseteq> h"
   6.278 +  proof
   6.279 +    fix x from fg have "f x \<sqsubseteq> g x" ..
   6.280 +    also from gh have "\<dots> \<sqsubseteq> h x" ..
   6.281 +    finally show "f x \<sqsubseteq> h x" .
   6.282 +  qed
   6.283 +qed
   6.284 +
   6.285 +instance fun :: ("term", partial_order) partial_order
   6.286 +proof intro_classes
   6.287 +  fix f g :: "'a \<Rightarrow> 'b::partial_order"
   6.288 +  assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
   6.289 +  show "f = g"
   6.290 +  proof
   6.291 +    fix x from fg have "f x \<sqsubseteq> g x" ..
   6.292 +    also from gf have "\<dots> \<sqsubseteq> f x" ..
   6.293 +    finally show "f x = g x" .
   6.294 +  qed
   6.295 +qed
   6.296 +
   6.297 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Lattice/ROOT.ML	Fri Oct 06 01:04:56 2000 +0200
     7.3 @@ -0,0 +1,8 @@
     7.4 +(*  Title:      HOL/Lattice/ROOT.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Markus Wenzel, TU Muenchen
     7.7 +
     7.8 +Basic theory of lattices and orders.
     7.9 +*)
    7.10 +
    7.11 +time_use_thy "CompleteLattice";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Lattice/document/root.bib	Fri Oct 06 01:04:56 2000 +0200
     8.3 @@ -0,0 +1,48 @@
     8.4 +
     8.5 +@InProceedings{Bauer-Wenzel:2000:HB,
     8.6 +  author =       {Gertrud Bauer and Markus Wenzel},
     8.7 +  title =        {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
     8.8 +      {I}sabelle/{I}sar},
     8.9 +  booktitle =    {Types for Proofs and Programs: TYPES'99},
    8.10 +  editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
    8.11 +                  and Jan Smith},
    8.12 +  series =       {LNCS},
    8.13 +  year =         2000
    8.14 +}
    8.15 +
    8.16 +@Book{Davey-Priestley:1990,
    8.17 +  author        = {B. A. Davey and H. A. Priestley},
    8.18 +  title         = {Introduction to Lattices and Order},
    8.19 +  publisher     = {Cambridge University Press},
    8.20 +  year          = 1990}
    8.21 +
    8.22 +@InProceedings{Wenzel:1999:TPHOL,
    8.23 +  author =       {Markus Wenzel},
    8.24 +  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
    8.25 +  crossref =     {tphols99}}
    8.26 +
    8.27 +
    8.28 +@Manual{Wenzel:2000:axclass,
    8.29 +  author        = {Markus Wenzel},
    8.30 +  title         = {Using Axiomatic Type Classes in Isabelle},
    8.31 +  year          = 2000,
    8.32 +  institution   = {TU Munich},
    8.33 +  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
    8.34 +}
    8.35 +
    8.36 +@Manual{Wenzel:2000:isar-ref,
    8.37 +  author        = {Markus Wenzel},
    8.38 +  title         = {The {Isabelle/Isar} Reference Manual},
    8.39 +  year          = 2000,
    8.40 +  institution   = {TU Munich},
    8.41 +  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
    8.42 +}
    8.43 +
    8.44 +@Proceedings{tphols99,
    8.45 +  title         = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    8.46 +  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    8.47 +  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
    8.48 +                  Paulin, C. and Thery, L.},
    8.49 +  series        = {LNCS},
    8.50 +  volume        = 1690,
    8.51 +  year          = 1999}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Lattice/document/root.tex	Fri Oct 06 01:04:56 2000 +0200
     9.3 @@ -0,0 +1,56 @@
     9.4 +
     9.5 +% $Id$
     9.6 +
     9.7 +\documentclass[11pt,a4paper]{article}
     9.8 +\usepackage{isabelle,isabellesym,pdfsetup}
     9.9 +\usepackage[only,bigsqcap]{stmaryrd}
    9.10 +
    9.11 +\urlstyle{rm}\isabellestyle{it}
    9.12 +\pagestyle{headings}
    9.13 +
    9.14 +\hyphenation{Isabelle}
    9.15 +\hyphenation{Isar}
    9.16 +
    9.17 +
    9.18 +\begin{document}
    9.19 +
    9.20 +\title{Lattices and Orders in Isabelle/HOL}
    9.21 +\author{Markus Wenzel \\ TU M\"unchen}
    9.22 +\maketitle
    9.23 +
    9.24 +\begin{abstract}
    9.25 +  We consider abstract structures of orders and lattices.  Many fundamental
    9.26 +  concepts of lattice theory are developed, including dual structures,
    9.27 +  properties of bounds versus algebraic laws, lattice operations versus
    9.28 +  set-theoretic ones etc.  We also give example instantiations of lattices and
    9.29 +  orders, such as direct products and function spaces.  Well-known properties
    9.30 +  are demonstrated, like the Knaster-Tarski Theorem for complete lattices.
    9.31 +  
    9.32 +  This formal theory development may serve as an example of applying
    9.33 +  Isabelle/HOL to the domain of mathematical reasoning about ``axiomatic''
    9.34 +  structures.  Apart from the simply-typed classical set-theory of HOL, we
    9.35 +  employ Isabelle's system of axiomatic type classes for expressing structures
    9.36 +  and functors in a light-weight manner.  Proofs are expressed in the Isar
    9.37 +  language for readable formal proof, while aiming at its ``best-style'' of
    9.38 +  representing formal reasoning.
    9.39 +\end{abstract}
    9.40 +
    9.41 +\tableofcontents
    9.42 +
    9.43 +\newpage
    9.44 +{
    9.45 +  \parindent 0pt\parskip 0.7ex
    9.46 +  \pagestyle{myheadings}
    9.47 +  \renewcommand{\isamarkupheader}[1]{\markright{THEORY~``\isabellecontext''}\section{#1}}
    9.48 +  \input{session}
    9.49 +}
    9.50 +
    9.51 +\nocite{Wenzel:1999:TPHOL}
    9.52 +\nocite{Wenzel:2000:isar-ref}
    9.53 +\nocite{Wenzel:2000:axclass}
    9.54 +\nocite{Bauer-Wenzel:2000:HB}
    9.55 +
    9.56 +\bibliographystyle{abbrv}
    9.57 +\bibliography{root}
    9.58 +
    9.59 +\end{document}