src/HOL/Algebra/Lattice.thy
 author wenzelm Thu Apr 22 11:01:34 2004 +0200 (2004-04-22) changeset 14651 02b8f3bcf7fe parent 14577 dbb95b825244 child 14666 65f8680c3f16 permissions -rw-r--r--
improved notation;
 ballarin@14551 ` 1` ```(* ``` ballarin@14551 ` 2` ``` Title: Orders and Lattices ``` ballarin@14551 ` 3` ``` Id: \$Id\$ ``` ballarin@14551 ` 4` ``` Author: Clemens Ballarin, started 7 November 2003 ``` ballarin@14551 ` 5` ``` Copyright: Clemens Ballarin ``` ballarin@14551 ` 6` ```*) ``` ballarin@14551 ` 7` wenzelm@14577 ` 8` ```header {* Order and Lattices *} ``` ballarin@14551 ` 9` wenzelm@14577 ` 10` ```theory Lattice = Group: ``` ballarin@14551 ` 11` ballarin@14551 ` 12` ```subsection {* Partial Orders *} ``` ballarin@14551 ` 13` ballarin@14551 ` 14` ```record 'a order = "'a partial_object" + ``` ballarin@14551 ` 15` ``` le :: "['a, 'a] => bool" (infixl "\\" 50) ``` ballarin@14551 ` 16` ballarin@14551 ` 17` ```locale order_syntax = struct L ``` ballarin@14551 ` 18` ballarin@14551 ` 19` ```locale partial_order = order_syntax + ``` ballarin@14551 ` 20` ``` assumes refl [intro, simp]: ``` ballarin@14551 ` 21` ``` "x \ carrier L ==> x \ x" ``` ballarin@14551 ` 22` ``` and anti_sym [intro]: ``` ballarin@14551 ` 23` ``` "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x = y" ``` ballarin@14551 ` 24` ``` and trans [trans]: ``` ballarin@14551 ` 25` ``` "[| x \ y; y \ z; ``` ballarin@14551 ` 26` ``` x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z" ``` ballarin@14551 ` 27` wenzelm@14651 ` 28` ```constdefs (structure L) ``` wenzelm@14651 ` 29` ``` less :: "[_, 'a, 'a] => bool" (infixl "\\" 50) ``` wenzelm@14651 ` 30` ``` "x \ y == x \ y & x ~= y" ``` ballarin@14551 ` 31` wenzelm@14651 ` 32` ``` -- {* Upper and lower bounds of a set. *} ``` wenzelm@14651 ` 33` ``` Upper :: "[_, 'a set] => 'a set" ``` ballarin@14551 ` 34` ``` "Upper L A == {u. (ALL x. x \ A \ carrier L --> le L x u)} \ ``` ballarin@14551 ` 35` ``` carrier L" ``` ballarin@14551 ` 36` wenzelm@14651 ` 37` ``` Lower :: "[_, 'a set] => 'a set" ``` ballarin@14551 ` 38` ``` "Lower L A == {l. (ALL x. x \ A \ carrier L --> le L l x)} \ ``` ballarin@14551 ` 39` ``` carrier L" ``` ballarin@14551 ` 40` wenzelm@14651 ` 41` ``` -- {* Least and greatest, as predicate. *} ``` wenzelm@14651 ` 42` ``` least :: "[_, 'a, 'a set] => bool" ``` ballarin@14551 ` 43` ``` "least L l A == A \ carrier L & l \ A & (ALL x : A. le L l x)" ``` ballarin@14551 ` 44` wenzelm@14651 ` 45` ``` greatest :: "[_, 'a, 'a set] => bool" ``` ballarin@14551 ` 46` ``` "greatest L g A == A \ carrier L & g \ A & (ALL x : A. le L x g)" ``` ballarin@14551 ` 47` wenzelm@14651 ` 48` ``` -- {* Supremum and infimum *} ``` wenzelm@14651 ` 49` ``` sup :: "[_, 'a set] => 'a" ("\\_" [90] 90) ``` wenzelm@14651 ` 50` ``` "\A == THE x. least L x (Upper L A)" ``` ballarin@14551 ` 51` wenzelm@14651 ` 52` ``` inf :: "[_, 'a set] => 'a" ("\\_" [90] 90) ``` wenzelm@14651 ` 53` ``` "\A == THE x. greatest L x (Lower L A)" ``` ballarin@14551 ` 54` wenzelm@14651 ` 55` ``` join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65) ``` wenzelm@14651 ` 56` ``` "x \ y == sup L {x, y}" ``` ballarin@14551 ` 57` wenzelm@14651 ` 58` ``` meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 65) ``` wenzelm@14651 ` 59` ``` "x \ y == inf L {x, y}" ``` ballarin@14551 ` 60` wenzelm@14651 ` 61` wenzelm@14651 ` 62` ```subsubsection {* Upper *} ``` ballarin@14551 ` 63` ballarin@14551 ` 64` ```lemma Upper_closed [intro, simp]: ``` ballarin@14551 ` 65` ``` "Upper L A \ carrier L" ``` ballarin@14551 ` 66` ``` by (unfold Upper_def) clarify ``` ballarin@14551 ` 67` ballarin@14551 ` 68` ```lemma UpperD [dest]: ``` ballarin@14551 ` 69` ``` includes order_syntax ``` ballarin@14551 ` 70` ``` shows "[| u \ Upper L A; x \ A; A \ carrier L |] ==> x \ u" ``` ballarin@14551 ` 71` ``` by (unfold Upper_def) blast ``` ballarin@14551 ` 72` ballarin@14551 ` 73` ```lemma Upper_memI: ``` ballarin@14551 ` 74` ``` includes order_syntax ``` ballarin@14551 ` 75` ``` shows "[| !! y. y \ A ==> y \ x; x \ carrier L |] ==> x \ Upper L A" ``` ballarin@14551 ` 76` ``` by (unfold Upper_def) blast ``` ballarin@14551 ` 77` ballarin@14551 ` 78` ```lemma Upper_antimono: ``` ballarin@14551 ` 79` ``` "A \ B ==> Upper L B \ Upper L A" ``` ballarin@14551 ` 80` ``` by (unfold Upper_def) blast ``` ballarin@14551 ` 81` wenzelm@14651 ` 82` wenzelm@14651 ` 83` ```subsubsection {* Lower *} ``` ballarin@14551 ` 84` ballarin@14551 ` 85` ```lemma Lower_closed [intro, simp]: ``` ballarin@14551 ` 86` ``` "Lower L A \ carrier L" ``` ballarin@14551 ` 87` ``` by (unfold Lower_def) clarify ``` ballarin@14551 ` 88` ballarin@14551 ` 89` ```lemma LowerD [dest]: ``` ballarin@14551 ` 90` ``` includes order_syntax ``` ballarin@14551 ` 91` ``` shows "[| l \ Lower L A; x \ A; A \ carrier L |] ==> l \ x" ``` ballarin@14551 ` 92` ``` by (unfold Lower_def) blast ``` ballarin@14551 ` 93` ballarin@14551 ` 94` ```lemma Lower_memI: ``` ballarin@14551 ` 95` ``` includes order_syntax ``` ballarin@14551 ` 96` ``` shows "[| !! y. y \ A ==> x \ y; x \ carrier L |] ==> x \ Lower L A" ``` ballarin@14551 ` 97` ``` by (unfold Lower_def) blast ``` ballarin@14551 ` 98` ballarin@14551 ` 99` ```lemma Lower_antimono: ``` ballarin@14551 ` 100` ``` "A \ B ==> Lower L B \ Lower L A" ``` ballarin@14551 ` 101` ``` by (unfold Lower_def) blast ``` ballarin@14551 ` 102` wenzelm@14651 ` 103` wenzelm@14651 ` 104` ```subsubsection {* least *} ``` ballarin@14551 ` 105` ballarin@14551 ` 106` ```lemma least_carrier [intro, simp]: ``` ballarin@14551 ` 107` ``` shows "least L l A ==> l \ carrier L" ``` ballarin@14551 ` 108` ``` by (unfold least_def) fast ``` ballarin@14551 ` 109` ballarin@14551 ` 110` ```lemma least_mem: ``` ballarin@14551 ` 111` ``` "least L l A ==> l \ A" ``` ballarin@14551 ` 112` ``` by (unfold least_def) fast ``` ballarin@14551 ` 113` ballarin@14551 ` 114` ```lemma (in partial_order) least_unique: ``` ballarin@14551 ` 115` ``` "[| least L x A; least L y A |] ==> x = y" ``` ballarin@14551 ` 116` ``` by (unfold least_def) blast ``` ballarin@14551 ` 117` ballarin@14551 ` 118` ```lemma least_le: ``` ballarin@14551 ` 119` ``` includes order_syntax ``` ballarin@14551 ` 120` ``` shows "[| least L x A; a \ A |] ==> x \ a" ``` ballarin@14551 ` 121` ``` by (unfold least_def) fast ``` ballarin@14551 ` 122` ballarin@14551 ` 123` ```lemma least_UpperI: ``` ballarin@14551 ` 124` ``` includes order_syntax ``` ballarin@14551 ` 125` ``` assumes above: "!! x. x \ A ==> x \ s" ``` ballarin@14551 ` 126` ``` and below: "!! y. y \ Upper L A ==> s \ y" ``` ballarin@14551 ` 127` ``` and L: "A \ carrier L" "s \ carrier L" ``` ballarin@14551 ` 128` ``` shows "least L s (Upper L A)" ``` ballarin@14551 ` 129` ```proof (unfold least_def, intro conjI) ``` ballarin@14551 ` 130` ``` show "Upper L A \ carrier L" by simp ``` ballarin@14551 ` 131` ```next ``` ballarin@14551 ` 132` ``` from above L show "s \ Upper L A" by (simp add: Upper_def) ``` ballarin@14551 ` 133` ```next ``` ballarin@14551 ` 134` ``` from below show "ALL x : Upper L A. s \ x" by fast ``` ballarin@14551 ` 135` ```qed ``` ballarin@14551 ` 136` wenzelm@14651 ` 137` wenzelm@14651 ` 138` ```subsubsection {* greatest *} ``` ballarin@14551 ` 139` ballarin@14551 ` 140` ```lemma greatest_carrier [intro, simp]: ``` ballarin@14551 ` 141` ``` shows "greatest L l A ==> l \ carrier L" ``` ballarin@14551 ` 142` ``` by (unfold greatest_def) fast ``` ballarin@14551 ` 143` ballarin@14551 ` 144` ```lemma greatest_mem: ``` ballarin@14551 ` 145` ``` "greatest L l A ==> l \ A" ``` ballarin@14551 ` 146` ``` by (unfold greatest_def) fast ``` ballarin@14551 ` 147` ballarin@14551 ` 148` ```lemma (in partial_order) greatest_unique: ``` ballarin@14551 ` 149` ``` "[| greatest L x A; greatest L y A |] ==> x = y" ``` ballarin@14551 ` 150` ``` by (unfold greatest_def) blast ``` ballarin@14551 ` 151` ballarin@14551 ` 152` ```lemma greatest_le: ``` ballarin@14551 ` 153` ``` includes order_syntax ``` ballarin@14551 ` 154` ``` shows "[| greatest L x A; a \ A |] ==> a \ x" ``` ballarin@14551 ` 155` ``` by (unfold greatest_def) fast ``` ballarin@14551 ` 156` ballarin@14551 ` 157` ```lemma greatest_LowerI: ``` ballarin@14551 ` 158` ``` includes order_syntax ``` ballarin@14551 ` 159` ``` assumes below: "!! x. x \ A ==> i \ x" ``` ballarin@14551 ` 160` ``` and above: "!! y. y \ Lower L A ==> y \ i" ``` ballarin@14551 ` 161` ``` and L: "A \ carrier L" "i \ carrier L" ``` ballarin@14551 ` 162` ``` shows "greatest L i (Lower L A)" ``` ballarin@14551 ` 163` ```proof (unfold greatest_def, intro conjI) ``` ballarin@14551 ` 164` ``` show "Lower L A \ carrier L" by simp ``` ballarin@14551 ` 165` ```next ``` ballarin@14551 ` 166` ``` from below L show "i \ Lower L A" by (simp add: Lower_def) ``` ballarin@14551 ` 167` ```next ``` ballarin@14551 ` 168` ``` from above show "ALL x : Lower L A. x \ i" by fast ``` ballarin@14551 ` 169` ```qed ``` ballarin@14551 ` 170` ballarin@14551 ` 171` ```subsection {* Lattices *} ``` ballarin@14551 ` 172` ballarin@14551 ` 173` ```locale lattice = partial_order + ``` ballarin@14551 ` 174` ``` assumes sup_of_two_exists: ``` ballarin@14551 ` 175` ``` "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})" ``` ballarin@14551 ` 176` ``` and inf_of_two_exists: ``` ballarin@14551 ` 177` ``` "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})" ``` ballarin@14551 ` 178` ballarin@14551 ` 179` ```lemma least_Upper_above: ``` ballarin@14551 ` 180` ``` includes order_syntax ``` ballarin@14551 ` 181` ``` shows "[| least L s (Upper L A); x \ A; A \ carrier L |] ==> x \ s" ``` ballarin@14551 ` 182` ``` by (unfold least_def) blast ``` ballarin@14551 ` 183` ballarin@14551 ` 184` ```lemma greatest_Lower_above: ``` ballarin@14551 ` 185` ``` includes order_syntax ``` ballarin@14551 ` 186` ``` shows "[| greatest L i (Lower L A); x \ A; A \ carrier L |] ==> i \ x" ``` ballarin@14551 ` 187` ``` by (unfold greatest_def) blast ``` ballarin@14551 ` 188` ballarin@14551 ` 189` ```subsubsection {* Supremum *} ``` ballarin@14551 ` 190` ballarin@14551 ` 191` ```lemma (in lattice) joinI: ``` ballarin@14551 ` 192` ``` "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |] ``` ballarin@14551 ` 193` ``` ==> P (x \ y)" ``` ballarin@14551 ` 194` ```proof (unfold join_def sup_def) ``` ballarin@14551 ` 195` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 196` ``` and P: "!!l. least L l (Upper L {x, y}) ==> P l" ``` ballarin@14551 ` 197` ``` with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast ``` ballarin@14551 ` 198` ``` with L show "P (THE l. least L l (Upper L {x, y}))" ``` ballarin@14551 ` 199` ``` by (fast intro: theI2 least_unique P) ``` ballarin@14551 ` 200` ```qed ``` ballarin@14551 ` 201` ballarin@14551 ` 202` ```lemma (in lattice) join_closed [simp]: ``` ballarin@14551 ` 203` ``` "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L" ``` ballarin@14551 ` 204` ``` by (rule joinI) (rule least_carrier) ``` ballarin@14551 ` 205` wenzelm@14651 ` 206` ```lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) ``` ballarin@14551 ` 207` ``` "x \ carrier L ==> least L x (Upper L {x})" ``` ballarin@14551 ` 208` ``` by (rule least_UpperI) fast+ ``` ballarin@14551 ` 209` ballarin@14551 ` 210` ```lemma (in partial_order) sup_of_singleton [simp]: ``` ballarin@14551 ` 211` ``` includes order_syntax ``` ballarin@14551 ` 212` ``` shows "x \ carrier L ==> \ {x} = x" ``` ballarin@14551 ` 213` ``` by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) ``` ballarin@14551 ` 214` ballarin@14551 ` 215` ```text {* Condition on A: supremum exists. *} ``` ballarin@14551 ` 216` ballarin@14551 ` 217` ```lemma (in lattice) sup_insertI: ``` ballarin@14551 ` 218` ``` "[| !!s. least L s (Upper L (insert x A)) ==> P s; ``` ballarin@14551 ` 219` ``` least L a (Upper L A); x \ carrier L; A \ carrier L |] ``` ballarin@14551 ` 220` ``` ==> P (\ (insert x A))" ``` ballarin@14551 ` 221` ```proof (unfold sup_def) ``` ballarin@14551 ` 222` ``` assume L: "x \ carrier L" "A \ carrier L" ``` ballarin@14551 ` 223` ``` and P: "!!l. least L l (Upper L (insert x A)) ==> P l" ``` ballarin@14551 ` 224` ``` and least_a: "least L a (Upper L A)" ``` ballarin@14551 ` 225` ``` from L least_a have La: "a \ carrier L" by simp ``` ballarin@14551 ` 226` ``` from L sup_of_two_exists least_a ``` ballarin@14551 ` 227` ``` obtain s where least_s: "least L s (Upper L {a, x})" by blast ``` ballarin@14551 ` 228` ``` show "P (THE l. least L l (Upper L (insert x A)))" ``` ballarin@14551 ` 229` ``` proof (rule theI2 [where a = s]) ``` ballarin@14551 ` 230` ``` show "least L s (Upper L (insert x A))" ``` ballarin@14551 ` 231` ``` proof (rule least_UpperI) ``` ballarin@14551 ` 232` ``` fix z ``` ballarin@14551 ` 233` ``` assume xA: "z \ insert x A" ``` ballarin@14551 ` 234` ``` show "z \ s" ``` ballarin@14551 ` 235` ``` proof - ``` ballarin@14551 ` 236` ``` { ``` ballarin@14551 ` 237` ``` assume "z = x" then have ?thesis ``` ballarin@14551 ` 238` ``` by (simp add: least_Upper_above [OF least_s] L La) ``` ballarin@14551 ` 239` ``` } ``` ballarin@14551 ` 240` ``` moreover ``` ballarin@14551 ` 241` ``` { ``` ballarin@14551 ` 242` ``` assume "z \ A" ``` ballarin@14551 ` 243` ``` with L least_s least_a have ?thesis ``` ballarin@14551 ` 244` ``` by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) ``` ballarin@14551 ` 245` ``` } ``` ballarin@14551 ` 246` ``` moreover note xA ``` ballarin@14551 ` 247` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 248` ``` qed ``` ballarin@14551 ` 249` ``` next ``` ballarin@14551 ` 250` ``` fix y ``` ballarin@14551 ` 251` ``` assume y: "y \ Upper L (insert x A)" ``` ballarin@14551 ` 252` ``` show "s \ y" ``` ballarin@14551 ` 253` ``` proof (rule least_le [OF least_s], rule Upper_memI) ``` ballarin@14551 ` 254` ``` fix z ``` ballarin@14551 ` 255` ``` assume z: "z \ {a, x}" ``` ballarin@14551 ` 256` ``` show "z \ y" ``` ballarin@14551 ` 257` ``` proof - ``` ballarin@14551 ` 258` ``` { ``` ballarin@14551 ` 259` ``` have y': "y \ Upper L A" ``` ballarin@14551 ` 260` ``` apply (rule subsetD [where A = "Upper L (insert x A)"]) ``` ballarin@14551 ` 261` ``` apply (rule Upper_antimono) apply clarify apply assumption ``` ballarin@14551 ` 262` ``` done ``` ballarin@14551 ` 263` ``` assume "z = a" ``` ballarin@14551 ` 264` ``` with y' least_a have ?thesis by (fast dest: least_le) ``` ballarin@14551 ` 265` ``` } ``` ballarin@14551 ` 266` ``` moreover ``` ballarin@14551 ` 267` ``` { ``` ballarin@14551 ` 268` ``` assume "z = x" ``` ballarin@14551 ` 269` ``` with y L have ?thesis by blast ``` ballarin@14551 ` 270` ``` } ``` ballarin@14551 ` 271` ``` moreover note z ``` ballarin@14551 ` 272` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 273` ``` qed ``` ballarin@14551 ` 274` ``` qed (rule Upper_closed [THEN subsetD]) ``` ballarin@14551 ` 275` ``` next ``` ballarin@14551 ` 276` ``` from L show "insert x A \ carrier L" by simp ``` ballarin@14551 ` 277` ``` next ``` ballarin@14551 ` 278` ``` from least_s show "s \ carrier L" by simp ``` ballarin@14551 ` 279` ``` qed ``` ballarin@14551 ` 280` ```next ``` ballarin@14551 ` 281` ``` fix l ``` ballarin@14551 ` 282` ``` assume least_l: "least L l (Upper L (insert x A))" ``` ballarin@14551 ` 283` ``` show "l = s" ``` ballarin@14551 ` 284` ``` proof (rule least_unique) ``` ballarin@14551 ` 285` ``` show "least L s (Upper L (insert x A))" ``` ballarin@14551 ` 286` ``` proof (rule least_UpperI) ``` ballarin@14551 ` 287` ``` fix z ``` ballarin@14551 ` 288` ``` assume xA: "z \ insert x A" ``` ballarin@14551 ` 289` ``` show "z \ s" ``` ballarin@14551 ` 290` ``` proof - ``` ballarin@14551 ` 291` ``` { ``` ballarin@14551 ` 292` ``` assume "z = x" then have ?thesis ``` ballarin@14551 ` 293` ``` by (simp add: least_Upper_above [OF least_s] L La) ``` ballarin@14551 ` 294` ``` } ``` ballarin@14551 ` 295` ``` moreover ``` ballarin@14551 ` 296` ``` { ``` ballarin@14551 ` 297` ``` assume "z \ A" ``` ballarin@14551 ` 298` ``` with L least_s least_a have ?thesis ``` ballarin@14551 ` 299` ``` by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) ``` ballarin@14551 ` 300` ``` } ``` ballarin@14551 ` 301` ``` moreover note xA ``` ballarin@14551 ` 302` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 303` ``` qed ``` ballarin@14551 ` 304` ``` next ``` ballarin@14551 ` 305` ``` fix y ``` ballarin@14551 ` 306` ``` assume y: "y \ Upper L (insert x A)" ``` ballarin@14551 ` 307` ``` show "s \ y" ``` ballarin@14551 ` 308` ``` proof (rule least_le [OF least_s], rule Upper_memI) ``` ballarin@14551 ` 309` ``` fix z ``` ballarin@14551 ` 310` ``` assume z: "z \ {a, x}" ``` ballarin@14551 ` 311` ``` show "z \ y" ``` ballarin@14551 ` 312` ``` proof - ``` ballarin@14551 ` 313` ``` { ``` ballarin@14551 ` 314` ``` have y': "y \ Upper L A" ``` ballarin@14551 ` 315` ``` apply (rule subsetD [where A = "Upper L (insert x A)"]) ``` ballarin@14551 ` 316` ``` apply (rule Upper_antimono) apply clarify apply assumption ``` ballarin@14551 ` 317` ``` done ``` ballarin@14551 ` 318` ``` assume "z = a" ``` ballarin@14551 ` 319` ``` with y' least_a have ?thesis by (fast dest: least_le) ``` ballarin@14551 ` 320` ``` } ``` ballarin@14551 ` 321` ``` moreover ``` ballarin@14551 ` 322` ``` { ``` ballarin@14551 ` 323` ``` assume "z = x" ``` ballarin@14551 ` 324` ``` with y L have ?thesis by blast ``` ballarin@14551 ` 325` ``` } ``` ballarin@14551 ` 326` ``` moreover note z ``` ballarin@14551 ` 327` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 328` ``` qed ``` ballarin@14551 ` 329` ``` qed (rule Upper_closed [THEN subsetD]) ``` ballarin@14551 ` 330` ``` next ``` ballarin@14551 ` 331` ``` from L show "insert x A \ carrier L" by simp ``` ballarin@14551 ` 332` ``` next ``` ballarin@14551 ` 333` ``` from least_s show "s \ carrier L" by simp ``` ballarin@14551 ` 334` ``` qed ``` ballarin@14551 ` 335` ``` qed ``` ballarin@14551 ` 336` ``` qed ``` ballarin@14551 ` 337` ```qed ``` ballarin@14551 ` 338` ballarin@14551 ` 339` ```lemma (in lattice) finite_sup_least: ``` ballarin@14551 ` 340` ``` "[| finite A; A \ carrier L; A ~= {} |] ==> least L (\ A) (Upper L A)" ``` ballarin@14551 ` 341` ```proof (induct set: Finites) ``` ballarin@14551 ` 342` ``` case empty then show ?case by simp ``` ballarin@14551 ` 343` ```next ``` ballarin@14551 ` 344` ``` case (insert A x) ``` ballarin@14551 ` 345` ``` show ?case ``` ballarin@14551 ` 346` ``` proof (cases "A = {}") ``` ballarin@14551 ` 347` ``` case True ``` ballarin@14551 ` 348` ``` with insert show ?thesis by (simp add: sup_of_singletonI) ``` ballarin@14551 ` 349` ``` next ``` ballarin@14551 ` 350` ``` case False ``` ballarin@14551 ` 351` ``` from insert show ?thesis ``` ballarin@14551 ` 352` ``` proof (rule_tac sup_insertI) ``` ballarin@14551 ` 353` ``` from False insert show "least L (\ A) (Upper L A)" by simp ``` ballarin@14551 ` 354` ``` qed simp_all ``` ballarin@14551 ` 355` ``` qed ``` ballarin@14551 ` 356` ```qed ``` ballarin@14551 ` 357` ballarin@14551 ` 358` ```lemma (in lattice) finite_sup_insertI: ``` ballarin@14551 ` 359` ``` assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" ``` ballarin@14551 ` 360` ``` and xA: "finite A" "x \ carrier L" "A \ carrier L" ``` ballarin@14551 ` 361` ``` shows "P (\ (insert x A))" ``` ballarin@14551 ` 362` ```proof (cases "A = {}") ``` ballarin@14551 ` 363` ``` case True with P and xA show ?thesis ``` ballarin@14551 ` 364` ``` by (simp add: sup_of_singletonI) ``` ballarin@14551 ` 365` ```next ``` ballarin@14551 ` 366` ``` case False with P and xA show ?thesis ``` ballarin@14551 ` 367` ``` by (simp add: sup_insertI finite_sup_least) ``` ballarin@14551 ` 368` ```qed ``` ballarin@14551 ` 369` ballarin@14551 ` 370` ```lemma (in lattice) finite_sup_closed: ``` ballarin@14551 ` 371` ``` "[| finite A; A \ carrier L; A ~= {} |] ==> \ A \ carrier L" ``` ballarin@14551 ` 372` ```proof (induct set: Finites) ``` ballarin@14551 ` 373` ``` case empty then show ?case by simp ``` ballarin@14551 ` 374` ```next ``` ballarin@14551 ` 375` ``` case (insert A x) then show ?case ``` ballarin@14551 ` 376` ``` by (rule_tac finite_sup_insertI) (simp_all) ``` ballarin@14551 ` 377` ```qed ``` ballarin@14551 ` 378` ballarin@14551 ` 379` ```lemma (in lattice) join_left: ``` ballarin@14551 ` 380` ``` "[| x \ carrier L; y \ carrier L |] ==> x \ x \ y" ``` ballarin@14551 ` 381` ``` by (rule joinI [folded join_def]) (blast dest: least_mem ) ``` ballarin@14551 ` 382` ballarin@14551 ` 383` ```lemma (in lattice) join_right: ``` ballarin@14551 ` 384` ``` "[| x \ carrier L; y \ carrier L |] ==> y \ x \ y" ``` ballarin@14551 ` 385` ``` by (rule joinI [folded join_def]) (blast dest: least_mem ) ``` ballarin@14551 ` 386` ballarin@14551 ` 387` ```lemma (in lattice) sup_of_two_least: ``` ballarin@14551 ` 388` ``` "[| x \ carrier L; y \ carrier L |] ==> least L (\ {x, y}) (Upper L {x, y})" ``` ballarin@14551 ` 389` ```proof (unfold sup_def) ``` ballarin@14551 ` 390` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 391` ``` with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast ``` ballarin@14551 ` 392` ``` with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" ``` ballarin@14551 ` 393` ``` by (fast intro: theI2 least_unique) (* blast fails *) ``` ballarin@14551 ` 394` ```qed ``` ballarin@14551 ` 395` ballarin@14551 ` 396` ```lemma (in lattice) join_le: ``` ballarin@14551 ` 397` ``` assumes sub: "x \ z" "y \ z" ``` ballarin@14551 ` 398` ``` and L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 399` ``` shows "x \ y \ z" ``` ballarin@14551 ` 400` ```proof (rule joinI) ``` ballarin@14551 ` 401` ``` fix s ``` ballarin@14551 ` 402` ``` assume "least L s (Upper L {x, y})" ``` ballarin@14551 ` 403` ``` with sub L show "s \ z" by (fast elim: least_le intro: Upper_memI) ``` ballarin@14551 ` 404` ```qed ``` ballarin@14551 ` 405` ``` ``` ballarin@14551 ` 406` ```lemma (in lattice) join_assoc_lemma: ``` ballarin@14551 ` 407` ``` assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 408` ``` shows "x \ (y \ z) = \ {x, y, z}" ``` ballarin@14551 ` 409` ```proof (rule finite_sup_insertI) ``` wenzelm@14651 ` 410` ``` -- {* The textbook argument in Jacobson I, p 457 *} ``` ballarin@14551 ` 411` ``` fix s ``` ballarin@14551 ` 412` ``` assume sup: "least L s (Upper L {x, y, z})" ``` ballarin@14551 ` 413` ``` show "x \ (y \ z) = s" ``` ballarin@14551 ` 414` ``` proof (rule anti_sym) ``` ballarin@14551 ` 415` ``` from sup L show "x \ (y \ z) \ s" ``` ballarin@14551 ` 416` ``` by (fastsimp intro!: join_le elim: least_Upper_above) ``` ballarin@14551 ` 417` ``` next ``` ballarin@14551 ` 418` ``` from sup L show "s \ x \ (y \ z)" ``` ballarin@14551 ` 419` ``` by (erule_tac least_le) ``` ballarin@14551 ` 420` ``` (blast intro!: Upper_memI intro: trans join_left join_right join_closed) ``` ballarin@14551 ` 421` ``` qed (simp_all add: L least_carrier [OF sup]) ``` ballarin@14551 ` 422` ```qed (simp_all add: L) ``` ballarin@14551 ` 423` ballarin@14551 ` 424` ```lemma join_comm: ``` ballarin@14551 ` 425` ``` includes order_syntax ``` ballarin@14551 ` 426` ``` shows "x \ y = y \ x" ``` ballarin@14551 ` 427` ``` by (unfold join_def) (simp add: insert_commute) ``` ballarin@14551 ` 428` ballarin@14551 ` 429` ```lemma (in lattice) join_assoc: ``` ballarin@14551 ` 430` ``` assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 431` ``` shows "(x \ y) \ z = x \ (y \ z)" ``` ballarin@14551 ` 432` ```proof - ``` ballarin@14551 ` 433` ``` have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm) ``` ballarin@14551 ` 434` ``` also from L have "... = \ {z, x, y}" by (simp add: join_assoc_lemma) ``` ballarin@14551 ` 435` ``` also from L have "... = \ {x, y, z}" by (simp add: insert_commute) ``` ballarin@14551 ` 436` ``` also from L have "... = x \ (y \ z)" by (simp add: join_assoc_lemma) ``` ballarin@14551 ` 437` ``` finally show ?thesis . ``` ballarin@14551 ` 438` ```qed ``` ballarin@14551 ` 439` ballarin@14551 ` 440` ```subsubsection {* Infimum *} ``` ballarin@14551 ` 441` ballarin@14551 ` 442` ```lemma (in lattice) meetI: ``` ballarin@14551 ` 443` ``` "[| !!i. greatest L i (Lower L {x, y}) ==> P i; ``` ballarin@14551 ` 444` ``` x \ carrier L; y \ carrier L |] ``` ballarin@14551 ` 445` ``` ==> P (x \ y)" ``` ballarin@14551 ` 446` ```proof (unfold meet_def inf_def) ``` ballarin@14551 ` 447` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 448` ``` and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" ``` ballarin@14551 ` 449` ``` with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast ``` ballarin@14551 ` 450` ``` with L show "P (THE g. greatest L g (Lower L {x, y}))" ``` ballarin@14551 ` 451` ``` by (fast intro: theI2 greatest_unique P) ``` ballarin@14551 ` 452` ```qed ``` ballarin@14551 ` 453` ballarin@14551 ` 454` ```lemma (in lattice) meet_closed [simp]: ``` ballarin@14551 ` 455` ``` "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L" ``` ballarin@14551 ` 456` ``` by (rule meetI) (rule greatest_carrier) ``` ballarin@14551 ` 457` wenzelm@14651 ` 458` ```lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) ``` ballarin@14551 ` 459` ``` "x \ carrier L ==> greatest L x (Lower L {x})" ``` ballarin@14551 ` 460` ``` by (rule greatest_LowerI) fast+ ``` ballarin@14551 ` 461` ballarin@14551 ` 462` ```lemma (in partial_order) inf_of_singleton [simp]: ``` ballarin@14551 ` 463` ``` includes order_syntax ``` ballarin@14551 ` 464` ``` shows "x \ carrier L ==> \ {x} = x" ``` ballarin@14551 ` 465` ``` by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) ``` ballarin@14551 ` 466` ballarin@14551 ` 467` ```text {* Condition on A: infimum exists. *} ``` ballarin@14551 ` 468` ballarin@14551 ` 469` ```lemma (in lattice) inf_insertI: ``` ballarin@14551 ` 470` ``` "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; ``` ballarin@14551 ` 471` ``` greatest L a (Lower L A); x \ carrier L; A \ carrier L |] ``` ballarin@14551 ` 472` ``` ==> P (\ (insert x A))" ``` ballarin@14551 ` 473` ```proof (unfold inf_def) ``` ballarin@14551 ` 474` ``` assume L: "x \ carrier L" "A \ carrier L" ``` ballarin@14551 ` 475` ``` and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" ``` ballarin@14551 ` 476` ``` and greatest_a: "greatest L a (Lower L A)" ``` ballarin@14551 ` 477` ``` from L greatest_a have La: "a \ carrier L" by simp ``` ballarin@14551 ` 478` ``` from L inf_of_two_exists greatest_a ``` ballarin@14551 ` 479` ``` obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast ``` ballarin@14551 ` 480` ``` show "P (THE g. greatest L g (Lower L (insert x A)))" ``` ballarin@14551 ` 481` ``` proof (rule theI2 [where a = i]) ``` ballarin@14551 ` 482` ``` show "greatest L i (Lower L (insert x A))" ``` ballarin@14551 ` 483` ``` proof (rule greatest_LowerI) ``` ballarin@14551 ` 484` ``` fix z ``` ballarin@14551 ` 485` ``` assume xA: "z \ insert x A" ``` ballarin@14551 ` 486` ``` show "i \ z" ``` ballarin@14551 ` 487` ``` proof - ``` ballarin@14551 ` 488` ``` { ``` ballarin@14551 ` 489` ``` assume "z = x" then have ?thesis ``` ballarin@14551 ` 490` ``` by (simp add: greatest_Lower_above [OF greatest_i] L La) ``` ballarin@14551 ` 491` ``` } ``` ballarin@14551 ` 492` ``` moreover ``` ballarin@14551 ` 493` ``` { ``` ballarin@14551 ` 494` ``` assume "z \ A" ``` ballarin@14551 ` 495` ``` with L greatest_i greatest_a have ?thesis ``` ballarin@14551 ` 496` ``` by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) ``` ballarin@14551 ` 497` ``` } ``` ballarin@14551 ` 498` ``` moreover note xA ``` ballarin@14551 ` 499` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 500` ``` qed ``` ballarin@14551 ` 501` ``` next ``` ballarin@14551 ` 502` ``` fix y ``` ballarin@14551 ` 503` ``` assume y: "y \ Lower L (insert x A)" ``` ballarin@14551 ` 504` ``` show "y \ i" ``` ballarin@14551 ` 505` ``` proof (rule greatest_le [OF greatest_i], rule Lower_memI) ``` ballarin@14551 ` 506` ``` fix z ``` ballarin@14551 ` 507` ``` assume z: "z \ {a, x}" ``` ballarin@14551 ` 508` ``` show "y \ z" ``` ballarin@14551 ` 509` ``` proof - ``` ballarin@14551 ` 510` ``` { ``` ballarin@14551 ` 511` ``` have y': "y \ Lower L A" ``` ballarin@14551 ` 512` ``` apply (rule subsetD [where A = "Lower L (insert x A)"]) ``` ballarin@14551 ` 513` ``` apply (rule Lower_antimono) apply clarify apply assumption ``` ballarin@14551 ` 514` ``` done ``` ballarin@14551 ` 515` ``` assume "z = a" ``` ballarin@14551 ` 516` ``` with y' greatest_a have ?thesis by (fast dest: greatest_le) ``` ballarin@14551 ` 517` ``` } ``` ballarin@14551 ` 518` ``` moreover ``` ballarin@14551 ` 519` ``` { ``` ballarin@14551 ` 520` ``` assume "z = x" ``` ballarin@14551 ` 521` ``` with y L have ?thesis by blast ``` ballarin@14551 ` 522` ``` } ``` ballarin@14551 ` 523` ``` moreover note z ``` ballarin@14551 ` 524` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 525` ``` qed ``` ballarin@14551 ` 526` ``` qed (rule Lower_closed [THEN subsetD]) ``` ballarin@14551 ` 527` ``` next ``` ballarin@14551 ` 528` ``` from L show "insert x A \ carrier L" by simp ``` ballarin@14551 ` 529` ``` next ``` ballarin@14551 ` 530` ``` from greatest_i show "i \ carrier L" by simp ``` ballarin@14551 ` 531` ``` qed ``` ballarin@14551 ` 532` ```next ``` ballarin@14551 ` 533` ``` fix g ``` ballarin@14551 ` 534` ``` assume greatest_g: "greatest L g (Lower L (insert x A))" ``` ballarin@14551 ` 535` ``` show "g = i" ``` ballarin@14551 ` 536` ``` proof (rule greatest_unique) ``` ballarin@14551 ` 537` ``` show "greatest L i (Lower L (insert x A))" ``` ballarin@14551 ` 538` ``` proof (rule greatest_LowerI) ``` ballarin@14551 ` 539` ``` fix z ``` ballarin@14551 ` 540` ``` assume xA: "z \ insert x A" ``` ballarin@14551 ` 541` ``` show "i \ z" ``` ballarin@14551 ` 542` ``` proof - ``` ballarin@14551 ` 543` ``` { ``` ballarin@14551 ` 544` ``` assume "z = x" then have ?thesis ``` ballarin@14551 ` 545` ``` by (simp add: greatest_Lower_above [OF greatest_i] L La) ``` ballarin@14551 ` 546` ``` } ``` ballarin@14551 ` 547` ``` moreover ``` ballarin@14551 ` 548` ``` { ``` ballarin@14551 ` 549` ``` assume "z \ A" ``` ballarin@14551 ` 550` ``` with L greatest_i greatest_a have ?thesis ``` ballarin@14551 ` 551` ``` by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) ``` ballarin@14551 ` 552` ``` } ``` ballarin@14551 ` 553` ``` moreover note xA ``` ballarin@14551 ` 554` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 555` ``` qed ``` ballarin@14551 ` 556` ``` next ``` ballarin@14551 ` 557` ``` fix y ``` ballarin@14551 ` 558` ``` assume y: "y \ Lower L (insert x A)" ``` ballarin@14551 ` 559` ``` show "y \ i" ``` ballarin@14551 ` 560` ``` proof (rule greatest_le [OF greatest_i], rule Lower_memI) ``` ballarin@14551 ` 561` ``` fix z ``` ballarin@14551 ` 562` ``` assume z: "z \ {a, x}" ``` ballarin@14551 ` 563` ``` show "y \ z" ``` ballarin@14551 ` 564` ``` proof - ``` ballarin@14551 ` 565` ``` { ``` ballarin@14551 ` 566` ``` have y': "y \ Lower L A" ``` ballarin@14551 ` 567` ``` apply (rule subsetD [where A = "Lower L (insert x A)"]) ``` ballarin@14551 ` 568` ``` apply (rule Lower_antimono) apply clarify apply assumption ``` ballarin@14551 ` 569` ``` done ``` ballarin@14551 ` 570` ``` assume "z = a" ``` ballarin@14551 ` 571` ``` with y' greatest_a have ?thesis by (fast dest: greatest_le) ``` ballarin@14551 ` 572` ``` } ``` ballarin@14551 ` 573` ``` moreover ``` ballarin@14551 ` 574` ``` { ``` ballarin@14551 ` 575` ``` assume "z = x" ``` ballarin@14551 ` 576` ``` with y L have ?thesis by blast ``` ballarin@14551 ` 577` ``` } ``` ballarin@14551 ` 578` ``` moreover note z ``` ballarin@14551 ` 579` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 580` ``` qed ``` ballarin@14551 ` 581` ``` qed (rule Lower_closed [THEN subsetD]) ``` ballarin@14551 ` 582` ``` next ``` ballarin@14551 ` 583` ``` from L show "insert x A \ carrier L" by simp ``` ballarin@14551 ` 584` ``` next ``` ballarin@14551 ` 585` ``` from greatest_i show "i \ carrier L" by simp ``` ballarin@14551 ` 586` ``` qed ``` ballarin@14551 ` 587` ``` qed ``` ballarin@14551 ` 588` ``` qed ``` ballarin@14551 ` 589` ```qed ``` ballarin@14551 ` 590` ballarin@14551 ` 591` ```lemma (in lattice) finite_inf_greatest: ``` ballarin@14551 ` 592` ``` "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\ A) (Lower L A)" ``` ballarin@14551 ` 593` ```proof (induct set: Finites) ``` ballarin@14551 ` 594` ``` case empty then show ?case by simp ``` ballarin@14551 ` 595` ```next ``` ballarin@14551 ` 596` ``` case (insert A x) ``` ballarin@14551 ` 597` ``` show ?case ``` ballarin@14551 ` 598` ``` proof (cases "A = {}") ``` ballarin@14551 ` 599` ``` case True ``` ballarin@14551 ` 600` ``` with insert show ?thesis by (simp add: inf_of_singletonI) ``` ballarin@14551 ` 601` ``` next ``` ballarin@14551 ` 602` ``` case False ``` ballarin@14551 ` 603` ``` from insert show ?thesis ``` ballarin@14551 ` 604` ``` proof (rule_tac inf_insertI) ``` ballarin@14551 ` 605` ``` from False insert show "greatest L (\ A) (Lower L A)" by simp ``` ballarin@14551 ` 606` ``` qed simp_all ``` ballarin@14551 ` 607` ``` qed ``` ballarin@14551 ` 608` ```qed ``` ballarin@14551 ` 609` ballarin@14551 ` 610` ```lemma (in lattice) finite_inf_insertI: ``` ballarin@14551 ` 611` ``` assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" ``` ballarin@14551 ` 612` ``` and xA: "finite A" "x \ carrier L" "A \ carrier L" ``` ballarin@14551 ` 613` ``` shows "P (\ (insert x A))" ``` ballarin@14551 ` 614` ```proof (cases "A = {}") ``` ballarin@14551 ` 615` ``` case True with P and xA show ?thesis ``` ballarin@14551 ` 616` ``` by (simp add: inf_of_singletonI) ``` ballarin@14551 ` 617` ```next ``` ballarin@14551 ` 618` ``` case False with P and xA show ?thesis ``` ballarin@14551 ` 619` ``` by (simp add: inf_insertI finite_inf_greatest) ``` ballarin@14551 ` 620` ```qed ``` ballarin@14551 ` 621` ballarin@14551 ` 622` ```lemma (in lattice) finite_inf_closed: ``` ballarin@14551 ` 623` ``` "[| finite A; A \ carrier L; A ~= {} |] ==> \ A \ carrier L" ``` ballarin@14551 ` 624` ```proof (induct set: Finites) ``` ballarin@14551 ` 625` ``` case empty then show ?case by simp ``` ballarin@14551 ` 626` ```next ``` ballarin@14551 ` 627` ``` case (insert A x) then show ?case ``` ballarin@14551 ` 628` ``` by (rule_tac finite_inf_insertI) (simp_all) ``` ballarin@14551 ` 629` ```qed ``` ballarin@14551 ` 630` ballarin@14551 ` 631` ```lemma (in lattice) meet_left: ``` ballarin@14551 ` 632` ``` "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x" ``` ballarin@14551 ` 633` ``` by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) ``` ballarin@14551 ` 634` ballarin@14551 ` 635` ```lemma (in lattice) meet_right: ``` ballarin@14551 ` 636` ``` "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y" ``` ballarin@14551 ` 637` ``` by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) ``` ballarin@14551 ` 638` ballarin@14551 ` 639` ```lemma (in lattice) inf_of_two_greatest: ``` ballarin@14551 ` 640` ``` "[| x \ carrier L; y \ carrier L |] ==> ``` ballarin@14551 ` 641` ``` greatest L (\ {x, y}) (Lower L {x, y})" ``` ballarin@14551 ` 642` ```proof (unfold inf_def) ``` ballarin@14551 ` 643` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 644` ``` with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast ``` ballarin@14551 ` 645` ``` with L ``` ballarin@14551 ` 646` ``` show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" ``` ballarin@14551 ` 647` ``` by (fast intro: theI2 greatest_unique) (* blast fails *) ``` ballarin@14551 ` 648` ```qed ``` ballarin@14551 ` 649` ballarin@14551 ` 650` ```lemma (in lattice) meet_le: ``` ballarin@14551 ` 651` ``` assumes sub: "z \ x" "z \ y" ``` ballarin@14551 ` 652` ``` and L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 653` ``` shows "z \ x \ y" ``` ballarin@14551 ` 654` ```proof (rule meetI) ``` ballarin@14551 ` 655` ``` fix i ``` ballarin@14551 ` 656` ``` assume "greatest L i (Lower L {x, y})" ``` ballarin@14551 ` 657` ``` with sub L show "z \ i" by (fast elim: greatest_le intro: Lower_memI) ``` ballarin@14551 ` 658` ```qed ``` ballarin@14551 ` 659` ``` ``` ballarin@14551 ` 660` ```lemma (in lattice) meet_assoc_lemma: ``` ballarin@14551 ` 661` ``` assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 662` ``` shows "x \ (y \ z) = \ {x, y, z}" ``` ballarin@14551 ` 663` ```proof (rule finite_inf_insertI) ``` ballarin@14551 ` 664` ``` txt {* The textbook argument in Jacobson I, p 457 *} ``` ballarin@14551 ` 665` ``` fix i ``` ballarin@14551 ` 666` ``` assume inf: "greatest L i (Lower L {x, y, z})" ``` ballarin@14551 ` 667` ``` show "x \ (y \ z) = i" ``` ballarin@14551 ` 668` ``` proof (rule anti_sym) ``` ballarin@14551 ` 669` ``` from inf L show "i \ x \ (y \ z)" ``` ballarin@14551 ` 670` ``` by (fastsimp intro!: meet_le elim: greatest_Lower_above) ``` ballarin@14551 ` 671` ``` next ``` ballarin@14551 ` 672` ``` from inf L show "x \ (y \ z) \ i" ``` ballarin@14551 ` 673` ``` by (erule_tac greatest_le) ``` ballarin@14551 ` 674` ``` (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) ``` ballarin@14551 ` 675` ``` qed (simp_all add: L greatest_carrier [OF inf]) ``` ballarin@14551 ` 676` ```qed (simp_all add: L) ``` ballarin@14551 ` 677` ballarin@14551 ` 678` ```lemma meet_comm: ``` ballarin@14551 ` 679` ``` includes order_syntax ``` ballarin@14551 ` 680` ``` shows "x \ y = y \ x" ``` ballarin@14551 ` 681` ``` by (unfold meet_def) (simp add: insert_commute) ``` ballarin@14551 ` 682` ballarin@14551 ` 683` ```lemma (in lattice) meet_assoc: ``` ballarin@14551 ` 684` ``` assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ``` ballarin@14551 ` 685` ``` shows "(x \ y) \ z = x \ (y \ z)" ``` ballarin@14551 ` 686` ```proof - ``` ballarin@14551 ` 687` ``` have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm) ``` ballarin@14551 ` 688` ``` also from L have "... = \ {z, x, y}" by (simp add: meet_assoc_lemma) ``` ballarin@14551 ` 689` ``` also from L have "... = \ {x, y, z}" by (simp add: insert_commute) ``` ballarin@14551 ` 690` ``` also from L have "... = x \ (y \ z)" by (simp add: meet_assoc_lemma) ``` ballarin@14551 ` 691` ``` finally show ?thesis . ``` ballarin@14551 ` 692` ```qed ``` ballarin@14551 ` 693` ballarin@14551 ` 694` ```subsection {* Total Orders *} ``` ballarin@14551 ` 695` ballarin@14551 ` 696` ```locale total_order = lattice + ``` ballarin@14551 ` 697` ``` assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" ``` ballarin@14551 ` 698` ballarin@14551 ` 699` ```text {* Introduction rule: the usual definition of total order *} ``` ballarin@14551 ` 700` ballarin@14551 ` 701` ```lemma (in partial_order) total_orderI: ``` ballarin@14551 ` 702` ``` assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" ``` ballarin@14551 ` 703` ``` shows "total_order L" ``` ballarin@14551 ` 704` ```proof (rule total_order.intro) ``` ballarin@14551 ` 705` ``` show "lattice_axioms L" ``` ballarin@14551 ` 706` ``` proof (rule lattice_axioms.intro) ``` ballarin@14551 ` 707` ``` fix x y ``` ballarin@14551 ` 708` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 709` ``` show "EX s. least L s (Upper L {x, y})" ``` ballarin@14551 ` 710` ``` proof - ``` ballarin@14551 ` 711` ``` note total L ``` ballarin@14551 ` 712` ``` moreover ``` ballarin@14551 ` 713` ``` { ``` ballarin@14551 ` 714` ``` assume "x \ y" ``` ballarin@14551 ` 715` ``` with L have "least L y (Upper L {x, y})" ``` ballarin@14551 ` 716` ``` by (rule_tac least_UpperI) auto ``` ballarin@14551 ` 717` ``` } ``` ballarin@14551 ` 718` ``` moreover ``` ballarin@14551 ` 719` ``` { ``` ballarin@14551 ` 720` ``` assume "y \ x" ``` ballarin@14551 ` 721` ``` with L have "least L x (Upper L {x, y})" ``` ballarin@14551 ` 722` ``` by (rule_tac least_UpperI) auto ``` ballarin@14551 ` 723` ``` } ``` ballarin@14551 ` 724` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 725` ``` qed ``` ballarin@14551 ` 726` ``` next ``` ballarin@14551 ` 727` ``` fix x y ``` ballarin@14551 ` 728` ``` assume L: "x \ carrier L" "y \ carrier L" ``` ballarin@14551 ` 729` ``` show "EX i. greatest L i (Lower L {x, y})" ``` ballarin@14551 ` 730` ``` proof - ``` ballarin@14551 ` 731` ``` note total L ``` ballarin@14551 ` 732` ``` moreover ``` ballarin@14551 ` 733` ``` { ``` ballarin@14551 ` 734` ``` assume "y \ x" ``` ballarin@14551 ` 735` ``` with L have "greatest L y (Lower L {x, y})" ``` ballarin@14551 ` 736` ``` by (rule_tac greatest_LowerI) auto ``` ballarin@14551 ` 737` ``` } ``` ballarin@14551 ` 738` ``` moreover ``` ballarin@14551 ` 739` ``` { ``` ballarin@14551 ` 740` ``` assume "x \ y" ``` ballarin@14551 ` 741` ``` with L have "greatest L x (Lower L {x, y})" ``` ballarin@14551 ` 742` ``` by (rule_tac greatest_LowerI) auto ``` ballarin@14551 ` 743` ``` } ``` ballarin@14551 ` 744` ``` ultimately show ?thesis by blast ``` ballarin@14551 ` 745` ``` qed ``` ballarin@14551 ` 746` ``` qed ``` ballarin@14551 ` 747` ```qed (assumption | rule total_order_axioms.intro)+ ``` ballarin@14551 ` 748` ballarin@14551 ` 749` ```subsection {* Complete lattices *} ``` ballarin@14551 ` 750` ballarin@14551 ` 751` ```locale complete_lattice = lattice + ``` ballarin@14551 ` 752` ``` assumes sup_exists: ``` ballarin@14551 ` 753` ``` "[| A \ carrier L |] ==> EX s. least L s (Upper L A)" ``` ballarin@14551 ` 754` ``` and inf_exists: ``` ballarin@14551 ` 755` ``` "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" ``` ballarin@14551 ` 756` ballarin@14551 ` 757` ```text {* Introduction rule: the usual definition of complete lattice *} ``` ballarin@14551 ` 758` ballarin@14551 ` 759` ```lemma (in partial_order) complete_latticeI: ``` ballarin@14551 ` 760` ``` assumes sup_exists: ``` ballarin@14551 ` 761` ``` "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)" ``` ballarin@14551 ` 762` ``` and inf_exists: ``` ballarin@14551 ` 763` ``` "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" ``` ballarin@14551 ` 764` ``` shows "complete_lattice L" ``` ballarin@14551 ` 765` ```proof (rule complete_lattice.intro) ``` ballarin@14551 ` 766` ``` show "lattice_axioms L" ``` ballarin@14551 ` 767` ``` by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ ``` ballarin@14551 ` 768` ```qed (assumption | rule complete_lattice_axioms.intro)+ ``` ballarin@14551 ` 769` wenzelm@14651 ` 770` ```constdefs (structure L) ``` wenzelm@14651 ` 771` ``` top :: "_ => 'a" ("\\") ``` wenzelm@14651 ` 772` ``` "\ == sup L (carrier L)" ``` ballarin@14551 ` 773` wenzelm@14651 ` 774` ``` bottom :: "_ => 'a" ("\\") ``` wenzelm@14651 ` 775` ``` "\ == inf L (carrier L)" ``` ballarin@14551 ` 776` ballarin@14551 ` 777` ballarin@14551 ` 778` ```lemma (in complete_lattice) supI: ``` ballarin@14551 ` 779` ``` "[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |] ``` wenzelm@14651 ` 780` ``` ==> P (\A)" ``` ballarin@14551 ` 781` ```proof (unfold sup_def) ``` ballarin@14551 ` 782` ``` assume L: "A \ carrier L" ``` ballarin@14551 ` 783` ``` and P: "!!l. least L l (Upper L A) ==> P l" ``` ballarin@14551 ` 784` ``` with sup_exists obtain s where "least L s (Upper L A)" by blast ``` ballarin@14551 ` 785` ``` with L show "P (THE l. least L l (Upper L A))" ``` ballarin@14551 ` 786` ``` by (fast intro: theI2 least_unique P) ``` ballarin@14551 ` 787` ```qed ``` ballarin@14551 ` 788` ballarin@14551 ` 789` ```lemma (in complete_lattice) sup_closed [simp]: ``` ballarin@14551 ` 790` ``` "A \ carrier L ==> \ A \ carrier L" ``` ballarin@14551 ` 791` ``` by (rule supI) simp_all ``` ballarin@14551 ` 792` ballarin@14551 ` 793` ```lemma (in complete_lattice) top_closed [simp, intro]: ``` ballarin@14551 ` 794` ``` "\ \ carrier L" ``` ballarin@14551 ` 795` ``` by (unfold top_def) simp ``` ballarin@14551 ` 796` ballarin@14551 ` 797` ```lemma (in complete_lattice) infI: ``` ballarin@14551 ` 798` ``` "[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |] ``` ballarin@14551 ` 799` ``` ==> P (\ A)" ``` ballarin@14551 ` 800` ```proof (unfold inf_def) ``` ballarin@14551 ` 801` ``` assume L: "A \ carrier L" ``` ballarin@14551 ` 802` ``` and P: "!!l. greatest L l (Lower L A) ==> P l" ``` ballarin@14551 ` 803` ``` with inf_exists obtain s where "greatest L s (Lower L A)" by blast ``` ballarin@14551 ` 804` ``` with L show "P (THE l. greatest L l (Lower L A))" ``` ballarin@14551 ` 805` ``` by (fast intro: theI2 greatest_unique P) ``` ballarin@14551 ` 806` ```qed ``` ballarin@14551 ` 807` ballarin@14551 ` 808` ```lemma (in complete_lattice) inf_closed [simp]: ``` ballarin@14551 ` 809` ``` "A \ carrier L ==> \ A \ carrier L" ``` ballarin@14551 ` 810` ``` by (rule infI) simp_all ``` ballarin@14551 ` 811` ballarin@14551 ` 812` ```lemma (in complete_lattice) bottom_closed [simp, intro]: ``` ballarin@14551 ` 813` ``` "\ \ carrier L" ``` ballarin@14551 ` 814` ``` by (unfold bottom_def) simp ``` ballarin@14551 ` 815` ballarin@14551 ` 816` ```text {* Jacobson: Theorem 8.1 *} ``` ballarin@14551 ` 817` ballarin@14551 ` 818` ```lemma Lower_empty [simp]: ``` ballarin@14551 ` 819` ``` "Lower L {} = carrier L" ``` ballarin@14551 ` 820` ``` by (unfold Lower_def) simp ``` ballarin@14551 ` 821` ballarin@14551 ` 822` ```lemma Upper_empty [simp]: ``` ballarin@14551 ` 823` ``` "Upper L {} = carrier L" ``` ballarin@14551 ` 824` ``` by (unfold Upper_def) simp ``` ballarin@14551 ` 825` ballarin@14551 ` 826` ```theorem (in partial_order) complete_lattice_criterion1: ``` ballarin@14551 ` 827` ``` assumes top_exists: "EX g. greatest L g (carrier L)" ``` ballarin@14551 ` 828` ``` and inf_exists: ``` ballarin@14551 ` 829` ``` "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" ``` ballarin@14551 ` 830` ``` shows "complete_lattice L" ``` ballarin@14551 ` 831` ```proof (rule complete_latticeI) ``` ballarin@14551 ` 832` ``` from top_exists obtain top where top: "greatest L top (carrier L)" .. ``` ballarin@14551 ` 833` ``` fix A ``` ballarin@14551 ` 834` ``` assume L: "A \ carrier L" ``` ballarin@14551 ` 835` ``` let ?B = "Upper L A" ``` ballarin@14551 ` 836` ``` from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le) ``` ballarin@14551 ` 837` ``` then have B_non_empty: "?B ~= {}" by fast ``` ballarin@14551 ` 838` ``` have B_L: "?B \ carrier L" by simp ``` ballarin@14551 ` 839` ``` from inf_exists [OF B_L B_non_empty] ``` ballarin@14551 ` 840` ``` obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. ``` ballarin@14551 ` 841` ``` have "least L b (Upper L A)" ``` ballarin@14551 ` 842` ```apply (rule least_UpperI) ``` ballarin@14551 ` 843` ``` apply (rule greatest_le [where A = "Lower L ?B"]) ``` ballarin@14551 ` 844` ``` apply (rule b_inf_B) ``` ballarin@14551 ` 845` ``` apply (rule Lower_memI) ``` ballarin@14551 ` 846` ``` apply (erule UpperD) ``` ballarin@14551 ` 847` ``` apply assumption ``` ballarin@14551 ` 848` ``` apply (rule L) ``` ballarin@14551 ` 849` ``` apply (fast intro: L [THEN subsetD]) ``` ballarin@14551 ` 850` ``` apply (erule greatest_Lower_above [OF b_inf_B]) ``` ballarin@14551 ` 851` ``` apply simp ``` ballarin@14551 ` 852` ``` apply (rule L) ``` ballarin@14551 ` 853` ```apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) ``` ballarin@14551 ` 854` ```done ``` ballarin@14551 ` 855` ``` then show "EX s. least L s (Upper L A)" .. ``` ballarin@14551 ` 856` ```next ``` ballarin@14551 ` 857` ``` fix A ``` ballarin@14551 ` 858` ``` assume L: "A \ carrier L" ``` ballarin@14551 ` 859` ``` show "EX i. greatest L i (Lower L A)" ``` ballarin@14551 ` 860` ``` proof (cases "A = {}") ``` ballarin@14551 ` 861` ``` case True then show ?thesis ``` ballarin@14551 ` 862` ``` by (simp add: top_exists) ``` ballarin@14551 ` 863` ``` next ``` ballarin@14551 ` 864` ``` case False with L show ?thesis ``` ballarin@14551 ` 865` ``` by (rule inf_exists) ``` ballarin@14551 ` 866` ``` qed ``` ballarin@14551 ` 867` ```qed ``` ballarin@14551 ` 868` ballarin@14551 ` 869` ```(* TODO: prove dual version *) ``` ballarin@14551 ` 870` ballarin@14551 ` 871` ```subsection {* Examples *} ``` ballarin@14551 ` 872` ballarin@14551 ` 873` ```subsubsection {* Powerset of a set is a complete lattice *} ``` ballarin@14551 ` 874` ballarin@14551 ` 875` ```theorem powerset_is_complete_lattice: ``` ballarin@14551 ` 876` ``` "complete_lattice (| carrier = Pow A, le = op \ |)" ``` ballarin@14551 ` 877` ``` (is "complete_lattice ?L") ``` ballarin@14551 ` 878` ```proof (rule partial_order.complete_latticeI) ``` ballarin@14551 ` 879` ``` show "partial_order ?L" ``` ballarin@14551 ` 880` ``` by (rule partial_order.intro) auto ``` ballarin@14551 ` 881` ```next ``` ballarin@14551 ` 882` ``` fix B ``` ballarin@14551 ` 883` ``` assume "B \ carrier ?L" ``` ballarin@14551 ` 884` ``` then have "least ?L (\ B) (Upper ?L B)" ``` ballarin@14551 ` 885` ``` by (fastsimp intro!: least_UpperI simp: Upper_def) ``` ballarin@14551 ` 886` ``` then show "EX s. least ?L s (Upper ?L B)" .. ``` ballarin@14551 ` 887` ```next ``` ballarin@14551 ` 888` ``` fix B ``` ballarin@14551 ` 889` ``` assume "B \ carrier ?L" ``` ballarin@14551 ` 890` ``` then have "greatest ?L (\ B \ A) (Lower ?L B)" ``` ballarin@14551 ` 891` ``` txt {* @{term "\ B"} is not the infimum of @{term B}: ``` ballarin@14551 ` 892` ``` @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *} ``` ballarin@14551 ` 893` ``` by (fastsimp intro!: greatest_LowerI simp: Lower_def) ``` ballarin@14551 ` 894` ``` then show "EX i. greatest ?L i (Lower ?L B)" .. ``` ballarin@14551 ` 895` ```qed ``` ballarin@14551 ` 896` ballarin@14551 ` 897` ```subsubsection {* Lattice of subgroups of a group *} ``` ballarin@14551 ` 898` ballarin@14551 ` 899` ```theorem (in group) subgroups_partial_order: ``` ballarin@14551 ` 900` ``` "partial_order (| carrier = {H. subgroup H G}, le = op \ |)" ``` ballarin@14551 ` 901` ``` by (rule partial_order.intro) simp_all ``` ballarin@14551 ` 902` ballarin@14551 ` 903` ```lemma (in group) subgroup_self: ``` ballarin@14551 ` 904` ``` "subgroup (carrier G) G" ``` ballarin@14551 ` 905` ``` by (rule subgroupI) auto ``` ballarin@14551 ` 906` ballarin@14551 ` 907` ```lemma (in group) subgroup_imp_group: ``` ballarin@14551 ` 908` ``` "subgroup H G ==> group (G(| carrier := H |))" ``` ballarin@14551 ` 909` ``` using subgroup.groupI [OF _ group.intro] . ``` ballarin@14551 ` 910` ballarin@14551 ` 911` ```lemma (in group) is_monoid [intro, simp]: ``` ballarin@14551 ` 912` ``` "monoid G" ``` ballarin@14551 ` 913` ``` by (rule monoid.intro) ``` ballarin@14551 ` 914` ballarin@14551 ` 915` ```lemma (in group) subgroup_inv_equality: ``` ballarin@14551 ` 916` ``` "[| subgroup H G; x \ H |] ==> m_inv (G (| carrier := H |)) x = inv x" ``` ballarin@14551 ` 917` ```apply (rule_tac inv_equality [THEN sym]) ``` ballarin@14551 ` 918` ``` apply (rule group.l_inv [OF subgroup_imp_group, simplified]) ``` ballarin@14551 ` 919` ``` apply assumption+ ``` ballarin@14551 ` 920` ``` apply (rule subsetD [OF subgroup.subset]) ``` ballarin@14551 ` 921` ``` apply assumption+ ``` ballarin@14551 ` 922` ```apply (rule subsetD [OF subgroup.subset]) ``` ballarin@14551 ` 923` ``` apply assumption ``` ballarin@14551 ` 924` ```apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) ``` ballarin@14551 ` 925` ``` apply assumption+ ``` ballarin@14551 ` 926` ```done ``` ballarin@14551 ` 927` ballarin@14551 ` 928` ```theorem (in group) subgroups_Inter: ``` ballarin@14551 ` 929` ``` assumes subgr: "(!!H. H \ A ==> subgroup H G)" ``` ballarin@14551 ` 930` ``` and not_empty: "A ~= {}" ``` ballarin@14551 ` 931` ``` shows "subgroup (\A) G" ``` ballarin@14551 ` 932` ```proof (rule subgroupI) ``` ballarin@14551 ` 933` ``` from subgr [THEN subgroup.subset] and not_empty ``` ballarin@14551 ` 934` ``` show "\A \ carrier G" by blast ``` ballarin@14551 ` 935` ```next ``` ballarin@14551 ` 936` ``` from subgr [THEN subgroup.one_closed] ``` ballarin@14551 ` 937` ``` show "\A ~= {}" by blast ``` ballarin@14551 ` 938` ```next ``` ballarin@14551 ` 939` ``` fix x assume "x \ \A" ``` ballarin@14551 ` 940` ``` with subgr [THEN subgroup.m_inv_closed] ``` ballarin@14551 ` 941` ``` show "inv x \ \A" by blast ``` ballarin@14551 ` 942` ```next ``` ballarin@14551 ` 943` ``` fix x y assume "x \ \A" "y \ \A" ``` ballarin@14551 ` 944` ``` with subgr [THEN subgroup.m_closed] ``` ballarin@14551 ` 945` ``` show "x \ y \ \A" by blast ``` ballarin@14551 ` 946` ```qed ``` ballarin@14551 ` 947` ballarin@14551 ` 948` ```theorem (in group) subgroups_complete_lattice: ``` ballarin@14551 ` 949` ``` "complete_lattice (| carrier = {H. subgroup H G}, le = op \ |)" ``` ballarin@14551 ` 950` ``` (is "complete_lattice ?L") ``` ballarin@14551 ` 951` ```proof (rule partial_order.complete_lattice_criterion1) ``` ballarin@14551 ` 952` ``` show "partial_order ?L" by (rule subgroups_partial_order) ``` ballarin@14551 ` 953` ```next ``` ballarin@14551 ` 954` ``` have "greatest ?L (carrier G) (carrier ?L)" ``` ballarin@14551 ` 955` ``` by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) ``` ballarin@14551 ` 956` ``` then show "EX G. greatest ?L G (carrier ?L)" .. ``` ballarin@14551 ` 957` ```next ``` ballarin@14551 ` 958` ``` fix A ``` ballarin@14551 ` 959` ``` assume L: "A \ carrier ?L" and non_empty: "A ~= {}" ``` ballarin@14551 ` 960` ``` then have Int_subgroup: "subgroup (\A) G" ``` ballarin@14551 ` 961` ``` by (fastsimp intro: subgroups_Inter) ``` ballarin@14551 ` 962` ``` have "greatest ?L (\A) (Lower ?L A)" ``` ballarin@14551 ` 963` ``` (is "greatest ?L ?Int _") ``` ballarin@14551 ` 964` ``` proof (rule greatest_LowerI) ``` ballarin@14551 ` 965` ``` fix H ``` ballarin@14551 ` 966` ``` assume H: "H \ A" ``` ballarin@14551 ` 967` ``` with L have subgroupH: "subgroup H G" by auto ``` ballarin@14551 ` 968` ``` from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) ``` ballarin@14551 ` 969` ``` from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") ``` ballarin@14551 ` 970` ``` by (rule subgroup_imp_group) ``` ballarin@14551 ` 971` ``` from groupH have monoidH: "monoid ?H" ``` ballarin@14551 ` 972` ``` by (rule group.is_monoid) ``` ballarin@14551 ` 973` ``` from H have Int_subset: "?Int \ H" by fastsimp ``` ballarin@14551 ` 974` ``` then show "le ?L ?Int H" by simp ``` ballarin@14551 ` 975` ``` next ``` ballarin@14551 ` 976` ``` fix H ``` ballarin@14551 ` 977` ``` assume H: "H \ Lower ?L A" ``` ballarin@14551 ` 978` ``` with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) ``` ballarin@14551 ` 979` ``` next ``` ballarin@14551 ` 980` ``` show "A \ carrier ?L" by (rule L) ``` ballarin@14551 ` 981` ``` next ``` ballarin@14551 ` 982` ``` show "?Int \ carrier ?L" by simp (rule Int_subgroup) ``` ballarin@14551 ` 983` ``` qed ``` ballarin@14551 ` 984` ``` then show "EX I. greatest ?L I (Lower ?L A)" .. ``` ballarin@14551 ` 985` ```qed ``` ballarin@14551 ` 986` ballarin@14551 ` 987` `end`