QuotMain.thy
changeset 307 9aa3aba71ecc
parent 303 991b0e53f9dc
child 310 fec6301a1989
equal deleted inserted replaced
305:d7b60303adb8 307:9aa3aba71ecc
   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 =