equal
deleted
inserted
replaced
868 end |
868 end |
869 *} |
869 *} |
870 |
870 |
871 section {* Cleaning the goal *} |
871 section {* Cleaning the goal *} |
872 |
872 |
|
873 lemma prod_fun_id: "prod_fun id id = id" |
|
874 apply (simp add: prod_fun_def) |
|
875 done |
|
876 lemma map_id: "map id x = x" |
|
877 apply (induct x) |
|
878 apply (simp_all add: map.simps) |
|
879 done |
|
880 |
873 text {* expects atomized definition *} |
881 text {* expects atomized definition *} |
874 ML {* |
882 ML {* |
875 fun add_lower_defs_aux ctxt thm = |
883 fun add_lower_defs_aux ctxt thm = |
876 let |
884 let |
877 val e1 = @{thm fun_cong} OF [thm]; |
885 val e1 = @{thm fun_cong} OF [thm]; |
878 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; |
886 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; |
879 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; |
887 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; |
880 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g; |
888 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g |
881 val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h |
|
882 in |
889 in |
883 thm :: (add_lower_defs_aux ctxt i) |
890 thm :: (add_lower_defs_aux ctxt h) |
884 end |
891 end |
885 handle _ => [thm] |
892 handle _ => [thm] |
886 *} |
893 *} |
887 |
894 |
888 ML {* |
895 ML {* |