equal
deleted
inserted
replaced
133 qed |
133 qed |
134 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
134 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
135 qed |
135 qed |
136 |
136 |
137 end |
137 end |
138 |
|
139 (* EQUALS_RSP is stronger *) |
|
140 lemma equiv_trans2: |
|
141 assumes e: "EQUIV R" |
|
142 and ac: "R a c" |
|
143 and bd: "R b d" |
|
144 shows "R a b = R c d" |
|
145 using ac bd e |
|
146 unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def |
|
147 by (blast) |
|
148 |
138 |
149 section {* type definition for the quotient type *} |
139 section {* type definition for the quotient type *} |
150 |
140 |
151 (* the auxiliary data for the quotient types *) |
141 (* the auxiliary data for the quotient types *) |
152 use "quotient_info.ML" |
142 use "quotient_info.ML" |
1341 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1331 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1342 let |
1332 let |
1343 val rthm' = atomize_thm rthm |
1333 val rthm' = atomize_thm rthm |
1344 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1334 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1345 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1335 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1346 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1336 val quotients = quotient_rules_get lthy |
|
1337 val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients |
1347 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1338 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1348 in |
1339 in |
1349 EVERY1 |
1340 EVERY1 |
1350 [rtac rule, |
1341 [rtac rule, |
1351 RANGE [rtac rthm', |
1342 RANGE [rtac rthm', |