equal
deleted
inserted
replaced
689 |
689 |
690 ML {* |
690 ML {* |
691 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
691 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
692 *} |
692 *} |
693 |
693 |
|
694 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
|
695 by (rule eq_reflection) (simp add: prod_fun_def) |
|
696 |
|
697 lemma map_id: "map id \<equiv> id" |
|
698 apply (rule eq_reflection) |
|
699 apply (rule ext) |
|
700 apply (rule_tac list="x" in list.induct) |
|
701 apply (simp_all) |
|
702 done |
|
703 |
694 ML {* |
704 ML {* |
695 fun quotient_tac quot_thm = |
705 fun quotient_tac quot_thm = |
696 REPEAT_ALL_NEW (FIRST' [ |
706 REPEAT_ALL_NEW (FIRST' [ |
697 rtac @{thm FUN_QUOTIENT}, |
707 rtac @{thm FUN_QUOTIENT}, |
698 rtac quot_thm, |
708 rtac quot_thm, |
699 rtac @{thm IDENTITY_QUOTIENT}, |
709 rtac @{thm IDENTITY_QUOTIENT}, |
700 (* For functional identity quotients, (op = ---> op =) *) |
710 (* For functional identity quotients, (op = ---> op =) *) |
701 CHANGED' ( |
711 CHANGED' ( |
702 (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN' |
712 (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} |
703 rtac @{thm IDENTITY_QUOTIENT} |
713 ))) |
704 ) |
|
705 ]) |
714 ]) |
706 *} |
715 *} |
707 |
716 |
708 ML {* |
717 ML {* |
709 fun LAMBDA_RES_TAC ctxt i st = |
718 fun LAMBDA_RES_TAC ctxt i st = |
806 end |
815 end |
807 *} |
816 *} |
808 |
817 |
809 section {* Cleaning the goal *} |
818 section {* Cleaning the goal *} |
810 |
819 |
811 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
|
812 by (rule eq_reflection) (simp add: prod_fun_def) |
|
813 |
|
814 lemma map_id: "map id \<equiv> id" |
|
815 apply (rule eq_reflection) |
|
816 apply (rule ext) |
|
817 apply (rule_tac list="x" in list.induct) |
|
818 apply (simp_all) |
|
819 done |
|
820 |
820 |
821 ML {* |
821 ML {* |
822 fun simp_ids lthy thm = |
822 fun simp_ids lthy thm = |
823 MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm |
823 MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm |
824 *} |
824 *} |