Various changes to HOL-Algebra;
authorballarin
Tue Apr 13 09:42:40 2004 +0200 (2004-04-13)
changeset 145512cb6ff394bfb
parent 14550 b13da5649bf9
child 14552 e88f52b775a5
Various changes to HOL-Algebra;
Locale instantiation.
NEWS
src/FOL/ex/LocaleInst.thy
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/ROOT.ML
src/HOL/Algebra/document/root.tex
src/HOL/IsaMakefile
src/HOL/Set.thy
     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