equal
deleted
inserted
replaced
85 by (rtac (Un_least RS Un_least) 1); |
85 by (rtac (Un_least RS Un_least) 1); |
86 by (rtac subset_refl 1); |
86 by (rtac subset_refl 1); |
87 by (rtac prem 1); |
87 by (rtac prem 1); |
88 by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); |
88 by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); |
89 by (rtac (mono RS monoD) 1); |
89 by (rtac (mono RS monoD) 1); |
90 by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1); |
90 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
91 by (rtac Un_upper2 1); |
91 by (rtac Un_upper2 1); |
92 qed "coinduct3_lemma"; |
92 qed "coinduct3_lemma"; |
93 |
93 |
94 val prems = goal Gfp.thy |
94 val prems = goal Gfp.thy |
95 "[| mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
95 "[| mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |