src/HOL/Partial_Function.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61841 4d3527b94f2a
child 62390 842917225d56
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (* Title:    HOL/Partial_Function.thy
     2    Author:   Alexander Krauss, TU Muenchen
     3 *)
     4 
     5 section \<open>Partial Function Definitions\<close>
     6 
     7 theory Partial_Function
     8 imports Complete_Partial_Order Fun_Def_Base Option
     9 keywords "partial_function" :: thy_decl
    10 begin
    11 
    12 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
    13 ML_file "Tools/Function/partial_function.ML"
    14 
    15 lemma (in ccpo) in_chain_finite:
    16   assumes "Complete_Partial_Order.chain op \<le> A" "finite A" "A \<noteq> {}"
    17   shows "\<Squnion>A \<in> A"
    18 using assms(2,1,3)
    19 proof induction
    20   case empty thus ?case by simp
    21 next
    22   case (insert x A)
    23   note chain = \<open>Complete_Partial_Order.chain op \<le> (insert x A)\<close>
    24   show ?case
    25   proof(cases "A = {}")
    26     case True thus ?thesis by simp
    27   next
    28     case False
    29     from chain have chain': "Complete_Partial_Order.chain op \<le> A"
    30       by(rule chain_subset) blast
    31     hence "\<Squnion>A \<in> A" using False by(rule insert.IH)
    32     show ?thesis
    33     proof(cases "x \<le> \<Squnion>A")
    34       case True
    35       have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
    36         by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
    37       hence "\<Squnion>insert x A = \<Squnion>A"
    38         by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
    39       with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
    40     next
    41       case False
    42       with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
    43       have "\<Squnion>insert x A = x"
    44         by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
    45       thus ?thesis by simp
    46     qed
    47   qed
    48 qed
    49 
    50 subsection \<open>Axiomatic setup\<close>
    51 
    52 text \<open>This techical locale constains the requirements for function
    53   definitions with ccpo fixed points.\<close>
    54 
    55 definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
    56 definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
    57 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
    58 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
    59 
    60 lemma chain_fun: 
    61   assumes A: "chain (fun_ord ord) A"
    62   shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    63 proof (rule chainI)
    64   fix x y assume "x \<in> ?C" "y \<in> ?C"
    65   then obtain f g where fg: "f \<in> A" "g \<in> A" 
    66     and [simp]: "x = f a" "y = g a" by blast
    67   from chainD[OF A fg]
    68   show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    69 qed
    70 
    71 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    72 by (rule monotoneI) (auto simp: fun_ord_def)
    73 
    74 lemma let_mono[partial_function_mono]:
    75   "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
    76   \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
    77 by (simp add: Let_def)
    78 
    79 lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    80 \<Longrightarrow> monotone orda ordb G
    81 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
    82 unfolding monotone_def by simp
    83 
    84 definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
    85 
    86 locale partial_function_definitions = 
    87   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    88   fixes lub :: "'a set \<Rightarrow> 'a"
    89   assumes leq_refl: "leq x x"
    90   assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
    91   assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
    92   assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
    93   assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
    94 
    95 lemma partial_function_lift:
    96   assumes "partial_function_definitions ord lb"
    97   shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
    98 proof -
    99   interpret partial_function_definitions ord lb by fact
   100 
   101   show ?thesis
   102   proof
   103     fix x show "?ordf x x"
   104       unfolding fun_ord_def by (auto simp: leq_refl)
   105   next
   106     fix x y z assume "?ordf x y" "?ordf y z"
   107     thus "?ordf x z" unfolding fun_ord_def 
   108       by (force dest: leq_trans)
   109   next
   110     fix x y assume "?ordf x y" "?ordf y x"
   111     thus "x = y" unfolding fun_ord_def
   112       by (force intro!: dest: leq_antisym)
   113   next
   114     fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
   115     thus "?ordf f (?lubf A)"
   116       unfolding fun_lub_def fun_ord_def
   117       by (blast intro: lub_upper chain_fun[OF A] f)
   118   next
   119     fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
   120     assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
   121     show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
   122       by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
   123    qed
   124 qed
   125 
   126 lemma ccpo: assumes "partial_function_definitions ord lb"
   127   shows "class.ccpo lb ord (mk_less ord)"
   128 using assms unfolding partial_function_definitions_def mk_less_def
   129 by unfold_locales blast+
   130 
   131 lemma partial_function_image:
   132   assumes "partial_function_definitions ord Lub"
   133   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
   134   assumes inv: "\<And>x. f (g x) = x"
   135   shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
   136 proof -
   137   let ?iord = "img_ord f ord"
   138   let ?ilub = "img_lub f g Lub"
   139 
   140   interpret partial_function_definitions ord Lub by fact
   141   show ?thesis
   142   proof
   143     fix A x assume "chain ?iord A" "x \<in> A"
   144     then have "chain ord (f ` A)" "f x \<in> f ` A"
   145       by (auto simp: img_ord_def intro: chainI dest: chainD)
   146     thus "?iord x (?ilub A)"
   147       unfolding inv img_lub_def img_ord_def by (rule lub_upper)
   148   next
   149     fix A x assume "chain ?iord A"
   150       and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
   151     then have "chain ord (f ` A)"
   152       by (auto simp: img_ord_def intro: chainI dest: chainD)
   153     thus "?iord (?ilub A) x"
   154       unfolding inv img_lub_def img_ord_def
   155       by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
   156   qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
   157 qed
   158 
   159 context partial_function_definitions
   160 begin
   161 
   162 abbreviation "le_fun \<equiv> fun_ord leq"
   163 abbreviation "lub_fun \<equiv> fun_lub lub"
   164 abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun"
   165 abbreviation "mono_body \<equiv> monotone le_fun leq"
   166 abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun"
   167 
   168 text \<open>Interpret manually, to avoid flooding everything with facts about
   169   orders\<close>
   170 
   171 lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"
   172 apply (rule ccpo)
   173 apply (rule partial_function_lift)
   174 apply (rule partial_function_definitions_axioms)
   175 done
   176 
   177 text \<open>The crucial fixed-point theorem\<close>
   178 
   179 lemma mono_body_fixp: 
   180   "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
   181 by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
   182 
   183 text \<open>Version with curry/uncurry combinators, to be used by package\<close>
   184 
   185 lemma fixp_rule_uc:
   186   fixes F :: "'c \<Rightarrow> 'c" and
   187     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   188     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   189   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   190   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   191   assumes inverse: "\<And>f. C (U f) = f"
   192   shows "f = F f"
   193 proof -
   194   have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
   195   also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
   196     by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
   197   also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
   198   also have "... = F f" by (simp add: eq)
   199   finally show "f = F f" .
   200 qed
   201 
   202 text \<open>Fixpoint induction rule\<close>
   203 
   204 lemma fixp_induct_uc:
   205   fixes F :: "'c \<Rightarrow> 'c"
   206     and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
   207     and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   208     and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
   209   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   210     and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   211     and inverse: "\<And>f. U (C f) = f"
   212     and adm: "ccpo.admissible lub_fun le_fun P"
   213     and bot: "P (\<lambda>_. lub {})"
   214     and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
   215   shows "P (U f)"
   216 unfolding eq inverse
   217 apply (rule ccpo.fixp_induct[OF ccpo adm])
   218 apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
   219 apply (rule_tac f5="C x" in step)
   220 apply (simp add: inverse)
   221 done
   222 
   223 
   224 text \<open>Rules for @{term mono_body}:\<close>
   225 
   226 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
   227 by (rule monotoneI) (rule leq_refl)
   228 
   229 end
   230 
   231 
   232 subsection \<open>Flat interpretation: tailrec and option\<close>
   233 
   234 definition 
   235   "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
   236 
   237 definition 
   238   "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
   239 
   240 lemma flat_interpretation:
   241   "partial_function_definitions (flat_ord b) (flat_lub b)"
   242 proof
   243   fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
   244   show "flat_ord b x (flat_lub b A)"
   245   proof cases
   246     assume "x = b"
   247     thus ?thesis by (simp add: flat_ord_def)
   248   next
   249     assume "x \<noteq> b"
   250     with 1 have "A - {b} = {x}"
   251       by (auto elim: chainE simp: flat_ord_def)
   252     then have "flat_lub b A = x"
   253       by (auto simp: flat_lub_def)
   254     thus ?thesis by (auto simp: flat_ord_def)
   255   qed
   256 next
   257   fix A z assume A: "chain (flat_ord b) A"
   258     and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
   259   show "flat_ord b (flat_lub b A) z"
   260   proof cases
   261     assume "A \<subseteq> {b}"
   262     thus ?thesis
   263       by (auto simp: flat_lub_def flat_ord_def)
   264   next
   265     assume nb: "\<not> A \<subseteq> {b}"
   266     then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
   267     with A have "A - {b} = {y}"
   268       by (auto elim: chainE simp: flat_ord_def)
   269     with nb have "flat_lub b A = y"
   270       by (auto simp: flat_lub_def)
   271     with z y show ?thesis by auto    
   272   qed
   273 qed (auto simp: flat_ord_def)
   274 
   275 lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y"
   276 by(auto simp add: flat_ord_def)
   277 
   278 lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
   279 by(auto simp add: flat_ord_def)
   280 
   281 lemma antisymP_flat_ord: "antisymP (flat_ord a)"
   282 by(rule antisymI)(auto dest: flat_ord_antisym)
   283 
   284 interpretation tailrec:
   285   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   286   rewrites "flat_lub undefined {} \<equiv> undefined"
   287 by (rule flat_interpretation)(simp add: flat_lub_def)
   288 
   289 interpretation option:
   290   partial_function_definitions "flat_ord None" "flat_lub None"
   291   rewrites "flat_lub None {} \<equiv> None"
   292 by (rule flat_interpretation)(simp add: flat_lub_def)
   293 
   294 
   295 abbreviation "tailrec_ord \<equiv> flat_ord undefined"
   296 abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
   297 
   298 lemma tailrec_admissible:
   299   "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
   300      (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))"
   301 proof(intro ccpo.admissibleI strip)
   302   fix A x
   303   assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
   304     and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)"
   305     and defined: "fun_lub (flat_lub c) A x \<noteq> c"
   306   from defined obtain f where f: "f \<in> A" "f x \<noteq> c"
   307     by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
   308   hence "P x (f x)" by(rule P)
   309   moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x"
   310     by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
   311   hence "fun_lub (flat_lub c) A x = f x"
   312     using f by(auto simp add: fun_lub_def flat_lub_def)
   313   ultimately show "P x (fun_lub (flat_lub c) A x)" by simp
   314 qed
   315 
   316 lemma fixp_induct_tailrec:
   317   fixes F :: "'c \<Rightarrow> 'c" and
   318     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   319     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
   320     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
   321     x :: "'b"
   322   assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)"
   323   assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))"
   324   assumes inverse2: "\<And>f. U (C f) = f"
   325   assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y"
   326   assumes result: "U f x = y"
   327   assumes defined: "y \<noteq> c"
   328   shows "P x y"
   329 proof -
   330   have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
   331     by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
   332       (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
   333   thus ?thesis using result defined by blast
   334 qed
   335 
   336 lemma admissible_image:
   337   assumes pfun: "partial_function_definitions le lub"
   338   assumes adm: "ccpo.admissible lub le (P o g)"
   339   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
   340   assumes inv: "\<And>x. f (g x) = x"
   341   shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
   342 proof (rule ccpo.admissibleI)
   343   fix A assume "chain (img_ord f le) A"
   344   then have ch': "chain le (f ` A)"
   345     by (auto simp: img_ord_def intro: chainI dest: chainD)
   346   assume "A \<noteq> {}"
   347   assume P_A: "\<forall>x\<in>A. P x"
   348   have "(P o g) (lub (f ` A))" using adm ch'
   349   proof (rule ccpo.admissibleD)
   350     fix x assume "x \<in> f ` A"
   351     with P_A show "(P o g) x" by (auto simp: inj[OF inv])
   352   qed(simp add: \<open>A \<noteq> {}\<close>)
   353   thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
   354 qed
   355 
   356 lemma admissible_fun:
   357   assumes pfun: "partial_function_definitions le lub"
   358   assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
   359   shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
   360 proof (rule ccpo.admissibleI)
   361   fix A :: "('b \<Rightarrow> 'a) set"
   362   assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
   363   assume ch: "chain (fun_ord le) A"
   364   assume "A \<noteq> {}"
   365   hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto
   366   show "\<forall>x. Q x (fun_lub lub A x)"
   367     unfolding fun_lub_def
   368     by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
   369       (auto simp: Q)
   370 qed
   371 
   372 
   373 abbreviation "option_ord \<equiv> flat_ord None"
   374 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
   375 
   376 lemma bind_mono[partial_function_mono]:
   377 assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
   378 shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
   379 proof (rule monotoneI)
   380   fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
   381   with mf
   382   have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
   383   then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
   384     unfolding flat_ord_def by auto    
   385   also from mg
   386   have "\<And>y'. option_ord (C y' f) (C y' g)"
   387     by (rule monotoneD) (rule fg)
   388   then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
   389     unfolding flat_ord_def by (cases "B g") auto
   390   finally (option.leq_trans)
   391   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
   392 qed
   393 
   394 lemma flat_lub_in_chain:
   395   assumes ch: "chain (flat_ord b) A "
   396   assumes lub: "flat_lub b A = a"
   397   shows "a = b \<or> a \<in> A"
   398 proof (cases "A \<subseteq> {b}")
   399   case True
   400   then have "flat_lub b A = b" unfolding flat_lub_def by simp
   401   with lub show ?thesis by simp
   402 next
   403   case False
   404   then obtain c where "c \<in> A" and "c \<noteq> b" by auto
   405   { fix z assume "z \<in> A"
   406     from chainD[OF ch \<open>c \<in> A\<close> this] have "z = c \<or> z = b"
   407       unfolding flat_ord_def using \<open>c \<noteq> b\<close> by auto }
   408   with False have "A - {b} = {c}" by auto
   409   with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
   410   with \<open>c \<in> A\<close> lub show ?thesis by simp
   411 qed
   412 
   413 lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
   414   (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
   415 proof (rule ccpo.admissibleI)
   416   fix A :: "('a \<Rightarrow> 'b option) set"
   417   assume ch: "chain option.le_fun A"
   418     and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
   419   from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
   420   show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
   421   proof (intro allI impI)
   422     fix x y assume "option.lub_fun A x = Some y"
   423     from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
   424     have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
   425     then have "\<exists>f\<in>A. f x = Some y" by auto
   426     with IH show "P x y" by auto
   427   qed
   428 qed
   429 
   430 lemma fixp_induct_option:
   431   fixes F :: "'c \<Rightarrow> 'c" and
   432     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
   433     C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
   434     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
   435   assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
   436   assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))"
   437   assumes inverse2: "\<And>f. U (C f) = f"
   438   assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y"
   439   assumes defined: "U f x = Some y"
   440   shows "P x y"
   441   using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
   442   unfolding fun_lub_def flat_lub_def by(auto 9 2)
   443 
   444 declaration \<open>Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
   445   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
   446   (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
   447 
   448 declaration \<open>Partial_Function.init "option" @{term option.fixp_fun}
   449   @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
   450   (SOME @{thm fixp_induct_option})\<close>
   451 
   452 hide_const (open) chain
   453 
   454 end