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