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 lemma tst: "EQUIV bla" |
|
140 sorry |
|
141 |
|
142 lemma equiv_trans2: |
|
143 assumes e: "EQUIV R" |
|
144 and ac: "R a c" |
|
145 and bd: "R b d" |
|
146 shows "R a b = R c d" |
|
147 using ac bd e |
|
148 unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def |
|
149 by (blast) |
138 |
150 |
139 section {* type definition for the quotient type *} |
151 section {* type definition for the quotient type *} |
140 |
152 |
141 (* the auxiliary data for the quotient types *) |
153 (* the auxiliary data for the quotient types *) |
142 use "quotient_info.ML" |
154 use "quotient_info.ML" |
801 end |
813 end |
802 handle _ => no_tac) |
814 handle _ => no_tac) |
803 *} |
815 *} |
804 |
816 |
805 ML {* |
817 ML {* |
806 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans_thm rsp_thms = |
818 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
807 (FIRST' [ |
819 (FIRST' [ |
808 rtac trans_thm, |
820 FIRST' (map rtac trans2), |
809 LAMBDA_RES_TAC ctxt, |
821 LAMBDA_RES_TAC ctxt, |
810 rtac @{thm RES_FORALL_RSP}, |
822 rtac @{thm RES_FORALL_RSP}, |
811 ball_rsp_tac ctxt, |
823 ball_rsp_tac ctxt, |
812 rtac @{thm RES_EXISTS_RSP}, |
824 rtac @{thm RES_EXISTS_RSP}, |
813 bex_rsp_tac ctxt, |
825 bex_rsp_tac ctxt, |
1114 end) lthy |
1126 end) lthy |
1115 *} |
1127 *} |
1116 |
1128 |
1117 ML {* |
1129 ML {* |
1118 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1130 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1119 fun lift_tac lthy rthm rel_eqv rty quot trans2 rsp_thms defs = |
1131 fun lift_tac lthy rthm rel_eqv rty quot rsp_thms defs = |
1120 ObjectLogic.full_atomize_tac |
1132 ObjectLogic.full_atomize_tac |
1121 THEN' gen_frees_tac lthy |
1133 THEN' gen_frees_tac lthy |
1122 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1134 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1123 let |
1135 let |
1124 val rthm' = atomize_thm rthm |
1136 val rthm' = atomize_thm rthm |
1125 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1137 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1126 val aps = find_aps (prop_of rthm') (term_of concl) |
1138 val aps = find_aps (prop_of rthm') (term_of concl) |
1127 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1139 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
|
1140 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1128 in |
1141 in |
1129 EVERY1 |
1142 EVERY1 |
1130 [rtac rule, |
1143 [rtac rule, |
1131 RANGE [rtac rthm', |
1144 RANGE [rtac rthm', |
1132 regularize_tac lthy rel_eqv rel_refl, |
1145 regularize_tac lthy rel_eqv rel_refl, |