src/HOL/Partial_Function.thy
author blanchet
Sun May 04 18:14:58 2014 +0200 (2014-05-04)
changeset 56846 9df717fef2bb
parent 55085 0e8e4dc55866
child 57959 1bfed12a7646
permissions -rw-r--r--
renamed 'xxx_size' to 'size_xxx' for old datatype package
     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 Fun_Def_Base Option
     9 keywords "partial_function" :: thy_decl
    10 begin
    11 
    12 ML_file "Tools/Function/partial_function.ML"
    13 setup Partial_Function.setup
    14 
    15 subsection {* Axiomatic setup *}
    16 
    17 text {* This techical locale constains the requirements for function
    18   definitions with ccpo fixed points. *}
    19 
    20 definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
    21 definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
    22 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
    23 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
    24 
    25 lemma chain_fun: 
    26   assumes A: "chain (fun_ord ord) A"
    27   shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    28 proof (rule chainI)
    29   fix x y assume "x \<in> ?C" "y \<in> ?C"
    30   then obtain f g where fg: "f \<in> A" "g \<in> A" 
    31     and [simp]: "x = f a" "y = g a" by blast
    32   from chainD[OF A fg]
    33   show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    34 qed
    35 
    36 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    37 by (rule monotoneI) (auto simp: fun_ord_def)
    38 
    39 lemma let_mono[partial_function_mono]:
    40   "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
    41   \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
    42 by (simp add: Let_def)
    43 
    44 lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    45 \<Longrightarrow> monotone orda ordb G
    46 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
    47 unfolding monotone_def by simp
    48 
    49 definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
    50 
    51 locale partial_function_definitions = 
    52   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    53   fixes lub :: "'a set \<Rightarrow> 'a"
    54   assumes leq_refl: "leq x x"
    55   assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
    56   assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
    57   assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
    58   assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
    59 
    60 lemma partial_function_lift:
    61   assumes "partial_function_definitions ord lb"
    62   shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
    63 proof -
    64   interpret partial_function_definitions ord lb by fact
    65 
    66   show ?thesis
    67   proof
    68     fix x show "?ordf x x"
    69       unfolding fun_ord_def by (auto simp: leq_refl)
    70   next
    71     fix x y z assume "?ordf x y" "?ordf y z"
    72     thus "?ordf x z" unfolding fun_ord_def 
    73       by (force dest: leq_trans)
    74   next
    75     fix x y assume "?ordf x y" "?ordf y x"
    76     thus "x = y" unfolding fun_ord_def
    77       by (force intro!: dest: leq_antisym)
    78   next
    79     fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
    80     thus "?ordf f (?lubf A)"
    81       unfolding fun_lub_def fun_ord_def
    82       by (blast intro: lub_upper chain_fun[OF A] f)
    83   next
    84     fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
    85     assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
    86     show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
    87       by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
    88    qed
    89 qed
    90 
    91 lemma ccpo: assumes "partial_function_definitions ord lb"
    92   shows "class.ccpo lb ord (mk_less ord)"
    93 using assms unfolding partial_function_definitions_def mk_less_def
    94 by unfold_locales blast+
    95 
    96 lemma partial_function_image:
    97   assumes "partial_function_definitions ord Lub"
    98   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
    99   assumes inv: "\<And>x. f (g x) = x"
   100   shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
   101 proof -
   102   let ?iord = "img_ord f ord"
   103   let ?ilub = "img_lub f g Lub"
   104 
   105   interpret partial_function_definitions ord Lub by fact
   106   show ?thesis
   107   proof
   108     fix A x assume "chain ?iord A" "x \<in> A"
   109     then have "chain ord (f ` A)" "f x \<in> f ` A"
   110       by (auto simp: img_ord_def intro: chainI dest: chainD)
   111     thus "?iord x (?ilub A)"
   112       unfolding inv img_lub_def img_ord_def by (rule lub_upper)
   113   next
   114     fix A x assume "chain ?iord A"
   115       and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
   116     then have "chain ord (f ` A)"
   117       by (auto simp: img_ord_def intro: chainI dest: chainD)
   118     thus "?iord (?ilub A) x"
   119       unfolding inv img_lub_def img_ord_def
   120       by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
   121   qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
   122 qed
   123 
   124 context partial_function_definitions
   125 begin
   126 
   127 abbreviation "le_fun \<equiv> fun_ord leq"
   128 abbreviation "lub_fun \<equiv> fun_lub lub"
   129 abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun"
   130 abbreviation "mono_body \<equiv> monotone le_fun leq"
   131 abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun"
   132 
   133 text {* Interpret manually, to avoid flooding everything with facts about
   134   orders *}
   135 
   136 lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"
   137 apply (rule ccpo)
   138 apply (rule partial_function_lift)
   139 apply (rule partial_function_definitions_axioms)
   140 done
   141 
   142 text {* The crucial fixed-point theorem *}
   143 
   144 lemma mono_body_fixp: 
   145   "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
   146 by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
   147 
   148 text {* Version with curry/uncurry combinators, to be used by package *}
   149 
   150 lemma fixp_rule_uc:
   151   fixes F :: "'c \<Rightarrow> 'c" and
   152     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   153     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   154   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   155   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   156   assumes inverse: "\<And>f. C (U f) = f"
   157   shows "f = F f"
   158 proof -
   159   have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
   160   also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
   161     by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
   162   also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
   163   also have "... = F f" by (simp add: eq)
   164   finally show "f = F f" .
   165 qed
   166 
   167 text {* Fixpoint induction rule *}
   168 
   169 lemma fixp_induct_uc:
   170   fixes F :: "'c \<Rightarrow> 'c" and
   171     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   172     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
   173     P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
   174   assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   175   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   176   assumes inverse: "\<And>f. U (C f) = f"
   177   assumes adm: "ccpo.admissible lub_fun le_fun P"
   178   and bot: "P (\<lambda>_. lub {})"
   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 bot fun_lub_def)[2]
   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   where "flat_lub undefined {} \<equiv> undefined"
   241 by (rule flat_interpretation)(simp add: flat_lub_def)
   242 
   243 interpretation option!:
   244   partial_function_definitions "flat_ord None" "flat_lub None"
   245   where "flat_lub None {} \<equiv> None"
   246 by (rule flat_interpretation)(simp add: flat_lub_def)
   247 
   248 
   249 abbreviation "tailrec_ord \<equiv> flat_ord undefined"
   250 abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
   251 
   252 lemma tailrec_admissible:
   253   "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
   254      (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))"
   255 proof(intro ccpo.admissibleI strip)
   256   fix A x
   257   assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
   258     and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)"
   259     and defined: "fun_lub (flat_lub c) A x \<noteq> c"
   260   from defined obtain f where f: "f \<in> A" "f x \<noteq> c"
   261     by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
   262   hence "P x (f x)" by(rule P)
   263   moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x"
   264     by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
   265   hence "fun_lub (flat_lub c) A x = f x"
   266     using f by(auto simp add: fun_lub_def flat_lub_def)
   267   ultimately show "P x (fun_lub (flat_lub c) A x)" by simp
   268 qed
   269 
   270 lemma fixp_induct_tailrec:
   271   fixes F :: "'c \<Rightarrow> 'c" and
   272     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   273     C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
   274     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
   275     x :: "'b"
   276   assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)"
   277   assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))"
   278   assumes inverse2: "\<And>f. U (C f) = f"
   279   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"
   280   assumes result: "U f x = y"
   281   assumes defined: "y \<noteq> c"
   282   shows "P x y"
   283 proof -
   284   have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
   285     by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
   286       (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
   287   thus ?thesis using result defined by blast
   288 qed
   289 
   290 lemma admissible_image:
   291   assumes pfun: "partial_function_definitions le lub"
   292   assumes adm: "ccpo.admissible lub le (P o g)"
   293   assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
   294   assumes inv: "\<And>x. f (g x) = x"
   295   shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
   296 proof (rule ccpo.admissibleI)
   297   fix A assume "chain (img_ord f le) A"
   298   then have ch': "chain le (f ` A)"
   299     by (auto simp: img_ord_def intro: chainI dest: chainD)
   300   assume "A \<noteq> {}"
   301   assume P_A: "\<forall>x\<in>A. P x"
   302   have "(P o g) (lub (f ` A))" using adm ch'
   303   proof (rule ccpo.admissibleD)
   304     fix x assume "x \<in> f ` A"
   305     with P_A show "(P o g) x" by (auto simp: inj[OF inv])
   306   qed(simp add: `A \<noteq> {}`)
   307   thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
   308 qed
   309 
   310 lemma admissible_fun:
   311   assumes pfun: "partial_function_definitions le lub"
   312   assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
   313   shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
   314 proof (rule ccpo.admissibleI)
   315   fix A :: "('b \<Rightarrow> 'a) set"
   316   assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
   317   assume ch: "chain (fun_ord le) A"
   318   assume "A \<noteq> {}"
   319   hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto
   320   show "\<forall>x. Q x (fun_lub lub A x)"
   321     unfolding fun_lub_def
   322     by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
   323       (auto simp: Q)
   324 qed
   325 
   326 
   327 abbreviation "option_ord \<equiv> flat_ord None"
   328 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
   329 
   330 lemma bind_mono[partial_function_mono]:
   331 assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
   332 shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
   333 proof (rule monotoneI)
   334   fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
   335   with mf
   336   have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
   337   then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
   338     unfolding flat_ord_def by auto    
   339   also from mg
   340   have "\<And>y'. option_ord (C y' f) (C y' g)"
   341     by (rule monotoneD) (rule fg)
   342   then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
   343     unfolding flat_ord_def by (cases "B g") auto
   344   finally (option.leq_trans)
   345   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
   346 qed
   347 
   348 lemma flat_lub_in_chain:
   349   assumes ch: "chain (flat_ord b) A "
   350   assumes lub: "flat_lub b A = a"
   351   shows "a = b \<or> a \<in> A"
   352 proof (cases "A \<subseteq> {b}")
   353   case True
   354   then have "flat_lub b A = b" unfolding flat_lub_def by simp
   355   with lub show ?thesis by simp
   356 next
   357   case False
   358   then obtain c where "c \<in> A" and "c \<noteq> b" by auto
   359   { fix z assume "z \<in> A"
   360     from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
   361       unfolding flat_ord_def using `c \<noteq> b` by auto }
   362   with False have "A - {b} = {c}" by auto
   363   with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
   364   with `c \<in> A` lub show ?thesis by simp
   365 qed
   366 
   367 lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
   368   (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
   369 proof (rule ccpo.admissibleI)
   370   fix A :: "('a \<Rightarrow> 'b option) set"
   371   assume ch: "chain option.le_fun A"
   372     and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
   373   from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
   374   show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
   375   proof (intro allI impI)
   376     fix x y assume "option.lub_fun A x = Some y"
   377     from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
   378     have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
   379     then have "\<exists>f\<in>A. f x = Some y" by auto
   380     with IH show "P x y" by auto
   381   qed
   382 qed
   383 
   384 lemma fixp_induct_option:
   385   fixes F :: "'c \<Rightarrow> 'c" and
   386     U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
   387     C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
   388     P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
   389   assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
   390   assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))"
   391   assumes inverse2: "\<And>f. U (C f) = f"
   392   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"
   393   assumes defined: "U f x = Some y"
   394   shows "P x y"
   395   using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
   396   unfolding fun_lub_def flat_lub_def by(auto 9 2)
   397 
   398 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
   399   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
   400   (SOME @{thm fixp_induct_tailrec[where c=undefined]}) *}
   401 
   402 declaration {* Partial_Function.init "option" @{term option.fixp_fun}
   403   @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
   404   (SOME @{thm fixp_induct_option}) *}
   405 
   406 hide_const (open) chain
   407 
   408 end