equal
deleted
inserted
replaced
53 |
53 |
54 (**** Proof of Knaster-Tarski Theorem for the lfp ****) |
54 (**** Proof of Knaster-Tarski Theorem for the lfp ****) |
55 |
55 |
56 (*lfp is contained in each pre-fixedpoint*) |
56 (*lfp is contained in each pre-fixedpoint*) |
57 Goalw [lfp_def] |
57 Goalw [lfp_def] |
58 "!!A. [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; |
58 "[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; |
59 by (Blast_tac 1); |
59 by (Blast_tac 1); |
60 (*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) |
60 (*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) |
61 qed "lfp_lowerbound"; |
61 qed "lfp_lowerbound"; |
62 |
62 |
63 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) |
63 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) |
256 by (rtac (Un_upper2 RS subset_trans) 1); |
256 by (rtac (Un_upper2 RS subset_trans) 1); |
257 by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); |
257 by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); |
258 qed "coinduct_lemma"; |
258 qed "coinduct_lemma"; |
259 |
259 |
260 (*strong version*) |
260 (*strong version*) |
261 Goal |
261 Goal "[| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ |
262 "!!X D. [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ |
|
263 \ a : gfp(D,h)"; |
262 \ a : gfp(D,h)"; |
264 by (rtac weak_coinduct 1); |
263 by (rtac weak_coinduct 1); |
265 by (etac coinduct_lemma 2); |
264 by (etac coinduct_lemma 2); |
266 by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); |
265 by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); |
267 qed "coinduct"; |
266 qed "coinduct"; |