equal
deleted
inserted
replaced
837 end |
837 end |
838 *} |
838 *} |
839 |
839 |
840 section {* Cleaning the goal *} |
840 section {* Cleaning the goal *} |
841 |
841 |
842 lemma prod_fun_id: "prod_fun id id = id" |
842 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
843 by (simp add: prod_fun_def) |
843 by (rule eq_reflection) (simp add: prod_fun_def) |
844 |
844 |
845 lemma map_id: "map id x = x" |
845 lemma map_id: "map id \<equiv> id" |
846 by (induct x) (simp_all) |
846 apply (rule eq_reflection) |
|
847 apply (rule ext) |
|
848 apply (rule_tac list="x" in list.induct) |
|
849 apply (simp_all) |
|
850 done |
847 |
851 |
848 ML {* |
852 ML {* |
849 fun simp_ids lthy thm = |
853 fun simp_ids lthy thm = |
850 thm |
854 MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm |
851 |> MetaSimplifier.rewrite_rule @{thms id_def_sym} |
855 *} |
852 |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id} |
856 |
|
857 ML {* |
|
858 fun simp_ids_trm trm = |
|
859 trm |> |
|
860 MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} |
|
861 |> cprop_of |> Thm.dest_equals |> snd |
|
862 |
853 *} |
863 *} |
854 |
864 |
855 text {* expects atomized definition *} |
865 text {* expects atomized definition *} |
856 ML {* |
866 ML {* |
857 fun add_lower_defs_aux lthy thm = |
867 fun add_lower_defs_aux lthy thm = |