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