author wenzelm Fri Oct 06 01:04:56 2000 +0200 (2000-10-06) changeset 10157 6d3987f3aad9 parent 10156 9d4d5852eb47 child 10158 00fdd5c330ea
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
 NEWS file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Lattice/Bounds.thy file | annotate | diff | revisions src/HOL/Lattice/CompleteLattice.thy file | annotate | diff | revisions src/HOL/Lattice/Lattice.thy file | annotate | diff | revisions src/HOL/Lattice/Orders.thy file | annotate | diff | revisions src/HOL/Lattice/ROOT.ML file | annotate | diff | revisions src/HOL/Lattice/document/root.bib file | annotate | diff | revisions src/HOL/Lattice/document/root.tex file | annotate | diff | revisions
     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) 4.42 + Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_"  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.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.47 +  \renewcommand{\isamarkupheader}{\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}