140 ML {* |
140 ML {* |
141 fun lift_thm_my_int lthy t = |
141 fun lift_thm_my_int lthy t = |
142 lift_thm lthy qty ty_name rsp_thms defs t |
142 lift_thm lthy qty ty_name rsp_thms defs t |
143 *} |
143 *} |
144 |
144 |
|
145 ML {* |
|
146 fun regularize_goal thm rel_eqv rel_refl lthy qtrm = |
|
147 let |
|
148 val reg_trm = mk_REGULARIZE_goal @{context} (prop_of thm) qtrm; |
|
149 fun tac ctxt = |
|
150 (ObjectLogic.full_atomize_tac) THEN' |
|
151 REPEAT_ALL_NEW (FIRST' [ |
|
152 rtac rel_refl, |
|
153 atac, |
|
154 rtac @{thm universal_twice}, |
|
155 (rtac @{thm impI} THEN' atac), |
|
156 rtac @{thm implication_twice}, |
|
157 EqSubst.eqsubst_tac ctxt [0] |
|
158 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
159 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
160 (* For a = b \<longrightarrow> a \<approx> b *) |
|
161 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
162 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
163 ]); |
|
164 val cthm = Goal.prove lthy [] [] reg_trm |
|
165 (fn {context, ...} => tac context 1); |
|
166 in |
|
167 cthm OF [thm] |
|
168 end |
|
169 *} |
|
170 |
|
171 ML {* |
|
172 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = |
|
173 let |
|
174 val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); |
|
175 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
176 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
|
177 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
178 in |
|
179 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
|
180 end |
|
181 *} |
|
182 |
|
183 |
|
184 ML {* |
|
185 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
|
186 let |
|
187 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
|
188 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
|
189 val consts = lookup_quot_consts defs; |
|
190 val t_a = atomize_thm rthm; |
|
191 val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; |
|
192 val t_r = regularize_goal t_a rel_eqv rel_refl lthy goal_a; |
|
193 val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; |
|
194 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
|
195 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
196 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
197 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
198 val abs = findabs rty (prop_of t_a); |
|
199 val aps = findaps rty (prop_of t_a); |
|
200 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
|
201 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
202 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
203 val defs_sym = flat (map (add_lower_defs lthy) defs); |
|
204 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
205 val t_id = simp_ids lthy t_l; |
|
206 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
207 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
208 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
209 val t_rv = ObjectLogic.rulify t_r |
|
210 in |
|
211 Thm.varifyT t_rv |
|
212 end |
|
213 *} |
|
214 |
|
215 ML {* |
|
216 fun lift_thm_g_my_int lthy t g = |
|
217 lift_thm_goal lthy qty ty_name rsp_thms defs t g |
|
218 *} |
|
219 |
145 print_quotients |
220 print_quotients |
146 ML {* quotdata_lookup @{context} "IntEx.my_int" *} |
221 ML {* quotdata_lookup @{context} "IntEx.my_int" *} |
147 ML {* quotdata_lookup @{context} "my_int" *} |
222 ML {* quotdata_lookup @{context} "my_int" *} |
148 |
223 |
149 ML {* |
224 ML {* |