723 ML {*

   724 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =

   725   let

   726     val rt = build_repabs_term lthy thm constructors rty qty;

   727     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);

   728     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

   729       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));

   730     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

   731   in

   732     (rt, cthm, thm)

   733   end

   734 *}

   735 

   736 ML {*

   737 fun repabs_eq2 lthy (rt, thm, othm) =

   738   let

   739     fun tac2 ctxt =

   740      (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))

   741      THEN' (rtac othm);

   742     val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);

   743   in

   744     cthm

   745   end

   746 *}

   747 

   766 text {* expects atomized definition *}

   767 ML {*

   768   fun add_lower_defs_aux ctxt thm =

   769     let

   770       val e1 = @{thm fun_cong} OF [thm]

   771       val f = eqsubst_thm ctxt @{thms fun_map.simps} e1

   772     in

   773       thm :: (add_lower_defs_aux ctxt f)

   774     end

   775     handle _ => [thm]

   776 *}

   777 

   778 ML {*

   779 fun add_lower_defs ctxt defs =

   780   let

   781     val defs_pre_sym = map symmetric defs

   782     val defs_atom = map atomize_thm defs_pre_sym

   783     val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)

   784     val defs_sym = map (fn t => eq_reflection OF [t]) defs_all

   785   in

   786     map Thm.varifyT defs_sym

   787   end

   788 *}

   789 

   790