src/HOL/Complete_Partial_Order.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 40252 029400b6c893 child 46041 1e3ff542e83e permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
 krauss@40106 ` 1` ```(* Title: HOL/Complete_Partial_Order.thy ``` krauss@40106 ` 2` ``` Author: Brian Huffman, Portland State University ``` krauss@40106 ` 3` ``` Author: Alexander Krauss, TU Muenchen ``` krauss@40106 ` 4` ```*) ``` krauss@40106 ` 5` krauss@40106 ` 6` ```header {* Chain-complete partial orders and their fixpoints *} ``` krauss@40106 ` 7` krauss@40106 ` 8` ```theory Complete_Partial_Order ``` krauss@40106 ` 9` ```imports Product_Type ``` krauss@40106 ` 10` ```begin ``` krauss@40106 ` 11` krauss@40106 ` 12` ```subsection {* Monotone functions *} ``` krauss@40106 ` 13` krauss@40106 ` 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" ``` krauss@40106 ` 17` ```where "monotone orda ordb f \ (\x y. orda x y \ ordb (f x) (f y))" ``` krauss@40106 ` 18` krauss@40106 ` 19` ```lemma monotoneI[intro?]: "(\x y. orda x y \ ordb (f x) (f y)) ``` krauss@40106 ` 20` ``` \ monotone orda ordb f" ``` krauss@40106 ` 21` ```unfolding monotone_def by iprover ``` krauss@40106 ` 22` krauss@40106 ` 23` ```lemma monotoneD[dest?]: "monotone orda ordb f \ orda x y \ ordb (f x) (f y)" ``` krauss@40106 ` 24` ```unfolding monotone_def by iprover ``` krauss@40106 ` 25` krauss@40106 ` 26` krauss@40106 ` 27` ```subsection {* Chains *} ``` krauss@40106 ` 28` krauss@40106 ` 29` ```text {* 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. ``` krauss@40106 ` 31` ```*} ``` krauss@40106 ` 32` krauss@40106 ` 33` ```definition ``` krauss@40106 ` 34` ``` chain :: "('a \ 'a \ bool) \ 'a set \ bool" ``` krauss@40106 ` 35` ```where ``` krauss@40106 ` 36` ``` "chain ord S \ (\x\S. \y\S. ord x y \ ord y x)" ``` krauss@40106 ` 37` krauss@40106 ` 38` ```lemma chainI: ``` krauss@40106 ` 39` ``` assumes "\x y. x \ S \ y \ S \ ord x y \ ord y x" ``` krauss@40106 ` 40` ``` shows "chain ord S" ``` krauss@40106 ` 41` ```using assms unfolding chain_def by fast ``` krauss@40106 ` 42` krauss@40106 ` 43` ```lemma chainD: ``` krauss@40106 ` 44` ``` assumes "chain ord S" and "x \ S" and "y \ S" ``` krauss@40106 ` 45` ``` shows "ord x y \ ord y x" ``` krauss@40106 ` 46` ```using assms unfolding chain_def by fast ``` krauss@40106 ` 47` krauss@40106 ` 48` ```lemma chainE: ``` krauss@40106 ` 49` ``` assumes "chain ord S" and "x \ S" and "y \ S" ``` krauss@40106 ` 50` ``` obtains "ord x y" | "ord y x" ``` krauss@40106 ` 51` ```using assms unfolding chain_def by fast ``` krauss@40106 ` 52` krauss@40106 ` 53` ```subsection {* Chain-complete partial orders *} ``` krauss@40106 ` 54` krauss@40106 ` 55` ```text {* ``` krauss@40106 ` 56` ``` A ccpo has a least upper bound for any chain. In particular, the ``` krauss@40106 ` 57` ``` empty set is a chain, so every ccpo must have a bottom element. ``` krauss@40106 ` 58` ```*} ``` krauss@40106 ` 59` krauss@40106 ` 60` ```class ccpo = order + ``` krauss@40106 ` 61` ``` fixes lub :: "'a set \ 'a" ``` krauss@40106 ` 62` ``` assumes lub_upper: "chain (op \) A \ x \ A \ x \ lub A" ``` krauss@40106 ` 63` ``` assumes lub_least: "chain (op \) A \ (\x. x \ A \ x \ z) \ lub A \ z" ``` krauss@40106 ` 64` ```begin ``` krauss@40106 ` 65` krauss@40106 ` 66` ```subsection {* Transfinite iteration of a function *} ``` krauss@40106 ` 67` krauss@40106 ` 68` ```inductive_set iterates :: "('a \ 'a) \ 'a set" ``` krauss@40106 ` 69` ```for f :: "'a \ 'a" ``` krauss@40106 ` 70` ```where ``` krauss@40106 ` 71` ``` step: "x \ iterates f \ f x \ iterates f" ``` krauss@40106 ` 72` ```| lub: "chain (op \) M \ \x\M. x \ iterates f \ lub M \ iterates f" ``` krauss@40106 ` 73` krauss@40106 ` 74` ```lemma iterates_le_f: ``` krauss@40106 ` 75` ``` "x \ iterates f \ monotone (op \) (op \) f \ x \ f x" ``` krauss@40106 ` 76` ```by (induct x rule: iterates.induct) ``` krauss@40106 ` 77` ``` (force dest: monotoneD intro!: lub_upper lub_least)+ ``` krauss@40106 ` 78` krauss@40106 ` 79` ```lemma chain_iterates: ``` krauss@40106 ` 80` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 81` ``` shows "chain (op \) (iterates f)" (is "chain _ ?C") ``` krauss@40106 ` 82` ```proof (rule chainI) ``` krauss@40106 ` 83` ``` fix x y assume "x \ ?C" "y \ ?C" ``` krauss@40106 ` 84` ``` then show "x \ y \ y \ x" ``` krauss@40106 ` 85` ``` proof (induct x arbitrary: y rule: iterates.induct) ``` krauss@40106 ` 86` ``` fix x y assume y: "y \ ?C" ``` krauss@40106 ` 87` ``` and IH: "\z. z \ ?C \ x \ z \ z \ x" ``` krauss@40106 ` 88` ``` from y show "f x \ y \ y \ f x" ``` krauss@40106 ` 89` ``` proof (induct y rule: iterates.induct) ``` krauss@40106 ` 90` ``` case (step y) with IH f show ?case by (auto dest: monotoneD) ``` krauss@40106 ` 91` ``` next ``` krauss@40106 ` 92` ``` case (lub M) ``` krauss@40106 ` 93` ``` then have chM: "chain (op \) M" ``` krauss@40106 ` 94` ``` and IH': "\z. z \ M \ f x \ z \ z \ f x" by auto ``` krauss@40106 ` 95` ``` show "f x \ lub M \ lub M \ f x" ``` krauss@40106 ` 96` ``` proof (cases "\z\M. f x \ z") ``` krauss@40106 ` 97` ``` case True then have "f x \ lub M" ``` krauss@40106 ` 98` ``` apply rule ``` krauss@40106 ` 99` ``` apply (erule order_trans) ``` krauss@40106 ` 100` ``` by (rule lub_upper[OF chM]) ``` krauss@40106 ` 101` ``` thus ?thesis .. ``` krauss@40106 ` 102` ``` next ``` krauss@40106 ` 103` ``` case False with IH' ``` krauss@40106 ` 104` ``` show ?thesis by (auto intro: lub_least[OF chM]) ``` krauss@40106 ` 105` ``` qed ``` krauss@40106 ` 106` ``` qed ``` krauss@40106 ` 107` ``` next ``` krauss@40106 ` 108` ``` case (lub M y) ``` krauss@40106 ` 109` ``` show ?case ``` krauss@40106 ` 110` ``` proof (cases "\x\M. y \ x") ``` krauss@40106 ` 111` ``` case True then have "y \ lub M" ``` krauss@40106 ` 112` ``` apply rule ``` krauss@40106 ` 113` ``` apply (erule order_trans) ``` krauss@40106 ` 114` ``` by (rule lub_upper[OF lub(1)]) ``` krauss@40106 ` 115` ``` thus ?thesis .. ``` krauss@40106 ` 116` ``` next ``` krauss@40106 ` 117` ``` case False with lub ``` krauss@40106 ` 118` ``` show ?thesis by (auto intro: lub_least) ``` krauss@40106 ` 119` ``` qed ``` krauss@40106 ` 120` ``` qed ``` krauss@40106 ` 121` ```qed ``` krauss@40106 ` 122` krauss@40106 ` 123` ```subsection {* Fixpoint combinator *} ``` krauss@40106 ` 124` krauss@40106 ` 125` ```definition ``` krauss@40106 ` 126` ``` fixp :: "('a \ 'a) \ 'a" ``` krauss@40106 ` 127` ```where ``` krauss@40106 ` 128` ``` "fixp f = lub (iterates f)" ``` krauss@40106 ` 129` krauss@40106 ` 130` ```lemma iterates_fixp: ``` krauss@40106 ` 131` ``` assumes f: "monotone (op \) (op \) f" shows "fixp f \ iterates f" ``` krauss@40106 ` 132` ```unfolding fixp_def ``` krauss@40106 ` 133` ```by (simp add: iterates.lub chain_iterates f) ``` krauss@40106 ` 134` krauss@40106 ` 135` ```lemma fixp_unfold: ``` krauss@40106 ` 136` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 137` ``` shows "fixp f = f (fixp f)" ``` krauss@40106 ` 138` ```proof (rule antisym) ``` krauss@40106 ` 139` ``` show "fixp f \ f (fixp f)" ``` krauss@40106 ` 140` ``` by (intro iterates_le_f iterates_fixp f) ``` krauss@40106 ` 141` ``` have "f (fixp f) \ lub (iterates f)" ``` krauss@40106 ` 142` ``` by (intro lub_upper chain_iterates f iterates.step iterates_fixp) ``` krauss@40106 ` 143` ``` thus "f (fixp f) \ fixp f" ``` krauss@40106 ` 144` ``` unfolding fixp_def . ``` krauss@40106 ` 145` ```qed ``` krauss@40106 ` 146` krauss@40106 ` 147` ```lemma fixp_lowerbound: ``` krauss@40106 ` 148` ``` assumes f: "monotone (op \) (op \) f" and z: "f z \ z" shows "fixp f \ z" ``` krauss@40106 ` 149` ```unfolding fixp_def ``` krauss@40106 ` 150` ```proof (rule lub_least[OF chain_iterates[OF f]]) ``` krauss@40106 ` 151` ``` fix x assume "x \ iterates f" ``` krauss@40106 ` 152` ``` thus "x \ z" ``` krauss@40106 ` 153` ``` proof (induct x rule: iterates.induct) ``` krauss@40106 ` 154` ``` fix x assume "x \ z" with f have "f x \ f z" by (rule monotoneD) ``` krauss@40106 ` 155` ``` also note z finally show "f x \ z" . ``` krauss@40106 ` 156` ``` qed (auto intro: lub_least) ``` krauss@40106 ` 157` ```qed ``` krauss@40106 ` 158` krauss@40106 ` 159` krauss@40106 ` 160` ```subsection {* Fixpoint induction *} ``` krauss@40106 ` 161` krauss@40106 ` 162` ```definition ``` krauss@40106 ` 163` ``` admissible :: "('a \ bool) \ bool" ``` krauss@40106 ` 164` ```where ``` krauss@40106 ` 165` ``` "admissible P = (\A. chain (op \) A \ (\x\A. P x) \ P (lub A))" ``` krauss@40106 ` 166` krauss@40106 ` 167` ```lemma admissibleI: ``` krauss@40106 ` 168` ``` assumes "\A. chain (op \) A \ \x\A. P x \ P (lub A)" ``` krauss@40106 ` 169` ``` shows "admissible P" ``` krauss@40106 ` 170` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 171` krauss@40106 ` 172` ```lemma admissibleD: ``` krauss@40106 ` 173` ``` assumes "admissible P" ``` krauss@40106 ` 174` ``` assumes "chain (op \) A" ``` krauss@40106 ` 175` ``` assumes "\x. x \ A \ P x" ``` krauss@40106 ` 176` ``` shows "P (lub A)" ``` krauss@40106 ` 177` ```using assms by (auto simp: admissible_def) ``` krauss@40106 ` 178` krauss@40106 ` 179` ```lemma fixp_induct: ``` krauss@40106 ` 180` ``` assumes adm: "admissible P" ``` krauss@40106 ` 181` ``` assumes mono: "monotone (op \) (op \) f" ``` krauss@40106 ` 182` ``` assumes step: "\x. P x \ P (f x)" ``` krauss@40106 ` 183` ``` shows "P (fixp f)" ``` krauss@40106 ` 184` ```unfolding fixp_def using adm chain_iterates[OF mono] ``` krauss@40106 ` 185` ```proof (rule admissibleD) ``` krauss@40106 ` 186` ``` fix x assume "x \ iterates f" ``` krauss@40106 ` 187` ``` thus "P x" ``` krauss@40106 ` 188` ``` by (induct rule: iterates.induct) ``` krauss@40106 ` 189` ``` (auto intro: step admissibleD adm) ``` krauss@40106 ` 190` ```qed ``` krauss@40106 ` 191` krauss@40106 ` 192` ```lemma admissible_True: "admissible (\x. True)" ``` krauss@40106 ` 193` ```unfolding admissible_def by simp ``` krauss@40106 ` 194` krauss@40106 ` 195` ```lemma admissible_False: "\ admissible (\x. False)" ``` krauss@40106 ` 196` ```unfolding admissible_def chain_def by simp ``` krauss@40106 ` 197` krauss@40106 ` 198` ```lemma admissible_const: "admissible (\x. t) = t" ``` krauss@40106 ` 199` ```by (cases t, simp_all add: admissible_True admissible_False) ``` krauss@40106 ` 200` krauss@40106 ` 201` ```lemma admissible_conj: ``` krauss@40106 ` 202` ``` assumes "admissible (\x. P x)" ``` krauss@40106 ` 203` ``` assumes "admissible (\x. Q x)" ``` krauss@40106 ` 204` ``` shows "admissible (\x. P x \ Q x)" ``` krauss@40106 ` 205` ```using assms unfolding admissible_def by simp ``` krauss@40106 ` 206` krauss@40106 ` 207` ```lemma admissible_all: ``` krauss@40106 ` 208` ``` assumes "\y. admissible (\x. P x y)" ``` krauss@40106 ` 209` ``` shows "admissible (\x. \y. P x y)" ``` krauss@40106 ` 210` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 211` krauss@40106 ` 212` ```lemma admissible_ball: ``` krauss@40106 ` 213` ``` assumes "\y. y \ A \ admissible (\x. P x y)" ``` krauss@40106 ` 214` ``` shows "admissible (\x. \y\A. P x y)" ``` krauss@40106 ` 215` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 216` krauss@40106 ` 217` ```lemma chain_compr: "chain (op \) A \ chain (op \) {x \ A. P x}" ``` krauss@40106 ` 218` ```unfolding chain_def by fast ``` krauss@40106 ` 219` krauss@40106 ` 220` ```lemma admissible_disj_lemma: ``` krauss@40106 ` 221` ``` assumes A: "chain (op \)A" ``` krauss@40106 ` 222` ``` assumes P: "\x\A. \y\A. x \ y \ P y" ``` krauss@40106 ` 223` ``` shows "lub A = lub {x \ A. P x}" ``` krauss@40106 ` 224` ```proof (rule antisym) ``` krauss@40106 ` 225` ``` have *: "chain (op \) {x \ A. P x}" ``` krauss@40106 ` 226` ``` by (rule chain_compr [OF A]) ``` krauss@40106 ` 227` ``` show "lub A \ lub {x \ A. P x}" ``` krauss@40106 ` 228` ``` apply (rule lub_least [OF A]) ``` krauss@40106 ` 229` ``` apply (drule P [rule_format], clarify) ``` krauss@40106 ` 230` ``` apply (erule order_trans) ``` krauss@40106 ` 231` ``` apply (simp add: lub_upper [OF *]) ``` krauss@40106 ` 232` ``` done ``` krauss@40106 ` 233` ``` show "lub {x \ A. P x} \ lub A" ``` krauss@40106 ` 234` ``` apply (rule lub_least [OF *]) ``` krauss@40106 ` 235` ``` apply clarify ``` krauss@40106 ` 236` ``` apply (simp add: lub_upper [OF A]) ``` krauss@40106 ` 237` ``` done ``` krauss@40106 ` 238` ```qed ``` krauss@40106 ` 239` krauss@40106 ` 240` ```lemma admissible_disj: ``` krauss@40106 ` 241` ``` fixes P Q :: "'a \ bool" ``` krauss@40106 ` 242` ``` assumes P: "admissible (\x. P x)" ``` krauss@40106 ` 243` ``` assumes Q: "admissible (\x. Q x)" ``` krauss@40106 ` 244` ``` shows "admissible (\x. P x \ Q x)" ``` krauss@40106 ` 245` ```proof (rule admissibleI) ``` krauss@40106 ` 246` ``` fix A :: "'a set" assume A: "chain (op \) A" ``` krauss@40106 ` 247` ``` assume "\x\A. P x \ Q x" ``` krauss@40106 ` 248` ``` hence "(\x\A. \y\A. x \ y \ P y) \ (\x\A. \y\A. x \ y \ Q y)" ``` krauss@40106 ` 249` ``` using chainD[OF A] by blast ``` krauss@40106 ` 250` ``` hence "lub A = lub {x \ A. P x} \ lub A = lub {x \ A. Q x}" ``` krauss@40106 ` 251` ``` using admissible_disj_lemma [OF A] by fast ``` krauss@40106 ` 252` ``` thus "P (lub A) \ Q (lub A)" ``` krauss@40106 ` 253` ``` apply (rule disjE, simp_all) ``` krauss@40106 ` 254` ``` apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp) ``` krauss@40106 ` 255` ``` apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp) ``` krauss@40106 ` 256` ``` done ``` krauss@40106 ` 257` ```qed ``` krauss@40106 ` 258` krauss@40106 ` 259` ```end ``` krauss@40106 ` 260` krauss@40252 ` 261` ```hide_const (open) lub iterates fixp admissible ``` krauss@40106 ` 262` krauss@40106 ` 263` ```end ```