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