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