author | ballarin |

Tue Apr 13 09:42:40 2004 +0200 (2004-04-13) | |

changeset 14551 | 2cb6ff394bfb |

parent 14550 | b13da5649bf9 |

child 14552 | e88f52b775a5 |

Various changes to HOL-Algebra;

Locale instantiation.

Locale instantiation.

1.1 --- a/NEWS Tue Apr 13 07:48:32 2004 +0200 1.2 +++ b/NEWS Tue Apr 13 09:42:40 2004 +0200 1.3 @@ -85,13 +85,17 @@ 1.4 - Rule sets <locale>.intro and <locale>.axioms no longer declared as 1.5 [intro?] and [elim?] (respectively) by default. 1.6 - Experimental command for instantiation of locales in proof contexts: 1.7 - instantiate <label>: <loc> 1.8 + instantiate <label>[<attrs>]: <loc> 1.9 Instantiates locale <loc> and adds all its theorems to the current context 1.10 - taking into account their attributes, and qualifying their names with 1.11 - <label>. If the locale has assumptions, a chained fact of the form 1.12 + taking into account their attributes. Label and attrs are optional 1.13 + modifiers, like in theorem declarations. If present, names of 1.14 + instantiated theorems are qualified with <label>, and the attributes 1.15 + <attrs> are applied after any attributes these theorems might have already. 1.16 + If the locale has assumptions, a chained fact of the form 1.17 "<loc> t1 ... tn" is expected from which instantiations of the parameters 1.18 - are derived. 1.19 - A few (very simple) examples can be found in FOL/ex/LocaleInst.thy. 1.20 + are derived. The command does not support old-style locales declared 1.21 + with "locale (open)". 1.22 + A few (very simple) examples can be found in FOL/ex/LocaleInst.thy. 1.23 1.24 * HOL: Tactic emulation methods induct_tac and case_tac understand static 1.25 (Isar) contexts.

2.1 --- a/src/FOL/ex/LocaleInst.thy Tue Apr 13 07:48:32 2004 +0200 2.2 +++ b/src/FOL/ex/LocaleInst.thy Tue Apr 13 09:42:40 2004 +0200 2.3 @@ -18,10 +18,18 @@ 2.4 2.5 lemma "[| A; B |] ==> A & B" 2.6 proof - 2.7 - instantiate my: L1 txt {* No chained fact required. *} 2.8 - assume B and A txt {* order reversed *} 2.9 + instantiate my: L1 txt {* No chained fact required. *} 2.10 + assume B and A txt {* order reversed *} 2.11 + then show "A & B" .. txt {* Applies @{thm my.rev_conjI}. *} 2.12 +qed 2.13 + 2.14 +locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] 2.15 + 2.16 +lemma "[| A; B |] ==> A & B" 2.17 +proof - 2.18 + instantiate [intro]: L11 txt {* Attribute supplied at instantiation. *} 2.19 + assume B and A 2.20 then show "A & B" .. 2.21 - txt {* Applies @{thm my.rev_conjI}. *} 2.22 qed 2.23 2.24 section {* Simple locale with assumptions *} 2.25 @@ -111,4 +119,15 @@ 2.26 show ?thesis by (rule lem) (* lem instantiated to True *) 2.27 qed 2.28 2.29 +section {* Instantiation in a context with target *} 2.30 + 2.31 +lemma (in L4) (* Target might confuse instantiation command. *) 2.32 + fixes A (infixl "$" 60) 2.33 + assumes A: "L4(A)" 2.34 + shows "(x::i) $ y $ z $ w = y $ x $ w $ z" 2.35 +proof - 2.36 + from A instantiate A: L4 2.37 + show ?thesis by (simp only: A.OP.AC) 2.38 +qed 2.39 + 2.40 end

3.1 --- a/src/HOL/Algebra/CRing.thy Tue Apr 13 07:48:32 2004 +0200 3.2 +++ b/src/HOL/Algebra/CRing.thy Tue Apr 13 09:42:40 2004 +0200 3.3 @@ -302,6 +302,9 @@ 3.4 and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==> 3.5 a = \<zero> | b = \<zero>" 3.6 3.7 +locale field = "domain" + 3.8 + assumes field_Units: "Units R = carrier R - {\<zero>}" 3.9 + 3.10 subsection {* Basic Facts of Rings *} 3.11 3.12 lemma ringI: 3.13 @@ -357,7 +360,7 @@ 3.14 "comm_monoid R" 3.15 by (auto intro!: comm_monoidI m_assoc m_comm) 3.16 3.17 -subsection {* Normaliser for Commutative Rings *} 3.18 +subsection {* Normaliser for Rings *} 3.19 3.20 lemma (in abelian_group) r_neg2: 3.21 "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"

4.1 --- a/src/HOL/Algebra/Group.thy Tue Apr 13 07:48:32 2004 +0200 4.2 +++ b/src/HOL/Algebra/Group.thy Tue Apr 13 09:42:40 2004 +0200 4.3 @@ -410,6 +410,7 @@ 4.4 shows "semigroup (G(| carrier := H |))" 4.5 using prems by fast 4.6 4.7 + 4.8 locale subgroup = submagma H G + 4.9 assumes one_closed [intro, simp]: "\<one> \<in> H" 4.10 and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"

5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 5.2 +++ b/src/HOL/Algebra/Lattice.thy Tue Apr 13 09:42:40 2004 +0200 5.3 @@ -0,0 +1,985 @@ 5.4 +(* 5.5 + Title: Orders and Lattices 5.6 + Id: $Id$ 5.7 + Author: Clemens Ballarin, started 7 November 2003 5.8 + Copyright: Clemens Ballarin 5.9 +*) 5.10 + 5.11 +theory Lattice = Group: 5.12 + 5.13 +section {* Order and Lattices *} 5.14 + 5.15 +subsection {* Partial Orders *} 5.16 + 5.17 +record 'a order = "'a partial_object" + 5.18 + le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) 5.19 + 5.20 +locale order_syntax = struct L 5.21 + 5.22 +locale partial_order = order_syntax + 5.23 + assumes refl [intro, simp]: 5.24 + "x \<in> carrier L ==> x \<sqsubseteq> x" 5.25 + and anti_sym [intro]: 5.26 + "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" 5.27 + and trans [trans]: 5.28 + "[| x \<sqsubseteq> y; y \<sqsubseteq> z; 5.29 + x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" 5.30 + 5.31 +constdefs 5.32 + less :: "[('a, 'm) order_scheme, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) 5.33 + "less L x y == le L x y & x ~= y" 5.34 + 5.35 + (* Upper and lower bounds of a set. *) 5.36 + Upper :: "[('a, 'm) order_scheme, 'a set] => 'a set" 5.37 + "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> le L x u)} \<inter> 5.38 + carrier L" 5.39 + 5.40 + Lower :: "[('a, 'm) order_scheme, 'a set] => 'a set" 5.41 + "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> le L l x)} \<inter> 5.42 + carrier L" 5.43 + 5.44 + (* Least and greatest, as predicate. *) 5.45 + least :: "[('a, 'm) order_scheme, 'a, 'a set] => bool" 5.46 + "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. le L l x)" 5.47 + 5.48 + greatest :: "[('a, 'm) order_scheme, 'a, 'a set] => bool" 5.49 + "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. le L x g)" 5.50 + 5.51 + (* Supremum and infimum *) 5.52 + sup :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) 5.53 + "sup L A == THE x. least L x (Upper L A)" 5.54 + 5.55 + inf :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) 5.56 + "inf L A == THE x. greatest L x (Lower L A)" 5.57 + 5.58 + join :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) 5.59 + "join L x y == sup L {x, y}" 5.60 + 5.61 + meet :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65) 5.62 + "meet L x y == inf L {x, y}" 5.63 + 5.64 +(* Upper *) 5.65 + 5.66 +lemma Upper_closed [intro, simp]: 5.67 + "Upper L A \<subseteq> carrier L" 5.68 + by (unfold Upper_def) clarify 5.69 + 5.70 +lemma UpperD [dest]: 5.71 + includes order_syntax 5.72 + shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" 5.73 + by (unfold Upper_def) blast 5.74 + 5.75 +lemma Upper_memI: 5.76 + includes order_syntax 5.77 + shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" 5.78 + by (unfold Upper_def) blast 5.79 + 5.80 +lemma Upper_antimono: 5.81 + "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" 5.82 + by (unfold Upper_def) blast 5.83 + 5.84 +(* Lower *) 5.85 + 5.86 +lemma Lower_closed [intro, simp]: 5.87 + "Lower L A \<subseteq> carrier L" 5.88 + by (unfold Lower_def) clarify 5.89 + 5.90 +lemma LowerD [dest]: 5.91 + includes order_syntax 5.92 + shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x" 5.93 + by (unfold Lower_def) blast 5.94 + 5.95 +lemma Lower_memI: 5.96 + includes order_syntax 5.97 + shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A" 5.98 + by (unfold Lower_def) blast 5.99 + 5.100 +lemma Lower_antimono: 5.101 + "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" 5.102 + by (unfold Lower_def) blast 5.103 + 5.104 +(* least *) 5.105 + 5.106 +lemma least_carrier [intro, simp]: 5.107 + shows "least L l A ==> l \<in> carrier L" 5.108 + by (unfold least_def) fast 5.109 + 5.110 +lemma least_mem: 5.111 + "least L l A ==> l \<in> A" 5.112 + by (unfold least_def) fast 5.113 + 5.114 +lemma (in partial_order) least_unique: 5.115 + "[| least L x A; least L y A |] ==> x = y" 5.116 + by (unfold least_def) blast 5.117 + 5.118 +lemma least_le: 5.119 + includes order_syntax 5.120 + shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a" 5.121 + by (unfold least_def) fast 5.122 + 5.123 +lemma least_UpperI: 5.124 + includes order_syntax 5.125 + assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" 5.126 + and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" 5.127 + and L: "A \<subseteq> carrier L" "s \<in> carrier L" 5.128 + shows "least L s (Upper L A)" 5.129 +proof (unfold least_def, intro conjI) 5.130 + show "Upper L A \<subseteq> carrier L" by simp 5.131 +next 5.132 + from above L show "s \<in> Upper L A" by (simp add: Upper_def) 5.133 +next 5.134 + from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast 5.135 +qed 5.136 + 5.137 +(* greatest *) 5.138 + 5.139 +lemma greatest_carrier [intro, simp]: 5.140 + shows "greatest L l A ==> l \<in> carrier L" 5.141 + by (unfold greatest_def) fast 5.142 + 5.143 +lemma greatest_mem: 5.144 + "greatest L l A ==> l \<in> A" 5.145 + by (unfold greatest_def) fast 5.146 + 5.147 +lemma (in partial_order) greatest_unique: 5.148 + "[| greatest L x A; greatest L y A |] ==> x = y" 5.149 + by (unfold greatest_def) blast 5.150 + 5.151 +lemma greatest_le: 5.152 + includes order_syntax 5.153 + shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" 5.154 + by (unfold greatest_def) fast 5.155 + 5.156 +lemma greatest_LowerI: 5.157 + includes order_syntax 5.158 + assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" 5.159 + and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" 5.160 + and L: "A \<subseteq> carrier L" "i \<in> carrier L" 5.161 + shows "greatest L i (Lower L A)" 5.162 +proof (unfold greatest_def, intro conjI) 5.163 + show "Lower L A \<subseteq> carrier L" by simp 5.164 +next 5.165 + from below L show "i \<in> Lower L A" by (simp add: Lower_def) 5.166 +next 5.167 + from above show "ALL x : Lower L A. x \<sqsubseteq> i" by fast 5.168 +qed 5.169 + 5.170 +subsection {* Lattices *} 5.171 + 5.172 +locale lattice = partial_order + 5.173 + assumes sup_of_two_exists: 5.174 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" 5.175 + and inf_of_two_exists: 5.176 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" 5.177 + 5.178 +lemma least_Upper_above: 5.179 + includes order_syntax 5.180 + shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" 5.181 + by (unfold least_def) blast 5.182 + 5.183 +lemma greatest_Lower_above: 5.184 + includes order_syntax 5.185 + shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" 5.186 + by (unfold greatest_def) blast 5.187 + 5.188 +subsubsection {* Supremum *} 5.189 + 5.190 +lemma (in lattice) joinI: 5.191 + "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] 5.192 + ==> P (x \<squnion> y)" 5.193 +proof (unfold join_def sup_def) 5.194 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.195 + and P: "!!l. least L l (Upper L {x, y}) ==> P l" 5.196 + with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 5.197 + with L show "P (THE l. least L l (Upper L {x, y}))" 5.198 + by (fast intro: theI2 least_unique P) 5.199 +qed 5.200 + 5.201 +lemma (in lattice) join_closed [simp]: 5.202 + "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" 5.203 + by (rule joinI) (rule least_carrier) 5.204 + 5.205 +lemma (in partial_order) sup_of_singletonI: 5.206 + (* only reflexivity needed ? *) 5.207 + "x \<in> carrier L ==> least L x (Upper L {x})" 5.208 + by (rule least_UpperI) fast+ 5.209 + 5.210 +lemma (in partial_order) sup_of_singleton [simp]: 5.211 + includes order_syntax 5.212 + shows "x \<in> carrier L ==> \<Squnion> {x} = x" 5.213 + by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) 5.214 + 5.215 +text {* Condition on A: supremum exists. *} 5.216 + 5.217 +lemma (in lattice) sup_insertI: 5.218 + "[| !!s. least L s (Upper L (insert x A)) ==> P s; 5.219 + least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] 5.220 + ==> P (\<Squnion> (insert x A))" 5.221 +proof (unfold sup_def) 5.222 + assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 5.223 + and P: "!!l. least L l (Upper L (insert x A)) ==> P l" 5.224 + and least_a: "least L a (Upper L A)" 5.225 + from L least_a have La: "a \<in> carrier L" by simp 5.226 + from L sup_of_two_exists least_a 5.227 + obtain s where least_s: "least L s (Upper L {a, x})" by blast 5.228 + show "P (THE l. least L l (Upper L (insert x A)))" 5.229 + proof (rule theI2 [where a = s]) 5.230 + show "least L s (Upper L (insert x A))" 5.231 + proof (rule least_UpperI) 5.232 + fix z 5.233 + assume xA: "z \<in> insert x A" 5.234 + show "z \<sqsubseteq> s" 5.235 + proof - 5.236 + { 5.237 + assume "z = x" then have ?thesis 5.238 + by (simp add: least_Upper_above [OF least_s] L La) 5.239 + } 5.240 + moreover 5.241 + { 5.242 + assume "z \<in> A" 5.243 + with L least_s least_a have ?thesis 5.244 + by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) 5.245 + } 5.246 + moreover note xA 5.247 + ultimately show ?thesis by blast 5.248 + qed 5.249 + next 5.250 + fix y 5.251 + assume y: "y \<in> Upper L (insert x A)" 5.252 + show "s \<sqsubseteq> y" 5.253 + proof (rule least_le [OF least_s], rule Upper_memI) 5.254 + fix z 5.255 + assume z: "z \<in> {a, x}" 5.256 + show "z \<sqsubseteq> y" 5.257 + proof - 5.258 + { 5.259 + have y': "y \<in> Upper L A" 5.260 + apply (rule subsetD [where A = "Upper L (insert x A)"]) 5.261 + apply (rule Upper_antimono) apply clarify apply assumption 5.262 + done 5.263 + assume "z = a" 5.264 + with y' least_a have ?thesis by (fast dest: least_le) 5.265 + } 5.266 + moreover 5.267 + { 5.268 + assume "z = x" 5.269 + with y L have ?thesis by blast 5.270 + } 5.271 + moreover note z 5.272 + ultimately show ?thesis by blast 5.273 + qed 5.274 + qed (rule Upper_closed [THEN subsetD]) 5.275 + next 5.276 + from L show "insert x A \<subseteq> carrier L" by simp 5.277 + next 5.278 + from least_s show "s \<in> carrier L" by simp 5.279 + qed 5.280 +next 5.281 + fix l 5.282 + assume least_l: "least L l (Upper L (insert x A))" 5.283 + show "l = s" 5.284 + proof (rule least_unique) 5.285 + show "least L s (Upper L (insert x A))" 5.286 + proof (rule least_UpperI) 5.287 + fix z 5.288 + assume xA: "z \<in> insert x A" 5.289 + show "z \<sqsubseteq> s" 5.290 + proof - 5.291 + { 5.292 + assume "z = x" then have ?thesis 5.293 + by (simp add: least_Upper_above [OF least_s] L La) 5.294 + } 5.295 + moreover 5.296 + { 5.297 + assume "z \<in> A" 5.298 + with L least_s least_a have ?thesis 5.299 + by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) 5.300 + } 5.301 + moreover note xA 5.302 + ultimately show ?thesis by blast 5.303 + qed 5.304 + next 5.305 + fix y 5.306 + assume y: "y \<in> Upper L (insert x A)" 5.307 + show "s \<sqsubseteq> y" 5.308 + proof (rule least_le [OF least_s], rule Upper_memI) 5.309 + fix z 5.310 + assume z: "z \<in> {a, x}" 5.311 + show "z \<sqsubseteq> y" 5.312 + proof - 5.313 + { 5.314 + have y': "y \<in> Upper L A" 5.315 + apply (rule subsetD [where A = "Upper L (insert x A)"]) 5.316 + apply (rule Upper_antimono) apply clarify apply assumption 5.317 + done 5.318 + assume "z = a" 5.319 + with y' least_a have ?thesis by (fast dest: least_le) 5.320 + } 5.321 + moreover 5.322 + { 5.323 + assume "z = x" 5.324 + with y L have ?thesis by blast 5.325 + } 5.326 + moreover note z 5.327 + ultimately show ?thesis by blast 5.328 + qed 5.329 + qed (rule Upper_closed [THEN subsetD]) 5.330 + next 5.331 + from L show "insert x A \<subseteq> carrier L" by simp 5.332 + next 5.333 + from least_s show "s \<in> carrier L" by simp 5.334 + qed 5.335 + qed 5.336 + qed 5.337 +qed 5.338 + 5.339 +lemma (in lattice) finite_sup_least: 5.340 + "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion> A) (Upper L A)" 5.341 +proof (induct set: Finites) 5.342 + case empty then show ?case by simp 5.343 +next 5.344 + case (insert A x) 5.345 + show ?case 5.346 + proof (cases "A = {}") 5.347 + case True 5.348 + with insert show ?thesis by (simp add: sup_of_singletonI) 5.349 + next 5.350 + case False 5.351 + from insert show ?thesis 5.352 + proof (rule_tac sup_insertI) 5.353 + from False insert show "least L (\<Squnion> A) (Upper L A)" by simp 5.354 + qed simp_all 5.355 + qed 5.356 +qed 5.357 + 5.358 +lemma (in lattice) finite_sup_insertI: 5.359 + assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" 5.360 + and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 5.361 + shows "P (\<Squnion> (insert x A))" 5.362 +proof (cases "A = {}") 5.363 + case True with P and xA show ?thesis 5.364 + by (simp add: sup_of_singletonI) 5.365 +next 5.366 + case False with P and xA show ?thesis 5.367 + by (simp add: sup_insertI finite_sup_least) 5.368 +qed 5.369 + 5.370 +lemma (in lattice) finite_sup_closed: 5.371 + "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion> A \<in> carrier L" 5.372 +proof (induct set: Finites) 5.373 + case empty then show ?case by simp 5.374 +next 5.375 + case (insert A x) then show ?case 5.376 + by (rule_tac finite_sup_insertI) (simp_all) 5.377 +qed 5.378 + 5.379 +lemma (in lattice) join_left: 5.380 + "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" 5.381 + by (rule joinI [folded join_def]) (blast dest: least_mem ) 5.382 + 5.383 +lemma (in lattice) join_right: 5.384 + "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" 5.385 + by (rule joinI [folded join_def]) (blast dest: least_mem ) 5.386 + 5.387 +lemma (in lattice) sup_of_two_least: 5.388 + "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion> {x, y}) (Upper L {x, y})" 5.389 +proof (unfold sup_def) 5.390 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.391 + with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 5.392 + with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" 5.393 + by (fast intro: theI2 least_unique) (* blast fails *) 5.394 +qed 5.395 + 5.396 +lemma (in lattice) join_le: 5.397 + assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" 5.398 + and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.399 + shows "x \<squnion> y \<sqsubseteq> z" 5.400 +proof (rule joinI) 5.401 + fix s 5.402 + assume "least L s (Upper L {x, y})" 5.403 + with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) 5.404 +qed 5.405 + 5.406 +lemma (in lattice) join_assoc_lemma: 5.407 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.408 + shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}" 5.409 +proof (rule finite_sup_insertI) 5.410 + (* The textbook argument in Jacobson I, p 457 *) 5.411 + fix s 5.412 + assume sup: "least L s (Upper L {x, y, z})" 5.413 + show "x \<squnion> (y \<squnion> z) = s" 5.414 + proof (rule anti_sym) 5.415 + from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" 5.416 + by (fastsimp intro!: join_le elim: least_Upper_above) 5.417 + next 5.418 + from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" 5.419 + by (erule_tac least_le) 5.420 + (blast intro!: Upper_memI intro: trans join_left join_right join_closed) 5.421 + qed (simp_all add: L least_carrier [OF sup]) 5.422 +qed (simp_all add: L) 5.423 + 5.424 +lemma join_comm: 5.425 + includes order_syntax 5.426 + shows "x \<squnion> y = y \<squnion> x" 5.427 + by (unfold join_def) (simp add: insert_commute) 5.428 + 5.429 +lemma (in lattice) join_assoc: 5.430 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.431 + shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 5.432 +proof - 5.433 + have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) 5.434 + also from L have "... = \<Squnion> {z, x, y}" by (simp add: join_assoc_lemma) 5.435 + also from L have "... = \<Squnion> {x, y, z}" by (simp add: insert_commute) 5.436 + also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) 5.437 + finally show ?thesis . 5.438 +qed 5.439 + 5.440 +subsubsection {* Infimum *} 5.441 + 5.442 +lemma (in lattice) meetI: 5.443 + "[| !!i. greatest L i (Lower L {x, y}) ==> P i; 5.444 + x \<in> carrier L; y \<in> carrier L |] 5.445 + ==> P (x \<sqinter> y)" 5.446 +proof (unfold meet_def inf_def) 5.447 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.448 + and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" 5.449 + with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast 5.450 + with L show "P (THE g. greatest L g (Lower L {x, y}))" 5.451 + by (fast intro: theI2 greatest_unique P) 5.452 +qed 5.453 + 5.454 +lemma (in lattice) meet_closed [simp]: 5.455 + "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" 5.456 + by (rule meetI) (rule greatest_carrier) 5.457 + 5.458 +lemma (in partial_order) inf_of_singletonI: 5.459 + (* only reflexivity needed ? *) 5.460 + "x \<in> carrier L ==> greatest L x (Lower L {x})" 5.461 + by (rule greatest_LowerI) fast+ 5.462 + 5.463 +lemma (in partial_order) inf_of_singleton [simp]: 5.464 + includes order_syntax 5.465 + shows "x \<in> carrier L ==> \<Sqinter> {x} = x" 5.466 + by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) 5.467 + 5.468 +text {* Condition on A: infimum exists. *} 5.469 + 5.470 +lemma (in lattice) inf_insertI: 5.471 + "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; 5.472 + greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] 5.473 + ==> P (\<Sqinter> (insert x A))" 5.474 +proof (unfold inf_def) 5.475 + assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 5.476 + and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" 5.477 + and greatest_a: "greatest L a (Lower L A)" 5.478 + from L greatest_a have La: "a \<in> carrier L" by simp 5.479 + from L inf_of_two_exists greatest_a 5.480 + obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast 5.481 + show "P (THE g. greatest L g (Lower L (insert x A)))" 5.482 + proof (rule theI2 [where a = i]) 5.483 + show "greatest L i (Lower L (insert x A))" 5.484 + proof (rule greatest_LowerI) 5.485 + fix z 5.486 + assume xA: "z \<in> insert x A" 5.487 + show "i \<sqsubseteq> z" 5.488 + proof - 5.489 + { 5.490 + assume "z = x" then have ?thesis 5.491 + by (simp add: greatest_Lower_above [OF greatest_i] L La) 5.492 + } 5.493 + moreover 5.494 + { 5.495 + assume "z \<in> A" 5.496 + with L greatest_i greatest_a have ?thesis 5.497 + by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) 5.498 + } 5.499 + moreover note xA 5.500 + ultimately show ?thesis by blast 5.501 + qed 5.502 + next 5.503 + fix y 5.504 + assume y: "y \<in> Lower L (insert x A)" 5.505 + show "y \<sqsubseteq> i" 5.506 + proof (rule greatest_le [OF greatest_i], rule Lower_memI) 5.507 + fix z 5.508 + assume z: "z \<in> {a, x}" 5.509 + show "y \<sqsubseteq> z" 5.510 + proof - 5.511 + { 5.512 + have y': "y \<in> Lower L A" 5.513 + apply (rule subsetD [where A = "Lower L (insert x A)"]) 5.514 + apply (rule Lower_antimono) apply clarify apply assumption 5.515 + done 5.516 + assume "z = a" 5.517 + with y' greatest_a have ?thesis by (fast dest: greatest_le) 5.518 + } 5.519 + moreover 5.520 + { 5.521 + assume "z = x" 5.522 + with y L have ?thesis by blast 5.523 + } 5.524 + moreover note z 5.525 + ultimately show ?thesis by blast 5.526 + qed 5.527 + qed (rule Lower_closed [THEN subsetD]) 5.528 + next 5.529 + from L show "insert x A \<subseteq> carrier L" by simp 5.530 + next 5.531 + from greatest_i show "i \<in> carrier L" by simp 5.532 + qed 5.533 +next 5.534 + fix g 5.535 + assume greatest_g: "greatest L g (Lower L (insert x A))" 5.536 + show "g = i" 5.537 + proof (rule greatest_unique) 5.538 + show "greatest L i (Lower L (insert x A))" 5.539 + proof (rule greatest_LowerI) 5.540 + fix z 5.541 + assume xA: "z \<in> insert x A" 5.542 + show "i \<sqsubseteq> z" 5.543 + proof - 5.544 + { 5.545 + assume "z = x" then have ?thesis 5.546 + by (simp add: greatest_Lower_above [OF greatest_i] L La) 5.547 + } 5.548 + moreover 5.549 + { 5.550 + assume "z \<in> A" 5.551 + with L greatest_i greatest_a have ?thesis 5.552 + by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) 5.553 + } 5.554 + moreover note xA 5.555 + ultimately show ?thesis by blast 5.556 + qed 5.557 + next 5.558 + fix y 5.559 + assume y: "y \<in> Lower L (insert x A)" 5.560 + show "y \<sqsubseteq> i" 5.561 + proof (rule greatest_le [OF greatest_i], rule Lower_memI) 5.562 + fix z 5.563 + assume z: "z \<in> {a, x}" 5.564 + show "y \<sqsubseteq> z" 5.565 + proof - 5.566 + { 5.567 + have y': "y \<in> Lower L A" 5.568 + apply (rule subsetD [where A = "Lower L (insert x A)"]) 5.569 + apply (rule Lower_antimono) apply clarify apply assumption 5.570 + done 5.571 + assume "z = a" 5.572 + with y' greatest_a have ?thesis by (fast dest: greatest_le) 5.573 + } 5.574 + moreover 5.575 + { 5.576 + assume "z = x" 5.577 + with y L have ?thesis by blast 5.578 + } 5.579 + moreover note z 5.580 + ultimately show ?thesis by blast 5.581 + qed 5.582 + qed (rule Lower_closed [THEN subsetD]) 5.583 + next 5.584 + from L show "insert x A \<subseteq> carrier L" by simp 5.585 + next 5.586 + from greatest_i show "i \<in> carrier L" by simp 5.587 + qed 5.588 + qed 5.589 + qed 5.590 +qed 5.591 + 5.592 +lemma (in lattice) finite_inf_greatest: 5.593 + "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter> A) (Lower L A)" 5.594 +proof (induct set: Finites) 5.595 + case empty then show ?case by simp 5.596 +next 5.597 + case (insert A x) 5.598 + show ?case 5.599 + proof (cases "A = {}") 5.600 + case True 5.601 + with insert show ?thesis by (simp add: inf_of_singletonI) 5.602 + next 5.603 + case False 5.604 + from insert show ?thesis 5.605 + proof (rule_tac inf_insertI) 5.606 + from False insert show "greatest L (\<Sqinter> A) (Lower L A)" by simp 5.607 + qed simp_all 5.608 + qed 5.609 +qed 5.610 + 5.611 +lemma (in lattice) finite_inf_insertI: 5.612 + assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" 5.613 + and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 5.614 + shows "P (\<Sqinter> (insert x A))" 5.615 +proof (cases "A = {}") 5.616 + case True with P and xA show ?thesis 5.617 + by (simp add: inf_of_singletonI) 5.618 +next 5.619 + case False with P and xA show ?thesis 5.620 + by (simp add: inf_insertI finite_inf_greatest) 5.621 +qed 5.622 + 5.623 +lemma (in lattice) finite_inf_closed: 5.624 + "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter> A \<in> carrier L" 5.625 +proof (induct set: Finites) 5.626 + case empty then show ?case by simp 5.627 +next 5.628 + case (insert A x) then show ?case 5.629 + by (rule_tac finite_inf_insertI) (simp_all) 5.630 +qed 5.631 + 5.632 +lemma (in lattice) meet_left: 5.633 + "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" 5.634 + by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) 5.635 + 5.636 +lemma (in lattice) meet_right: 5.637 + "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" 5.638 + by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) 5.639 + 5.640 +lemma (in lattice) inf_of_two_greatest: 5.641 + "[| x \<in> carrier L; y \<in> carrier L |] ==> 5.642 + greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" 5.643 +proof (unfold inf_def) 5.644 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.645 + with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast 5.646 + with L 5.647 + show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" 5.648 + by (fast intro: theI2 greatest_unique) (* blast fails *) 5.649 +qed 5.650 + 5.651 +lemma (in lattice) meet_le: 5.652 + assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" 5.653 + and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.654 + shows "z \<sqsubseteq> x \<sqinter> y" 5.655 +proof (rule meetI) 5.656 + fix i 5.657 + assume "greatest L i (Lower L {x, y})" 5.658 + with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) 5.659 +qed 5.660 + 5.661 +lemma (in lattice) meet_assoc_lemma: 5.662 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.663 + shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter> {x, y, z}" 5.664 +proof (rule finite_inf_insertI) 5.665 + txt {* The textbook argument in Jacobson I, p 457 *} 5.666 + fix i 5.667 + assume inf: "greatest L i (Lower L {x, y, z})" 5.668 + show "x \<sqinter> (y \<sqinter> z) = i" 5.669 + proof (rule anti_sym) 5.670 + from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" 5.671 + by (fastsimp intro!: meet_le elim: greatest_Lower_above) 5.672 + next 5.673 + from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" 5.674 + by (erule_tac greatest_le) 5.675 + (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) 5.676 + qed (simp_all add: L greatest_carrier [OF inf]) 5.677 +qed (simp_all add: L) 5.678 + 5.679 +lemma meet_comm: 5.680 + includes order_syntax 5.681 + shows "x \<sqinter> y = y \<sqinter> x" 5.682 + by (unfold meet_def) (simp add: insert_commute) 5.683 + 5.684 +lemma (in lattice) meet_assoc: 5.685 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 5.686 + shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 5.687 +proof - 5.688 + have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) 5.689 + also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) 5.690 + also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) 5.691 + also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) 5.692 + finally show ?thesis . 5.693 +qed 5.694 + 5.695 +subsection {* Total Orders *} 5.696 + 5.697 +locale total_order = lattice + 5.698 + assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" 5.699 + 5.700 +text {* Introduction rule: the usual definition of total order *} 5.701 + 5.702 +lemma (in partial_order) total_orderI: 5.703 + assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" 5.704 + shows "total_order L" 5.705 +proof (rule total_order.intro) 5.706 + show "lattice_axioms L" 5.707 + proof (rule lattice_axioms.intro) 5.708 + fix x y 5.709 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.710 + show "EX s. least L s (Upper L {x, y})" 5.711 + proof - 5.712 + note total L 5.713 + moreover 5.714 + { 5.715 + assume "x \<sqsubseteq> y" 5.716 + with L have "least L y (Upper L {x, y})" 5.717 + by (rule_tac least_UpperI) auto 5.718 + } 5.719 + moreover 5.720 + { 5.721 + assume "y \<sqsubseteq> x" 5.722 + with L have "least L x (Upper L {x, y})" 5.723 + by (rule_tac least_UpperI) auto 5.724 + } 5.725 + ultimately show ?thesis by blast 5.726 + qed 5.727 + next 5.728 + fix x y 5.729 + assume L: "x \<in> carrier L" "y \<in> carrier L" 5.730 + show "EX i. greatest L i (Lower L {x, y})" 5.731 + proof - 5.732 + note total L 5.733 + moreover 5.734 + { 5.735 + assume "y \<sqsubseteq> x" 5.736 + with L have "greatest L y (Lower L {x, y})" 5.737 + by (rule_tac greatest_LowerI) auto 5.738 + } 5.739 + moreover 5.740 + { 5.741 + assume "x \<sqsubseteq> y" 5.742 + with L have "greatest L x (Lower L {x, y})" 5.743 + by (rule_tac greatest_LowerI) auto 5.744 + } 5.745 + ultimately show ?thesis by blast 5.746 + qed 5.747 + qed 5.748 +qed (assumption | rule total_order_axioms.intro)+ 5.749 + 5.750 +subsection {* Complete lattices *} 5.751 + 5.752 +locale complete_lattice = lattice + 5.753 + assumes sup_exists: 5.754 + "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" 5.755 + and inf_exists: 5.756 + "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" 5.757 + 5.758 +text {* Introduction rule: the usual definition of complete lattice *} 5.759 + 5.760 +lemma (in partial_order) complete_latticeI: 5.761 + assumes sup_exists: 5.762 + "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" 5.763 + and inf_exists: 5.764 + "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" 5.765 + shows "complete_lattice L" 5.766 +proof (rule complete_lattice.intro) 5.767 + show "lattice_axioms L" 5.768 + by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ 5.769 +qed (assumption | rule complete_lattice_axioms.intro)+ 5.770 + 5.771 +constdefs 5.772 + top :: "('a, 'm) order_scheme => 'a" ("\<top>\<index>") 5.773 + "top L == sup L (carrier L)" 5.774 + 5.775 + bottom :: "('a, 'm) order_scheme => 'a" ("\<bottom>\<index>") 5.776 + "bottom L == inf L (carrier L)" 5.777 + 5.778 + 5.779 +lemma (in complete_lattice) supI: 5.780 + "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] 5.781 + ==> P (\<Squnion> A)" 5.782 +proof (unfold sup_def) 5.783 + assume L: "A \<subseteq> carrier L" 5.784 + and P: "!!l. least L l (Upper L A) ==> P l" 5.785 + with sup_exists obtain s where "least L s (Upper L A)" by blast 5.786 + with L show "P (THE l. least L l (Upper L A))" 5.787 + by (fast intro: theI2 least_unique P) 5.788 +qed 5.789 + 5.790 +lemma (in complete_lattice) sup_closed [simp]: 5.791 + "A \<subseteq> carrier L ==> \<Squnion> A \<in> carrier L" 5.792 + by (rule supI) simp_all 5.793 + 5.794 +lemma (in complete_lattice) top_closed [simp, intro]: 5.795 + "\<top> \<in> carrier L" 5.796 + by (unfold top_def) simp 5.797 + 5.798 +lemma (in complete_lattice) infI: 5.799 + "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] 5.800 + ==> P (\<Sqinter> A)" 5.801 +proof (unfold inf_def) 5.802 + assume L: "A \<subseteq> carrier L" 5.803 + and P: "!!l. greatest L l (Lower L A) ==> P l" 5.804 + with inf_exists obtain s where "greatest L s (Lower L A)" by blast 5.805 + with L show "P (THE l. greatest L l (Lower L A))" 5.806 + by (fast intro: theI2 greatest_unique P) 5.807 +qed 5.808 + 5.809 +lemma (in complete_lattice) inf_closed [simp]: 5.810 + "A \<subseteq> carrier L ==> \<Sqinter> A \<in> carrier L" 5.811 + by (rule infI) simp_all 5.812 + 5.813 +lemma (in complete_lattice) bottom_closed [simp, intro]: 5.814 + "\<bottom> \<in> carrier L" 5.815 + by (unfold bottom_def) simp 5.816 + 5.817 +text {* Jacobson: Theorem 8.1 *} 5.818 + 5.819 +lemma Lower_empty [simp]: 5.820 + "Lower L {} = carrier L" 5.821 + by (unfold Lower_def) simp 5.822 + 5.823 +lemma Upper_empty [simp]: 5.824 + "Upper L {} = carrier L" 5.825 + by (unfold Upper_def) simp 5.826 + 5.827 +theorem (in partial_order) complete_lattice_criterion1: 5.828 + assumes top_exists: "EX g. greatest L g (carrier L)" 5.829 + and inf_exists: 5.830 + "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" 5.831 + shows "complete_lattice L" 5.832 +proof (rule complete_latticeI) 5.833 + from top_exists obtain top where top: "greatest L top (carrier L)" .. 5.834 + fix A 5.835 + assume L: "A \<subseteq> carrier L" 5.836 + let ?B = "Upper L A" 5.837 + from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) 5.838 + then have B_non_empty: "?B ~= {}" by fast 5.839 + have B_L: "?B \<subseteq> carrier L" by simp 5.840 + from inf_exists [OF B_L B_non_empty] 5.841 + obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. 5.842 + have "least L b (Upper L A)" 5.843 +apply (rule least_UpperI) 5.844 + apply (rule greatest_le [where A = "Lower L ?B"]) 5.845 + apply (rule b_inf_B) 5.846 + apply (rule Lower_memI) 5.847 + apply (erule UpperD) 5.848 + apply assumption 5.849 + apply (rule L) 5.850 + apply (fast intro: L [THEN subsetD]) 5.851 + apply (erule greatest_Lower_above [OF b_inf_B]) 5.852 + apply simp 5.853 + apply (rule L) 5.854 +apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) 5.855 +done 5.856 + then show "EX s. least L s (Upper L A)" .. 5.857 +next 5.858 + fix A 5.859 + assume L: "A \<subseteq> carrier L" 5.860 + show "EX i. greatest L i (Lower L A)" 5.861 + proof (cases "A = {}") 5.862 + case True then show ?thesis 5.863 + by (simp add: top_exists) 5.864 + next 5.865 + case False with L show ?thesis 5.866 + by (rule inf_exists) 5.867 + qed 5.868 +qed 5.869 + 5.870 +(* TODO: prove dual version *) 5.871 + 5.872 +subsection {* Examples *} 5.873 + 5.874 +subsubsection {* Powerset of a set is a complete lattice *} 5.875 + 5.876 +theorem powerset_is_complete_lattice: 5.877 + "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" 5.878 + (is "complete_lattice ?L") 5.879 +proof (rule partial_order.complete_latticeI) 5.880 + show "partial_order ?L" 5.881 + by (rule partial_order.intro) auto 5.882 +next 5.883 + fix B 5.884 + assume "B \<subseteq> carrier ?L" 5.885 + then have "least ?L (\<Union> B) (Upper ?L B)" 5.886 + by (fastsimp intro!: least_UpperI simp: Upper_def) 5.887 + then show "EX s. least ?L s (Upper ?L B)" .. 5.888 +next 5.889 + fix B 5.890 + assume "B \<subseteq> carrier ?L" 5.891 + then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" 5.892 + txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: 5.893 + @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} 5.894 + by (fastsimp intro!: greatest_LowerI simp: Lower_def) 5.895 + then show "EX i. greatest ?L i (Lower ?L B)" .. 5.896 +qed 5.897 + 5.898 +subsubsection {* Lattice of subgroups of a group *} 5.899 + 5.900 +theorem (in group) subgroups_partial_order: 5.901 + "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" 5.902 + by (rule partial_order.intro) simp_all 5.903 + 5.904 +lemma (in group) subgroup_self: 5.905 + "subgroup (carrier G) G" 5.906 + by (rule subgroupI) auto 5.907 + 5.908 +lemma (in group) subgroup_imp_group: 5.909 + "subgroup H G ==> group (G(| carrier := H |))" 5.910 + using subgroup.groupI [OF _ group.intro] . 5.911 + 5.912 +lemma (in group) is_monoid [intro, simp]: 5.913 + "monoid G" 5.914 + by (rule monoid.intro) 5.915 + 5.916 +lemma (in group) subgroup_inv_equality: 5.917 + "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x" 5.918 +apply (rule_tac inv_equality [THEN sym]) 5.919 + apply (rule group.l_inv [OF subgroup_imp_group, simplified]) 5.920 + apply assumption+ 5.921 + apply (rule subsetD [OF subgroup.subset]) 5.922 + apply assumption+ 5.923 +apply (rule subsetD [OF subgroup.subset]) 5.924 + apply assumption 5.925 +apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) 5.926 + apply assumption+ 5.927 +done 5.928 + 5.929 +theorem (in group) subgroups_Inter: 5.930 + assumes subgr: "(!!H. H \<in> A ==> subgroup H G)" 5.931 + and not_empty: "A ~= {}" 5.932 + shows "subgroup (\<Inter>A) G" 5.933 +proof (rule subgroupI) 5.934 + from subgr [THEN subgroup.subset] and not_empty 5.935 + show "\<Inter>A \<subseteq> carrier G" by blast 5.936 +next 5.937 + from subgr [THEN subgroup.one_closed] 5.938 + show "\<Inter>A ~= {}" by blast 5.939 +next 5.940 + fix x assume "x \<in> \<Inter>A" 5.941 + with subgr [THEN subgroup.m_inv_closed] 5.942 + show "inv x \<in> \<Inter>A" by blast 5.943 +next 5.944 + fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" 5.945 + with subgr [THEN subgroup.m_closed] 5.946 + show "x \<otimes> y \<in> \<Inter>A" by blast 5.947 +qed 5.948 + 5.949 +theorem (in group) subgroups_complete_lattice: 5.950 + "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" 5.951 + (is "complete_lattice ?L") 5.952 +proof (rule partial_order.complete_lattice_criterion1) 5.953 + show "partial_order ?L" by (rule subgroups_partial_order) 5.954 +next 5.955 + have "greatest ?L (carrier G) (carrier ?L)" 5.956 + by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) 5.957 + then show "EX G. greatest ?L G (carrier ?L)" .. 5.958 +next 5.959 + fix A 5.960 + assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" 5.961 + then have Int_subgroup: "subgroup (\<Inter>A) G" 5.962 + by (fastsimp intro: subgroups_Inter) 5.963 + have "greatest ?L (\<Inter>A) (Lower ?L A)" 5.964 + (is "greatest ?L ?Int _") 5.965 + proof (rule greatest_LowerI) 5.966 + fix H 5.967 + assume H: "H \<in> A" 5.968 + with L have subgroupH: "subgroup H G" by auto 5.969 + from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) 5.970 + from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") 5.971 + by (rule subgroup_imp_group) 5.972 + from groupH have monoidH: "monoid ?H" 5.973 + by (rule group.is_monoid) 5.974 + from H have Int_subset: "?Int \<subseteq> H" by fastsimp 5.975 + then show "le ?L ?Int H" by simp 5.976 + next 5.977 + fix H 5.978 + assume H: "H \<in> Lower ?L A" 5.979 + with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) 5.980 + next 5.981 + show "A \<subseteq> carrier ?L" by (rule L) 5.982 + next 5.983 + show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) 5.984 + qed 5.985 + then show "EX I. greatest ?L I (Lower ?L A)" .. 5.986 +qed 5.987 + 5.988 +end 5.989 \ No newline at end of file

6.1 --- a/src/HOL/Algebra/ROOT.ML Tue Apr 13 07:48:32 2004 +0200 6.2 +++ b/src/HOL/Algebra/ROOT.ML Tue Apr 13 09:42:40 2004 +0200 6.3 @@ -16,6 +16,7 @@ 6.4 use_thy "FiniteProduct"; (* Product operator for commutative groups *) 6.5 use_thy "Sylow"; (* Sylow's theorem *) 6.6 use_thy "Bij"; (* Automorphism Groups *) 6.7 +use_thy "Lattice"; (* Lattices, and the complete lattice of subgroups *) 6.8 6.9 (* Rings *) 6.10

7.1 --- a/src/HOL/Algebra/document/root.tex Tue Apr 13 07:48:32 2004 +0200 7.2 +++ b/src/HOL/Algebra/document/root.tex Tue Apr 13 09:42:40 2004 +0200 7.3 @@ -22,7 +22,7 @@ 7.4 % \<twosuperior>, \<onehalf>, 7.5 % \<threesuperior>, \<threequarters> 7.6 % \<degree> 7.7 -%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter> 7.8 +\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter> 7.9 %\usepackage{wasysym} 7.10 %\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz> 7.11 %\usepackage{textcomp} % for \<zero> ... \<nine>, \<cent>

8.1 --- a/src/HOL/IsaMakefile Tue Apr 13 07:48:32 2004 +0200 8.2 +++ b/src/HOL/IsaMakefile Tue Apr 13 09:42:40 2004 +0200 8.3 @@ -341,6 +341,7 @@ 8.4 Algebra/Exponent.thy \ 8.5 Algebra/FiniteProduct.thy \ 8.6 Algebra/Group.thy \ 8.7 + Algebra/Lattice.thy \ 8.8 Algebra/Module.thy \ 8.9 Algebra/Sylow.thy \ 8.10 Algebra/UnivPoly.thy \

9.1 --- a/src/HOL/Set.thy Tue Apr 13 07:48:32 2004 +0200 9.2 +++ b/src/HOL/Set.thy Tue Apr 13 09:42:40 2004 +0200 9.3 @@ -943,6 +943,10 @@ 9.4 lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B" 9.5 by blast 9.6 9.7 +lemma Inter_subset: 9.8 + "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B" 9.9 + by blast 9.10 + 9.11 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A" 9.12 by (rules intro: InterI subsetI dest: subsetD) 9.13