equal
deleted
inserted
replaced
217 apply (rule ext) |
217 apply (rule ext) |
218 apply (rule_tac list="x" in list.induct) |
218 apply (rule_tac list="x" in list.induct) |
219 apply (simp_all) |
219 apply (simp_all) |
220 done |
220 done |
221 |
221 |
222 ML {* |
222 lemmas id_simps = |
223 fun simp_ids lthy thm = |
223 FUN_MAP_I[THEN eq_reflection] |
224 let |
224 id_apply[THEN eq_reflection] |
225 val thms = @{thms eq_reflection[OF FUN_MAP_I] |
225 id_def_sym prod_fun_id map_id |
226 eq_reflection[OF id_apply] |
226 |
227 id_def_sym prod_fun_id map_id} |
227 ML {* |
228 in |
228 fun simp_ids thm = |
229 MetaSimplifier.rewrite_rule thms thm |
229 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
230 end |
|
231 *} |
230 *} |
232 |
231 |
233 section {* Debugging infrastructure for testing tactics *} |
232 section {* Debugging infrastructure for testing tactics *} |
234 |
233 |
235 ML {* |
234 ML {* |
269 ML {* |
268 ML {* |
270 fun add_lower_defs_aux lthy thm = |
269 fun add_lower_defs_aux lthy thm = |
271 let |
270 let |
272 val e1 = @{thm fun_cong} OF [thm]; |
271 val e1 = @{thm fun_cong} OF [thm]; |
273 val f = eqsubst_thm lthy @{thms fun_map.simps} e1; |
272 val f = eqsubst_thm lthy @{thms fun_map.simps} e1; |
274 val g = simp_ids lthy f |
273 val g = simp_ids f |
275 in |
274 in |
276 (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) |
275 (simp_ids thm) :: (add_lower_defs_aux lthy g) |
277 end |
276 end |
278 handle _ => [simp_ids lthy thm] |
277 handle _ => [simp_ids thm] |
279 *} |
278 *} |
280 |
279 |
281 ML {* |
280 ML {* |
282 fun add_lower_defs lthy def = |
281 fun add_lower_defs lthy def = |
283 let |
282 let |
730 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
729 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
731 *} |
730 *} |
732 |
731 |
733 ML {* |
732 ML {* |
734 fun quotient_tac quot_thm = |
733 fun quotient_tac quot_thm = |
735 let |
|
736 val simps = @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] |
|
737 id_def_sym prod_fun_id map_id} |
|
738 in |
|
739 REPEAT_ALL_NEW (FIRST' [ |
734 REPEAT_ALL_NEW (FIRST' [ |
740 rtac @{thm FUN_QUOTIENT}, |
735 rtac @{thm FUN_QUOTIENT}, |
741 rtac quot_thm, |
736 rtac quot_thm, |
742 rtac @{thm IDENTITY_QUOTIENT}, |
737 rtac @{thm IDENTITY_QUOTIENT}, |
743 (* For functional identity quotients, (op = ---> op =) *) |
738 (* For functional identity quotients, (op = ---> op =) *) |
744 CHANGED' (simp_tac (HOL_ss addsimps simps)) |
739 CHANGED' (simp_tac (HOL_ss addsimps @{thms id_simps})) |
745 ]) |
740 ]) |
746 end |
|
747 *} |
741 *} |
748 |
742 |
749 ML {* |
743 ML {* |
750 fun LAMBDA_RES_TAC ctxt i st = |
744 fun LAMBDA_RES_TAC ctxt i st = |
751 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
745 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
915 val eq = Logic.mk_equals (llhs, rhs); |
909 val eq = Logic.mk_equals (llhs, rhs); |
916 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
910 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
917 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply}); |
911 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply}); |
918 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
912 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
919 val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t; |
913 val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t; |
|
914 (* FIXME/TODO: should that be id_simps? *) |
920 in |
915 in |
921 singleton (ProofContext.export lthy' lthy) t_id |
916 singleton (ProofContext.export lthy' lthy) t_id |
922 end |
917 end |
923 *} |
918 *} |
924 |
919 |