src/HOL/Partial_Function.thy
 author krauss Tue May 31 11:11:17 2011 +0200 (2011-05-31) changeset 43081 1a39c9898ae6 parent 43080 73a1d6a7ef1d child 43082 8d0c44de9773 permissions -rw-r--r--
admissibility on option type
1 (* Title:    HOL/Partial_Function.thy
2    Author:   Alexander Krauss, TU Muenchen
3 *)
5 header {* Partial Function Definitions *}
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
14 setup Partial_Function.setup
16 subsection {* Axiomatic setup *}
18 text {* This techical locale constains the requirements for function
19   definitions with ccpo fixed points. *}
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)))"
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
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)
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)
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
50 definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
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"
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
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
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+
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"
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
125 context partial_function_definitions
126 begin
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 abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
134 text {* Interpret manually, to avoid flooding everything with facts about
135   orders *}
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
143 text {* The crucial fixed-point theorem *}
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)
149 text {* Version with curry/uncurry combinators, to be used by package *}
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
168 text {* Rules for @{term mono_body}: *}
170 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
171 by (rule monotoneI) (rule leq_refl)
173 end
176 subsection {* Flat interpretation: tailrec and option *}
178 definition
179   "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
181 definition
182   "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
184 lemma flat_interpretation:
185   "partial_function_definitions (flat_ord b) (flat_lub b)"
186 proof
187   fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
188   show "flat_ord b x (flat_lub b A)"
189   proof cases
190     assume "x = b"
191     thus ?thesis by (simp add: flat_ord_def)
192   next
193     assume "x \<noteq> b"
194     with 1 have "A - {b} = {x}"
195       by (auto elim: chainE simp: flat_ord_def)
196     then have "flat_lub b A = x"
197       by (auto simp: flat_lub_def)
198     thus ?thesis by (auto simp: flat_ord_def)
199   qed
200 next
201   fix A z assume A: "chain (flat_ord b) A"
202     and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
203   show "flat_ord b (flat_lub b A) z"
204   proof cases
205     assume "A \<subseteq> {b}"
206     thus ?thesis
207       by (auto simp: flat_lub_def flat_ord_def)
208   next
209     assume nb: "\<not> A \<subseteq> {b}"
210     then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
211     with A have "A - {b} = {y}"
212       by (auto elim: chainE simp: flat_ord_def)
213     with nb have "flat_lub b A = y"
214       by (auto simp: flat_lub_def)
215     with z y show ?thesis by auto
216   qed
217 qed (auto simp: flat_ord_def)
219 interpretation tailrec!:
220   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
221 by (rule flat_interpretation)
223 interpretation option!:
224   partial_function_definitions "flat_ord None" "flat_lub None"
225 by (rule flat_interpretation)
227 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
228   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
230 declaration {* Partial_Function.init "option" @{term option.fixp_fun}
231   @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *}
234 abbreviation "option_ord \<equiv> flat_ord None"
235 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
237 lemma bind_mono[partial_function_mono]:
238 assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
239 shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
240 proof (rule monotoneI)
241   fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
242   with mf
243   have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
244   then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
245     unfolding flat_ord_def by auto
246   also from mg
247   have "\<And>y'. option_ord (C y' f) (C y' g)"
248     by (rule monotoneD) (rule fg)
249   then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
250     unfolding flat_ord_def by (cases "B g") auto
251   finally (option.leq_trans)
252   show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
253 qed
255 lemma flat_lub_in_chain:
256   assumes ch: "chain (flat_ord b) A "
257   assumes lub: "flat_lub b A = a"
258   shows "a = b \<or> a \<in> A"
259 proof (cases "A \<subseteq> {b}")
260   case True
261   then have "flat_lub b A = b" unfolding flat_lub_def by simp
262   with lub show ?thesis by simp
263 next
264   case False
265   then obtain c where "c \<in> A" and "c \<noteq> b" by auto
266   { fix z assume "z \<in> A"
267     from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
268       unfolding flat_ord_def using `c \<noteq> b` by auto }
269   with False have "A - {b} = {c}" by auto
270   with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
271   with `c \<in> A` lub show ?thesis by simp
272 qed
274 lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
275   (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
276 proof (rule ccpo.admissibleI[OF option.ccpo])
277   fix A :: "('a \<Rightarrow> 'b option) set"
278   assume ch: "chain option.le_fun A"
279     and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
280   from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
281   show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
282   proof (intro allI impI)
283     fix x y assume "option.lub_fun A x = Some y"
284     from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
285     have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
286     then have "\<exists>f\<in>A. f x = Some y" by auto
287     with IH show "P x y" by auto
288   qed
289 qed
292 hide_const (open) chain
294 end