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