src/HOL/Complete_Partial_Order.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63979 95c3ae4baba8 child 67399 eab6ce8368fa permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
 wenzelm@63612 ` 1` ```(* Title: HOL/Complete_Partial_Order.thy ``` wenzelm@63612 ` 2` ``` Author: Brian Huffman, Portland State University ``` wenzelm@63612 ` 3` ``` Author: Alexander Krauss, TU Muenchen ``` krauss@40106 ` 4` ```*) ``` krauss@40106 ` 5` wenzelm@60758 ` 6` ```section \Chain-complete partial orders and their fixpoints\ ``` krauss@40106 ` 7` krauss@40106 ` 8` ```theory Complete_Partial_Order ``` wenzelm@63612 ` 9` ``` imports Product_Type ``` krauss@40106 ` 10` ```begin ``` krauss@40106 ` 11` wenzelm@60758 ` 12` ```subsection \Monotone functions\ ``` krauss@40106 ` 13` wenzelm@60758 ` 14` ```text \Dictionary-passing version of @{const Orderings.mono}.\ ``` krauss@40106 ` 15` krauss@40106 ` 16` ```definition monotone :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool" ``` wenzelm@63612 ` 17` ``` where "monotone orda ordb f \ (\x y. orda x y \ ordb (f x) (f y))" ``` krauss@40106 ` 18` wenzelm@63612 ` 19` ```lemma monotoneI[intro?]: "(\x y. orda x y \ ordb (f x) (f y)) \ monotone orda ordb f" ``` wenzelm@63612 ` 20` ``` unfolding monotone_def by iprover ``` krauss@40106 ` 21` krauss@40106 ` 22` ```lemma monotoneD[dest?]: "monotone orda ordb f \ orda x y \ ordb (f x) (f y)" ``` wenzelm@63612 ` 23` ``` unfolding monotone_def by iprover ``` krauss@40106 ` 24` krauss@40106 ` 25` wenzelm@60758 ` 26` ```subsection \Chains\ ``` krauss@40106 ` 27` wenzelm@63612 ` 28` ```text \ ``` wenzelm@63612 ` 29` ``` A chain is a totally-ordered set. Chains are parameterized over ``` krauss@40106 ` 30` ``` the order for maximal flexibility, since type classes are not enough. ``` wenzelm@60758 ` 31` ```\ ``` krauss@40106 ` 32` wenzelm@63612 ` 33` ```definition chain :: "('a \ 'a \ bool) \ 'a set \ bool" ``` wenzelm@63612 ` 34` ``` where "chain ord S \ (\x\S. \y\S. ord x y \ ord y x)" ``` krauss@40106 ` 35` krauss@40106 ` 36` ```lemma chainI: ``` krauss@40106 ` 37` ``` assumes "\x y. x \ S \ y \ S \ ord x y \ ord y x" ``` krauss@40106 ` 38` ``` shows "chain ord S" ``` wenzelm@63612 ` 39` ``` using assms unfolding chain_def by fast ``` krauss@40106 ` 40` krauss@40106 ` 41` ```lemma chainD: ``` krauss@40106 ` 42` ``` assumes "chain ord S" and "x \ S" and "y \ S" ``` krauss@40106 ` 43` ``` shows "ord x y \ ord y x" ``` wenzelm@63612 ` 44` ``` using assms unfolding chain_def by fast ``` krauss@40106 ` 45` krauss@40106 ` 46` ```lemma chainE: ``` krauss@40106 ` 47` ``` assumes "chain ord S" and "x \ S" and "y \ S" ``` krauss@40106 ` 48` ``` obtains "ord x y" | "ord y x" ``` wenzelm@63612 ` 49` ``` using assms unfolding chain_def by fast ``` krauss@40106 ` 50` Andreas@54630 ` 51` ```lemma chain_empty: "chain ord {}" ``` wenzelm@63612 ` 52` ``` by (simp add: chain_def) ``` Andreas@54630 ` 53` Andreas@60057 ` 54` ```lemma chain_equality: "chain op = A \ (\x\A. \y\A. x = y)" ``` wenzelm@63612 ` 55` ``` by (auto simp add: chain_def) ``` wenzelm@63612 ` 56` wenzelm@63612 ` 57` ```lemma chain_subset: "chain ord A \ B \ A \ chain ord B" ``` wenzelm@63612 ` 58` ``` by (rule chainI) (blast dest: chainD) ``` Andreas@60057 ` 59` wenzelm@63612 ` 60` ```lemma chain_imageI: ``` wenzelm@63612 ` 61` ``` assumes chain: "chain le_a Y" ``` wenzelm@63612 ` 62` ``` and mono: "\x y. x \ Y \ y \ Y \ le_a x y \ le_b (f x) (f y)" ``` wenzelm@63612 ` 63` ``` shows "chain le_b (f ` Y)" ``` wenzelm@63612 ` 64` ``` by (blast intro: chainI dest: chainD[OF chain] mono) ``` Andreas@60061 ` 65` Andreas@60061 ` 66` wenzelm@60758 ` 67` ```subsection \Chain-complete partial orders\ ``` krauss@40106 ` 68` wenzelm@60758 ` 69` ```text \ ``` wenzelm@63612 ` 70` ``` A \ccpo\ has a least upper bound for any chain. In particular, the ``` wenzelm@63612 ` 71` ``` empty set is a chain, so every \ccpo\ must have a bottom element. ``` wenzelm@60758 ` 72` ```\ ``` krauss@40106 ` 73` huffman@46041 ` 74` ```class ccpo = order + Sup + ``` wenzelm@63612 ` 75` ``` assumes ccpo_Sup_upper: "chain (op \) A \ x \ A \ x \ Sup A" ``` wenzelm@63612 ` 76` ``` assumes ccpo_Sup_least: "chain (op \) A \ (\x. x \ A \ x \ z) \ Sup A \ z" ``` krauss@40106 ` 77` ```begin ``` krauss@40106 ` 78` Andreas@60061 ` 79` ```lemma chain_singleton: "Complete_Partial_Order.chain op \ {x}" ``` wenzelm@63612 ` 80` ``` by (rule chainI) simp ``` Andreas@60061 ` 81` Andreas@60061 ` 82` ```lemma ccpo_Sup_singleton [simp]: "\{x} = x" ``` wenzelm@63810 ` 83` ``` by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton) ``` wenzelm@63612 ` 84` Andreas@60061 ` 85` wenzelm@60758 ` 86` ```subsection \Transfinite iteration of a function\ ``` krauss@40106 ` 87` wenzelm@63612 ` 88` ```context notes [[inductive_internals]] ``` wenzelm@63612 ` 89` ```begin ``` Andreas@61689 ` 90` krauss@40106 ` 91` ```inductive_set iterates :: "('a \ 'a) \ 'a set" ``` wenzelm@63612 ` 92` ``` for f :: "'a \ 'a" ``` wenzelm@63612 ` 93` ``` where ``` wenzelm@63612 ` 94` ``` step: "x \ iterates f \ f x \ iterates f" ``` wenzelm@63612 ` 95` ``` | Sup: "chain (op \) M \ \x\M. x \ iterates f \ Sup M \ iterates f" ``` krauss@40106 ` 96` Andreas@61689 ` 97` ```end ``` Andreas@61689 ` 98` wenzelm@63612 ` 99` ```lemma iterates_le_f: "x \ iterates f \ monotone (op \) (op \) f \ x \ f x" ``` wenzelm@63612 ` 100` ``` by (induct x rule: iterates.induct) ``` wenzelm@63612 ` 101` ``` (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+ ``` krauss@40106 ` 102` krauss@40106 ` 103` ```lemma chain_iterates: ``` krauss@40106 ` 104` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 105` ``` shows "chain (op \) (iterates f)" (is "chain _ ?C") ``` krauss@40106 ` 106` ```proof (rule chainI) ``` wenzelm@63612 ` 107` ``` fix x y ``` wenzelm@63612 ` 108` ``` assume "x \ ?C" "y \ ?C" ``` krauss@40106 ` 109` ``` then show "x \ y \ y \ x" ``` krauss@40106 ` 110` ``` proof (induct x arbitrary: y rule: iterates.induct) ``` wenzelm@63612 ` 111` ``` fix x y ``` wenzelm@63612 ` 112` ``` assume y: "y \ ?C" ``` wenzelm@63612 ` 113` ``` and IH: "\z. z \ ?C \ x \ z \ z \ x" ``` krauss@40106 ` 114` ``` from y show "f x \ y \ y \ f x" ``` krauss@40106 ` 115` ``` proof (induct y rule: iterates.induct) ``` wenzelm@63612 ` 116` ``` case (step y) ``` wenzelm@63612 ` 117` ``` with IH f show ?case by (auto dest: monotoneD) ``` krauss@40106 ` 118` ``` next ``` huffman@46041 ` 119` ``` case (Sup M) ``` krauss@40106 ` 120` ``` then have chM: "chain (op \) M" ``` krauss@40106 ` 121` ``` and IH': "\z. z \ M \ f x \ z \ z \ f x" by auto ``` huffman@46041 ` 122` ``` show "f x \ Sup M \ Sup M \ f x" ``` krauss@40106 ` 123` ``` proof (cases "\z\M. f x \ z") ``` wenzelm@63612 ` 124` ``` case True ``` wenzelm@63612 ` 125` ``` then have "f x \ Sup M" ``` krauss@40106 ` 126` ``` apply rule ``` krauss@40106 ` 127` ``` apply (erule order_trans) ``` wenzelm@63612 ` 128` ``` apply (rule ccpo_Sup_upper[OF chM]) ``` wenzelm@63612 ` 129` ``` apply assumption ``` wenzelm@63612 ` 130` ``` done ``` wenzelm@63612 ` 131` ``` then show ?thesis .. ``` krauss@40106 ` 132` ``` next ``` wenzelm@63612 ` 133` ``` case False ``` wenzelm@63612 ` 134` ``` with IH' show ?thesis ``` wenzelm@63612 ` 135` ``` by (auto intro: ccpo_Sup_least[OF chM]) ``` krauss@40106 ` 136` ``` qed ``` krauss@40106 ` 137` ``` qed ``` krauss@40106 ` 138` ``` next ``` huffman@46041 ` 139` ``` case (Sup M y) ``` krauss@40106 ` 140` ``` show ?case ``` krauss@40106 ` 141` ``` proof (cases "\x\M. y \ x") ``` wenzelm@63612 ` 142` ``` case True ``` wenzelm@63612 ` 143` ``` then have "y \ Sup M" ``` krauss@40106 ` 144` ``` apply rule ``` krauss@40106 ` 145` ``` apply (erule order_trans) ``` wenzelm@63612 ` 146` ``` apply (rule ccpo_Sup_upper[OF Sup(1)]) ``` wenzelm@63612 ` 147` ``` apply assumption ``` wenzelm@63612 ` 148` ``` done ``` wenzelm@63612 ` 149` ``` then show ?thesis .. ``` krauss@40106 ` 150` ``` next ``` huffman@46041 ` 151` ``` case False with Sup ``` huffman@46041 ` 152` ``` show ?thesis by (auto intro: ccpo_Sup_least) ``` krauss@40106 ` 153` ``` qed ``` krauss@40106 ` 154` ``` qed ``` krauss@40106 ` 155` ```qed ``` krauss@40106 ` 156` Andreas@54630 ` 157` ```lemma bot_in_iterates: "Sup {} \ iterates f" ``` wenzelm@63612 ` 158` ``` by (auto intro: iterates.Sup simp add: chain_empty) ``` wenzelm@63612 ` 159` Andreas@54630 ` 160` wenzelm@60758 ` 161` ```subsection \Fixpoint combinator\ ``` krauss@40106 ` 162` wenzelm@63612 ` 163` ```definition fixp :: "('a \ 'a) \ 'a" ``` wenzelm@63612 ` 164` ``` where "fixp f = Sup (iterates f)" ``` krauss@40106 ` 165` krauss@40106 ` 166` ```lemma iterates_fixp: ``` wenzelm@63612 ` 167` ``` assumes f: "monotone (op \) (op \) f" ``` wenzelm@63612 ` 168` ``` shows "fixp f \ iterates f" ``` wenzelm@63612 ` 169` ``` unfolding fixp_def ``` wenzelm@63612 ` 170` ``` by (simp add: iterates.Sup chain_iterates f) ``` krauss@40106 ` 171` krauss@40106 ` 172` ```lemma fixp_unfold: ``` krauss@40106 ` 173` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 174` ``` shows "fixp f = f (fixp f)" ``` krauss@40106 ` 175` ```proof (rule antisym) ``` krauss@40106 ` 176` ``` show "fixp f \ f (fixp f)" ``` krauss@40106 ` 177` ``` by (intro iterates_le_f iterates_fixp f) ``` huffman@46041 ` 178` ``` have "f (fixp f) \ Sup (iterates f)" ``` huffman@46041 ` 179` ``` by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp) ``` wenzelm@63612 ` 180` ``` then show "f (fixp f) \ fixp f" ``` wenzelm@63612 ` 181` ``` by (simp only: fixp_def) ``` krauss@40106 ` 182` ```qed ``` krauss@40106 ` 183` krauss@40106 ` 184` ```lemma fixp_lowerbound: ``` wenzelm@63612 ` 185` ``` assumes f: "monotone (op \) (op \) f" ``` wenzelm@63612 ` 186` ``` and z: "f z \ z" ``` wenzelm@63612 ` 187` ``` shows "fixp f \ z" ``` wenzelm@63612 ` 188` ``` unfolding fixp_def ``` huffman@46041 ` 189` ```proof (rule ccpo_Sup_least[OF chain_iterates[OF f]]) ``` wenzelm@63612 ` 190` ``` fix x ``` wenzelm@63612 ` 191` ``` assume "x \ iterates f" ``` wenzelm@63612 ` 192` ``` then show "x \ z" ``` krauss@40106 ` 193` ``` proof (induct x rule: iterates.induct) ``` wenzelm@63612 ` 194` ``` case (step x) ``` wenzelm@63612 ` 195` ``` from f \x \ z\ have "f x \ f z" by (rule monotoneD) ``` wenzelm@63612 ` 196` ``` also note z ``` wenzelm@63612 ` 197` ``` finally show "f x \ z" . ``` wenzelm@63612 ` 198` ``` next ``` wenzelm@63612 ` 199` ``` case (Sup M) ``` wenzelm@63612 ` 200` ``` then show ?case ``` wenzelm@63612 ` 201` ``` by (auto intro: ccpo_Sup_least) ``` wenzelm@63612 ` 202` ``` qed ``` krauss@40106 ` 203` ```qed ``` krauss@40106 ` 204` Andreas@53361 ` 205` ```end ``` krauss@40106 ` 206` wenzelm@63612 ` 207` wenzelm@60758 ` 208` ```subsection \Fixpoint induction\ ``` krauss@40106 ` 209` wenzelm@60758 ` 210` ```setup \Sign.map_naming (Name_Space.mandatory_path "ccpo")\ ``` Andreas@53361 ` 211` Andreas@53361 ` 212` ```definition admissible :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('a \ bool) \ bool" ``` wenzelm@63612 ` 213` ``` where "admissible lub ord P \ (\A. chain ord A \ A \ {} \ (\x\A. P x) \ P (lub A))" ``` krauss@40106 ` 214` krauss@40106 ` 215` ```lemma admissibleI: ``` Andreas@54630 ` 216` ``` assumes "\A. chain ord A \ A \ {} \ \x\A. P x \ P (lub A)" ``` Andreas@53361 ` 217` ``` shows "ccpo.admissible lub ord P" ``` wenzelm@63612 ` 218` ``` using assms unfolding ccpo.admissible_def by fast ``` krauss@40106 ` 219` krauss@40106 ` 220` ```lemma admissibleD: ``` Andreas@53361 ` 221` ``` assumes "ccpo.admissible lub ord P" ``` Andreas@53361 ` 222` ``` assumes "chain ord A" ``` Andreas@54630 ` 223` ``` assumes "A \ {}" ``` krauss@40106 ` 224` ``` assumes "\x. x \ A \ P x" ``` Andreas@53361 ` 225` ``` shows "P (lub A)" ``` wenzelm@63612 ` 226` ``` using assms by (auto simp: ccpo.admissible_def) ``` krauss@40106 ` 227` wenzelm@60758 ` 228` ```setup \Sign.map_naming Name_Space.parent_path\ ``` Andreas@53361 ` 229` Andreas@53361 ` 230` ```lemma (in ccpo) fixp_induct: ``` Andreas@53361 ` 231` ``` assumes adm: "ccpo.admissible Sup (op \) P" ``` krauss@40106 ` 232` ``` assumes mono: "monotone (op \) (op \) f" ``` Andreas@54630 ` 233` ``` assumes bot: "P (Sup {})" ``` krauss@40106 ` 234` ``` assumes step: "\x. P x \ P (f x)" ``` krauss@40106 ` 235` ``` shows "P (fixp f)" ``` wenzelm@63612 ` 236` ``` unfolding fixp_def ``` wenzelm@63612 ` 237` ``` using adm chain_iterates[OF mono] ``` Andreas@53361 ` 238` ```proof (rule ccpo.admissibleD) ``` wenzelm@63612 ` 239` ``` show "iterates f \ {}" ``` wenzelm@63612 ` 240` ``` using bot_in_iterates by auto ``` wenzelm@63612 ` 241` ```next ``` wenzelm@63612 ` 242` ``` fix x ``` wenzelm@63612 ` 243` ``` assume "x \ iterates f" ``` wenzelm@63612 ` 244` ``` then show "P x" ``` wenzelm@63612 ` 245` ``` proof (induct rule: iterates.induct) ``` wenzelm@63612 ` 246` ``` case prems: (step x) ``` wenzelm@63612 ` 247` ``` from this(2) show ?case by (rule step) ``` wenzelm@63612 ` 248` ``` next ``` wenzelm@63612 ` 249` ``` case (Sup M) ``` wenzelm@63612 ` 250` ``` then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm) ``` wenzelm@63612 ` 251` ``` qed ``` krauss@40106 ` 252` ```qed ``` krauss@40106 ` 253` Andreas@53361 ` 254` ```lemma admissible_True: "ccpo.admissible lub ord (\x. True)" ``` wenzelm@63612 ` 255` ``` unfolding ccpo.admissible_def by simp ``` krauss@40106 ` 256` Andreas@54630 ` 257` ```(*lemma admissible_False: "\ ccpo.admissible lub ord (\x. False)" ``` Andreas@53361 ` 258` ```unfolding ccpo.admissible_def chain_def by simp ``` Andreas@54630 ` 259` ```*) ``` Andreas@54630 ` 260` ```lemma admissible_const: "ccpo.admissible lub ord (\x. t)" ``` wenzelm@63612 ` 261` ``` by (auto intro: ccpo.admissibleI) ``` krauss@40106 ` 262` krauss@40106 ` 263` ```lemma admissible_conj: ``` Andreas@53361 ` 264` ``` assumes "ccpo.admissible lub ord (\x. P x)" ``` Andreas@53361 ` 265` ``` assumes "ccpo.admissible lub ord (\x. Q x)" ``` Andreas@53361 ` 266` ``` shows "ccpo.admissible lub ord (\x. P x \ Q x)" ``` wenzelm@63612 ` 267` ``` using assms unfolding ccpo.admissible_def by simp ``` krauss@40106 ` 268` krauss@40106 ` 269` ```lemma admissible_all: ``` Andreas@53361 ` 270` ``` assumes "\y. ccpo.admissible lub ord (\x. P x y)" ``` Andreas@53361 ` 271` ``` shows "ccpo.admissible lub ord (\x. \y. P x y)" ``` wenzelm@63612 ` 272` ``` using assms unfolding ccpo.admissible_def by fast ``` krauss@40106 ` 273` krauss@40106 ` 274` ```lemma admissible_ball: ``` Andreas@53361 ` 275` ``` assumes "\y. y \ A \ ccpo.admissible lub ord (\x. P x y)" ``` Andreas@53361 ` 276` ``` shows "ccpo.admissible lub ord (\x. \y\A. P x y)" ``` wenzelm@63612 ` 277` ``` using assms unfolding ccpo.admissible_def by fast ``` krauss@40106 ` 278` Andreas@53361 ` 279` ```lemma chain_compr: "chain ord A \ chain ord {x \ A. P x}" ``` wenzelm@63612 ` 280` ``` unfolding chain_def by fast ``` krauss@40106 ` 281` wenzelm@63612 ` 282` ```context ccpo ``` wenzelm@63612 ` 283` ```begin ``` Andreas@53361 ` 284` krauss@40106 ` 285` ```lemma admissible_disj: ``` krauss@40106 ` 286` ``` fixes P Q :: "'a \ bool" ``` Andreas@53361 ` 287` ``` assumes P: "ccpo.admissible Sup (op \) (\x. P x)" ``` Andreas@53361 ` 288` ``` assumes Q: "ccpo.admissible Sup (op \) (\x. Q x)" ``` Andreas@53361 ` 289` ``` shows "ccpo.admissible Sup (op \) (\x. P x \ Q x)" ``` Andreas@53361 ` 290` ```proof (rule ccpo.admissibleI) ``` wenzelm@63612 ` 291` ``` fix A :: "'a set" ``` wenzelm@63810 ` 292` ``` assume chain: "chain (op \) A" ``` wenzelm@63810 ` 293` ``` assume A: "A \ {}" and P_Q: "\x\A. P x \ Q x" ``` wenzelm@63810 ` 294` ``` have "(\x\A. P x) \ (\x\A. \y\A. x \ y \ P y) \ (\x\A. Q x) \ (\x\A. \y\A. x \ y \ Q y)" ``` wenzelm@63810 ` 295` ``` (is "?P \ ?Q" is "?P1 \ ?P2 \ _") ``` wenzelm@63810 ` 296` ``` proof (rule disjCI) ``` wenzelm@63810 ` 297` ``` assume "\ ?Q" ``` wenzelm@63810 ` 298` ``` then consider "\x\A. \ Q x" | a where "a \ A" "\y\A. a \ y \ \ Q y" ``` wenzelm@63810 ` 299` ``` by blast ``` wenzelm@63810 ` 300` ``` then show ?P ``` wenzelm@63810 ` 301` ``` proof cases ``` wenzelm@63810 ` 302` ``` case 1 ``` wenzelm@63810 ` 303` ``` with P_Q have "\x\A. P x" by blast ``` wenzelm@63810 ` 304` ``` with A show ?P by blast ``` wenzelm@63810 ` 305` ``` next ``` wenzelm@63810 ` 306` ``` case 2 ``` wenzelm@63810 ` 307` ``` note a = \a \ A\ ``` wenzelm@63810 ` 308` ``` show ?P ``` wenzelm@63810 ` 309` ``` proof ``` wenzelm@63810 ` 310` ``` from P_Q 2 have *: "\y\A. a \ y \ P y" by blast ``` wenzelm@63810 ` 311` ``` with a have "P a" by blast ``` wenzelm@63810 ` 312` ``` with a show ?P1 by blast ``` wenzelm@63810 ` 313` ``` show ?P2 ``` wenzelm@63810 ` 314` ``` proof ``` wenzelm@63810 ` 315` ``` fix x ``` wenzelm@63810 ` 316` ``` assume x: "x \ A" ``` wenzelm@63810 ` 317` ``` with chain a show "\y\A. x \ y \ P y" ``` wenzelm@63810 ` 318` ``` proof (rule chainE) ``` wenzelm@63810 ` 319` ``` assume le: "a \ x" ``` wenzelm@63810 ` 320` ``` with * a x have "P x" by blast ``` wenzelm@63810 ` 321` ``` with x le show ?thesis by blast ``` wenzelm@63810 ` 322` ``` next ``` wenzelm@63810 ` 323` ``` assume "a \ x" ``` wenzelm@63810 ` 324` ``` with a \P a\ show ?thesis by blast ``` wenzelm@63810 ` 325` ``` qed ``` wenzelm@63810 ` 326` ``` qed ``` wenzelm@63810 ` 327` ``` qed ``` wenzelm@63810 ` 328` ``` qed ``` wenzelm@63810 ` 329` ``` qed ``` wenzelm@63810 ` 330` ``` moreover ``` wenzelm@63810 ` 331` ``` have "Sup A = Sup {x \ A. P x}" if "\x\A. \y\A. x \ y \ P y" for P ``` wenzelm@63810 ` 332` ``` proof (rule antisym) ``` wenzelm@63810 ` 333` ``` have chain_P: "chain (op \) {x \ A. P x}" ``` wenzelm@63810 ` 334` ``` by (rule chain_compr [OF chain]) ``` wenzelm@63810 ` 335` ``` show "Sup A \ Sup {x \ A. P x}" ``` wenzelm@63810 ` 336` ``` apply (rule ccpo_Sup_least [OF chain]) ``` wenzelm@63810 ` 337` ``` apply (drule that [rule_format]) ``` wenzelm@63810 ` 338` ``` apply clarify ``` wenzelm@63810 ` 339` ``` apply (erule order_trans) ``` wenzelm@63810 ` 340` ``` apply (simp add: ccpo_Sup_upper [OF chain_P]) ``` wenzelm@63810 ` 341` ``` done ``` wenzelm@63810 ` 342` ``` show "Sup {x \ A. P x} \ Sup A" ``` wenzelm@63810 ` 343` ``` apply (rule ccpo_Sup_least [OF chain_P]) ``` wenzelm@63810 ` 344` ``` apply clarify ``` wenzelm@63810 ` 345` ``` apply (simp add: ccpo_Sup_upper [OF chain]) ``` wenzelm@63810 ` 346` ``` done ``` wenzelm@63810 ` 347` ``` qed ``` wenzelm@63810 ` 348` ``` ultimately ``` wenzelm@63810 ` 349` ``` consider "\x. x \ A \ P x" "Sup A = Sup {x \ A. P x}" ``` wenzelm@63810 ` 350` ``` | "\x. x \ A \ Q x" "Sup A = Sup {x \ A. Q x}" ``` wenzelm@63810 ` 351` ``` by blast ``` wenzelm@63612 ` 352` ``` then show "P (Sup A) \ Q (Sup A)" ``` wenzelm@63810 ` 353` ``` apply cases ``` wenzelm@63612 ` 354` ``` apply simp_all ``` wenzelm@63612 ` 355` ``` apply (rule disjI1) ``` wenzelm@63810 ` 356` ``` apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp) ``` wenzelm@63612 ` 357` ``` apply (rule disjI2) ``` wenzelm@63810 ` 358` ``` apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp) ``` krauss@40106 ` 359` ``` done ``` krauss@40106 ` 360` ```qed ``` krauss@40106 ` 361` krauss@40106 ` 362` ```end ``` krauss@40106 ` 363` huffman@46041 ` 364` ```instance complete_lattice \ ccpo ``` wenzelm@61169 ` 365` ``` by standard (fast intro: Sup_upper Sup_least)+ ``` huffman@46041 ` 366` huffman@46041 ` 367` ```lemma lfp_eq_fixp: ``` wenzelm@63979 ` 368` ``` assumes mono: "mono f" ``` wenzelm@63612 ` 369` ``` shows "lfp f = fixp f" ``` huffman@46041 ` 370` ```proof (rule antisym) ``` wenzelm@63979 ` 371` ``` from mono have f': "monotone (op \) (op \) f" ``` huffman@46041 ` 372` ``` unfolding mono_def monotone_def . ``` huffman@46041 ` 373` ``` show "lfp f \ fixp f" ``` huffman@46041 ` 374` ``` by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl) ``` huffman@46041 ` 375` ``` show "fixp f \ lfp f" ``` wenzelm@63979 ` 376` ``` by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono]) ``` huffman@46041 ` 377` ```qed ``` huffman@46041 ` 378` Andreas@53361 ` 379` ```hide_const (open) iterates fixp ``` krauss@40106 ` 380` krauss@40106 ` 381` ```end ```