src/HOL/Partial_Function.thy
changeset 40107 374f3ef9f940
child 40252 029400b6c893
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Partial_Function.thy	Sat Oct 23 23:41:19 2010 +0200
     1.3 @@ -0,0 +1,247 @@
     1.4 +(* Title:    HOL/Partial_Function.thy
     1.5 +   Author:   Alexander Krauss, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Partial Function Definitions *}
     1.9 +
    1.10 +theory Partial_Function
    1.11 +imports Complete_Partial_Order Option
    1.12 +uses 
    1.13 +  "Tools/Function/function_lib.ML" 
    1.14 +  "Tools/Function/partial_function.ML" 
    1.15 +begin
    1.16 +
    1.17 +setup Partial_Function.setup
    1.18 +
    1.19 +subsection {* Axiomatic setup *}
    1.20 +
    1.21 +text {* This techical locale constains the requirements for function
    1.22 +  definitions with ccpo fixed points.  *}
    1.23 +
    1.24 +definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
    1.25 +definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
    1.26 +definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
    1.27 +definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
    1.28 +
    1.29 +lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    1.30 +by (rule monotoneI) (auto simp: fun_ord_def)
    1.31 +
    1.32 +lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    1.33 +\<Longrightarrow> monotone orda ordb G
    1.34 +\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
    1.35 +unfolding monotone_def by simp
    1.36 +
    1.37 +definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
    1.38 +
    1.39 +locale partial_function_definitions = 
    1.40 +  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.41 +  fixes lub :: "'a set \<Rightarrow> 'a"
    1.42 +  assumes leq_refl: "leq x x"
    1.43 +  assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
    1.44 +  assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
    1.45 +  assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
    1.46 +  assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
    1.47 +
    1.48 +lemma partial_function_lift:
    1.49 +  assumes "partial_function_definitions ord lb"
    1.50 +  shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
    1.51 +proof -
    1.52 +  interpret partial_function_definitions ord lb by fact
    1.53 +
    1.54 +  { fix A a assume A: "chain ?ordf A"
    1.55 +    have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    1.56 +    proof (rule chainI)
    1.57 +      fix x y assume "x \<in> ?C" "y \<in> ?C"
    1.58 +      then obtain f g where fg: "f \<in> A" "g \<in> A" 
    1.59 +        and [simp]: "x = f a" "y = g a" by blast
    1.60 +      from chainD[OF A fg]
    1.61 +      show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    1.62 +    qed }
    1.63 +  note chain_fun = this
    1.64 +
    1.65 +  show ?thesis
    1.66 +  proof
    1.67 +    fix x show "?ordf x x"
    1.68 +      unfolding fun_ord_def by (auto simp: leq_refl)
    1.69 +  next
    1.70 +    fix x y z assume "?ordf x y" "?ordf y z"
    1.71 +    thus "?ordf x z" unfolding fun_ord_def 
    1.72 +      by (force dest: leq_trans)
    1.73 +  next
    1.74 +    fix x y assume "?ordf x y" "?ordf y x"
    1.75 +    thus "x = y" unfolding fun_ord_def
    1.76 +      by (force intro!: ext dest: leq_antisym)
    1.77 +  next
    1.78 +    fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
    1.79 +    thus "?ordf f (?lubf A)"
    1.80 +      unfolding fun_lub_def fun_ord_def
    1.81 +      by (blast intro: lub_upper chain_fun[OF A] f)
    1.82 +  next
    1.83 +    fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
    1.84 +    assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
    1.85 +    show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
    1.86 +      by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
    1.87 +   qed
    1.88 +qed
    1.89 +
    1.90 +lemma ccpo: assumes "partial_function_definitions ord lb"
    1.91 +  shows "class.ccpo ord (mk_less ord) lb"
    1.92 +using assms unfolding partial_function_definitions_def mk_less_def
    1.93 +by unfold_locales blast+
    1.94 +
    1.95 +lemma partial_function_image:
    1.96 +  assumes "partial_function_definitions ord Lub"
    1.97 +  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
    1.98 +  assumes inv: "\<And>x. f (g x) = x"
    1.99 +  shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
   1.100 +proof -
   1.101 +  let ?iord = "img_ord f ord"
   1.102 +  let ?ilub = "img_lub f g Lub"
   1.103 +
   1.104 +  interpret partial_function_definitions ord Lub by fact
   1.105 +  show ?thesis
   1.106 +  proof
   1.107 +    fix A x assume "chain ?iord A" "x \<in> A"
   1.108 +    then have "chain ord (f ` A)" "f x \<in> f ` A"
   1.109 +      by (auto simp: img_ord_def intro: chainI dest: chainD)
   1.110 +    thus "?iord x (?ilub A)"
   1.111 +      unfolding inv img_lub_def img_ord_def by (rule lub_upper)
   1.112 +  next
   1.113 +    fix A x assume "chain ?iord A"
   1.114 +      and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
   1.115 +    then have "chain ord (f ` A)"
   1.116 +      by (auto simp: img_ord_def intro: chainI dest: chainD)
   1.117 +    thus "?iord (?ilub A) x"
   1.118 +      unfolding inv img_lub_def img_ord_def
   1.119 +      by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
   1.120 +  qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
   1.121 +qed
   1.122 +
   1.123 +context partial_function_definitions
   1.124 +begin
   1.125 +
   1.126 +abbreviation "le_fun \<equiv> fun_ord leq"
   1.127 +abbreviation "lub_fun \<equiv> fun_lub lub"
   1.128 +abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
   1.129 +abbreviation "mono_body \<equiv> monotone le_fun leq"
   1.130 +
   1.131 +text {* Interpret manually, to avoid flooding everything with facts about
   1.132 +  orders *}
   1.133 +
   1.134 +lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun"
   1.135 +apply (rule ccpo)
   1.136 +apply (rule partial_function_lift)
   1.137 +apply (rule partial_function_definitions_axioms)
   1.138 +done
   1.139 +
   1.140 +text {* The crucial fixed-point theorem *}
   1.141 +
   1.142 +lemma mono_body_fixp: 
   1.143 +  "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
   1.144 +by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
   1.145 +
   1.146 +text {* Version with curry/uncurry combinators, to be used by package *}
   1.147 +
   1.148 +lemma fixp_rule_uc:
   1.149 +  fixes F :: "'c \<Rightarrow> 'c" and
   1.150 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
   1.151 +    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
   1.152 +  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
   1.153 +  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   1.154 +  assumes inverse: "\<And>f. C (U f) = f"
   1.155 +  shows "f = F f"
   1.156 +proof -
   1.157 +  have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
   1.158 +  also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
   1.159 +    by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
   1.160 +  also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
   1.161 +  also have "... = F f" by (simp add: eq)
   1.162 +  finally show "f = F f" .
   1.163 +qed
   1.164 +
   1.165 +text {* Rules for @{term mono_body}: *}
   1.166 +
   1.167 +lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
   1.168 +by (rule monotoneI) (rule leq_refl)
   1.169 +
   1.170 +declaration {* Partial_Function.init @{term fixp_fun}
   1.171 +  @{term mono_body} @{thm fixp_rule_uc} *}
   1.172 +
   1.173 +end
   1.174 +
   1.175 +
   1.176 +subsection {* Flat interpretation: tailrec and option *}
   1.177 +
   1.178 +definition 
   1.179 +  "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
   1.180 +
   1.181 +definition 
   1.182 +  "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
   1.183 +
   1.184 +lemma flat_interpretation:
   1.185 +  "partial_function_definitions (flat_ord b) (flat_lub b)"
   1.186 +proof
   1.187 +  fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
   1.188 +  show "flat_ord b x (flat_lub b A)"
   1.189 +  proof cases
   1.190 +    assume "x = b"
   1.191 +    thus ?thesis by (simp add: flat_ord_def)
   1.192 +  next
   1.193 +    assume "x \<noteq> b"
   1.194 +    with 1 have "A - {b} = {x}"
   1.195 +      by (auto elim: chainE simp: flat_ord_def)
   1.196 +    then have "flat_lub b A = x"
   1.197 +      by (auto simp: flat_lub_def)
   1.198 +    thus ?thesis by (auto simp: flat_ord_def)
   1.199 +  qed
   1.200 +next
   1.201 +  fix A z assume A: "chain (flat_ord b) A"
   1.202 +    and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
   1.203 +  show "flat_ord b (flat_lub b A) z"
   1.204 +  proof cases
   1.205 +    assume "A \<subseteq> {b}"
   1.206 +    thus ?thesis
   1.207 +      by (auto simp: flat_lub_def flat_ord_def)
   1.208 +  next
   1.209 +    assume nb: "\<not> A \<subseteq> {b}"
   1.210 +    then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
   1.211 +    with A have "A - {b} = {y}"
   1.212 +      by (auto elim: chainE simp: flat_ord_def)
   1.213 +    with nb have "flat_lub b A = y"
   1.214 +      by (auto simp: flat_lub_def)
   1.215 +    with z y show ?thesis by auto    
   1.216 +  qed
   1.217 +qed (auto simp: flat_ord_def)
   1.218 +
   1.219 +interpretation tailrec!:
   1.220 +  partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   1.221 +by (rule flat_interpretation)
   1.222 +
   1.223 +interpretation option!:
   1.224 +  partial_function_definitions "flat_ord None" "flat_lub None"
   1.225 +by (rule flat_interpretation)
   1.226 +
   1.227 +abbreviation "option_ord \<equiv> flat_ord None"
   1.228 +abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
   1.229 +
   1.230 +lemma bind_mono[partial_function_mono]:
   1.231 +assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
   1.232 +shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
   1.233 +proof (rule monotoneI)
   1.234 +  fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
   1.235 +  with mf
   1.236 +  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
   1.237 +  then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
   1.238 +    unfolding flat_ord_def by auto    
   1.239 +  also from mg
   1.240 +  have "\<And>y'. option_ord (C y' f) (C y' g)"
   1.241 +    by (rule monotoneD) (rule fg)
   1.242 +  then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
   1.243 +    unfolding flat_ord_def by (cases "B g") auto
   1.244 +  finally (option.leq_trans)
   1.245 +  show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
   1.246 +qed
   1.247 +
   1.248 +
   1.249 +end
   1.250 +