src/HOL/Partial_Function.thy
 author kuncar Fri Dec 09 18:07:04 2011 +0100 (2011-12-09) changeset 45802 b16f976db515 parent 45297 3c9f17d017bf child 46041 1e3ff542e83e permissions -rw-r--r--
Quotient_Info stores only relation maps
```     1 (* Title:    HOL/Partial_Function.thy
```
```     2    Author:   Alexander Krauss, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Partial Function Definitions *}
```
```     6
```
```     7 theory Partial_Function
```
```     8 imports Complete_Partial_Order Option
```
```     9 uses
```
```    10   "Tools/Function/function_lib.ML"
```
```    11   "Tools/Function/partial_function.ML"
```
```    12 begin
```
```    13
```
```    14 setup Partial_Function.setup
```
```    15
```
```    16 subsection {* Axiomatic setup *}
```
```    17
```
```    18 text {* This techical locale constains the requirements for function
```
```    19   definitions with ccpo fixed points. *}
```
```    20
```
```    21 definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
```
```    22 definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
```
```    23 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
```
```    24 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
```
```    25
```
```    26 lemma chain_fun:
```
```    27   assumes A: "chain (fun_ord ord) A"
```
```    28   shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
```
```    29 proof (rule chainI)
```
```    30   fix x y assume "x \<in> ?C" "y \<in> ?C"
```
```    31   then obtain f g where fg: "f \<in> A" "g \<in> A"
```
```    32     and [simp]: "x = f a" "y = g a" by blast
```
```    33   from chainD[OF A fg]
```
```    34   show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
```
```    35 qed
```
```    36
```
```    37 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
```
```    38 by (rule monotoneI) (auto simp: fun_ord_def)
```
```    39
```
```    40 lemma let_mono[partial_function_mono]:
```
```    41   "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
```
```    42   \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
```
```    43 by (simp add: Let_def)
```
```    44
```
```    45 lemma if_mono[partial_function_mono]: "monotone orda ordb F
```
```    46 \<Longrightarrow> monotone orda ordb G
```
```    47 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
```
```    48 unfolding monotone_def by simp
```
```    49
```
```    50 definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
```
```    51
```
```    52 locale partial_function_definitions =
```
```    53   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```    54   fixes lub :: "'a set \<Rightarrow> 'a"
```
```    55   assumes leq_refl: "leq x x"
```
```    56   assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
```
```    57   assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
```
```    58   assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
```
```    59   assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
```
```    60
```
```    61 lemma partial_function_lift:
```
```    62   assumes "partial_function_definitions ord lb"
```
```    63   shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
```
```    64 proof -
```
```    65   interpret partial_function_definitions ord lb by fact
```
```    66
```
```    67   show ?thesis
```
```    68   proof
```
```    69     fix x show "?ordf x x"
```
```    70       unfolding fun_ord_def by (auto simp: leq_refl)
```
```    71   next
```
```    72     fix x y z assume "?ordf x y" "?ordf y z"
```
```    73     thus "?ordf x z" unfolding fun_ord_def
```
```    74       by (force dest: leq_trans)
```
```    75   next
```
```    76     fix x y assume "?ordf x y" "?ordf y x"
```
```    77     thus "x = y" unfolding fun_ord_def
```
```    78       by (force intro!: dest: leq_antisym)
```
```    79   next
```
```    80     fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
```
```    81     thus "?ordf f (?lubf A)"
```
```    82       unfolding fun_lub_def fun_ord_def
```
```    83       by (blast intro: lub_upper chain_fun[OF A] f)
```
```    84   next
```
```    85     fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
```
```    86     assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
```
```    87     show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
```
```    88       by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
```
```    89    qed
```
```    90 qed
```
```    91
```
```    92 lemma ccpo: assumes "partial_function_definitions ord lb"
```
```    93   shows "class.ccpo ord (mk_less ord) lb"
```
```    94 using assms unfolding partial_function_definitions_def mk_less_def
```
```    95 by unfold_locales blast+
```
```    96
```
```    97 lemma partial_function_image:
```
```    98   assumes "partial_function_definitions ord Lub"
```
```    99   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
```
```   100   assumes inv: "\<And>x. f (g x) = x"
```
```   101   shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
```
```   102 proof -
```
```   103   let ?iord = "img_ord f ord"
```
```   104   let ?ilub = "img_lub f g Lub"
```
```   105
```
```   106   interpret partial_function_definitions ord Lub by fact
```
```   107   show ?thesis
```
```   108   proof
```
```   109     fix A x assume "chain ?iord A" "x \<in> A"
```
```   110     then have "chain ord (f ` A)" "f x \<in> f ` A"
```
```   111       by (auto simp: img_ord_def intro: chainI dest: chainD)
```
```   112     thus "?iord x (?ilub A)"
```
```   113       unfolding inv img_lub_def img_ord_def by (rule lub_upper)
```
```   114   next
```
```   115     fix A x assume "chain ?iord A"
```
```   116       and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
```
```   117     then have "chain ord (f ` A)"
```
```   118       by (auto simp: img_ord_def intro: chainI dest: chainD)
```
```   119     thus "?iord (?ilub A) x"
```
```   120       unfolding inv img_lub_def img_ord_def
```
```   121       by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
```
```   122   qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
```
```   123 qed
```
```   124
```
```   125 context partial_function_definitions
```
```   126 begin
```
```   127
```
```   128 abbreviation "le_fun \<equiv> fun_ord leq"
```
```   129 abbreviation "lub_fun \<equiv> fun_lub lub"
```
```   130 abbreviation "fixp_fun \<equiv> ccpo.fixp le_fun lub_fun"
```
```   131 abbreviation "mono_body \<equiv> monotone le_fun leq"
```
```   132 abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
```
```   133
```
```   134 text {* Interpret manually, to avoid flooding everything with facts about
```
```   135   orders *}
```
```   136
```
```   137 lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun"
```
```   138 apply (rule ccpo)
```
```   139 apply (rule partial_function_lift)
```
```   140 apply (rule partial_function_definitions_axioms)
```
```   141 done
```
```   142
```
```   143 text {* The crucial fixed-point theorem *}
```
```   144
```
```   145 lemma mono_body_fixp:
```
```   146   "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
```
```   147 by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
```
```   148
```
```   149 text {* Version with curry/uncurry combinators, to be used by package *}
```
```   150
```
```   151 lemma fixp_rule_uc:
```
```   152   fixes F :: "'c \<Rightarrow> 'c" and
```
```   153     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
```
```   154     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
```
```   155   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
```
```   156   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
```
```   157   assumes inverse: "\<And>f. C (U f) = f"
```
```   158   shows "f = F f"
```
```   159 proof -
```
```   160   have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
```
```   161   also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
```
```   162     by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
```
```   163   also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
```
```   164   also have "... = F f" by (simp add: eq)
```
```   165   finally show "f = F f" .
```
```   166 qed
```
```   167
```
```   168 text {* Fixpoint induction rule *}
```
```   169
```
```   170 lemma fixp_induct_uc:
```
```   171   fixes F :: "'c \<Rightarrow> 'c" and
```
```   172     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
```
```   173     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
```
```   174     P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
```
```   175   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
```
```   176   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
```
```   177   assumes inverse: "\<And>f. U (C f) = f"
```
```   178   assumes adm: "ccpo.admissible le_fun lub_fun P"
```
```   179   assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
```
```   180   shows "P (U f)"
```
```   181 unfolding eq inverse
```
```   182 apply (rule ccpo.fixp_induct[OF ccpo adm])
```
```   183 apply (insert mono, auto simp: monotone_def fun_ord_def)[1]
```
```   184 by (rule_tac f="C x" in step, simp add: inverse)
```
```   185
```
```   186
```
```   187 text {* Rules for @{term mono_body}: *}
```
```   188
```
```   189 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
```
```   190 by (rule monotoneI) (rule leq_refl)
```
```   191
```
```   192 end
```
```   193
```
```   194
```
```   195 subsection {* Flat interpretation: tailrec and option *}
```
```   196
```
```   197 definition
```
```   198   "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
```
```   199
```
```   200 definition
```
```   201   "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
```
```   202
```
```   203 lemma flat_interpretation:
```
```   204   "partial_function_definitions (flat_ord b) (flat_lub b)"
```
```   205 proof
```
```   206   fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
```
```   207   show "flat_ord b x (flat_lub b A)"
```
```   208   proof cases
```
```   209     assume "x = b"
```
```   210     thus ?thesis by (simp add: flat_ord_def)
```
```   211   next
```
```   212     assume "x \<noteq> b"
```
```   213     with 1 have "A - {b} = {x}"
```
```   214       by (auto elim: chainE simp: flat_ord_def)
```
```   215     then have "flat_lub b A = x"
```
```   216       by (auto simp: flat_lub_def)
```
```   217     thus ?thesis by (auto simp: flat_ord_def)
```
```   218   qed
```
```   219 next
```
```   220   fix A z assume A: "chain (flat_ord b) A"
```
```   221     and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
```
```   222   show "flat_ord b (flat_lub b A) z"
```
```   223   proof cases
```
```   224     assume "A \<subseteq> {b}"
```
```   225     thus ?thesis
```
```   226       by (auto simp: flat_lub_def flat_ord_def)
```
```   227   next
```
```   228     assume nb: "\<not> A \<subseteq> {b}"
```
```   229     then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
```
```   230     with A have "A - {b} = {y}"
```
```   231       by (auto elim: chainE simp: flat_ord_def)
```
```   232     with nb have "flat_lub b A = y"
```
```   233       by (auto simp: flat_lub_def)
```
```   234     with z y show ?thesis by auto
```
```   235   qed
```
```   236 qed (auto simp: flat_ord_def)
```
```   237
```
```   238 interpretation tailrec!:
```
```   239   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
```
```   240 by (rule flat_interpretation)
```
```   241
```
```   242 interpretation option!:
```
```   243   partial_function_definitions "flat_ord None" "flat_lub None"
```
```   244 by (rule flat_interpretation)
```
```   245
```
```   246
```
```   247 abbreviation "option_ord \<equiv> flat_ord None"
```
```   248 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
```
```   249
```
```   250 lemma bind_mono[partial_function_mono]:
```
```   251 assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
```
```   252 shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
```
```   253 proof (rule monotoneI)
```
```   254   fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
```
```   255   with mf
```
```   256   have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
```
```   257   then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
```
```   258     unfolding flat_ord_def by auto
```
```   259   also from mg
```
```   260   have "\<And>y'. option_ord (C y' f) (C y' g)"
```
```   261     by (rule monotoneD) (rule fg)
```
```   262   then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
```
```   263     unfolding flat_ord_def by (cases "B g") auto
```
```   264   finally (option.leq_trans)
```
```   265   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
```
```   266 qed
```
```   267
```
```   268 lemma flat_lub_in_chain:
```
```   269   assumes ch: "chain (flat_ord b) A "
```
```   270   assumes lub: "flat_lub b A = a"
```
```   271   shows "a = b \<or> a \<in> A"
```
```   272 proof (cases "A \<subseteq> {b}")
```
```   273   case True
```
```   274   then have "flat_lub b A = b" unfolding flat_lub_def by simp
```
```   275   with lub show ?thesis by simp
```
```   276 next
```
```   277   case False
```
```   278   then obtain c where "c \<in> A" and "c \<noteq> b" by auto
```
```   279   { fix z assume "z \<in> A"
```
```   280     from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
```
```   281       unfolding flat_ord_def using `c \<noteq> b` by auto }
```
```   282   with False have "A - {b} = {c}" by auto
```
```   283   with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
```
```   284   with `c \<in> A` lub show ?thesis by simp
```
```   285 qed
```
```   286
```
```   287 lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
```
```   288   (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
```
```   289 proof (rule ccpo.admissibleI[OF option.ccpo])
```
```   290   fix A :: "('a \<Rightarrow> 'b option) set"
```
```   291   assume ch: "chain option.le_fun A"
```
```   292     and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
```
```   293   from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
```
```   294   show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
```
```   295   proof (intro allI impI)
```
```   296     fix x y assume "option.lub_fun A x = Some y"
```
```   297     from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
```
```   298     have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
```
```   299     then have "\<exists>f\<in>A. f x = Some y" by auto
```
```   300     with IH show "P x y" by auto
```
```   301   qed
```
```   302 qed
```
```   303
```
```   304 lemma fixp_induct_option:
```
```   305   fixes F :: "'c \<Rightarrow> 'c" and
```
```   306     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
```
```   307     C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
```
```   308     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
```
```   309   assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
```
```   310   assumes eq: "f \<equiv> C (ccpo.fixp (fun_ord option_ord) (fun_lub (flat_lub None)) (\<lambda>f. U (F (C f))))"
```
```   311   assumes inverse2: "\<And>f. U (C f) = f"
```
```   312   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"
```
```   313   assumes defined: "U f x = Some y"
```
```   314   shows "P x y"
```
```   315   using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
```
```   316   by blast
```
```   317
```
```   318 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
```
```   319   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
```
```   320
```
```   321 declaration {* Partial_Function.init "option" @{term option.fixp_fun}
```
```   322   @{term option.mono_body} @{thm option.fixp_rule_uc}
```
```   323   (SOME @{thm fixp_induct_option}) *}
```
```   324
```
```   325
```
```   326 hide_const (open) chain
```
```   327
```
```   328 end
```
```   329
```