equal
deleted
inserted
replaced
5 |
5 |
6 Lemmas and tactics for using the rule coinduct3 on [= and =. |
6 Lemmas and tactics for using the rule coinduct3 on [= and =. |
7 *) |
7 *) |
8 |
8 |
9 val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; |
9 val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; |
10 by (rtac ((mono RS lfp_Tarski) RS ssubst) 1); |
10 by (stac (mono RS lfp_Tarski) 1); |
11 by (rtac prem 1); |
11 by (rtac prem 1); |
12 qed "lfpI"; |
12 qed "lfpI"; |
13 |
13 |
14 val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A"; |
14 val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A"; |
15 by (simp_tac (term_ss addsimps prems) 1); |
15 by (simp_tac (term_ss addsimps prems) 1); |