author | wenzelm |
Mon, 12 Apr 2021 14:14:47 +0200 | |
changeset 73563 | 55b66a45bc94 |
parent 73411 | 1f1366966296 |
child 75669 | 43f5dfb7fa35 |
permissions | -rw-r--r-- |
40107 | 1 |
(* Title: HOL/Partial_Function.thy |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
*) |
|
4 |
||
60758 | 5 |
section \<open>Partial Function Definitions\<close> |
40107 | 6 |
|
7 |
theory Partial_Function |
|
66364 | 8 |
imports Complete_Partial_Order Option |
69913 | 9 |
keywords "partial_function" :: thy_defn |
40107 | 10 |
begin |
11 |
||
57959 | 12 |
named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
69605 | 13 |
ML_file \<open>Tools/Function/partial_function.ML\<close> |
57959 | 14 |
|
60062 | 15 |
lemma (in ccpo) in_chain_finite: |
67399 | 16 |
assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}" |
60062 | 17 |
shows "\<Squnion>A \<in> A" |
18 |
using assms(2,1,3) |
|
19 |
proof induction |
|
20 |
case empty thus ?case by simp |
|
21 |
next |
|
22 |
case (insert x A) |
|
67399 | 23 |
note chain = \<open>Complete_Partial_Order.chain (\<le>) (insert x A)\<close> |
60062 | 24 |
show ?case |
25 |
proof(cases "A = {}") |
|
26 |
case True thus ?thesis by simp |
|
27 |
next |
|
28 |
case False |
|
67399 | 29 |
from chain have chain': "Complete_Partial_Order.chain (\<le>) A" |
60062 | 30 |
by(rule chain_subset) blast |
31 |
hence "\<Squnion>A \<in> A" using False by(rule insert.IH) |
|
32 |
show ?thesis |
|
33 |
proof(cases "x \<le> \<Squnion>A") |
|
34 |
case True |
|
69745 | 35 |
have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain |
60062 | 36 |
by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain']) |
69745 | 37 |
hence "\<Squnion>(insert x A) = \<Squnion>A" |
73411 | 38 |
by(rule order.antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain']) |
60758 | 39 |
with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp |
60062 | 40 |
next |
41 |
case False |
|
60758 | 42 |
with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close> |
69745 | 43 |
have "\<Squnion>(insert x A) = x" |
73411 | 44 |
by(auto intro: order.antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain]) |
60062 | 45 |
thus ?thesis by simp |
46 |
qed |
|
47 |
qed |
|
48 |
qed |
|
40107 | 49 |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62390
diff
changeset
|
50 |
lemma (in ccpo) admissible_chfin: |
67399 | 51 |
"(\<forall>S. Complete_Partial_Order.chain (\<le>) S \<longrightarrow> finite S) |
52 |
\<Longrightarrow> ccpo.admissible Sup (\<le>) P" |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62390
diff
changeset
|
53 |
using in_chain_finite by (blast intro: ccpo.admissibleI) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62390
diff
changeset
|
54 |
|
60758 | 55 |
subsection \<open>Axiomatic setup\<close> |
40107 | 56 |
|
60758 | 57 |
text \<open>This techical locale constains the requirements for function |
58 |
definitions with ccpo fixed points.\<close> |
|
40107 | 59 |
|
60 |
definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))" |
|
61 |
definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})" |
|
62 |
definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))" |
|
63 |
definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))" |
|
64 |
||
43081 | 65 |
lemma chain_fun: |
66 |
assumes A: "chain (fun_ord ord) A" |
|
67 |
shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C") |
|
68 |
proof (rule chainI) |
|
69 |
fix x y assume "x \<in> ?C" "y \<in> ?C" |
|
70 |
then obtain f g where fg: "f \<in> A" "g \<in> A" |
|
71 |
and [simp]: "x = f a" "y = g a" by blast |
|
72 |
from chainD[OF A fg] |
|
73 |
show "ord x y \<or> ord y x" unfolding fun_ord_def by auto |
|
74 |
qed |
|
75 |
||
40107 | 76 |
lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" |
77 |
by (rule monotoneI) (auto simp: fun_ord_def) |
|
78 |
||
40288 | 79 |
lemma let_mono[partial_function_mono]: |
80 |
"(\<And>x. monotone orda ordb (\<lambda>f. b f x)) |
|
81 |
\<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))" |
|
82 |
by (simp add: Let_def) |
|
83 |
||
40107 | 84 |
lemma if_mono[partial_function_mono]: "monotone orda ordb F |
85 |
\<Longrightarrow> monotone orda ordb G |
|
86 |
\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)" |
|
87 |
unfolding monotone_def by simp |
|
88 |
||
89 |
definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)" |
|
90 |
||
91 |
locale partial_function_definitions = |
|
92 |
fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
93 |
fixes lub :: "'a set \<Rightarrow> 'a" |
|
94 |
assumes leq_refl: "leq x x" |
|
95 |
assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z" |
|
96 |
assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y" |
|
97 |
assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)" |
|
98 |
assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z" |
|
99 |
||
100 |
lemma partial_function_lift: |
|
101 |
assumes "partial_function_definitions ord lb" |
|
102 |
shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf") |
|
103 |
proof - |
|
104 |
interpret partial_function_definitions ord lb by fact |
|
105 |
||
106 |
show ?thesis |
|
107 |
proof |
|
108 |
fix x show "?ordf x x" |
|
109 |
unfolding fun_ord_def by (auto simp: leq_refl) |
|
110 |
next |
|
111 |
fix x y z assume "?ordf x y" "?ordf y z" |
|
112 |
thus "?ordf x z" unfolding fun_ord_def |
|
113 |
by (force dest: leq_trans) |
|
114 |
next |
|
115 |
fix x y assume "?ordf x y" "?ordf y x" |
|
116 |
thus "x = y" unfolding fun_ord_def |
|
43081 | 117 |
by (force intro!: dest: leq_antisym) |
40107 | 118 |
next |
119 |
fix A f assume f: "f \<in> A" and A: "chain ?ordf A" |
|
120 |
thus "?ordf f (?lubf A)" |
|
121 |
unfolding fun_lub_def fun_ord_def |
|
122 |
by (blast intro: lub_upper chain_fun[OF A] f) |
|
123 |
next |
|
124 |
fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a" |
|
125 |
assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g" |
|
126 |
show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def |
|
127 |
by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def]) |
|
128 |
qed |
|
129 |
qed |
|
130 |
||
131 |
lemma ccpo: assumes "partial_function_definitions ord lb" |
|
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
132 |
shows "class.ccpo lb ord (mk_less ord)" |
40107 | 133 |
using assms unfolding partial_function_definitions_def mk_less_def |
134 |
by unfold_locales blast+ |
|
135 |
||
136 |
lemma partial_function_image: |
|
137 |
assumes "partial_function_definitions ord Lub" |
|
138 |
assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" |
|
139 |
assumes inv: "\<And>x. f (g x) = x" |
|
140 |
shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)" |
|
141 |
proof - |
|
142 |
let ?iord = "img_ord f ord" |
|
143 |
let ?ilub = "img_lub f g Lub" |
|
144 |
||
145 |
interpret partial_function_definitions ord Lub by fact |
|
146 |
show ?thesis |
|
147 |
proof |
|
148 |
fix A x assume "chain ?iord A" "x \<in> A" |
|
149 |
then have "chain ord (f ` A)" "f x \<in> f ` A" |
|
150 |
by (auto simp: img_ord_def intro: chainI dest: chainD) |
|
151 |
thus "?iord x (?ilub A)" |
|
152 |
unfolding inv img_lub_def img_ord_def by (rule lub_upper) |
|
153 |
next |
|
154 |
fix A x assume "chain ?iord A" |
|
155 |
and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x" |
|
156 |
then have "chain ord (f ` A)" |
|
157 |
by (auto simp: img_ord_def intro: chainI dest: chainD) |
|
158 |
thus "?iord (?ilub A) x" |
|
159 |
unfolding inv img_lub_def img_ord_def |
|
160 |
by (rule lub_least) (auto dest: 1[unfolded img_ord_def]) |
|
161 |
qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj) |
|
162 |
qed |
|
163 |
||
164 |
context partial_function_definitions |
|
165 |
begin |
|
166 |
||
167 |
abbreviation "le_fun \<equiv> fun_ord leq" |
|
168 |
abbreviation "lub_fun \<equiv> fun_lub lub" |
|
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
169 |
abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun" |
40107 | 170 |
abbreviation "mono_body \<equiv> monotone le_fun leq" |
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
171 |
abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun" |
40107 | 172 |
|
60758 | 173 |
text \<open>Interpret manually, to avoid flooding everything with facts about |
174 |
orders\<close> |
|
40107 | 175 |
|
46041
1e3ff542e83e
remove constant 'ccpo.lub', re-use constant 'Sup' instead
huffman
parents:
45297
diff
changeset
|
176 |
lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)" |
40107 | 177 |
apply (rule ccpo) |
178 |
apply (rule partial_function_lift) |
|
179 |
apply (rule partial_function_definitions_axioms) |
|
180 |
done |
|
181 |
||
60758 | 182 |
text \<open>The crucial fixed-point theorem\<close> |
40107 | 183 |
|
184 |
lemma mono_body_fixp: |
|
185 |
"(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)" |
|
186 |
by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def) |
|
187 |
||
60758 | 188 |
text \<open>Version with curry/uncurry combinators, to be used by package\<close> |
40107 | 189 |
|
190 |
lemma fixp_rule_uc: |
|
191 |
fixes F :: "'c \<Rightarrow> 'c" and |
|
192 |
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and |
|
193 |
C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" |
|
194 |
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" |
|
195 |
assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" |
|
196 |
assumes inverse: "\<And>f. C (U f) = f" |
|
197 |
shows "f = F f" |
|
198 |
proof - |
|
199 |
have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq) |
|
200 |
also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))" |
|
201 |
by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl) |
|
202 |
also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse) |
|
203 |
also have "... = F f" by (simp add: eq) |
|
204 |
finally show "f = F f" . |
|
205 |
qed |
|
206 |
||
60758 | 207 |
text \<open>Fixpoint induction rule\<close> |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
208 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
209 |
lemma fixp_induct_uc: |
59647
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
210 |
fixes F :: "'c \<Rightarrow> 'c" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
211 |
and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
212 |
and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
213 |
and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
214 |
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" |
59647
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
215 |
and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
216 |
and inverse: "\<And>f. U (C f) = f" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
217 |
and adm: "ccpo.admissible lub_fun le_fun P" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
218 |
and bot: "P (\<lambda>_. lub {})" |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
219 |
and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))" |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
220 |
shows "P (U f)" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
221 |
unfolding eq inverse |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
222 |
apply (rule ccpo.fixp_induct[OF ccpo adm]) |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
223 |
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2] |
59647
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
224 |
apply (rule_tac f5="C x" in step) |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
225 |
apply (simp add: inverse) |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
59517
diff
changeset
|
226 |
done |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
227 |
|
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
228 |
|
69593 | 229 |
text \<open>Rules for \<^term>\<open>mono_body\<close>:\<close> |
40107 | 230 |
|
231 |
lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)" |
|
232 |
by (rule monotoneI) (rule leq_refl) |
|
233 |
||
234 |
end |
|
235 |
||
236 |
||
60758 | 237 |
subsection \<open>Flat interpretation: tailrec and option\<close> |
40107 | 238 |
|
239 |
definition |
|
240 |
"flat_ord b x y \<longleftrightarrow> x = b \<or> x = y" |
|
241 |
||
242 |
definition |
|
243 |
"flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))" |
|
244 |
||
245 |
lemma flat_interpretation: |
|
246 |
"partial_function_definitions (flat_ord b) (flat_lub b)" |
|
247 |
proof |
|
248 |
fix A x assume 1: "chain (flat_ord b) A" "x \<in> A" |
|
249 |
show "flat_ord b x (flat_lub b A)" |
|
250 |
proof cases |
|
251 |
assume "x = b" |
|
252 |
thus ?thesis by (simp add: flat_ord_def) |
|
253 |
next |
|
254 |
assume "x \<noteq> b" |
|
255 |
with 1 have "A - {b} = {x}" |
|
256 |
by (auto elim: chainE simp: flat_ord_def) |
|
257 |
then have "flat_lub b A = x" |
|
258 |
by (auto simp: flat_lub_def) |
|
259 |
thus ?thesis by (auto simp: flat_ord_def) |
|
260 |
qed |
|
261 |
next |
|
262 |
fix A z assume A: "chain (flat_ord b) A" |
|
263 |
and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z" |
|
264 |
show "flat_ord b (flat_lub b A) z" |
|
265 |
proof cases |
|
266 |
assume "A \<subseteq> {b}" |
|
267 |
thus ?thesis |
|
268 |
by (auto simp: flat_lub_def flat_ord_def) |
|
269 |
next |
|
270 |
assume nb: "\<not> A \<subseteq> {b}" |
|
271 |
then obtain y where y: "y \<in> A" "y \<noteq> b" by auto |
|
272 |
with A have "A - {b} = {y}" |
|
273 |
by (auto elim: chainE simp: flat_ord_def) |
|
274 |
with nb have "flat_lub b A = y" |
|
275 |
by (auto simp: flat_lub_def) |
|
276 |
with z y show ?thesis by auto |
|
277 |
qed |
|
278 |
qed (auto simp: flat_ord_def) |
|
279 |
||
59517 | 280 |
lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y" |
281 |
by(auto simp add: flat_ord_def) |
|
282 |
||
283 |
lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y" |
|
284 |
by(auto simp add: flat_ord_def) |
|
285 |
||
64634 | 286 |
lemma antisymp_flat_ord: "antisymp (flat_ord a)" |
287 |
by(rule antisympI)(auto dest: flat_ord_antisym) |
|
59517 | 288 |
|
61605 | 289 |
interpretation tailrec: |
40107 | 290 |
partial_function_definitions "flat_ord undefined" "flat_lub undefined" |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
60758
diff
changeset
|
291 |
rewrites "flat_lub undefined {} \<equiv> undefined" |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
292 |
by (rule flat_interpretation)(simp add: flat_lub_def) |
40107 | 293 |
|
61605 | 294 |
interpretation option: |
40107 | 295 |
partial_function_definitions "flat_ord None" "flat_lub None" |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
60758
diff
changeset
|
296 |
rewrites "flat_lub None {} \<equiv> None" |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
297 |
by (rule flat_interpretation)(simp add: flat_lub_def) |
40107 | 298 |
|
42949
618adb3584e5
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
krauss
parents:
40288
diff
changeset
|
299 |
|
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
300 |
abbreviation "tailrec_ord \<equiv> flat_ord undefined" |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
301 |
abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord" |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
302 |
|
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
303 |
lemma tailrec_admissible: |
53949 | 304 |
"ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) |
305 |
(\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))" |
|
53361
1cb7d3c0cf31
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents:
52728
diff
changeset
|
306 |
proof(intro ccpo.admissibleI strip) |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
307 |
fix A x |
53949 | 308 |
assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A" |
309 |
and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)" |
|
310 |
and defined: "fun_lub (flat_lub c) A x \<noteq> c" |
|
311 |
from defined obtain f where f: "f \<in> A" "f x \<noteq> c" |
|
62390 | 312 |
by(auto simp add: fun_lub_def flat_lub_def split: if_split_asm) |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
313 |
hence "P x (f x)" by(rule P) |
53949 | 314 |
moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x" |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
315 |
by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def) |
53949 | 316 |
hence "fun_lub (flat_lub c) A x = f x" |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
317 |
using f by(auto simp add: fun_lub_def flat_lub_def) |
53949 | 318 |
ultimately show "P x (fun_lub (flat_lub c) A x)" by simp |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
319 |
qed |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
320 |
|
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
321 |
lemma fixp_induct_tailrec: |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
322 |
fixes F :: "'c \<Rightarrow> 'c" and |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
323 |
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
324 |
C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
325 |
P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
326 |
x :: "'b" |
53949 | 327 |
assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)" |
328 |
assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))" |
|
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
329 |
assumes inverse2: "\<And>f. U (C f) = f" |
53949 | 330 |
assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y" |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
331 |
assumes result: "U f x = y" |
53949 | 332 |
assumes defined: "y \<noteq> c" |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
333 |
shows "P x y" |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
334 |
proof - |
53949 | 335 |
have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y" |
336 |
by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2]) |
|
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
337 |
(auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def) |
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
338 |
thus ?thesis using result defined by blast |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
339 |
qed |
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
340 |
|
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
341 |
lemma admissible_image: |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
342 |
assumes pfun: "partial_function_definitions le lub" |
67091 | 343 |
assumes adm: "ccpo.admissible lub le (P \<circ> g)" |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
344 |
assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
345 |
assumes inv: "\<And>x. f (g x) = x" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
346 |
shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P" |
53361
1cb7d3c0cf31
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents:
52728
diff
changeset
|
347 |
proof (rule ccpo.admissibleI) |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
348 |
fix A assume "chain (img_ord f le) A" |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
349 |
then have ch': "chain le (f ` A)" |
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
350 |
by (auto simp: img_ord_def intro: chainI dest: chainD) |
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
351 |
assume "A \<noteq> {}" |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
352 |
assume P_A: "\<forall>x\<in>A. P x" |
67091 | 353 |
have "(P \<circ> g) (lub (f ` A))" using adm ch' |
53361
1cb7d3c0cf31
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents:
52728
diff
changeset
|
354 |
proof (rule ccpo.admissibleD) |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
355 |
fix x assume "x \<in> f ` A" |
67091 | 356 |
with P_A show "(P \<circ> g) x" by (auto simp: inj[OF inv]) |
60758 | 357 |
qed(simp add: \<open>A \<noteq> {}\<close>) |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
358 |
thus "P (img_lub f g lub A)" unfolding img_lub_def by simp |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
359 |
qed |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
360 |
|
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
361 |
lemma admissible_fun: |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
362 |
assumes pfun: "partial_function_definitions le lub" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
363 |
assumes adm: "\<And>x. ccpo.admissible lub le (Q x)" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
364 |
shows "ccpo.admissible (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))" |
53361
1cb7d3c0cf31
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents:
52728
diff
changeset
|
365 |
proof (rule ccpo.admissibleI) |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
366 |
fix A :: "('b \<Rightarrow> 'a) set" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
367 |
assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
368 |
assume ch: "chain (fun_ord le) A" |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
369 |
assume "A \<noteq> {}" |
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
370 |
hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
371 |
show "\<forall>x. Q x (fun_lub lub A x)" |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
372 |
unfolding fun_lub_def |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
373 |
by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty]) |
51485
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
374 |
(auto simp: Q) |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
375 |
qed |
637aa1649ac7
added rudimentary induction rule for partial_function (heap)
krauss
parents:
51459
diff
changeset
|
376 |
|
51459
bc3651180a09
add induction rule for partial_function (tailrec)
Andreas Lochbihler
parents:
48891
diff
changeset
|
377 |
|
40107 | 378 |
abbreviation "option_ord \<equiv> flat_ord None" |
379 |
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
|
380 |
||
381 |
lemma bind_mono[partial_function_mono]: |
|
382 |
assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)" |
|
383 |
shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))" |
|
384 |
proof (rule monotoneI) |
|
385 |
fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g" |
|
386 |
with mf |
|
387 |
have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) |
|
388 |
then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))" |
|
389 |
unfolding flat_ord_def by auto |
|
390 |
also from mg |
|
391 |
have "\<And>y'. option_ord (C y' f) (C y' g)" |
|
392 |
by (rule monotoneD) (rule fg) |
|
393 |
then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))" |
|
394 |
unfolding flat_ord_def by (cases "B g") auto |
|
395 |
finally (option.leq_trans) |
|
396 |
show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" . |
|
397 |
qed |
|
398 |
||
43081 | 399 |
lemma flat_lub_in_chain: |
400 |
assumes ch: "chain (flat_ord b) A " |
|
401 |
assumes lub: "flat_lub b A = a" |
|
402 |
shows "a = b \<or> a \<in> A" |
|
403 |
proof (cases "A \<subseteq> {b}") |
|
404 |
case True |
|
405 |
then have "flat_lub b A = b" unfolding flat_lub_def by simp |
|
406 |
with lub show ?thesis by simp |
|
407 |
next |
|
408 |
case False |
|
409 |
then obtain c where "c \<in> A" and "c \<noteq> b" by auto |
|
410 |
{ fix z assume "z \<in> A" |
|
60758 | 411 |
from chainD[OF ch \<open>c \<in> A\<close> this] have "z = c \<or> z = b" |
412 |
unfolding flat_ord_def using \<open>c \<noteq> b\<close> by auto } |
|
43081 | 413 |
with False have "A - {b} = {c}" by auto |
414 |
with False have "flat_lub b A = c" by (auto simp: flat_lub_def) |
|
60758 | 415 |
with \<open>c \<in> A\<close> lub show ?thesis by simp |
43081 | 416 |
qed |
417 |
||
418 |
lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option). |
|
419 |
(\<forall>x y. f x = Some y \<longrightarrow> P x y))" |
|
53361
1cb7d3c0cf31
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Andreas Lochbihler
parents:
52728
diff
changeset
|
420 |
proof (rule ccpo.admissibleI) |
43081 | 421 |
fix A :: "('a \<Rightarrow> 'b option) set" |
422 |
assume ch: "chain option.le_fun A" |
|
423 |
and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y" |
|
424 |
from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun) |
|
425 |
show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y" |
|
426 |
proof (intro allI impI) |
|
427 |
fix x y assume "option.lub_fun A x = Some y" |
|
428 |
from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]] |
|
429 |
have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp |
|
430 |
then have "\<exists>f\<in>A. f x = Some y" by auto |
|
431 |
with IH show "P x y" by auto |
|
432 |
qed |
|
433 |
qed |
|
434 |
||
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
435 |
lemma fixp_induct_option: |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
436 |
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
|
437 |
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
|
438 |
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
|
439 |
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
|
440 |
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
|
441 |
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
|
442 |
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
|
443 |
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
|
444 |
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
|
445 |
shows "P x y" |
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
446 |
using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] |
54630
9061af4d5ebc
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Andreas Lochbihler
parents:
53949
diff
changeset
|
447 |
unfolding fun_lub_def flat_lub_def by(auto 9 2) |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
448 |
|
69593 | 449 |
declaration \<open>Partial_Function.init "tailrec" \<^term>\<open>tailrec.fixp_fun\<close> |
450 |
\<^term>\<open>tailrec.mono_body\<close> @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc} |
|
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61605
diff
changeset
|
451 |
(SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close> |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
452 |
|
69593 | 453 |
declaration \<open>Partial_Function.init "option" \<^term>\<open>option.fixp_fun\<close> |
454 |
\<^term>\<open>option.mono_body\<close> @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc} |
|
60758 | 455 |
(SOME @{thm fixp_induct_option})\<close> |
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset
|
456 |
|
40252
029400b6c893
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
krauss
parents:
40107
diff
changeset
|
457 |
hide_const (open) chain |
40107 | 458 |
|
459 |
end |