src/HOL/Complete_Partial_Order.thy
 author huffman Thu Dec 29 18:54:07 2011 +0100 (2011-12-29) changeset 46041 1e3ff542e83e parent 40252 029400b6c893 child 53361 1cb7d3c0cf31 permissions -rw-r--r--
remove constant 'ccpo.lub', re-use constant 'Sup' instead
 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` huffman@46041 ` 60` ```class ccpo = order + Sup + ``` huffman@46041 ` 61` ``` assumes ccpo_Sup_upper: "\chain (op \) A; x \ A\ \ x \ Sup A" ``` huffman@46041 ` 62` ``` assumes ccpo_Sup_least: "\chain (op \) A; \x. x \ A \ x \ z\ \ Sup A \ z" ``` krauss@40106 ` 63` ```begin ``` krauss@40106 ` 64` krauss@40106 ` 65` ```subsection {* Transfinite iteration of a function *} ``` krauss@40106 ` 66` krauss@40106 ` 67` ```inductive_set iterates :: "('a \ 'a) \ 'a set" ``` krauss@40106 ` 68` ```for f :: "'a \ 'a" ``` krauss@40106 ` 69` ```where ``` krauss@40106 ` 70` ``` step: "x \ iterates f \ f x \ iterates f" ``` huffman@46041 ` 71` ```| Sup: "chain (op \) M \ \x\M. x \ iterates f \ Sup M \ iterates f" ``` krauss@40106 ` 72` krauss@40106 ` 73` ```lemma iterates_le_f: ``` krauss@40106 ` 74` ``` "x \ iterates f \ monotone (op \) (op \) f \ x \ f x" ``` krauss@40106 ` 75` ```by (induct x rule: iterates.induct) ``` huffman@46041 ` 76` ``` (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+ ``` krauss@40106 ` 77` krauss@40106 ` 78` ```lemma chain_iterates: ``` krauss@40106 ` 79` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 80` ``` shows "chain (op \) (iterates f)" (is "chain _ ?C") ``` krauss@40106 ` 81` ```proof (rule chainI) ``` krauss@40106 ` 82` ``` fix x y assume "x \ ?C" "y \ ?C" ``` krauss@40106 ` 83` ``` then show "x \ y \ y \ x" ``` krauss@40106 ` 84` ``` proof (induct x arbitrary: y rule: iterates.induct) ``` krauss@40106 ` 85` ``` fix x y assume y: "y \ ?C" ``` krauss@40106 ` 86` ``` and IH: "\z. z \ ?C \ x \ z \ z \ x" ``` krauss@40106 ` 87` ``` from y show "f x \ y \ y \ f x" ``` krauss@40106 ` 88` ``` proof (induct y rule: iterates.induct) ``` krauss@40106 ` 89` ``` case (step y) with IH f show ?case by (auto dest: monotoneD) ``` krauss@40106 ` 90` ``` next ``` huffman@46041 ` 91` ``` case (Sup M) ``` krauss@40106 ` 92` ``` then have chM: "chain (op \) M" ``` krauss@40106 ` 93` ``` and IH': "\z. z \ M \ f x \ z \ z \ f x" by auto ``` huffman@46041 ` 94` ``` show "f x \ Sup M \ Sup M \ f x" ``` krauss@40106 ` 95` ``` proof (cases "\z\M. f x \ z") ``` huffman@46041 ` 96` ``` case True then have "f x \ Sup M" ``` krauss@40106 ` 97` ``` apply rule ``` krauss@40106 ` 98` ``` apply (erule order_trans) ``` huffman@46041 ` 99` ``` by (rule ccpo_Sup_upper[OF chM]) ``` krauss@40106 ` 100` ``` thus ?thesis .. ``` krauss@40106 ` 101` ``` next ``` krauss@40106 ` 102` ``` case False with IH' ``` huffman@46041 ` 103` ``` show ?thesis by (auto intro: ccpo_Sup_least[OF chM]) ``` krauss@40106 ` 104` ``` qed ``` krauss@40106 ` 105` ``` qed ``` krauss@40106 ` 106` ``` next ``` huffman@46041 ` 107` ``` case (Sup M y) ``` krauss@40106 ` 108` ``` show ?case ``` krauss@40106 ` 109` ``` proof (cases "\x\M. y \ x") ``` huffman@46041 ` 110` ``` case True then have "y \ Sup M" ``` krauss@40106 ` 111` ``` apply rule ``` krauss@40106 ` 112` ``` apply (erule order_trans) ``` huffman@46041 ` 113` ``` by (rule ccpo_Sup_upper[OF Sup(1)]) ``` krauss@40106 ` 114` ``` thus ?thesis .. ``` krauss@40106 ` 115` ``` next ``` huffman@46041 ` 116` ``` case False with Sup ``` huffman@46041 ` 117` ``` show ?thesis by (auto intro: ccpo_Sup_least) ``` krauss@40106 ` 118` ``` qed ``` krauss@40106 ` 119` ``` qed ``` krauss@40106 ` 120` ```qed ``` krauss@40106 ` 121` krauss@40106 ` 122` ```subsection {* Fixpoint combinator *} ``` krauss@40106 ` 123` krauss@40106 ` 124` ```definition ``` krauss@40106 ` 125` ``` fixp :: "('a \ 'a) \ 'a" ``` krauss@40106 ` 126` ```where ``` huffman@46041 ` 127` ``` "fixp f = Sup (iterates f)" ``` krauss@40106 ` 128` krauss@40106 ` 129` ```lemma iterates_fixp: ``` krauss@40106 ` 130` ``` assumes f: "monotone (op \) (op \) f" shows "fixp f \ iterates f" ``` krauss@40106 ` 131` ```unfolding fixp_def ``` huffman@46041 ` 132` ```by (simp add: iterates.Sup chain_iterates f) ``` krauss@40106 ` 133` krauss@40106 ` 134` ```lemma fixp_unfold: ``` krauss@40106 ` 135` ``` assumes f: "monotone (op \) (op \) f" ``` krauss@40106 ` 136` ``` shows "fixp f = f (fixp f)" ``` krauss@40106 ` 137` ```proof (rule antisym) ``` krauss@40106 ` 138` ``` show "fixp f \ f (fixp f)" ``` krauss@40106 ` 139` ``` by (intro iterates_le_f iterates_fixp f) ``` huffman@46041 ` 140` ``` have "f (fixp f) \ Sup (iterates f)" ``` huffman@46041 ` 141` ``` by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp) ``` krauss@40106 ` 142` ``` thus "f (fixp f) \ fixp f" ``` krauss@40106 ` 143` ``` unfolding fixp_def . ``` krauss@40106 ` 144` ```qed ``` krauss@40106 ` 145` krauss@40106 ` 146` ```lemma fixp_lowerbound: ``` krauss@40106 ` 147` ``` assumes f: "monotone (op \) (op \) f" and z: "f z \ z" shows "fixp f \ z" ``` krauss@40106 ` 148` ```unfolding fixp_def ``` huffman@46041 ` 149` ```proof (rule ccpo_Sup_least[OF chain_iterates[OF f]]) ``` krauss@40106 ` 150` ``` fix x assume "x \ iterates f" ``` krauss@40106 ` 151` ``` thus "x \ z" ``` krauss@40106 ` 152` ``` proof (induct x rule: iterates.induct) ``` krauss@40106 ` 153` ``` fix x assume "x \ z" with f have "f x \ f z" by (rule monotoneD) ``` krauss@40106 ` 154` ``` also note z finally show "f x \ z" . ``` huffman@46041 ` 155` ``` qed (auto intro: ccpo_Sup_least) ``` krauss@40106 ` 156` ```qed ``` krauss@40106 ` 157` krauss@40106 ` 158` krauss@40106 ` 159` ```subsection {* Fixpoint induction *} ``` krauss@40106 ` 160` krauss@40106 ` 161` ```definition ``` krauss@40106 ` 162` ``` admissible :: "('a \ bool) \ bool" ``` krauss@40106 ` 163` ```where ``` huffman@46041 ` 164` ``` "admissible P = (\A. chain (op \) A \ (\x\A. P x) \ P (Sup A))" ``` krauss@40106 ` 165` krauss@40106 ` 166` ```lemma admissibleI: ``` huffman@46041 ` 167` ``` assumes "\A. chain (op \) A \ \x\A. P x \ P (Sup A)" ``` krauss@40106 ` 168` ``` shows "admissible P" ``` krauss@40106 ` 169` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 170` krauss@40106 ` 171` ```lemma admissibleD: ``` krauss@40106 ` 172` ``` assumes "admissible P" ``` krauss@40106 ` 173` ``` assumes "chain (op \) A" ``` krauss@40106 ` 174` ``` assumes "\x. x \ A \ P x" ``` huffman@46041 ` 175` ``` shows "P (Sup A)" ``` krauss@40106 ` 176` ```using assms by (auto simp: admissible_def) ``` krauss@40106 ` 177` krauss@40106 ` 178` ```lemma fixp_induct: ``` krauss@40106 ` 179` ``` assumes adm: "admissible P" ``` krauss@40106 ` 180` ``` assumes mono: "monotone (op \) (op \) f" ``` krauss@40106 ` 181` ``` assumes step: "\x. P x \ P (f x)" ``` krauss@40106 ` 182` ``` shows "P (fixp f)" ``` krauss@40106 ` 183` ```unfolding fixp_def using adm chain_iterates[OF mono] ``` krauss@40106 ` 184` ```proof (rule admissibleD) ``` krauss@40106 ` 185` ``` fix x assume "x \ iterates f" ``` krauss@40106 ` 186` ``` thus "P x" ``` krauss@40106 ` 187` ``` by (induct rule: iterates.induct) ``` krauss@40106 ` 188` ``` (auto intro: step admissibleD adm) ``` krauss@40106 ` 189` ```qed ``` krauss@40106 ` 190` krauss@40106 ` 191` ```lemma admissible_True: "admissible (\x. True)" ``` krauss@40106 ` 192` ```unfolding admissible_def by simp ``` krauss@40106 ` 193` krauss@40106 ` 194` ```lemma admissible_False: "\ admissible (\x. False)" ``` krauss@40106 ` 195` ```unfolding admissible_def chain_def by simp ``` krauss@40106 ` 196` krauss@40106 ` 197` ```lemma admissible_const: "admissible (\x. t) = t" ``` krauss@40106 ` 198` ```by (cases t, simp_all add: admissible_True admissible_False) ``` krauss@40106 ` 199` krauss@40106 ` 200` ```lemma admissible_conj: ``` krauss@40106 ` 201` ``` assumes "admissible (\x. P x)" ``` krauss@40106 ` 202` ``` assumes "admissible (\x. Q x)" ``` krauss@40106 ` 203` ``` shows "admissible (\x. P x \ Q x)" ``` krauss@40106 ` 204` ```using assms unfolding admissible_def by simp ``` krauss@40106 ` 205` krauss@40106 ` 206` ```lemma admissible_all: ``` krauss@40106 ` 207` ``` assumes "\y. admissible (\x. P x y)" ``` krauss@40106 ` 208` ``` shows "admissible (\x. \y. P x y)" ``` krauss@40106 ` 209` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 210` krauss@40106 ` 211` ```lemma admissible_ball: ``` krauss@40106 ` 212` ``` assumes "\y. y \ A \ admissible (\x. P x y)" ``` krauss@40106 ` 213` ``` shows "admissible (\x. \y\A. P x y)" ``` krauss@40106 ` 214` ```using assms unfolding admissible_def by fast ``` krauss@40106 ` 215` krauss@40106 ` 216` ```lemma chain_compr: "chain (op \) A \ chain (op \) {x \ A. P x}" ``` krauss@40106 ` 217` ```unfolding chain_def by fast ``` krauss@40106 ` 218` krauss@40106 ` 219` ```lemma admissible_disj_lemma: ``` krauss@40106 ` 220` ``` assumes A: "chain (op \)A" ``` krauss@40106 ` 221` ``` assumes P: "\x\A. \y\A. x \ y \ P y" ``` huffman@46041 ` 222` ``` shows "Sup A = Sup {x \ A. P x}" ``` krauss@40106 ` 223` ```proof (rule antisym) ``` krauss@40106 ` 224` ``` have *: "chain (op \) {x \ A. P x}" ``` krauss@40106 ` 225` ``` by (rule chain_compr [OF A]) ``` huffman@46041 ` 226` ``` show "Sup A \ Sup {x \ A. P x}" ``` huffman@46041 ` 227` ``` apply (rule ccpo_Sup_least [OF A]) ``` krauss@40106 ` 228` ``` apply (drule P [rule_format], clarify) ``` krauss@40106 ` 229` ``` apply (erule order_trans) ``` huffman@46041 ` 230` ``` apply (simp add: ccpo_Sup_upper [OF *]) ``` krauss@40106 ` 231` ``` done ``` huffman@46041 ` 232` ``` show "Sup {x \ A. P x} \ Sup A" ``` huffman@46041 ` 233` ``` apply (rule ccpo_Sup_least [OF *]) ``` krauss@40106 ` 234` ``` apply clarify ``` huffman@46041 ` 235` ``` apply (simp add: ccpo_Sup_upper [OF A]) ``` krauss@40106 ` 236` ``` done ``` krauss@40106 ` 237` ```qed ``` krauss@40106 ` 238` krauss@40106 ` 239` ```lemma admissible_disj: ``` krauss@40106 ` 240` ``` fixes P Q :: "'a \ bool" ``` krauss@40106 ` 241` ``` assumes P: "admissible (\x. P x)" ``` krauss@40106 ` 242` ``` assumes Q: "admissible (\x. Q x)" ``` krauss@40106 ` 243` ``` shows "admissible (\x. P x \ Q x)" ``` krauss@40106 ` 244` ```proof (rule admissibleI) ``` krauss@40106 ` 245` ``` fix A :: "'a set" assume A: "chain (op \) A" ``` krauss@40106 ` 246` ``` assume "\x\A. P x \ Q x" ``` krauss@40106 ` 247` ``` hence "(\x\A. \y\A. x \ y \ P y) \ (\x\A. \y\A. x \ y \ Q y)" ``` krauss@40106 ` 248` ``` using chainD[OF A] by blast ``` huffman@46041 ` 249` ``` hence "Sup A = Sup {x \ A. P x} \ Sup A = Sup {x \ A. Q x}" ``` krauss@40106 ` 250` ``` using admissible_disj_lemma [OF A] by fast ``` huffman@46041 ` 251` ``` thus "P (Sup A) \ Q (Sup A)" ``` krauss@40106 ` 252` ``` apply (rule disjE, simp_all) ``` krauss@40106 ` 253` ``` apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp) ``` krauss@40106 ` 254` ``` apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp) ``` krauss@40106 ` 255` ``` done ``` krauss@40106 ` 256` ```qed ``` krauss@40106 ` 257` krauss@40106 ` 258` ```end ``` krauss@40106 ` 259` huffman@46041 ` 260` ```instance complete_lattice \ ccpo ``` huffman@46041 ` 261` ``` by default (fast intro: Sup_upper Sup_least)+ ``` huffman@46041 ` 262` huffman@46041 ` 263` ```lemma lfp_eq_fixp: ``` huffman@46041 ` 264` ``` assumes f: "mono f" shows "lfp f = fixp f" ``` huffman@46041 ` 265` ```proof (rule antisym) ``` huffman@46041 ` 266` ``` from f have f': "monotone (op \) (op \) f" ``` huffman@46041 ` 267` ``` unfolding mono_def monotone_def . ``` huffman@46041 ` 268` ``` show "lfp f \ fixp f" ``` huffman@46041 ` 269` ``` by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl) ``` huffman@46041 ` 270` ``` show "fixp f \ lfp f" ``` huffman@46041 ` 271` ``` by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl) ``` huffman@46041 ` 272` ```qed ``` huffman@46041 ` 273` huffman@46041 ` 274` ```hide_const (open) iterates fixp admissible ``` krauss@40106 ` 275` krauss@40106 ` 276` ```end ```