src/HOL/Partial_Function.thy
author krauss
Fri Oct 29 21:41:14 2010 +0200 (2010-10-29)
changeset 40288 520199d8b66e
parent 40252 029400b6c893
child 42949 618adb3584e5
permissions -rw-r--r--
added rule let_mono
     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 call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    27 by (rule monotoneI) (auto simp: fun_ord_def)
    28 
    29 lemma let_mono[partial_function_mono]:
    30   "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
    31   \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
    32 by (simp add: Let_def)
    33 
    34 lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    35 \<Longrightarrow> monotone orda ordb G
    36 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
    37 unfolding monotone_def by simp
    38 
    39 definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
    40 
    41 locale partial_function_definitions = 
    42   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    43   fixes lub :: "'a set \<Rightarrow> 'a"
    44   assumes leq_refl: "leq x x"
    45   assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
    46   assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
    47   assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
    48   assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
    49 
    50 lemma partial_function_lift:
    51   assumes "partial_function_definitions ord lb"
    52   shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
    53 proof -
    54   interpret partial_function_definitions ord lb by fact
    55 
    56   { fix A a assume A: "chain ?ordf A"
    57     have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    58     proof (rule chainI)
    59       fix x y assume "x \<in> ?C" "y \<in> ?C"
    60       then obtain f g where fg: "f \<in> A" "g \<in> A" 
    61         and [simp]: "x = f a" "y = g a" by blast
    62       from chainD[OF A fg]
    63       show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    64     qed }
    65   note chain_fun = this
    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!: ext 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 == ccpo.fixp le_fun lub_fun"
   131 abbreviation "mono_body \<equiv> monotone le_fun leq"
   132 
   133 text {* Interpret manually, to avoid flooding everything with facts about
   134   orders *}
   135 
   136 lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_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 {* Rules for @{term mono_body}: *}
   168 
   169 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
   170 by (rule monotoneI) (rule leq_refl)
   171 
   172 declaration {* Partial_Function.init @{term fixp_fun}
   173   @{term mono_body} @{thm fixp_rule_uc} *}
   174 
   175 end
   176 
   177 
   178 subsection {* Flat interpretation: tailrec and option *}
   179 
   180 definition 
   181   "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
   182 
   183 definition 
   184   "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
   185 
   186 lemma flat_interpretation:
   187   "partial_function_definitions (flat_ord b) (flat_lub b)"
   188 proof
   189   fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
   190   show "flat_ord b x (flat_lub b A)"
   191   proof cases
   192     assume "x = b"
   193     thus ?thesis by (simp add: flat_ord_def)
   194   next
   195     assume "x \<noteq> b"
   196     with 1 have "A - {b} = {x}"
   197       by (auto elim: chainE simp: flat_ord_def)
   198     then have "flat_lub b A = x"
   199       by (auto simp: flat_lub_def)
   200     thus ?thesis by (auto simp: flat_ord_def)
   201   qed
   202 next
   203   fix A z assume A: "chain (flat_ord b) A"
   204     and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
   205   show "flat_ord b (flat_lub b A) z"
   206   proof cases
   207     assume "A \<subseteq> {b}"
   208     thus ?thesis
   209       by (auto simp: flat_lub_def flat_ord_def)
   210   next
   211     assume nb: "\<not> A \<subseteq> {b}"
   212     then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
   213     with A have "A - {b} = {y}"
   214       by (auto elim: chainE simp: flat_ord_def)
   215     with nb have "flat_lub b A = y"
   216       by (auto simp: flat_lub_def)
   217     with z y show ?thesis by auto    
   218   qed
   219 qed (auto simp: flat_ord_def)
   220 
   221 interpretation tailrec!:
   222   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   223 by (rule flat_interpretation)
   224 
   225 interpretation option!:
   226   partial_function_definitions "flat_ord None" "flat_lub None"
   227 by (rule flat_interpretation)
   228 
   229 abbreviation "option_ord \<equiv> flat_ord None"
   230 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
   231 
   232 lemma bind_mono[partial_function_mono]:
   233 assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
   234 shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
   235 proof (rule monotoneI)
   236   fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
   237   with mf
   238   have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
   239   then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
   240     unfolding flat_ord_def by auto    
   241   also from mg
   242   have "\<And>y'. option_ord (C y' f) (C y' g)"
   243     by (rule monotoneD) (rule fg)
   244   then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
   245     unfolding flat_ord_def by (cases "B g") auto
   246   finally (option.leq_trans)
   247   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
   248 qed
   249 
   250 hide_const (open) chain
   251 
   252 end
   253