163 also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse) |
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) |
164 also have "... = F f" by (simp add: eq) |
165 finally show "f = F f" . |
165 finally show "f = F f" . |
166 qed |
166 qed |
167 |
167 |
|
168 text {* Fixpoint induction rule *} |
|
169 |
|
170 lemma fixp_induct_uc: |
|
171 fixes F :: "'c \<Rightarrow> 'c" and |
|
172 U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and |
|
173 C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and |
|
174 P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" |
|
175 assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" |
|
176 assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" |
|
177 assumes inverse: "\<And>f. U (C f) = f" |
|
178 assumes adm: "ccpo.admissible le_fun lub_fun P" |
|
179 assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))" |
|
180 shows "P (U f)" |
|
181 unfolding eq inverse |
|
182 apply (rule ccpo.fixp_induct[OF ccpo adm]) |
|
183 apply (insert mono, auto simp: monotone_def fun_ord_def)[1] |
|
184 by (rule_tac f="C x" in step, simp add: inverse) |
|
185 |
|
186 |
168 text {* Rules for @{term mono_body}: *} |
187 text {* Rules for @{term mono_body}: *} |
169 |
188 |
170 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)" |
189 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)" |
171 by (rule monotoneI) (rule leq_refl) |
190 by (rule monotoneI) (rule leq_refl) |
172 |
191 |
221 by (rule flat_interpretation) |
240 by (rule flat_interpretation) |
222 |
241 |
223 interpretation option!: |
242 interpretation option!: |
224 partial_function_definitions "flat_ord None" "flat_lub None" |
243 partial_function_definitions "flat_ord None" "flat_lub None" |
225 by (rule flat_interpretation) |
244 by (rule flat_interpretation) |
226 |
|
227 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} |
|
228 @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} |
|
229 |
|
230 declaration {* Partial_Function.init "option" @{term option.fixp_fun} |
|
231 @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *} |
|
232 |
245 |
233 |
246 |
234 abbreviation "option_ord \<equiv> flat_ord None" |
247 abbreviation "option_ord \<equiv> flat_ord None" |
235 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
248 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
236 |
249 |
286 then have "\<exists>f\<in>A. f x = Some y" by auto |
299 then have "\<exists>f\<in>A. f x = Some y" by auto |
287 with IH show "P x y" by auto |
300 with IH show "P x y" by auto |
288 qed |
301 qed |
289 qed |
302 qed |
290 |
303 |
|
304 lemma fixp_induct_option: |
|
305 fixes F :: "'c \<Rightarrow> 'c" and |
|
306 U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and |
|
307 C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and |
|
308 P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" |
|
309 assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)" |
|
310 assumes eq: "f \<equiv> C (ccpo.fixp (fun_ord option_ord) (fun_lub (flat_lub None)) (\<lambda>f. U (F (C f))))" |
|
311 assumes inverse2: "\<And>f. U (C f) = f" |
|
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" |
|
313 assumes defined: "U f x = Some y" |
|
314 shows "P x y" |
|
315 using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] |
|
316 by blast |
|
317 |
|
318 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} |
|
319 @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} |
|
320 |
|
321 declaration {* Partial_Function.init "option" @{term option.fixp_fun} |
|
322 @{term option.mono_body} @{thm option.fixp_rule_uc} |
|
323 (SOME @{thm fixp_induct_option}) *} |
|
324 |
291 |
325 |
292 hide_const (open) chain |
326 hide_const (open) chain |
293 |
327 |
294 end |
328 end |
295 |
329 |