212 \ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; |
212 \ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; |
213 by (cut_facts_tac (equivA::prems) 1); |
213 by (cut_facts_tac (equivA::prems) 1); |
214 by (safe_tac rel_cs); |
214 by (safe_tac rel_cs); |
215 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); |
215 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); |
216 by (assume_tac 1); |
216 by (assume_tac 1); |
217 by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class, |
217 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, |
218 congruent2_implies_congruent]) 1); |
218 congruent2_implies_congruent]) 1); |
219 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); |
219 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); |
220 by (fast_tac rel_cs 1); |
220 by (fast_tac rel_cs 1); |
221 qed "congruent2_implies_congruent_UN"; |
221 qed "congruent2_implies_congruent_UN"; |
222 |
222 |
223 val prems as equivA::_ = goal Equiv.thy |
223 val prems as equivA::_ = goal Equiv.thy |
224 "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ |
224 "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ |
225 \ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; |
225 \ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; |
226 by (cut_facts_tac prems 1); |
226 by (cut_facts_tac prems 1); |
227 by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class, |
227 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, |
228 congruent2_implies_congruent, |
228 congruent2_implies_congruent, |
229 congruent2_implies_congruent_UN]) 1); |
229 congruent2_implies_congruent_UN]) 1); |
230 qed "UN_equiv_class2"; |
230 qed "UN_equiv_class2"; |
231 |
231 |
232 (*type checking*) |
232 (*type checking*) |
233 val prems = goalw Equiv.thy [quotient_def] |
233 val prems = goalw Equiv.thy [quotient_def] |
234 "[| equiv A r; congruent2 r b; \ |
234 "[| equiv A r; congruent2 r b; \ |