44 val comp_equivI = result(); |
44 val comp_equivI = result(); |
45 |
45 |
46 (** Equivalence classes **) |
46 (** Equivalence classes **) |
47 |
47 |
48 (*Lemma for the next result*) |
48 (*Lemma for the next result*) |
49 goalw Equiv.thy [equiv_def,trans_def,sym_def] |
49 goalw Equiv.thy [trans_def,sym_def] |
50 "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} <= r``{b}"; |
50 "!!A r. [| sym(r); trans(r); <a,b>: r |] ==> r``{a} <= r``{b}"; |
51 by (fast_tac ZF_cs 1); |
51 by (fast_tac ZF_cs 1); |
52 val equiv_class_subset = result(); |
52 val equiv_class_subset = result(); |
53 |
53 |
54 goal Equiv.thy "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}"; |
54 goalw Equiv.thy [equiv_def] |
55 by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); |
55 "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}"; |
56 by (rewrite_goals_tac [equiv_def,sym_def]); |
56 by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset])); |
|
57 by (rewrite_goals_tac [sym_def]); |
57 by (fast_tac ZF_cs 1); |
58 by (fast_tac ZF_cs 1); |
58 val equiv_class_eq = result(); |
59 val equiv_class_eq = result(); |
59 |
60 |
60 val prems = goalw Equiv.thy [equiv_def,refl_def] |
61 val prems = goalw Equiv.thy [equiv_def,refl_def] |
61 "[| equiv(A,r); a: A |] ==> a: r``{a}"; |
62 "[| equiv(A,r); a: A |] ==> a: r``{a}"; |