author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 48891 | c0eafbd55de3 |
child 51459 | bc3651180a09 |
permissions | -rw-r--r-- |
40107 | 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 |
|
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46041
diff
changeset
|
9 |
keywords "partial_function" :: thy_decl |
40107 | 10 |
begin |
11 |
||
48891 | 12 |
ML_file "Tools/Function/function_lib.ML" |
13 |
ML_file "Tools/Function/partial_function.ML" |
|
40107 | 14 |
setup Partial_Function.setup |
15 |
||
16 |
subsection {* Axiomatic setup *} |
|
17 |
||
18 |
text {* This techical locale constains the requirements for function |
|
42949
618adb3584e5
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
krauss
parents:
40288
diff
changeset
|
19 |
definitions with ccpo fixed points. *} |
40107 | 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 |
||
43081 | 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 |
|
36 |
||
40107 | 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) |
|
39 |
||
40288 | 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) |
|
44 |
||
40107 | 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 |
|
49 |
||
50 |
definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)" |
|
51 |
||
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" |
|
60 |
||
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 |
|
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 |
|
43081 | 78 |
by (force intro!: dest: leq_antisym) |
40107 | 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" |
|
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
93 |
shows "class.ccpo lb ord (mk_less ord)" |
40107 | 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" |
|
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
130 |
abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun" |
40107 | 131 |
abbreviation "mono_body \<equiv> monotone le_fun leq" |
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
132 |
abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun" |
40107 | 133 |
|
134 |
text {* Interpret manually, to avoid flooding everything with facts about |
|
135 |
orders *} |
|
136 |
||
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
137 |
lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)" |
40107 | 138 |
apply (rule ccpo) |
139 |
apply (rule partial_function_lift) |
|
140 |
apply (rule partial_function_definitions_axioms) |
|
141 |
done |
|
142 |
||
143 |
text {* The crucial fixed-point theorem *} |
|
144 |
||
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) |
|
148 |
||
149 |
text {* Version with curry/uncurry combinators, to be used by package *} |
|
150 |
||
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 |
|
167 |
||
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
168 |
text {* Fixpoint induction rule *} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
169 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
170 |
lemma fixp_induct_uc: |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
171 |
fixes F :: "'c \<Rightarrow> 'c" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
172 |
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
173 |
C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
174 |
P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
175 |
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
176 |
assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
177 |
assumes inverse: "\<And>f. U (C f) = f" |
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
178 |
assumes adm: "ccpo.admissible lub_fun le_fun P" |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
179 |
assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
180 |
shows "P (U f)" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
181 |
unfolding eq inverse |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
182 |
apply (rule ccpo.fixp_induct[OF ccpo adm]) |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
183 |
apply (insert mono, auto simp: monotone_def fun_ord_def)[1] |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
184 |
by (rule_tac f="C x" in step, simp add: inverse) |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
185 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
186 |
|
40107 | 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 |
by (rule flat_interpretation) |
|
241 |
||
242 |
interpretation option!: |
|
243 |
partial_function_definitions "flat_ord None" "flat_lub None" |
|
244 |
by (rule flat_interpretation) |
|
245 |
||
42949
618adb3584e5
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
krauss
parents:
40288
diff
changeset
|
246 |
|
40107 | 247 |
abbreviation "option_ord \<equiv> flat_ord None" |
248 |
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
|
249 |
||
250 |
lemma bind_mono[partial_function_mono]: |
|
251 |
assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)" |
|
252 |
shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))" |
|
253 |
proof (rule monotoneI) |
|
254 |
fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g" |
|
255 |
with mf |
|
256 |
have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) |
|
257 |
then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))" |
|
258 |
unfolding flat_ord_def by auto |
|
259 |
also from mg |
|
260 |
have "\<And>y'. option_ord (C y' f) (C y' g)" |
|
261 |
by (rule monotoneD) (rule fg) |
|
262 |
then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))" |
|
263 |
unfolding flat_ord_def by (cases "B g") auto |
|
264 |
finally (option.leq_trans) |
|
265 |
show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" . |
|
266 |
qed |
|
267 |
||
43081 | 268 |
lemma flat_lub_in_chain: |
269 |
assumes ch: "chain (flat_ord b) A " |
|
270 |
assumes lub: "flat_lub b A = a" |
|
271 |
shows "a = b \<or> a \<in> A" |
|
272 |
proof (cases "A \<subseteq> {b}") |
|
273 |
case True |
|
274 |
then have "flat_lub b A = b" unfolding flat_lub_def by simp |
|
275 |
with lub show ?thesis by simp |
|
276 |
next |
|
277 |
case False |
|
278 |
then obtain c where "c \<in> A" and "c \<noteq> b" by auto |
|
279 |
{ fix z assume "z \<in> A" |
|
280 |
from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b" |
|
281 |
unfolding flat_ord_def using `c \<noteq> b` by auto } |
|
282 |
with False have "A - {b} = {c}" by auto |
|
283 |
with False have "flat_lub b A = c" by (auto simp: flat_lub_def) |
|
284 |
with `c \<in> A` lub show ?thesis by simp |
|
285 |
qed |
|
286 |
||
287 |
lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option). |
|
288 |
(\<forall>x y. f x = Some y \<longrightarrow> P x y))" |
|
289 |
proof (rule ccpo.admissibleI[OF option.ccpo]) |
|
290 |
fix A :: "('a \<Rightarrow> 'b option) set" |
|
291 |
assume ch: "chain option.le_fun A" |
|
292 |
and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y" |
|
293 |
from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun) |
|
294 |
show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y" |
|
295 |
proof (intro allI impI) |
|
296 |
fix x y assume "option.lub_fun A x = Some y" |
|
297 |
from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]] |
|
298 |
have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp |
|
299 |
then have "\<exists>f\<in>A. f x = Some y" by auto |
|
300 |
with IH show "P x y" by auto |
|
301 |
qed |
|
302 |
qed |
|
303 |
||
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
304 |
lemma fixp_induct_option: |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
305 |
fixes F :: "'c \<Rightarrow> 'c" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
306 |
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
307 |
C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
308 |
P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
309 |
assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)" |
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
310 |
assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))" |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
311 |
assumes inverse2: "\<And>f. U (C f) = f" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
312 |
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" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
313 |
assumes defined: "U f x = Some y" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
314 |
shows "P x y" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
315 |
using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
316 |
by blast |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
317 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
318 |
declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
319 |
@{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
320 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
321 |
declaration {* Partial_Function.init "option" @{term option.fixp_fun} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
322 |
@{term option.mono_body} @{thm option.fixp_rule_uc} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
323 |
(SOME @{thm fixp_induct_option}) *} |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
324 |
|
43081 | 325 |
|
40252
029400b6c893
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
krauss
parents:
40107
diff
changeset
|
326 |
hide_const (open) chain |
40107 | 327 |
|
328 |
end |