src/HOL/Partial_Function.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 46041 1e3ff542e83e child 46950 d0181abdbdac permissions -rw-r--r--
 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@42949 ` 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@43081 ` 26` ```lemma chain_fun: ``` krauss@43081 ` 27` ``` assumes A: "chain (fun_ord ord) A" ``` krauss@43081 ` 28` ``` shows "chain ord {y. \f\A. y = f a}" (is "chain ord ?C") ``` krauss@43081 ` 29` ```proof (rule chainI) ``` krauss@43081 ` 30` ``` fix x y assume "x \ ?C" "y \ ?C" ``` krauss@43081 ` 31` ``` then obtain f g where fg: "f \ A" "g \ A" ``` krauss@43081 ` 32` ``` and [simp]: "x = f a" "y = g a" by blast ``` krauss@43081 ` 33` ``` from chainD[OF A fg] ``` krauss@43081 ` 34` ``` show "ord x y \ ord y x" unfolding fun_ord_def by auto ``` krauss@43081 ` 35` ```qed ``` krauss@43081 ` 36` krauss@40107 ` 37` ```lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\f. f t)" ``` krauss@40107 ` 38` ```by (rule monotoneI) (auto simp: fun_ord_def) ``` krauss@40107 ` 39` krauss@40288 ` 40` ```lemma let_mono[partial_function_mono]: ``` krauss@40288 ` 41` ``` "(\x. monotone orda ordb (\f. b f x)) ``` krauss@40288 ` 42` ``` \ monotone orda ordb (\f. Let t (b f))" ``` krauss@40288 ` 43` ```by (simp add: Let_def) ``` krauss@40288 ` 44` krauss@40107 ` 45` ```lemma if_mono[partial_function_mono]: "monotone orda ordb F ``` krauss@40107 ` 46` ```\ monotone orda ordb G ``` krauss@40107 ` 47` ```\ monotone orda ordb (\f. if c then F f else G f)" ``` krauss@40107 ` 48` ```unfolding monotone_def by simp ``` krauss@40107 ` 49` krauss@40107 ` 50` ```definition "mk_less R = (\x y. R x y \ \ R y x)" ``` krauss@40107 ` 51` krauss@40107 ` 52` ```locale partial_function_definitions = ``` krauss@40107 ` 53` ``` fixes leq :: "'a \ 'a \ bool" ``` krauss@40107 ` 54` ``` fixes lub :: "'a set \ 'a" ``` krauss@40107 ` 55` ``` assumes leq_refl: "leq x x" ``` krauss@40107 ` 56` ``` assumes leq_trans: "leq x y \ leq y z \ leq x z" ``` krauss@40107 ` 57` ``` assumes leq_antisym: "leq x y \ leq y x \ x = y" ``` krauss@40107 ` 58` ``` assumes lub_upper: "chain leq A \ x \ A \ leq x (lub A)" ``` krauss@40107 ` 59` ``` assumes lub_least: "chain leq A \ (\x. x \ A \ leq x z) \ leq (lub A) z" ``` krauss@40107 ` 60` krauss@40107 ` 61` ```lemma partial_function_lift: ``` krauss@40107 ` 62` ``` assumes "partial_function_definitions ord lb" ``` krauss@40107 ` 63` ``` shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf") ``` krauss@40107 ` 64` ```proof - ``` krauss@40107 ` 65` ``` interpret partial_function_definitions ord lb by fact ``` 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@43081 ` 78` ``` by (force intro!: 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" ``` huffman@46041 ` 93` ``` shows "class.ccpo lb ord (mk_less ord)" ``` 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" ``` huffman@46041 ` 130` ```abbreviation "fixp_fun \ ccpo.fixp lub_fun le_fun" ``` krauss@40107 ` 131` ```abbreviation "mono_body \ monotone le_fun leq" ``` huffman@46041 ` 132` ```abbreviation "admissible \ ccpo.admissible lub_fun le_fun" ``` krauss@40107 ` 133` krauss@40107 ` 134` ```text {* Interpret manually, to avoid flooding everything with facts about ``` krauss@40107 ` 135` ``` orders *} ``` krauss@40107 ` 136` huffman@46041 ` 137` ```lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)" ``` krauss@40107 ` 138` ```apply (rule ccpo) ``` krauss@40107 ` 139` ```apply (rule partial_function_lift) ``` krauss@40107 ` 140` ```apply (rule partial_function_definitions_axioms) ``` krauss@40107 ` 141` ```done ``` krauss@40107 ` 142` krauss@40107 ` 143` ```text {* The crucial fixed-point theorem *} ``` krauss@40107 ` 144` krauss@40107 ` 145` ```lemma mono_body_fixp: ``` krauss@40107 ` 146` ``` "(\x. mono_body (\f. F f x)) \ fixp_fun F = F (fixp_fun F)" ``` krauss@40107 ` 147` ```by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def) ``` krauss@40107 ` 148` krauss@40107 ` 149` ```text {* Version with curry/uncurry combinators, to be used by package *} ``` krauss@40107 ` 150` krauss@40107 ` 151` ```lemma fixp_rule_uc: ``` krauss@40107 ` 152` ``` fixes F :: "'c \ 'c" and ``` krauss@40107 ` 153` ``` U :: "'c \ 'b \ 'a" and ``` krauss@40107 ` 154` ``` C :: "('b \ 'a) \ 'c" ``` krauss@40107 ` 155` ``` assumes mono: "\x. mono_body (\f. U (F (C f)) x)" ``` krauss@40107 ` 156` ``` assumes eq: "f \ C (fixp_fun (\f. U (F (C f))))" ``` krauss@40107 ` 157` ``` assumes inverse: "\f. C (U f) = f" ``` krauss@40107 ` 158` ``` shows "f = F f" ``` krauss@40107 ` 159` ```proof - ``` krauss@40107 ` 160` ``` have "f = C (fixp_fun (\f. U (F (C f))))" by (simp add: eq) ``` krauss@40107 ` 161` ``` also have "... = C (U (F (C (fixp_fun (\f. U (F (C f)))))))" ``` krauss@40107 ` 162` ``` by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl) ``` krauss@40107 ` 163` ``` also have "... = F (C (fixp_fun (\f. U (F (C f)))))" by (rule inverse) ``` krauss@40107 ` 164` ``` also have "... = F f" by (simp add: eq) ``` krauss@40107 ` 165` ``` finally show "f = F f" . ``` krauss@40107 ` 166` ```qed ``` krauss@40107 ` 167` krauss@43082 ` 168` ```text {* Fixpoint induction rule *} ``` krauss@43082 ` 169` krauss@43082 ` 170` ```lemma fixp_induct_uc: ``` krauss@43082 ` 171` ``` fixes F :: "'c \ 'c" and ``` krauss@43082 ` 172` ``` U :: "'c \ 'b \ 'a" and ``` krauss@43082 ` 173` ``` C :: "('b \ 'a) \ 'c" and ``` krauss@43082 ` 174` ``` P :: "('b \ 'a) \ bool" ``` krauss@43082 ` 175` ``` assumes mono: "\x. mono_body (\f. U (F (C f)) x)" ``` krauss@43082 ` 176` ``` assumes eq: "f \ C (fixp_fun (\f. U (F (C f))))" ``` krauss@43082 ` 177` ``` assumes inverse: "\f. U (C f) = f" ``` huffman@46041 ` 178` ``` assumes adm: "ccpo.admissible lub_fun le_fun P" ``` krauss@43082 ` 179` ``` assumes step: "\f. P (U f) \ P (U (F f))" ``` krauss@43082 ` 180` ``` shows "P (U f)" ``` krauss@43082 ` 181` ```unfolding eq inverse ``` krauss@43082 ` 182` ```apply (rule ccpo.fixp_induct[OF ccpo adm]) ``` krauss@43082 ` 183` ```apply (insert mono, auto simp: monotone_def fun_ord_def)[1] ``` krauss@43082 ` 184` ```by (rule_tac f="C x" in step, simp add: inverse) ``` krauss@43082 ` 185` krauss@43082 ` 186` krauss@40107 ` 187` ```text {* Rules for @{term mono_body}: *} ``` krauss@40107 ` 188` krauss@40107 ` 189` ```lemma const_mono[partial_function_mono]: "monotone ord leq (\f. c)" ``` krauss@40107 ` 190` ```by (rule monotoneI) (rule leq_refl) ``` krauss@40107 ` 191` krauss@40107 ` 192` ```end ``` krauss@40107 ` 193` krauss@40107 ` 194` krauss@40107 ` 195` ```subsection {* Flat interpretation: tailrec and option *} ``` krauss@40107 ` 196` krauss@40107 ` 197` ```definition ``` krauss@40107 ` 198` ``` "flat_ord b x y \ x = b \ x = y" ``` krauss@40107 ` 199` krauss@40107 ` 200` ```definition ``` krauss@40107 ` 201` ``` "flat_lub b A = (if A \ {b} then b else (THE x. x \ A - {b}))" ``` krauss@40107 ` 202` krauss@40107 ` 203` ```lemma flat_interpretation: ``` krauss@40107 ` 204` ``` "partial_function_definitions (flat_ord b) (flat_lub b)" ``` krauss@40107 ` 205` ```proof ``` krauss@40107 ` 206` ``` fix A x assume 1: "chain (flat_ord b) A" "x \ A" ``` krauss@40107 ` 207` ``` show "flat_ord b x (flat_lub b A)" ``` krauss@40107 ` 208` ``` proof cases ``` krauss@40107 ` 209` ``` assume "x = b" ``` krauss@40107 ` 210` ``` thus ?thesis by (simp add: flat_ord_def) ``` krauss@40107 ` 211` ``` next ``` krauss@40107 ` 212` ``` assume "x \ b" ``` krauss@40107 ` 213` ``` with 1 have "A - {b} = {x}" ``` krauss@40107 ` 214` ``` by (auto elim: chainE simp: flat_ord_def) ``` krauss@40107 ` 215` ``` then have "flat_lub b A = x" ``` krauss@40107 ` 216` ``` by (auto simp: flat_lub_def) ``` krauss@40107 ` 217` ``` thus ?thesis by (auto simp: flat_ord_def) ``` krauss@40107 ` 218` ``` qed ``` krauss@40107 ` 219` ```next ``` krauss@40107 ` 220` ``` fix A z assume A: "chain (flat_ord b) A" ``` krauss@40107 ` 221` ``` and z: "\x. x \ A \ flat_ord b x z" ``` krauss@40107 ` 222` ``` show "flat_ord b (flat_lub b A) z" ``` krauss@40107 ` 223` ``` proof cases ``` krauss@40107 ` 224` ``` assume "A \ {b}" ``` krauss@40107 ` 225` ``` thus ?thesis ``` krauss@40107 ` 226` ``` by (auto simp: flat_lub_def flat_ord_def) ``` krauss@40107 ` 227` ``` next ``` krauss@40107 ` 228` ``` assume nb: "\ A \ {b}" ``` krauss@40107 ` 229` ``` then obtain y where y: "y \ A" "y \ b" by auto ``` krauss@40107 ` 230` ``` with A have "A - {b} = {y}" ``` krauss@40107 ` 231` ``` by (auto elim: chainE simp: flat_ord_def) ``` krauss@40107 ` 232` ``` with nb have "flat_lub b A = y" ``` krauss@40107 ` 233` ``` by (auto simp: flat_lub_def) ``` krauss@40107 ` 234` ``` with z y show ?thesis by auto ``` krauss@40107 ` 235` ``` qed ``` krauss@40107 ` 236` ```qed (auto simp: flat_ord_def) ``` krauss@40107 ` 237` krauss@40107 ` 238` ```interpretation tailrec!: ``` krauss@40107 ` 239` ``` partial_function_definitions "flat_ord undefined" "flat_lub undefined" ``` krauss@40107 ` 240` ```by (rule flat_interpretation) ``` krauss@40107 ` 241` krauss@40107 ` 242` ```interpretation option!: ``` krauss@40107 ` 243` ``` partial_function_definitions "flat_ord None" "flat_lub None" ``` krauss@40107 ` 244` ```by (rule flat_interpretation) ``` krauss@40107 ` 245` krauss@42949 ` 246` krauss@40107 ` 247` ```abbreviation "option_ord \ flat_ord None" ``` krauss@40107 ` 248` ```abbreviation "mono_option \ monotone (fun_ord option_ord) option_ord" ``` krauss@40107 ` 249` krauss@40107 ` 250` ```lemma bind_mono[partial_function_mono]: ``` krauss@40107 ` 251` ```assumes mf: "mono_option B" and mg: "\y. mono_option (\f. C y f)" ``` krauss@40107 ` 252` ```shows "mono_option (\f. Option.bind (B f) (\y. C y f))" ``` krauss@40107 ` 253` ```proof (rule monotoneI) ``` krauss@40107 ` 254` ``` fix f g :: "'a \ 'b option" assume fg: "fun_ord option_ord f g" ``` krauss@40107 ` 255` ``` with mf ``` krauss@40107 ` 256` ``` have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) ``` krauss@40107 ` 257` ``` then have "option_ord (Option.bind (B f) (\y. C y f)) (Option.bind (B g) (\y. C y f))" ``` krauss@40107 ` 258` ``` unfolding flat_ord_def by auto ``` krauss@40107 ` 259` ``` also from mg ``` krauss@40107 ` 260` ``` have "\y'. option_ord (C y' f) (C y' g)" ``` krauss@40107 ` 261` ``` by (rule monotoneD) (rule fg) ``` krauss@40107 ` 262` ``` then have "option_ord (Option.bind (B g) (\y'. C y' f)) (Option.bind (B g) (\y'. C y' g))" ``` krauss@40107 ` 263` ``` unfolding flat_ord_def by (cases "B g") auto ``` krauss@40107 ` 264` ``` finally (option.leq_trans) ``` krauss@40107 ` 265` ``` show "option_ord (Option.bind (B f) (\y. C y f)) (Option.bind (B g) (\y'. C y' g))" . ``` krauss@40107 ` 266` ```qed ``` krauss@40107 ` 267` krauss@43081 ` 268` ```lemma flat_lub_in_chain: ``` krauss@43081 ` 269` ``` assumes ch: "chain (flat_ord b) A " ``` krauss@43081 ` 270` ``` assumes lub: "flat_lub b A = a" ``` krauss@43081 ` 271` ``` shows "a = b \ a \ A" ``` krauss@43081 ` 272` ```proof (cases "A \ {b}") ``` krauss@43081 ` 273` ``` case True ``` krauss@43081 ` 274` ``` then have "flat_lub b A = b" unfolding flat_lub_def by simp ``` krauss@43081 ` 275` ``` with lub show ?thesis by simp ``` krauss@43081 ` 276` ```next ``` krauss@43081 ` 277` ``` case False ``` krauss@43081 ` 278` ``` then obtain c where "c \ A" and "c \ b" by auto ``` krauss@43081 ` 279` ``` { fix z assume "z \ A" ``` krauss@43081 ` 280` ``` from chainD[OF ch `c \ A` this] have "z = c \ z = b" ``` krauss@43081 ` 281` ``` unfolding flat_ord_def using `c \ b` by auto } ``` krauss@43081 ` 282` ``` with False have "A - {b} = {c}" by auto ``` krauss@43081 ` 283` ``` with False have "flat_lub b A = c" by (auto simp: flat_lub_def) ``` krauss@43081 ` 284` ``` with `c \ A` lub show ?thesis by simp ``` krauss@43081 ` 285` ```qed ``` krauss@43081 ` 286` krauss@43081 ` 287` ```lemma option_admissible: "option.admissible (%(f::'a \ 'b option). ``` krauss@43081 ` 288` ``` (\x y. f x = Some y \ P x y))" ``` krauss@43081 ` 289` ```proof (rule ccpo.admissibleI[OF option.ccpo]) ``` krauss@43081 ` 290` ``` fix A :: "('a \ 'b option) set" ``` krauss@43081 ` 291` ``` assume ch: "chain option.le_fun A" ``` krauss@43081 ` 292` ``` and IH: "\f\A. \x y. f x = Some y \ P x y" ``` krauss@43081 ` 293` ``` from ch have ch': "\x. chain option_ord {y. \f\A. y = f x}" by (rule chain_fun) ``` krauss@43081 ` 294` ``` show "\x y. option.lub_fun A x = Some y \ P x y" ``` krauss@43081 ` 295` ``` proof (intro allI impI) ``` krauss@43081 ` 296` ``` fix x y assume "option.lub_fun A x = Some y" ``` krauss@43081 ` 297` ``` from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]] ``` krauss@43081 ` 298` ``` have "Some y \ {y. \f\A. y = f x}" by simp ``` krauss@43081 ` 299` ``` then have "\f\A. f x = Some y" by auto ``` krauss@43081 ` 300` ``` with IH show "P x y" by auto ``` krauss@43081 ` 301` ``` qed ``` krauss@43081 ` 302` ```qed ``` krauss@43081 ` 303` krauss@43082 ` 304` ```lemma fixp_induct_option: ``` krauss@43082 ` 305` ``` fixes F :: "'c \ 'c" and ``` krauss@43082 ` 306` ``` U :: "'c \ 'b \ 'a option" and ``` krauss@43082 ` 307` ``` C :: "('b \ 'a option) \ 'c" and ``` krauss@43082 ` 308` ``` P :: "'b \ 'a \ bool" ``` krauss@43082 ` 309` ``` assumes mono: "\x. mono_option (\f. U (F (C f)) x)" ``` huffman@46041 ` 310` ``` assumes eq: "f \ C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\f. U (F (C f))))" ``` krauss@43082 ` 311` ``` assumes inverse2: "\f. U (C f) = f" ``` krauss@43082 ` 312` ``` assumes step: "\f x y. (\x y. U f x = Some y \ P x y) \ U (F f) x = Some y \ P x y" ``` krauss@43082 ` 313` ``` assumes defined: "U f x = Some y" ``` krauss@43082 ` 314` ``` shows "P x y" ``` krauss@43082 ` 315` ``` using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] ``` krauss@43082 ` 316` ``` by blast ``` krauss@43082 ` 317` krauss@43082 ` 318` ```declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} ``` krauss@43082 ` 319` ``` @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} ``` krauss@43082 ` 320` krauss@43082 ` 321` ```declaration {* Partial_Function.init "option" @{term option.fixp_fun} ``` krauss@43082 ` 322` ``` @{term option.mono_body} @{thm option.fixp_rule_uc} ``` krauss@43082 ` 323` ``` (SOME @{thm fixp_induct_option}) *} ``` krauss@43082 ` 324` krauss@43081 ` 325` krauss@40252 ` 326` ```hide_const (open) chain ``` krauss@40107 ` 327` krauss@40107 ` 328` ```end ```