src/HOL/Library/Lattice_Constructions.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (19 months ago) changeset 67951 655aa11359dc parent 62390 842917225d56 permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
 Andreas@57998 ` 1` ```(* Title: HOL/Library/Lattice_Constructions.thy ``` bulwahn@37915 ` 2` ``` Author: Lukas Bulwahn ``` bulwahn@37915 ` 3` ``` Copyright 2010 TU Muenchen ``` bulwahn@37915 ` 4` ```*) ``` bulwahn@37915 ` 5` Andreas@57998 ` 6` ```theory Lattice_Constructions ``` wenzelm@57645 ` 7` ```imports Main ``` bulwahn@37915 ` 8` ```begin ``` bulwahn@37915 ` 9` wenzelm@60500 ` 10` ```subsection \Values extended by a bottom element\ ``` bulwahn@37915 ` 11` blanchet@58310 ` 12` ```datatype 'a bot = Value 'a | Bot ``` bulwahn@37915 ` 13` bulwahn@37915 ` 14` ```instantiation bot :: (preorder) preorder ``` bulwahn@37915 ` 15` ```begin ``` bulwahn@37915 ` 16` bulwahn@37915 ` 17` ```definition less_eq_bot where ``` bulwahn@37915 ` 18` ``` "x \ y \ (case x of Bot \ True | Value x \ (case y of Bot \ False | Value y \ x \ y))" ``` bulwahn@37915 ` 19` bulwahn@37915 ` 20` ```definition less_bot where ``` bulwahn@37915 ` 21` ``` "x < y \ (case y of Bot \ False | Value y \ (case x of Bot \ True | Value x \ x < y))" ``` bulwahn@37915 ` 22` bulwahn@37915 ` 23` ```lemma less_eq_bot_Bot [simp]: "Bot \ x" ``` bulwahn@37915 ` 24` ``` by (simp add: less_eq_bot_def) ``` bulwahn@37915 ` 25` bulwahn@37915 ` 26` ```lemma less_eq_bot_Bot_code [code]: "Bot \ x \ True" ``` bulwahn@37915 ` 27` ``` by simp ``` bulwahn@37915 ` 28` bulwahn@37915 ` 29` ```lemma less_eq_bot_Bot_is_Bot: "x \ Bot \ x = Bot" ``` bulwahn@37915 ` 30` ``` by (cases x) (simp_all add: less_eq_bot_def) ``` bulwahn@37915 ` 31` bulwahn@37915 ` 32` ```lemma less_eq_bot_Value_Bot [simp, code]: "Value x \ Bot \ False" ``` bulwahn@37915 ` 33` ``` by (simp add: less_eq_bot_def) ``` bulwahn@37915 ` 34` bulwahn@37915 ` 35` ```lemma less_eq_bot_Value [simp, code]: "Value x \ Value y \ x \ y" ``` bulwahn@37915 ` 36` ``` by (simp add: less_eq_bot_def) ``` bulwahn@37915 ` 37` bulwahn@37915 ` 38` ```lemma less_bot_Bot [simp, code]: "x < Bot \ False" ``` bulwahn@37915 ` 39` ``` by (simp add: less_bot_def) ``` bulwahn@37915 ` 40` bulwahn@37915 ` 41` ```lemma less_bot_Bot_is_Value: "Bot < x \ \z. x = Value z" ``` bulwahn@37915 ` 42` ``` by (cases x) (simp_all add: less_bot_def) ``` bulwahn@37915 ` 43` bulwahn@37915 ` 44` ```lemma less_bot_Bot_Value [simp]: "Bot < Value x" ``` bulwahn@37915 ` 45` ``` by (simp add: less_bot_def) ``` bulwahn@37915 ` 46` bulwahn@37915 ` 47` ```lemma less_bot_Bot_Value_code [code]: "Bot < Value x \ True" ``` bulwahn@37915 ` 48` ``` by simp ``` bulwahn@37915 ` 49` bulwahn@37915 ` 50` ```lemma less_bot_Value [simp, code]: "Value x < Value y \ x < y" ``` bulwahn@37915 ` 51` ``` by (simp add: less_bot_def) ``` bulwahn@37915 ` 52` wenzelm@60508 ` 53` ```instance ``` wenzelm@60679 ` 54` ``` by standard ``` wenzelm@60508 ` 55` ``` (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits) ``` bulwahn@37915 ` 56` wenzelm@60508 ` 57` ```end ``` bulwahn@37915 ` 58` wenzelm@60508 ` 59` ```instance bot :: (order) order ``` wenzelm@60679 ` 60` ``` by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits) ``` bulwahn@37915 ` 61` wenzelm@60508 ` 62` ```instance bot :: (linorder) linorder ``` wenzelm@60679 ` 63` ``` by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits) ``` bulwahn@37915 ` 64` haftmann@43815 ` 65` ```instantiation bot :: (order) bot ``` bulwahn@37915 ` 66` ```begin ``` wenzelm@60508 ` 67` ``` definition "bot = Bot" ``` wenzelm@60508 ` 68` ``` instance .. ``` bulwahn@37915 ` 69` ```end ``` bulwahn@37915 ` 70` bulwahn@37915 ` 71` ```instantiation bot :: (top) top ``` bulwahn@37915 ` 72` ```begin ``` wenzelm@60508 ` 73` ``` definition "top = Value top" ``` wenzelm@60508 ` 74` ``` instance .. ``` bulwahn@37915 ` 75` ```end ``` bulwahn@37915 ` 76` bulwahn@37915 ` 77` ```instantiation bot :: (semilattice_inf) semilattice_inf ``` bulwahn@37915 ` 78` ```begin ``` bulwahn@37915 ` 79` bulwahn@37915 ` 80` ```definition inf_bot ``` bulwahn@37915 ` 81` ```where ``` wenzelm@60508 ` 82` ``` "inf x y = ``` wenzelm@60508 ` 83` ``` (case x of ``` wenzelm@60508 ` 84` ``` Bot \ Bot ``` wenzelm@60508 ` 85` ``` | Value v \ ``` wenzelm@60508 ` 86` ``` (case y of ``` wenzelm@60508 ` 87` ``` Bot \ Bot ``` wenzelm@60508 ` 88` ``` | Value v' \ Value (inf v v')))" ``` bulwahn@37915 ` 89` wenzelm@60508 ` 90` ```instance ``` wenzelm@60679 ` 91` ``` by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits) ``` bulwahn@37915 ` 92` bulwahn@37915 ` 93` ```end ``` bulwahn@37915 ` 94` bulwahn@37915 ` 95` ```instantiation bot :: (semilattice_sup) semilattice_sup ``` bulwahn@37915 ` 96` ```begin ``` bulwahn@37915 ` 97` bulwahn@37915 ` 98` ```definition sup_bot ``` bulwahn@37915 ` 99` ```where ``` wenzelm@60508 ` 100` ``` "sup x y = ``` wenzelm@60508 ` 101` ``` (case x of ``` wenzelm@60508 ` 102` ``` Bot \ y ``` wenzelm@60508 ` 103` ``` | Value v \ ``` wenzelm@60508 ` 104` ``` (case y of ``` wenzelm@60508 ` 105` ``` Bot \ x ``` wenzelm@60508 ` 106` ``` | Value v' \ Value (sup v v')))" ``` bulwahn@37915 ` 107` wenzelm@60508 ` 108` ```instance ``` wenzelm@60679 ` 109` ``` by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits) ``` bulwahn@37915 ` 110` bulwahn@37915 ` 111` ```end ``` bulwahn@37915 ` 112` Andreas@57543 ` 113` ```instance bot :: (lattice) bounded_lattice_bot ``` wenzelm@60508 ` 114` ``` by intro_classes (simp add: bot_bot_def) ``` bulwahn@37915 ` 115` wenzelm@60508 ` 116` wenzelm@60508 ` 117` ```subsection \Values extended by a top element\ ``` bulwahn@37915 ` 118` blanchet@58310 ` 119` ```datatype 'a top = Value 'a | Top ``` bulwahn@37915 ` 120` bulwahn@37915 ` 121` ```instantiation top :: (preorder) preorder ``` bulwahn@37915 ` 122` ```begin ``` bulwahn@37915 ` 123` bulwahn@37915 ` 124` ```definition less_eq_top where ``` bulwahn@37915 ` 125` ``` "x \ y \ (case y of Top \ True | Value y \ (case x of Top \ False | Value x \ x \ y))" ``` bulwahn@37915 ` 126` bulwahn@37915 ` 127` ```definition less_top where ``` bulwahn@37915 ` 128` ``` "x < y \ (case x of Top \ False | Value x \ (case y of Top \ True | Value y \ x < y))" ``` bulwahn@37915 ` 129` wenzelm@60508 ` 130` ```lemma less_eq_top_Top [simp]: "x \ Top" ``` bulwahn@37915 ` 131` ``` by (simp add: less_eq_top_def) ``` bulwahn@37915 ` 132` bulwahn@37915 ` 133` ```lemma less_eq_top_Top_code [code]: "x \ Top \ True" ``` bulwahn@37915 ` 134` ``` by simp ``` bulwahn@37915 ` 135` bulwahn@37915 ` 136` ```lemma less_eq_top_is_Top: "Top \ x \ x = Top" ``` bulwahn@37915 ` 137` ``` by (cases x) (simp_all add: less_eq_top_def) ``` bulwahn@37915 ` 138` bulwahn@37915 ` 139` ```lemma less_eq_top_Top_Value [simp, code]: "Top \ Value x \ False" ``` bulwahn@37915 ` 140` ``` by (simp add: less_eq_top_def) ``` bulwahn@37915 ` 141` bulwahn@37915 ` 142` ```lemma less_eq_top_Value_Value [simp, code]: "Value x \ Value y \ x \ y" ``` bulwahn@37915 ` 143` ``` by (simp add: less_eq_top_def) ``` bulwahn@37915 ` 144` bulwahn@37915 ` 145` ```lemma less_top_Top [simp, code]: "Top < x \ False" ``` bulwahn@37915 ` 146` ``` by (simp add: less_top_def) ``` bulwahn@37915 ` 147` bulwahn@37915 ` 148` ```lemma less_top_Top_is_Value: "x < Top \ \z. x = Value z" ``` bulwahn@37915 ` 149` ``` by (cases x) (simp_all add: less_top_def) ``` bulwahn@37915 ` 150` bulwahn@37915 ` 151` ```lemma less_top_Value_Top [simp]: "Value x < Top" ``` bulwahn@37915 ` 152` ``` by (simp add: less_top_def) ``` bulwahn@37915 ` 153` bulwahn@37915 ` 154` ```lemma less_top_Value_Top_code [code]: "Value x < Top \ True" ``` bulwahn@37915 ` 155` ``` by simp ``` bulwahn@37915 ` 156` bulwahn@37915 ` 157` ```lemma less_top_Value [simp, code]: "Value x < Value y \ x < y" ``` bulwahn@37915 ` 158` ``` by (simp add: less_top_def) ``` bulwahn@37915 ` 159` wenzelm@60508 ` 160` ```instance ``` wenzelm@60679 ` 161` ``` by standard ``` wenzelm@60508 ` 162` ``` (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits) ``` bulwahn@37915 ` 163` wenzelm@60508 ` 164` ```end ``` bulwahn@37915 ` 165` wenzelm@60508 ` 166` ```instance top :: (order) order ``` wenzelm@60679 ` 167` ``` by standard (auto simp add: less_eq_top_def less_top_def split: top.splits) ``` bulwahn@37915 ` 168` wenzelm@60508 ` 169` ```instance top :: (linorder) linorder ``` wenzelm@60679 ` 170` ``` by standard (auto simp add: less_eq_top_def less_top_def split: top.splits) ``` bulwahn@37915 ` 171` haftmann@43815 ` 172` ```instantiation top :: (order) top ``` bulwahn@37915 ` 173` ```begin ``` wenzelm@60508 ` 174` ``` definition "top = Top" ``` wenzelm@60508 ` 175` ``` instance .. ``` bulwahn@37915 ` 176` ```end ``` bulwahn@37915 ` 177` bulwahn@37915 ` 178` ```instantiation top :: (bot) bot ``` bulwahn@37915 ` 179` ```begin ``` wenzelm@60508 ` 180` ``` definition "bot = Value bot" ``` wenzelm@60508 ` 181` ``` instance .. ``` bulwahn@37915 ` 182` ```end ``` bulwahn@37915 ` 183` bulwahn@37915 ` 184` ```instantiation top :: (semilattice_inf) semilattice_inf ``` bulwahn@37915 ` 185` ```begin ``` bulwahn@37915 ` 186` bulwahn@37915 ` 187` ```definition inf_top ``` bulwahn@37915 ` 188` ```where ``` wenzelm@60508 ` 189` ``` "inf x y = ``` wenzelm@60508 ` 190` ``` (case x of ``` wenzelm@60508 ` 191` ``` Top \ y ``` wenzelm@60508 ` 192` ``` | Value v \ ``` wenzelm@60508 ` 193` ``` (case y of ``` wenzelm@60508 ` 194` ``` Top \ x ``` wenzelm@60508 ` 195` ``` | Value v' \ Value (inf v v')))" ``` bulwahn@37915 ` 196` wenzelm@60508 ` 197` ```instance ``` wenzelm@60679 ` 198` ``` by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits) ``` bulwahn@37915 ` 199` bulwahn@37915 ` 200` ```end ``` bulwahn@37915 ` 201` bulwahn@37915 ` 202` ```instantiation top :: (semilattice_sup) semilattice_sup ``` bulwahn@37915 ` 203` ```begin ``` bulwahn@37915 ` 204` bulwahn@37915 ` 205` ```definition sup_top ``` bulwahn@37915 ` 206` ```where ``` wenzelm@60508 ` 207` ``` "sup x y = ``` wenzelm@60508 ` 208` ``` (case x of ``` wenzelm@60508 ` 209` ``` Top \ Top ``` wenzelm@60508 ` 210` ``` | Value v \ ``` wenzelm@60508 ` 211` ``` (case y of ``` wenzelm@60508 ` 212` ``` Top \ Top ``` wenzelm@60508 ` 213` ``` | Value v' \ Value (sup v v')))" ``` bulwahn@37915 ` 214` wenzelm@60508 ` 215` ```instance ``` wenzelm@60679 ` 216` ``` by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits) ``` bulwahn@37915 ` 217` bulwahn@37915 ` 218` ```end ``` bulwahn@37915 ` 219` Andreas@57543 ` 220` ```instance top :: (lattice) bounded_lattice_top ``` wenzelm@60679 ` 221` ``` by standard (simp add: top_top_def) ``` wenzelm@60508 ` 222` bulwahn@37915 ` 223` wenzelm@60500 ` 224` ```subsection \Values extended by a top and a bottom element\ ``` bulwahn@37918 ` 225` blanchet@58310 ` 226` ```datatype 'a flat_complete_lattice = Value 'a | Bot | Top ``` bulwahn@37918 ` 227` bulwahn@37918 ` 228` ```instantiation flat_complete_lattice :: (type) order ``` bulwahn@37918 ` 229` ```begin ``` bulwahn@37918 ` 230` wenzelm@60508 ` 231` ```definition less_eq_flat_complete_lattice ``` wenzelm@60508 ` 232` ```where ``` wenzelm@60508 ` 233` ``` "x \ y \ ``` wenzelm@60508 ` 234` ``` (case x of ``` wenzelm@60508 ` 235` ``` Bot \ True ``` wenzelm@60508 ` 236` ``` | Value v1 \ ``` wenzelm@60508 ` 237` ``` (case y of ``` wenzelm@60508 ` 238` ``` Bot \ False ``` wenzelm@60508 ` 239` ``` | Value v2 \ v1 = v2 ``` wenzelm@60508 ` 240` ``` | Top \ True) ``` wenzelm@60508 ` 241` ``` | Top \ y = Top)" ``` bulwahn@37918 ` 242` wenzelm@60508 ` 243` ```definition less_flat_complete_lattice ``` wenzelm@60508 ` 244` ```where ``` wenzelm@60508 ` 245` ``` "x < y = ``` wenzelm@60508 ` 246` ``` (case x of ``` wenzelm@60508 ` 247` ``` Bot \ y \ Bot ``` wenzelm@60508 ` 248` ``` | Value v1 \ y = Top ``` wenzelm@60508 ` 249` ``` | Top \ False)" ``` bulwahn@37918 ` 250` wenzelm@60508 ` 251` ```lemma [simp]: "Bot \ y" ``` wenzelm@60508 ` 252` ``` unfolding less_eq_flat_complete_lattice_def by auto ``` wenzelm@60508 ` 253` wenzelm@60508 ` 254` ```lemma [simp]: "y \ Top" ``` wenzelm@60508 ` 255` ``` unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits) ``` bulwahn@37918 ` 256` bulwahn@37918 ` 257` ```lemma greater_than_two_values: ``` wenzelm@60509 ` 258` ``` assumes "a \ b" "Value a \ z" "Value b \ z" ``` bulwahn@37918 ` 259` ``` shows "z = Top" ``` wenzelm@60508 ` 260` ``` using assms ``` wenzelm@60508 ` 261` ``` by (cases z) (auto simp add: less_eq_flat_complete_lattice_def) ``` bulwahn@37918 ` 262` bulwahn@37918 ` 263` ```lemma lesser_than_two_values: ``` wenzelm@60509 ` 264` ``` assumes "a \ b" "z \ Value a" "z \ Value b" ``` bulwahn@37918 ` 265` ``` shows "z = Bot" ``` wenzelm@60508 ` 266` ``` using assms ``` wenzelm@60508 ` 267` ``` by (cases z) (auto simp add: less_eq_flat_complete_lattice_def) ``` bulwahn@37918 ` 268` wenzelm@60508 ` 269` ```instance ``` wenzelm@60679 ` 270` ``` by standard ``` wenzelm@60508 ` 271` ``` (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def ``` wenzelm@60508 ` 272` ``` split: flat_complete_lattice.splits) ``` bulwahn@37918 ` 273` bulwahn@37918 ` 274` ```end ``` bulwahn@37918 ` 275` bulwahn@37918 ` 276` ```instantiation flat_complete_lattice :: (type) bot ``` bulwahn@37918 ` 277` ```begin ``` wenzelm@60508 ` 278` ``` definition "bot = Bot" ``` wenzelm@60508 ` 279` ``` instance .. ``` bulwahn@37918 ` 280` ```end ``` bulwahn@37918 ` 281` bulwahn@37918 ` 282` ```instantiation flat_complete_lattice :: (type) top ``` bulwahn@37918 ` 283` ```begin ``` wenzelm@60508 ` 284` ``` definition "top = Top" ``` wenzelm@60508 ` 285` ``` instance .. ``` bulwahn@37918 ` 286` ```end ``` bulwahn@37918 ` 287` bulwahn@37918 ` 288` ```instantiation flat_complete_lattice :: (type) lattice ``` bulwahn@37918 ` 289` ```begin ``` bulwahn@37918 ` 290` bulwahn@37918 ` 291` ```definition inf_flat_complete_lattice ``` bulwahn@37918 ` 292` ```where ``` wenzelm@60508 ` 293` ``` "inf x y = ``` wenzelm@60508 ` 294` ``` (case x of ``` wenzelm@60508 ` 295` ``` Bot \ Bot ``` wenzelm@60508 ` 296` ``` | Value v1 \ ``` wenzelm@60508 ` 297` ``` (case y of ``` wenzelm@60508 ` 298` ``` Bot \ Bot ``` wenzelm@60508 ` 299` ``` | Value v2 \ if v1 = v2 then x else Bot ``` wenzelm@60508 ` 300` ``` | Top \ x) ``` wenzelm@60508 ` 301` ``` | Top \ y)" ``` bulwahn@37918 ` 302` bulwahn@37918 ` 303` ```definition sup_flat_complete_lattice ``` bulwahn@37918 ` 304` ```where ``` wenzelm@60508 ` 305` ``` "sup x y = ``` wenzelm@60508 ` 306` ``` (case x of ``` wenzelm@60508 ` 307` ``` Bot \ y ``` wenzelm@60508 ` 308` ``` | Value v1 \ ``` wenzelm@60508 ` 309` ``` (case y of ``` wenzelm@60508 ` 310` ``` Bot \ x ``` wenzelm@60508 ` 311` ``` | Value v2 \ if v1 = v2 then x else Top ``` wenzelm@60508 ` 312` ``` | Top \ Top) ``` wenzelm@60508 ` 313` ``` | Top \ Top)" ``` bulwahn@37918 ` 314` wenzelm@60508 ` 315` ```instance ``` wenzelm@60679 ` 316` ``` by standard ``` wenzelm@60508 ` 317` ``` (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def ``` wenzelm@60508 ` 318` ``` less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits) ``` bulwahn@37918 ` 319` bulwahn@37918 ` 320` ```end ``` bulwahn@37918 ` 321` bulwahn@37918 ` 322` ```instantiation flat_complete_lattice :: (type) complete_lattice ``` bulwahn@37918 ` 323` ```begin ``` bulwahn@37918 ` 324` bulwahn@37918 ` 325` ```definition Sup_flat_complete_lattice ``` bulwahn@37918 ` 326` ```where ``` wenzelm@60508 ` 327` ``` "Sup A = ``` wenzelm@60508 ` 328` ``` (if A = {} \ A = {Bot} then Bot ``` wenzelm@60508 ` 329` ``` else if \v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v}) ``` wenzelm@60508 ` 330` ``` else Top)" ``` bulwahn@37918 ` 331` bulwahn@37918 ` 332` ```definition Inf_flat_complete_lattice ``` bulwahn@37918 ` 333` ```where ``` wenzelm@60508 ` 334` ``` "Inf A = ``` wenzelm@60508 ` 335` ``` (if A = {} \ A = {Top} then Top ``` wenzelm@60508 ` 336` ``` else if \v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v}) ``` wenzelm@60508 ` 337` ``` else Bot)" ``` wenzelm@60508 ` 338` bulwahn@37918 ` 339` ```instance ``` bulwahn@37918 ` 340` ```proof ``` wenzelm@60508 ` 341` ``` fix x :: "'a flat_complete_lattice" ``` wenzelm@60508 ` 342` ``` fix A ``` wenzelm@60508 ` 343` ``` assume "x \ A" ``` bulwahn@37918 ` 344` ``` { ``` bulwahn@37918 ` 345` ``` fix v ``` bulwahn@37918 ` 346` ``` assume "A - {Top} = {Value v}" ``` wenzelm@60508 ` 347` ``` then have "(THE v. A - {Top} = {Value v}) = v" ``` bulwahn@37918 ` 348` ``` by (auto intro!: the1_equality) ``` bulwahn@37918 ` 349` ``` moreover ``` wenzelm@60508 ` 350` ``` from \x \ A\ \A - {Top} = {Value v}\ have "x = Top \ x = Value v" ``` bulwahn@37918 ` 351` ``` by auto ``` wenzelm@60508 ` 352` ``` ultimately have "Value (THE v. A - {Top} = {Value v}) \ x" ``` bulwahn@37918 ` 353` ``` by auto ``` bulwahn@37918 ` 354` ``` } ``` wenzelm@60508 ` 355` ``` with \x \ A\ show "Inf A \ x" ``` bulwahn@37918 ` 356` ``` unfolding Inf_flat_complete_lattice_def ``` nipkow@44890 ` 357` ``` by fastforce ``` bulwahn@37918 ` 358` ```next ``` wenzelm@60508 ` 359` ``` fix z :: "'a flat_complete_lattice" ``` wenzelm@60508 ` 360` ``` fix A ``` wenzelm@60509 ` 361` ``` show "z \ Inf A" if z: "\x. x \ A \ z \ x" ``` wenzelm@60509 ` 362` ``` proof - ``` wenzelm@60509 ` 363` ``` consider "A = {} \ A = {Top}" ``` wenzelm@60509 ` 364` ``` | "A \ {}" "A \ {Top}" "\v. A - {Top} = {Value v}" ``` wenzelm@60509 ` 365` ``` | "A \ {}" "A \ {Top}" "\ (\v. A - {Top} = {Value v})" ``` wenzelm@60509 ` 366` ``` by blast ``` wenzelm@60509 ` 367` ``` then show ?thesis ``` wenzelm@60509 ` 368` ``` proof cases ``` wenzelm@60509 ` 369` ``` case 1 ``` wenzelm@60509 ` 370` ``` then have "Inf A = Top" ``` wenzelm@60509 ` 371` ``` unfolding Inf_flat_complete_lattice_def by auto ``` wenzelm@60509 ` 372` ``` then show ?thesis by simp ``` wenzelm@60509 ` 373` ``` next ``` wenzelm@60509 ` 374` ``` case 2 ``` wenzelm@60509 ` 375` ``` then obtain v where v1: "A - {Top} = {Value v}" ``` bulwahn@37918 ` 376` ``` by auto ``` wenzelm@60509 ` 377` ``` then have v2: "(THE v. A - {Top} = {Value v}) = v" ``` wenzelm@60509 ` 378` ``` by (auto intro!: the1_equality) ``` wenzelm@60509 ` 379` ``` from 2 v2 have Inf: "Inf A = Value v" ``` wenzelm@60509 ` 380` ``` unfolding Inf_flat_complete_lattice_def by simp ``` wenzelm@60509 ` 381` ``` from v1 have "Value v \ A" by blast ``` wenzelm@60509 ` 382` ``` then have "z \ Value v" by (rule z) ``` wenzelm@60509 ` 383` ``` with Inf show ?thesis by simp ``` bulwahn@37918 ` 384` ``` next ``` wenzelm@60509 ` 385` ``` case 3 ``` wenzelm@60509 ` 386` ``` then have Inf: "Inf A = Bot" ``` wenzelm@60509 ` 387` ``` unfolding Inf_flat_complete_lattice_def by auto ``` wenzelm@60509 ` 388` ``` have "z \ Bot" ``` wenzelm@60509 ` 389` ``` proof (cases "A - {Top} = {Bot}") ``` wenzelm@60509 ` 390` ``` case True ``` wenzelm@60509 ` 391` ``` then have "Bot \ A" by blast ``` wenzelm@60509 ` 392` ``` then show ?thesis by (rule z) ``` wenzelm@60509 ` 393` ``` next ``` wenzelm@60509 ` 394` ``` case False ``` wenzelm@60509 ` 395` ``` from 3 obtain a1 where a1: "a1 \ A - {Top}" ``` wenzelm@60509 ` 396` ``` by auto ``` wenzelm@60509 ` 397` ``` from 3 False a1 obtain a2 where "a2 \ A - {Top} \ a1 \ a2" ``` wenzelm@60509 ` 398` ``` by (cases a1) auto ``` wenzelm@60509 ` 399` ``` with a1 z[of "a1"] z[of "a2"] show ?thesis ``` wenzelm@60509 ` 400` ``` apply (cases a1) ``` wenzelm@60509 ` 401` ``` apply auto ``` wenzelm@60509 ` 402` ``` apply (cases a2) ``` wenzelm@60509 ` 403` ``` apply auto ``` wenzelm@60509 ` 404` ``` apply (auto dest!: lesser_than_two_values) ``` wenzelm@60509 ` 405` ``` done ``` wenzelm@60509 ` 406` ``` qed ``` wenzelm@60509 ` 407` ``` with Inf show ?thesis by simp ``` bulwahn@37918 ` 408` ``` qed ``` wenzelm@60509 ` 409` ``` qed ``` bulwahn@37918 ` 410` ```next ``` wenzelm@60508 ` 411` ``` fix x :: "'a flat_complete_lattice" ``` wenzelm@60508 ` 412` ``` fix A ``` wenzelm@60508 ` 413` ``` assume "x \ A" ``` bulwahn@37918 ` 414` ``` { ``` bulwahn@37918 ` 415` ``` fix v ``` bulwahn@37918 ` 416` ``` assume "A - {Bot} = {Value v}" ``` wenzelm@60508 ` 417` ``` then have "(THE v. A - {Bot} = {Value v}) = v" ``` bulwahn@37918 ` 418` ``` by (auto intro!: the1_equality) ``` bulwahn@37918 ` 419` ``` moreover ``` wenzelm@60508 ` 420` ``` from \x \ A\ \A - {Bot} = {Value v}\ have "x = Bot \ x = Value v" ``` bulwahn@37918 ` 421` ``` by auto ``` wenzelm@60508 ` 422` ``` ultimately have "x \ Value (THE v. A - {Bot} = {Value v})" ``` bulwahn@37918 ` 423` ``` by auto ``` bulwahn@37918 ` 424` ``` } ``` wenzelm@60508 ` 425` ``` with \x \ A\ show "x \ Sup A" ``` bulwahn@37918 ` 426` ``` unfolding Sup_flat_complete_lattice_def ``` nipkow@44890 ` 427` ``` by fastforce ``` bulwahn@37918 ` 428` ```next ``` wenzelm@60508 ` 429` ``` fix z :: "'a flat_complete_lattice" ``` wenzelm@60508 ` 430` ``` fix A ``` wenzelm@60509 ` 431` ``` show "Sup A \ z" if z: "\x. x \ A \ x \ z" ``` wenzelm@60509 ` 432` ``` proof - ``` wenzelm@60509 ` 433` ``` consider "A = {} \ A = {Bot}" ``` wenzelm@60509 ` 434` ``` | "A \ {}" "A \ {Bot}" "\v. A - {Bot} = {Value v}" ``` wenzelm@60509 ` 435` ``` | "A \ {}" "A \ {Bot}" "\ (\v. A - {Bot} = {Value v})" ``` wenzelm@60509 ` 436` ``` by blast ``` wenzelm@60509 ` 437` ``` then show ?thesis ``` wenzelm@60509 ` 438` ``` proof cases ``` wenzelm@60509 ` 439` ``` case 1 ``` wenzelm@60509 ` 440` ``` then have "Sup A = Bot" ``` wenzelm@60509 ` 441` ``` unfolding Sup_flat_complete_lattice_def by auto ``` wenzelm@60509 ` 442` ``` then show ?thesis by simp ``` wenzelm@60509 ` 443` ``` next ``` wenzelm@60509 ` 444` ``` case 2 ``` wenzelm@60509 ` 445` ``` then obtain v where v1: "A - {Bot} = {Value v}" ``` bulwahn@37918 ` 446` ``` by auto ``` wenzelm@60509 ` 447` ``` then have v2: "(THE v. A - {Bot} = {Value v}) = v" ``` wenzelm@60509 ` 448` ``` by (auto intro!: the1_equality) ``` wenzelm@60509 ` 449` ``` from 2 v2 have Sup: "Sup A = Value v" ``` wenzelm@60509 ` 450` ``` unfolding Sup_flat_complete_lattice_def by simp ``` wenzelm@60509 ` 451` ``` from v1 have "Value v \ A" by blast ``` wenzelm@60509 ` 452` ``` then have "Value v \ z" by (rule z) ``` wenzelm@60509 ` 453` ``` with Sup show ?thesis by simp ``` bulwahn@37918 ` 454` ``` next ``` wenzelm@60509 ` 455` ``` case 3 ``` wenzelm@60509 ` 456` ``` then have Sup: "Sup A = Top" ``` wenzelm@60509 ` 457` ``` unfolding Sup_flat_complete_lattice_def by auto ``` wenzelm@60509 ` 458` ``` have "Top \ z" ``` wenzelm@60509 ` 459` ``` proof (cases "A - {Bot} = {Top}") ``` wenzelm@60509 ` 460` ``` case True ``` wenzelm@60509 ` 461` ``` then have "Top \ A" by blast ``` wenzelm@60509 ` 462` ``` then show ?thesis by (rule z) ``` wenzelm@60509 ` 463` ``` next ``` wenzelm@60509 ` 464` ``` case False ``` wenzelm@60509 ` 465` ``` from 3 obtain a1 where a1: "a1 \ A - {Bot}" ``` wenzelm@60509 ` 466` ``` by auto ``` wenzelm@60509 ` 467` ``` from 3 False a1 obtain a2 where "a2 \ A - {Bot} \ a1 \ a2" ``` wenzelm@60509 ` 468` ``` by (cases a1) auto ``` wenzelm@60509 ` 469` ``` with a1 z[of "a1"] z[of "a2"] show ?thesis ``` wenzelm@60509 ` 470` ``` apply (cases a1) ``` wenzelm@60509 ` 471` ``` apply auto ``` wenzelm@60509 ` 472` ``` apply (cases a2) ``` wenzelm@60509 ` 473` ``` apply (auto dest!: greater_than_two_values) ``` wenzelm@60509 ` 474` ``` done ``` wenzelm@60509 ` 475` ``` qed ``` wenzelm@60509 ` 476` ``` with Sup show ?thesis by simp ``` bulwahn@37918 ` 477` ``` qed ``` wenzelm@60509 ` 478` ``` qed ``` Andreas@57543 ` 479` ```next ``` Andreas@57543 ` 480` ``` show "Inf {} = (top :: 'a flat_complete_lattice)" ``` wenzelm@60508 ` 481` ``` by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def) ``` Andreas@57543 ` 482` ``` show "Sup {} = (bot :: 'a flat_complete_lattice)" ``` wenzelm@60508 ` 483` ``` by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def) ``` bulwahn@37918 ` 484` ```qed ``` bulwahn@37918 ` 485` bulwahn@37918 ` 486` ```end ``` bulwahn@37918 ` 487` nipkow@62390 ` 488` ```end ```