slotosch@2640
|
1 |
(* Title: HOLCF/Fix.thy
|
clasohm@1479
|
2 |
Author: Franz Regensburger
|
huffman@35794
|
3 |
Author: Brian Huffman
|
nipkow@243
|
4 |
*)
|
nipkow@243
|
5 |
|
huffman@15577
|
6 |
header {* Fixed point operator and admissibility *}
|
huffman@15577
|
7 |
|
huffman@15577
|
8 |
theory Fix
|
huffman@35939
|
9 |
imports Cfun
|
huffman@15577
|
10 |
begin
|
nipkow@243
|
11 |
|
wenzelm@36452
|
12 |
default_sort pcpo
|
huffman@16082
|
13 |
|
huffman@18093
|
14 |
subsection {* Iteration *}
|
huffman@16005
|
15 |
|
haftmann@34928
|
16 |
primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
|
haftmann@34928
|
17 |
"iterate 0 = (\<Lambda> F x. x)"
|
haftmann@34928
|
18 |
| "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
|
berghofe@5192
|
19 |
|
huffman@18093
|
20 |
text {* Derive inductive properties of iterate from primitive recursion *}
|
huffman@15576
|
21 |
|
huffman@18074
|
22 |
lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
|
huffman@18074
|
23 |
by simp
|
huffman@18074
|
24 |
|
huffman@18074
|
25 |
lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)"
|
huffman@18074
|
26 |
by simp
|
huffman@18074
|
27 |
|
huffman@18074
|
28 |
declare iterate.simps [simp del]
|
huffman@18074
|
29 |
|
huffman@18074
|
30 |
lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
|
huffman@27270
|
31 |
by (induct n) simp_all
|
huffman@27270
|
32 |
|
huffman@27270
|
33 |
lemma iterate_iterate:
|
huffman@27270
|
34 |
"iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
|
huffman@27270
|
35 |
by (induct m) simp_all
|
huffman@15576
|
36 |
|
krauss@36075
|
37 |
text {* The sequence of function iterations is a chain. *}
|
huffman@15576
|
38 |
|
huffman@18074
|
39 |
lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
|
krauss@36075
|
40 |
by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
|
huffman@15576
|
41 |
|
huffman@18093
|
42 |
|
huffman@18093
|
43 |
subsection {* Least fixed point operator *}
|
huffman@18093
|
44 |
|
wenzelm@25131
|
45 |
definition
|
wenzelm@25131
|
46 |
"fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
|
wenzelm@25131
|
47 |
"fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
|
huffman@18093
|
48 |
|
huffman@18093
|
49 |
text {* Binder syntax for @{term fix} *}
|
huffman@18093
|
50 |
|
huffman@27316
|
51 |
abbreviation
|
huffman@27316
|
52 |
fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "FIX " 10) where
|
huffman@27316
|
53 |
"fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
|
huffman@18093
|
54 |
|
huffman@27316
|
55 |
notation (xsymbols)
|
huffman@27316
|
56 |
fix_syn (binder "\<mu> " 10)
|
huffman@18093
|
57 |
|
huffman@18093
|
58 |
text {* Properties of @{term fix} *}
|
huffman@18074
|
59 |
|
huffman@18090
|
60 |
text {* direct connection between @{term fix} and iteration *}
|
huffman@18074
|
61 |
|
huffman@18074
|
62 |
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
|
huffman@40185
|
63 |
unfolding fix_def by simp
|
huffman@18074
|
64 |
|
huffman@35055
|
65 |
lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
|
huffman@35055
|
66 |
unfolding fix_def2
|
huffman@35055
|
67 |
using chain_iterate by (rule is_ub_thelub)
|
huffman@35055
|
68 |
|
huffman@15637
|
69 |
text {*
|
huffman@15637
|
70 |
Kleene's fixed point theorems for continuous functions in pointed
|
huffman@15637
|
71 |
omega cpo's
|
huffman@15637
|
72 |
*}
|
huffman@15576
|
73 |
|
huffman@18074
|
74 |
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
|
huffman@18074
|
75 |
apply (simp add: fix_def2)
|
huffman@16005
|
76 |
apply (subst lub_range_shift [of _ 1, symmetric])
|
huffman@16005
|
77 |
apply (rule chain_iterate)
|
huffman@15576
|
78 |
apply (subst contlub_cfun_arg)
|
huffman@15576
|
79 |
apply (rule chain_iterate)
|
huffman@16005
|
80 |
apply simp
|
huffman@15576
|
81 |
done
|
huffman@15576
|
82 |
|
huffman@31076
|
83 |
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
|
huffman@18074
|
84 |
apply (simp add: fix_def2)
|
huffman@40735
|
85 |
apply (rule lub_below)
|
huffman@15576
|
86 |
apply (rule chain_iterate)
|
huffman@16214
|
87 |
apply (induct_tac i)
|
huffman@16214
|
88 |
apply simp
|
huffman@16214
|
89 |
apply simp
|
huffman@31076
|
90 |
apply (erule rev_below_trans)
|
huffman@15576
|
91 |
apply (erule monofun_cfun_arg)
|
huffman@15576
|
92 |
done
|
huffman@15576
|
93 |
|
huffman@16214
|
94 |
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
|
huffman@31076
|
95 |
by (rule fix_least_below, simp)
|
huffman@15576
|
96 |
|
huffman@27185
|
97 |
lemma fix_eqI:
|
huffman@27185
|
98 |
assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
|
huffman@27185
|
99 |
shows "fix\<cdot>F = x"
|
huffman@31076
|
100 |
apply (rule below_antisym)
|
huffman@27185
|
101 |
apply (rule fix_least [OF fixed])
|
huffman@27185
|
102 |
apply (rule least [OF fix_eq [symmetric]])
|
huffman@15576
|
103 |
done
|
huffman@15576
|
104 |
|
huffman@16214
|
105 |
lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
|
huffman@15637
|
106 |
by (simp add: fix_eq [symmetric])
|
huffman@15576
|
107 |
|
huffman@16214
|
108 |
lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
|
huffman@15637
|
109 |
by (erule fix_eq2 [THEN cfun_fun_cong])
|
huffman@15576
|
110 |
|
huffman@16214
|
111 |
lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
|
huffman@15576
|
112 |
apply (erule ssubst)
|
huffman@15576
|
113 |
apply (rule fix_eq)
|
huffman@15576
|
114 |
done
|
huffman@15576
|
115 |
|
huffman@16214
|
116 |
lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
|
huffman@16214
|
117 |
by (erule fix_eq4 [THEN cfun_fun_cong])
|
huffman@15576
|
118 |
|
huffman@16556
|
119 |
text {* strictness of @{term fix} *}
|
huffman@16556
|
120 |
|
huffman@40559
|
121 |
lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
|
huffman@16917
|
122 |
apply (rule iffI)
|
huffman@16917
|
123 |
apply (erule subst)
|
huffman@16917
|
124 |
apply (rule fix_eq [symmetric])
|
huffman@16917
|
125 |
apply (erule fix_least [THEN UU_I])
|
huffman@16917
|
126 |
done
|
huffman@16917
|
127 |
|
huffman@16556
|
128 |
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
|
huffman@40559
|
129 |
by (simp add: fix_bottom_iff)
|
huffman@16556
|
130 |
|
huffman@16556
|
131 |
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
|
huffman@40559
|
132 |
by (simp add: fix_bottom_iff)
|
huffman@16556
|
133 |
|
huffman@16556
|
134 |
text {* @{term fix} applied to identity and constant functions *}
|
huffman@16556
|
135 |
|
huffman@16556
|
136 |
lemma fix_id: "(\<mu> x. x) = \<bottom>"
|
huffman@16556
|
137 |
by (simp add: fix_strict)
|
huffman@16556
|
138 |
|
huffman@16556
|
139 |
lemma fix_const: "(\<mu> x. c) = c"
|
huffman@18074
|
140 |
by (subst fix_eq, simp)
|
huffman@16556
|
141 |
|
huffman@18090
|
142 |
subsection {* Fixed point induction *}
|
huffman@18090
|
143 |
|
huffman@18090
|
144 |
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
|
huffman@27185
|
145 |
unfolding fix_def2
|
huffman@25925
|
146 |
apply (erule admD)
|
huffman@18090
|
147 |
apply (rule chain_iterate)
|
huffman@27185
|
148 |
apply (rule nat_induct, simp_all)
|
huffman@18090
|
149 |
done
|
huffman@18090
|
150 |
|
huffman@18090
|
151 |
lemma def_fix_ind:
|
huffman@18090
|
152 |
"\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
|
huffman@18090
|
153 |
by (simp add: fix_ind)
|
huffman@18090
|
154 |
|
huffman@27185
|
155 |
lemma fix_ind2:
|
huffman@27185
|
156 |
assumes adm: "adm P"
|
huffman@27185
|
157 |
assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)"
|
huffman@27185
|
158 |
assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))"
|
huffman@27185
|
159 |
shows "P (fix\<cdot>F)"
|
huffman@27185
|
160 |
unfolding fix_def2
|
huffman@27185
|
161 |
apply (rule admD [OF adm chain_iterate])
|
huffman@27185
|
162 |
apply (rule nat_less_induct)
|
huffman@27185
|
163 |
apply (case_tac n)
|
huffman@27185
|
164 |
apply (simp add: 0)
|
huffman@27185
|
165 |
apply (case_tac nat)
|
huffman@27185
|
166 |
apply (simp add: 1)
|
huffman@27185
|
167 |
apply (frule_tac x=nat in spec)
|
huffman@27185
|
168 |
apply (simp add: step)
|
huffman@27185
|
169 |
done
|
huffman@27185
|
170 |
|
huffman@33581
|
171 |
lemma parallel_fix_ind:
|
huffman@33581
|
172 |
assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
|
huffman@33581
|
173 |
assumes base: "P \<bottom> \<bottom>"
|
huffman@33581
|
174 |
assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
|
huffman@33581
|
175 |
shows "P (fix\<cdot>F) (fix\<cdot>G)"
|
huffman@33581
|
176 |
proof -
|
huffman@33581
|
177 |
from adm have adm': "adm (split P)"
|
huffman@33581
|
178 |
unfolding split_def .
|
huffman@33581
|
179 |
have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
|
huffman@33581
|
180 |
by (induct_tac i, simp add: base, simp add: step)
|
huffman@33581
|
181 |
hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
|
huffman@33581
|
182 |
by simp
|
huffman@33581
|
183 |
hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
|
huffman@33581
|
184 |
by - (rule admD [OF adm'], simp, assumption)
|
huffman@33581
|
185 |
hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
|
huffman@41019
|
186 |
by (simp add: lub_Pair)
|
huffman@33581
|
187 |
hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
|
huffman@33581
|
188 |
by simp
|
huffman@33581
|
189 |
thus "P (fix\<cdot>F) (fix\<cdot>G)"
|
huffman@33581
|
190 |
by (simp add: fix_def2)
|
huffman@33581
|
191 |
qed
|
huffman@33581
|
192 |
|
huffman@35930
|
193 |
subsection {* Fixed-points on product types *}
|
huffman@18093
|
194 |
|
huffman@18095
|
195 |
text {*
|
huffman@18095
|
196 |
Bekic's Theorem: Simultaneous fixed points over pairs
|
huffman@18095
|
197 |
can be written in terms of separate fixed points.
|
huffman@18095
|
198 |
*}
|
huffman@18095
|
199 |
|
huffman@18095
|
200 |
lemma fix_cprod:
|
huffman@18095
|
201 |
"fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
|
huffman@35921
|
202 |
(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
|
huffman@35921
|
203 |
\<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
|
huffman@35921
|
204 |
(is "fix\<cdot>F = (?x, ?y)")
|
huffman@27185
|
205 |
proof (rule fix_eqI)
|
huffman@35921
|
206 |
have 1: "fst (F\<cdot>(?x, ?y)) = ?x"
|
huffman@18095
|
207 |
by (rule trans [symmetric, OF fix_eq], simp)
|
huffman@35921
|
208 |
have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
|
huffman@18095
|
209 |
by (rule trans [symmetric, OF fix_eq], simp)
|
huffman@35921
|
210 |
from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
|
huffman@18095
|
211 |
next
|
huffman@18095
|
212 |
fix z assume F_z: "F\<cdot>z = z"
|
huffman@35921
|
213 |
obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
|
huffman@35921
|
214 |
from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp
|
huffman@35921
|
215 |
from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp
|
huffman@35921
|
216 |
let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))"
|
huffman@18095
|
217 |
have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
|
huffman@35921
|
218 |
hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
|
huffman@35921
|
219 |
by (simp add: fst_monofun monofun_cfun)
|
huffman@35921
|
220 |
hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp
|
huffman@31076
|
221 |
hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
|
huffman@35921
|
222 |
hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
|
huffman@35921
|
223 |
by (simp add: snd_monofun monofun_cfun)
|
huffman@35921
|
224 |
hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp
|
huffman@31076
|
225 |
hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
|
huffman@35921
|
226 |
show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp
|
huffman@18095
|
227 |
qed
|
huffman@18095
|
228 |
|
nipkow@243
|
229 |
end
|