equal
deleted
inserted
replaced
219 apply (simp_all) |
219 apply (simp_all) |
220 done |
220 done |
221 |
221 |
222 ML {* |
222 ML {* |
223 fun simp_ids lthy thm = |
223 fun simp_ids lthy thm = |
224 MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm |
224 let |
|
225 val thms = @{thms eq_reflection[OF FUN_MAP_I] |
|
226 eq_reflection[OF id_apply] |
|
227 id_def_sym prod_fun_id map_id} |
|
228 in |
|
229 MetaSimplifier.rewrite_rule thms thm |
|
230 end |
225 *} |
231 *} |
226 |
232 |
227 section {* Does the same as 'subst' in a given theorem *} |
233 section {* Does the same as 'subst' in a given theorem *} |
228 |
234 |
229 ML {* |
235 ML {* |
236 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
242 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
237 val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); |
243 val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); |
238 val cgoal = cterm_of (ProofContext.theory_of ctxt) goal |
244 val cgoal = cterm_of (ProofContext.theory_of ctxt) goal |
239 val rt = Goal.prove_internal [] cgoal (fn _ => tac); |
245 val rt = Goal.prove_internal [] cgoal (fn _ => tac); |
240 in |
246 in |
241 @{thm Pure.equal_elim_rule1} OF [rt, thm] |
247 @{thm equal_elim_rule1} OF [rt, thm] |
242 end |
248 end |
243 *} |
249 *} |
244 |
250 |
245 section {* Infrastructure about definitions *} |
251 section {* Infrastructure about definitions *} |
246 |
252 |
310 end |
316 end |
311 *} |
317 *} |
312 |
318 |
313 |
319 |
314 |
320 |
315 (******************************************) |
321 section {* Regularization *} |
316 (******************************************) |
|
317 (* version with explicit qtrm *) |
|
318 (******************************************) |
|
319 (******************************************) |
|
320 |
322 |
321 |
323 |
322 ML {* |
324 ML {* |
323 (* |
325 (* |
324 Regularizing an rtrm means: |
326 Regularizing an rtrm means: |
735 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
737 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
736 *} |
738 *} |
737 |
739 |
738 ML {* |
740 ML {* |
739 fun quotient_tac quot_thm = |
741 fun quotient_tac quot_thm = |
|
742 let |
|
743 val simps = @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] |
|
744 id_def_sym prod_fun_id map_id} |
|
745 in |
740 REPEAT_ALL_NEW (FIRST' [ |
746 REPEAT_ALL_NEW (FIRST' [ |
741 rtac @{thm FUN_QUOTIENT}, |
747 rtac @{thm FUN_QUOTIENT}, |
742 rtac quot_thm, |
748 rtac quot_thm, |
743 rtac @{thm IDENTITY_QUOTIENT}, |
749 rtac @{thm IDENTITY_QUOTIENT}, |
744 (* For functional identity quotients, (op = ---> op =) *) |
750 (* For functional identity quotients, (op = ---> op =) *) |
745 CHANGED' ( |
751 CHANGED' (simp_tac (HOL_ss addsimps simps)) |
746 (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} |
|
747 ))) |
|
748 ]) |
752 ]) |
|
753 end |
749 *} |
754 *} |
750 |
755 |
751 ML {* |
756 ML {* |
752 fun LAMBDA_RES_TAC ctxt i st = |
757 fun LAMBDA_RES_TAC ctxt i st = |
753 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
758 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
1209 in |
1214 in |
1210 rtac rule i |
1215 rtac rule i |
1211 end) |
1216 end) |
1212 *} |
1217 *} |
1213 |
1218 |
1214 (* General outline of the lifting procedure *) |
1219 section {* General outline of the lifting procedure *} |
|
1220 |
|
1221 |
1215 (* **************************************** *) |
1222 (* **************************************** *) |
1216 (* *) |
1223 (* *) |
1217 (* - A is the original raw theorem *) |
1224 (* - A is the original raw theorem *) |
1218 (* - B is the regularized theorem *) |
1225 (* - B is the regularized theorem *) |
1219 (* - C is the rep/abs injected version of B *) |
1226 (* - C is the rep/abs injected version of B *) |