equal
deleted
inserted
replaced
215 done |
215 done |
216 |
216 |
217 lemma coinduct3: |
217 lemma coinduct3: |
218 "[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" |
218 "[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" |
219 apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) |
219 apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) |
220 apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) |
220 apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst]) |
|
221 apply (simp_all) |
221 done |
222 done |
222 |
223 |
223 |
224 |
224 text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, |
225 text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, |
225 to control unfolding*} |
226 to control unfolding*} |