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