equal
deleted
inserted
replaced
212 |
212 |
213 subsection {* Recursive types *} |
213 subsection {* Recursive types *} |
214 |
214 |
215 subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} |
215 subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} |
216 |
216 |
217 lemma NatM: "mono(%X. Unit+X)"; |
217 lemma NatM: "mono(%X. Unit+X)" |
218 apply (rule PlusM constM idM)+ |
218 apply (rule PlusM constM idM)+ |
219 done |
219 done |
220 |
220 |
221 lemma def_NatB: "Nat = Unit + Nat" |
221 lemma def_NatB: "Nat = Unit + Nat" |
222 apply (rule def_lfp_Tarski [OF Nat_def]) |
222 apply (rule def_lfp_Tarski [OF Nat_def]) |
356 assumes "a:A" |
356 assumes "a:A" |
357 and "!!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X)" |
357 and "!!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X)" |
358 shows "t(a) : gfp(B)" |
358 shows "t(a) : gfp(B)" |
359 apply (rule coinduct) |
359 apply (rule coinduct) |
360 apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI) |
360 apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI) |
361 apply (blast intro!: prems)+ |
361 apply (blast intro!: assms)+ |
362 done |
362 done |
363 |
363 |
364 lemma def_gfpI: |
364 lemma def_gfpI: |
365 "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> |
365 "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> |
366 t(a) : C" |
366 t(a) : C" |