src/HOL/Partial_Function.thy
author Andreas Lochbihler
Tue Mar 19 13:19:21 2013 +0100 (2013-03-19)
changeset 51459 bc3651180a09
parent 48891 c0eafbd55de3
child 51485 637aa1649ac7
permissions -rw-r--r--
add induction rule for partial_function (tailrec)
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
wenzelm@46950
     9
keywords "partial_function" :: thy_decl
krauss@40107
    10
begin
krauss@40107
    11
wenzelm@48891
    12
ML_file "Tools/Function/function_lib.ML"
wenzelm@48891
    13
ML_file "Tools/Function/partial_function.ML"
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 \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
krauss@40107
    22
definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
krauss@40107
    23
definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
krauss@40107
    24
definition "img_lub f g Lub = (\<lambda>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. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
krauss@43081
    29
proof (rule chainI)
krauss@43081
    30
  fix x y assume "x \<in> ?C" "y \<in> ?C"
krauss@43081
    31
  then obtain f g where fg: "f \<in> A" "g \<in> 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 \<or> 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 (\<lambda>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
  "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
krauss@40288
    42
  \<Longrightarrow> monotone orda ordb (\<lambda>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
\<Longrightarrow> monotone orda ordb G
krauss@40107
    47
\<Longrightarrow> monotone orda ordb (\<lambda>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 = (\<lambda>x y. R x y \<and> \<not> R y x)"
krauss@40107
    51
krauss@40107
    52
locale partial_function_definitions = 
krauss@40107
    53
  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
krauss@40107
    54
  fixes lub :: "'a set \<Rightarrow> 'a"
krauss@40107
    55
  assumes leq_refl: "leq x x"
krauss@40107
    56
  assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
krauss@40107
    57
  assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
krauss@40107
    58
  assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
krauss@40107
    59
  assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> 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 \<in> 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 \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
krauss@40107
    86
    assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?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: "\<And>x y. f x = f y \<Longrightarrow> x = y"
krauss@40107
   100
  assumes inv: "\<And>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 \<in> A"
krauss@40107
   110
    then have "chain ord (f ` A)" "f x \<in> 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: "\<And>z. z \<in> A \<Longrightarrow> ?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 \<equiv> fun_ord leq"
krauss@40107
   129
abbreviation "lub_fun \<equiv> fun_lub lub"
huffman@46041
   130
abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun"
krauss@40107
   131
abbreviation "mono_body \<equiv> monotone le_fun leq"
huffman@46041
   132
abbreviation "admissible \<equiv> 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
  "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> 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 \<Rightarrow> 'c" and
krauss@40107
   153
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
krauss@40107
   154
    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
krauss@40107
   155
  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
krauss@40107
   156
  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
krauss@40107
   157
  assumes inverse: "\<And>f. C (U f) = f"
krauss@40107
   158
  shows "f = F f"
krauss@40107
   159
proof -
krauss@40107
   160
  have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
krauss@40107
   161
  also have "... = C (U (F (C (fixp_fun (\<lambda>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 (\<lambda>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 \<Rightarrow> 'c" and
krauss@43082
   172
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
krauss@43082
   173
    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
krauss@43082
   174
    P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
krauss@43082
   175
  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
krauss@43082
   176
  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
krauss@43082
   177
  assumes inverse: "\<And>f. U (C f) = f"
huffman@46041
   178
  assumes adm: "ccpo.admissible lub_fun le_fun P"
krauss@43082
   179
  assumes step: "\<And>f. P (U f) \<Longrightarrow> 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 (\<lambda>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 \<longleftrightarrow> x = b \<or> x = y"
krauss@40107
   199
krauss@40107
   200
definition 
krauss@40107
   201
  "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> 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 \<in> 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 \<noteq> 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: "\<And>x. x \<in> A \<Longrightarrow> 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 \<subseteq> {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: "\<not> A \<subseteq> {b}"
krauss@40107
   229
    then obtain y where y: "y \<in> A" "y \<noteq> 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
Andreas@51459
   247
abbreviation "tailrec_ord \<equiv> flat_ord undefined"
Andreas@51459
   248
abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
Andreas@51459
   249
Andreas@51459
   250
lemma tailrec_admissible:
Andreas@51459
   251
  "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord)
Andreas@51459
   252
     (\<lambda>a. \<forall>x. a x \<noteq> undefined \<longrightarrow> P x (a x))"
Andreas@51459
   253
proof(intro ccpo.admissibleI[OF tailrec.ccpo] strip)
Andreas@51459
   254
  fix A x
Andreas@51459
   255
  assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A"
Andreas@51459
   256
    and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> undefined \<longrightarrow> P x (f x)"
Andreas@51459
   257
    and defined: "fun_lub (flat_lub undefined) A x \<noteq> undefined"
Andreas@51459
   258
  from defined obtain f where f: "f \<in> A" "f x \<noteq> undefined"
Andreas@51459
   259
    by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
Andreas@51459
   260
  hence "P x (f x)" by(rule P)
Andreas@51459
   261
  moreover from chain f have "\<forall>f' \<in> A. f' x = undefined \<or> f' x = f x"
Andreas@51459
   262
    by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
Andreas@51459
   263
  hence "fun_lub (flat_lub undefined) A x = f x"
Andreas@51459
   264
    using f by(auto simp add: fun_lub_def flat_lub_def)
Andreas@51459
   265
  ultimately show "P x (fun_lub (flat_lub undefined) A x)" by simp
Andreas@51459
   266
qed
Andreas@51459
   267
Andreas@51459
   268
lemma fixp_induct_tailrec:
Andreas@51459
   269
  fixes F :: "'c \<Rightarrow> 'c" and
Andreas@51459
   270
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
Andreas@51459
   271
    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
Andreas@51459
   272
    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
Andreas@51459
   273
    x :: "'b"
Andreas@51459
   274
  assumes mono: "\<And>x. mono_tailrec (\<lambda>f. U (F (C f)) x)"
Andreas@51459
   275
  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (\<lambda>f. U (F (C f))))"
Andreas@51459
   276
  assumes inverse2: "\<And>f. U (C f) = f"
Andreas@51459
   277
  assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> undefined \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> undefined \<Longrightarrow> P x y"
Andreas@51459
   278
  assumes result: "U f x = y"
Andreas@51459
   279
  assumes defined: "y \<noteq> undefined"
Andreas@51459
   280
  shows "P x y"
Andreas@51459
   281
proof -
Andreas@51459
   282
  have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> undefined \<longrightarrow> P x y"
Andreas@51459
   283
    by(rule tailrec.fixp_induct_uc[of U F C, OF mono eq inverse2])(auto intro: step tailrec_admissible)
Andreas@51459
   284
  thus ?thesis using result defined by blast
Andreas@51459
   285
qed
Andreas@51459
   286
Andreas@51459
   287
krauss@40107
   288
abbreviation "option_ord \<equiv> flat_ord None"
krauss@40107
   289
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
krauss@40107
   290
krauss@40107
   291
lemma bind_mono[partial_function_mono]:
krauss@40107
   292
assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
krauss@40107
   293
shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
krauss@40107
   294
proof (rule monotoneI)
krauss@40107
   295
  fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
krauss@40107
   296
  with mf
krauss@40107
   297
  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
krauss@40107
   298
  then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
krauss@40107
   299
    unfolding flat_ord_def by auto    
krauss@40107
   300
  also from mg
krauss@40107
   301
  have "\<And>y'. option_ord (C y' f) (C y' g)"
krauss@40107
   302
    by (rule monotoneD) (rule fg)
krauss@40107
   303
  then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
krauss@40107
   304
    unfolding flat_ord_def by (cases "B g") auto
krauss@40107
   305
  finally (option.leq_trans)
krauss@40107
   306
  show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
krauss@40107
   307
qed
krauss@40107
   308
krauss@43081
   309
lemma flat_lub_in_chain:
krauss@43081
   310
  assumes ch: "chain (flat_ord b) A "
krauss@43081
   311
  assumes lub: "flat_lub b A = a"
krauss@43081
   312
  shows "a = b \<or> a \<in> A"
krauss@43081
   313
proof (cases "A \<subseteq> {b}")
krauss@43081
   314
  case True
krauss@43081
   315
  then have "flat_lub b A = b" unfolding flat_lub_def by simp
krauss@43081
   316
  with lub show ?thesis by simp
krauss@43081
   317
next
krauss@43081
   318
  case False
krauss@43081
   319
  then obtain c where "c \<in> A" and "c \<noteq> b" by auto
krauss@43081
   320
  { fix z assume "z \<in> A"
krauss@43081
   321
    from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
krauss@43081
   322
      unfolding flat_ord_def using `c \<noteq> b` by auto }
krauss@43081
   323
  with False have "A - {b} = {c}" by auto
krauss@43081
   324
  with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
krauss@43081
   325
  with `c \<in> A` lub show ?thesis by simp
krauss@43081
   326
qed
krauss@43081
   327
krauss@43081
   328
lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
krauss@43081
   329
  (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
krauss@43081
   330
proof (rule ccpo.admissibleI[OF option.ccpo])
krauss@43081
   331
  fix A :: "('a \<Rightarrow> 'b option) set"
krauss@43081
   332
  assume ch: "chain option.le_fun A"
krauss@43081
   333
    and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
krauss@43081
   334
  from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
krauss@43081
   335
  show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
krauss@43081
   336
  proof (intro allI impI)
krauss@43081
   337
    fix x y assume "option.lub_fun A x = Some y"
krauss@43081
   338
    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
krauss@43081
   339
    have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
krauss@43081
   340
    then have "\<exists>f\<in>A. f x = Some y" by auto
krauss@43081
   341
    with IH show "P x y" by auto
krauss@43081
   342
  qed
krauss@43081
   343
qed
krauss@43081
   344
krauss@43082
   345
lemma fixp_induct_option:
krauss@43082
   346
  fixes F :: "'c \<Rightarrow> 'c" and
krauss@43082
   347
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
krauss@43082
   348
    C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
krauss@43082
   349
    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
krauss@43082
   350
  assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
huffman@46041
   351
  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))"
krauss@43082
   352
  assumes inverse2: "\<And>f. U (C f) = f"
krauss@43082
   353
  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"
krauss@43082
   354
  assumes defined: "U f x = Some y"
krauss@43082
   355
  shows "P x y"
krauss@43082
   356
  using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
krauss@43082
   357
  by blast
krauss@43082
   358
krauss@43082
   359
declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
Andreas@51459
   360
  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} 
Andreas@51459
   361
  (SOME @{thm fixp_induct_tailrec}) *}
krauss@43082
   362
krauss@43082
   363
declaration {* Partial_Function.init "option" @{term option.fixp_fun}
krauss@43082
   364
  @{term option.mono_body} @{thm option.fixp_rule_uc} 
krauss@43082
   365
  (SOME @{thm fixp_induct_option}) *}
krauss@43082
   366
krauss@40252
   367
hide_const (open) chain
krauss@40107
   368
krauss@40107
   369
end