src/HOL/Partial_Function.thy
 author haftmann Mon Nov 29 13:44:54 2010 +0100 (2010-11-29) changeset 40815 6e2d17cc0d1d parent 40288 520199d8b66e child 42949 618adb3584e5 permissions -rw-r--r--
equivI has replaced equiv.intro
 krauss@40107 ` 1` ```(* Title: HOL/Partial_Function.thy ``` krauss@40107 ` 2` ``` Author: Alexander Krauss, TU Muenchen ``` krauss@40107 ` 3` ```*) ``` krauss@40107 ` 4` krauss@40107 ` 5` ```header {* Partial Function Definitions *} ``` krauss@40107 ` 6` krauss@40107 ` 7` ```theory Partial_Function ``` krauss@40107 ` 8` ```imports Complete_Partial_Order Option ``` krauss@40107 ` 9` ```uses ``` krauss@40107 ` 10` ``` "Tools/Function/function_lib.ML" ``` krauss@40107 ` 11` ``` "Tools/Function/partial_function.ML" ``` krauss@40107 ` 12` ```begin ``` krauss@40107 ` 13` krauss@40107 ` 14` ```setup Partial_Function.setup ``` krauss@40107 ` 15` krauss@40107 ` 16` ```subsection {* Axiomatic setup *} ``` krauss@40107 ` 17` krauss@40107 ` 18` ```text {* This techical locale constains the requirements for function ``` krauss@40107 ` 19` ``` definitions with ccpo fixed points. *} ``` krauss@40107 ` 20` krauss@40107 ` 21` ```definition "fun_ord ord f g \ (\x. ord (f x) (g x))" ``` krauss@40107 ` 22` ```definition "fun_lub L A = (\x. L {y. \f\A. y = f x})" ``` krauss@40107 ` 23` ```definition "img_ord f ord = (\x y. ord (f x) (f y))" ``` krauss@40107 ` 24` ```definition "img_lub f g Lub = (\A. g (Lub (f ` A)))" ``` krauss@40107 ` 25` krauss@40107 ` 26` ```lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\f. f t)" ``` krauss@40107 ` 27` ```by (rule monotoneI) (auto simp: fun_ord_def) ``` krauss@40107 ` 28` krauss@40288 ` 29` ```lemma let_mono[partial_function_mono]: ``` krauss@40288 ` 30` ``` "(\x. monotone orda ordb (\f. b f x)) ``` krauss@40288 ` 31` ``` \ monotone orda ordb (\f. Let t (b f))" ``` krauss@40288 ` 32` ```by (simp add: Let_def) ``` krauss@40288 ` 33` krauss@40107 ` 34` ```lemma if_mono[partial_function_mono]: "monotone orda ordb F ``` krauss@40107 ` 35` ```\ monotone orda ordb G ``` krauss@40107 ` 36` ```\ monotone orda ordb (\f. if c then F f else G f)" ``` krauss@40107 ` 37` ```unfolding monotone_def by simp ``` krauss@40107 ` 38` krauss@40107 ` 39` ```definition "mk_less R = (\x y. R x y \ \ R y x)" ``` krauss@40107 ` 40` krauss@40107 ` 41` ```locale partial_function_definitions = ``` krauss@40107 ` 42` ``` fixes leq :: "'a \ 'a \ bool" ``` krauss@40107 ` 43` ``` fixes lub :: "'a set \ 'a" ``` krauss@40107 ` 44` ``` assumes leq_refl: "leq x x" ``` krauss@40107 ` 45` ``` assumes leq_trans: "leq x y \ leq y z \ leq x z" ``` krauss@40107 ` 46` ``` assumes leq_antisym: "leq x y \ leq y x \ x = y" ``` krauss@40107 ` 47` ``` assumes lub_upper: "chain leq A \ x \ A \ leq x (lub A)" ``` krauss@40107 ` 48` ``` assumes lub_least: "chain leq A \ (\x. x \ A \ leq x z) \ leq (lub A) z" ``` krauss@40107 ` 49` krauss@40107 ` 50` ```lemma partial_function_lift: ``` krauss@40107 ` 51` ``` assumes "partial_function_definitions ord lb" ``` krauss@40107 ` 52` ``` shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf") ``` krauss@40107 ` 53` ```proof - ``` krauss@40107 ` 54` ``` interpret partial_function_definitions ord lb by fact ``` krauss@40107 ` 55` krauss@40107 ` 56` ``` { fix A a assume A: "chain ?ordf A" ``` krauss@40107 ` 57` ``` have "chain ord {y. \f\A. y = f a}" (is "chain ord ?C") ``` krauss@40107 ` 58` ``` proof (rule chainI) ``` krauss@40107 ` 59` ``` fix x y assume "x \ ?C" "y \ ?C" ``` krauss@40107 ` 60` ``` then obtain f g where fg: "f \ A" "g \ A" ``` krauss@40107 ` 61` ``` and [simp]: "x = f a" "y = g a" by blast ``` krauss@40107 ` 62` ``` from chainD[OF A fg] ``` krauss@40107 ` 63` ``` show "ord x y \ ord y x" unfolding fun_ord_def by auto ``` krauss@40107 ` 64` ``` qed } ``` krauss@40107 ` 65` ``` note chain_fun = this ``` krauss@40107 ` 66` krauss@40107 ` 67` ``` show ?thesis ``` krauss@40107 ` 68` ``` proof ``` krauss@40107 ` 69` ``` fix x show "?ordf x x" ``` krauss@40107 ` 70` ``` unfolding fun_ord_def by (auto simp: leq_refl) ``` krauss@40107 ` 71` ``` next ``` krauss@40107 ` 72` ``` fix x y z assume "?ordf x y" "?ordf y z" ``` krauss@40107 ` 73` ``` thus "?ordf x z" unfolding fun_ord_def ``` krauss@40107 ` 74` ``` by (force dest: leq_trans) ``` krauss@40107 ` 75` ``` next ``` krauss@40107 ` 76` ``` fix x y assume "?ordf x y" "?ordf y x" ``` krauss@40107 ` 77` ``` thus "x = y" unfolding fun_ord_def ``` krauss@40107 ` 78` ``` by (force intro!: ext dest: leq_antisym) ``` krauss@40107 ` 79` ``` next ``` krauss@40107 ` 80` ``` fix A f assume f: "f \ A" and A: "chain ?ordf A" ``` krauss@40107 ` 81` ``` thus "?ordf f (?lubf A)" ``` krauss@40107 ` 82` ``` unfolding fun_lub_def fun_ord_def ``` krauss@40107 ` 83` ``` by (blast intro: lub_upper chain_fun[OF A] f) ``` krauss@40107 ` 84` ``` next ``` krauss@40107 ` 85` ``` fix A :: "('b \ 'a) set" and g :: "'b \ 'a" ``` krauss@40107 ` 86` ``` assume A: "chain ?ordf A" and g: "\f. f \ A \ ?ordf f g" ``` krauss@40107 ` 87` ``` show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def ``` krauss@40107 ` 88` ``` by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def]) ``` krauss@40107 ` 89` ``` qed ``` krauss@40107 ` 90` ```qed ``` krauss@40107 ` 91` krauss@40107 ` 92` ```lemma ccpo: assumes "partial_function_definitions ord lb" ``` krauss@40107 ` 93` ``` shows "class.ccpo ord (mk_less ord) lb" ``` krauss@40107 ` 94` ```using assms unfolding partial_function_definitions_def mk_less_def ``` krauss@40107 ` 95` ```by unfold_locales blast+ ``` krauss@40107 ` 96` krauss@40107 ` 97` ```lemma partial_function_image: ``` krauss@40107 ` 98` ``` assumes "partial_function_definitions ord Lub" ``` krauss@40107 ` 99` ``` assumes inj: "\x y. f x = f y \ x = y" ``` krauss@40107 ` 100` ``` assumes inv: "\x. f (g x) = x" ``` krauss@40107 ` 101` ``` shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)" ``` krauss@40107 ` 102` ```proof - ``` krauss@40107 ` 103` ``` let ?iord = "img_ord f ord" ``` krauss@40107 ` 104` ``` let ?ilub = "img_lub f g Lub" ``` krauss@40107 ` 105` krauss@40107 ` 106` ``` interpret partial_function_definitions ord Lub by fact ``` krauss@40107 ` 107` ``` show ?thesis ``` krauss@40107 ` 108` ``` proof ``` krauss@40107 ` 109` ``` fix A x assume "chain ?iord A" "x \ A" ``` krauss@40107 ` 110` ``` then have "chain ord (f ` A)" "f x \ f ` A" ``` krauss@40107 ` 111` ``` by (auto simp: img_ord_def intro: chainI dest: chainD) ``` krauss@40107 ` 112` ``` thus "?iord x (?ilub A)" ``` krauss@40107 ` 113` ``` unfolding inv img_lub_def img_ord_def by (rule lub_upper) ``` krauss@40107 ` 114` ``` next ``` krauss@40107 ` 115` ``` fix A x assume "chain ?iord A" ``` krauss@40107 ` 116` ``` and 1: "\z. z \ A \ ?iord z x" ``` krauss@40107 ` 117` ``` then have "chain ord (f ` A)" ``` krauss@40107 ` 118` ``` by (auto simp: img_ord_def intro: chainI dest: chainD) ``` krauss@40107 ` 119` ``` thus "?iord (?ilub A) x" ``` krauss@40107 ` 120` ``` unfolding inv img_lub_def img_ord_def ``` krauss@40107 ` 121` ``` by (rule lub_least) (auto dest: 1[unfolded img_ord_def]) ``` krauss@40107 ` 122` ``` qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj) ``` krauss@40107 ` 123` ```qed ``` krauss@40107 ` 124` krauss@40107 ` 125` ```context partial_function_definitions ``` krauss@40107 ` 126` ```begin ``` krauss@40107 ` 127` krauss@40107 ` 128` ```abbreviation "le_fun \ fun_ord leq" ``` krauss@40107 ` 129` ```abbreviation "lub_fun \ fun_lub lub" ``` krauss@40107 ` 130` ```abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun" ``` krauss@40107 ` 131` ```abbreviation "mono_body \ monotone le_fun leq" ``` krauss@40107 ` 132` krauss@40107 ` 133` ```text {* Interpret manually, to avoid flooding everything with facts about ``` krauss@40107 ` 134` ``` orders *} ``` krauss@40107 ` 135` krauss@40107 ` 136` ```lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun" ``` krauss@40107 ` 137` ```apply (rule ccpo) ``` krauss@40107 ` 138` ```apply (rule partial_function_lift) ``` krauss@40107 ` 139` ```apply (rule partial_function_definitions_axioms) ``` krauss@40107 ` 140` ```done ``` krauss@40107 ` 141` krauss@40107 ` 142` ```text {* The crucial fixed-point theorem *} ``` krauss@40107 ` 143` krauss@40107 ` 144` ```lemma mono_body_fixp: ``` krauss@40107 ` 145` ``` "(\x. mono_body (\f. F f x)) \ fixp_fun F = F (fixp_fun F)" ``` krauss@40107 ` 146` ```by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def) ``` krauss@40107 ` 147` krauss@40107 ` 148` ```text {* Version with curry/uncurry combinators, to be used by package *} ``` krauss@40107 ` 149` krauss@40107 ` 150` ```lemma fixp_rule_uc: ``` krauss@40107 ` 151` ``` fixes F :: "'c \ 'c" and ``` krauss@40107 ` 152` ``` U :: "'c \ 'b \ 'a" and ``` krauss@40107 ` 153` ``` C :: "('b \ 'a) \ 'c" ``` krauss@40107 ` 154` ``` assumes mono: "\x. mono_body (\f. U (F (C f)) x)" ``` krauss@40107 ` 155` ``` assumes eq: "f \ C (fixp_fun (\f. U (F (C f))))" ``` krauss@40107 ` 156` ``` assumes inverse: "\f. C (U f) = f" ``` krauss@40107 ` 157` ``` shows "f = F f" ``` krauss@40107 ` 158` ```proof - ``` krauss@40107 ` 159` ``` have "f = C (fixp_fun (\f. U (F (C f))))" by (simp add: eq) ``` krauss@40107 ` 160` ``` also have "... = C (U (F (C (fixp_fun (\f. U (F (C f)))))))" ``` krauss@40107 ` 161` ``` by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl) ``` krauss@40107 ` 162` ``` also have "... = F (C (fixp_fun (\f. U (F (C f)))))" by (rule inverse) ``` krauss@40107 ` 163` ``` also have "... = F f" by (simp add: eq) ``` krauss@40107 ` 164` ``` finally show "f = F f" . ``` krauss@40107 ` 165` ```qed ``` krauss@40107 ` 166` krauss@40107 ` 167` ```text {* Rules for @{term mono_body}: *} ``` krauss@40107 ` 168` krauss@40107 ` 169` ```lemma const_mono[partial_function_mono]: "monotone ord leq (\f. c)" ``` krauss@40107 ` 170` ```by (rule monotoneI) (rule leq_refl) ``` krauss@40107 ` 171` krauss@40107 ` 172` ```declaration {* Partial_Function.init @{term fixp_fun} ``` krauss@40107 ` 173` ``` @{term mono_body} @{thm fixp_rule_uc} *} ``` krauss@40107 ` 174` krauss@40107 ` 175` ```end ``` krauss@40107 ` 176` krauss@40107 ` 177` krauss@40107 ` 178` ```subsection {* Flat interpretation: tailrec and option *} ``` krauss@40107 ` 179` krauss@40107 ` 180` ```definition ``` krauss@40107 ` 181` ``` "flat_ord b x y \ x = b \ x = y" ``` krauss@40107 ` 182` krauss@40107 ` 183` ```definition ``` krauss@40107 ` 184` ``` "flat_lub b A = (if A \ {b} then b else (THE x. x \ A - {b}))" ``` krauss@40107 ` 185` krauss@40107 ` 186` ```lemma flat_interpretation: ``` krauss@40107 ` 187` ``` "partial_function_definitions (flat_ord b) (flat_lub b)" ``` krauss@40107 ` 188` ```proof ``` krauss@40107 ` 189` ``` fix A x assume 1: "chain (flat_ord b) A" "x \ A" ``` krauss@40107 ` 190` ``` show "flat_ord b x (flat_lub b A)" ``` krauss@40107 ` 191` ``` proof cases ``` krauss@40107 ` 192` ``` assume "x = b" ``` krauss@40107 ` 193` ``` thus ?thesis by (simp add: flat_ord_def) ``` krauss@40107 ` 194` ``` next ``` krauss@40107 ` 195` ``` assume "x \ b" ``` krauss@40107 ` 196` ``` with 1 have "A - {b} = {x}" ``` krauss@40107 ` 197` ``` by (auto elim: chainE simp: flat_ord_def) ``` krauss@40107 ` 198` ``` then have "flat_lub b A = x" ``` krauss@40107 ` 199` ``` by (auto simp: flat_lub_def) ``` krauss@40107 ` 200` ``` thus ?thesis by (auto simp: flat_ord_def) ``` krauss@40107 ` 201` ``` qed ``` krauss@40107 ` 202` ```next ``` krauss@40107 ` 203` ``` fix A z assume A: "chain (flat_ord b) A" ``` krauss@40107 ` 204` ``` and z: "\x. x \ A \ flat_ord b x z" ``` krauss@40107 ` 205` ``` show "flat_ord b (flat_lub b A) z" ``` krauss@40107 ` 206` ``` proof cases ``` krauss@40107 ` 207` ``` assume "A \ {b}" ``` krauss@40107 ` 208` ``` thus ?thesis ``` krauss@40107 ` 209` ``` by (auto simp: flat_lub_def flat_ord_def) ``` krauss@40107 ` 210` ``` next ``` krauss@40107 ` 211` ``` assume nb: "\ A \ {b}" ``` krauss@40107 ` 212` ``` then obtain y where y: "y \ A" "y \ b" by auto ``` krauss@40107 ` 213` ``` with A have "A - {b} = {y}" ``` krauss@40107 ` 214` ``` by (auto elim: chainE simp: flat_ord_def) ``` krauss@40107 ` 215` ``` with nb have "flat_lub b A = y" ``` krauss@40107 ` 216` ``` by (auto simp: flat_lub_def) ``` krauss@40107 ` 217` ``` with z y show ?thesis by auto ``` krauss@40107 ` 218` ``` qed ``` krauss@40107 ` 219` ```qed (auto simp: flat_ord_def) ``` krauss@40107 ` 220` krauss@40107 ` 221` ```interpretation tailrec!: ``` krauss@40107 ` 222` ``` partial_function_definitions "flat_ord undefined" "flat_lub undefined" ``` krauss@40107 ` 223` ```by (rule flat_interpretation) ``` krauss@40107 ` 224` krauss@40107 ` 225` ```interpretation option!: ``` krauss@40107 ` 226` ``` partial_function_definitions "flat_ord None" "flat_lub None" ``` krauss@40107 ` 227` ```by (rule flat_interpretation) ``` krauss@40107 ` 228` krauss@40107 ` 229` ```abbreviation "option_ord \ flat_ord None" ``` krauss@40107 ` 230` ```abbreviation "mono_option \ monotone (fun_ord option_ord) option_ord" ``` krauss@40107 ` 231` krauss@40107 ` 232` ```lemma bind_mono[partial_function_mono]: ``` krauss@40107 ` 233` ```assumes mf: "mono_option B" and mg: "\y. mono_option (\f. C y f)" ``` krauss@40107 ` 234` ```shows "mono_option (\f. Option.bind (B f) (\y. C y f))" ``` krauss@40107 ` 235` ```proof (rule monotoneI) ``` krauss@40107 ` 236` ``` fix f g :: "'a \ 'b option" assume fg: "fun_ord option_ord f g" ``` krauss@40107 ` 237` ``` with mf ``` krauss@40107 ` 238` ``` have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) ``` krauss@40107 ` 239` ``` then have "option_ord (Option.bind (B f) (\y. C y f)) (Option.bind (B g) (\y. C y f))" ``` krauss@40107 ` 240` ``` unfolding flat_ord_def by auto ``` krauss@40107 ` 241` ``` also from mg ``` krauss@40107 ` 242` ``` have "\y'. option_ord (C y' f) (C y' g)" ``` krauss@40107 ` 243` ``` by (rule monotoneD) (rule fg) ``` krauss@40107 ` 244` ``` then have "option_ord (Option.bind (B g) (\y'. C y' f)) (Option.bind (B g) (\y'. C y' g))" ``` krauss@40107 ` 245` ``` unfolding flat_ord_def by (cases "B g") auto ``` krauss@40107 ` 246` ``` finally (option.leq_trans) ``` krauss@40107 ` 247` ``` show "option_ord (Option.bind (B f) (\y. C y f)) (Option.bind (B g) (\y'. C y' g))" . ``` krauss@40107 ` 248` ```qed ``` krauss@40107 ` 249` krauss@40252 ` 250` ```hide_const (open) chain ``` krauss@40107 ` 251` krauss@40107 ` 252` ```end ``` krauss@40107 ` 253`