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