equal
deleted
inserted
replaced
79 |
79 |
80 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *) |
80 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *) |
81 |
81 |
82 val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)"; |
82 val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)"; |
83 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1); |
83 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1); |
84 by (rtac (monoh RS monoD) 1); |
84 by (rtac (monoh RS @{thm monoD}) 1); |
85 by (rtac (UnE RS subsetI) 1); |
85 by (rtac (UnE RS subsetI) 1); |
86 by (assume_tac 1); |
86 by (assume_tac 1); |
87 by (blast_tac (claset() addSIs [cih]) 1); |
87 by (blast_tac (claset() addSIs [cih]) 1); |
88 by (rtac (monoh RS monoD RS subsetD) 1); |
88 by (rtac (monoh RS @{thm monoD} RS subsetD) 1); |
89 by (rtac (thm "Un_upper2") 1); |
89 by (rtac (thm "Un_upper2") 1); |
90 by (etac (monoh RS gfp_lemma2 RS subsetD) 1); |
90 by (etac (monoh RS gfp_lemma2 RS subsetD) 1); |
91 qed "gfp_coind2"; |
91 qed "gfp_coind2"; |
92 |
92 |
93 val [gfph,monoh,caseh] = goal (the_context ()) |
93 val [gfph,monoh,caseh] = goal (the_context ()) |