4 

     5 

     6 section {*  Infrastructure about definitions *}

     7 

     8 (* Does the same as 'subst' in a given theorem *)

     9 ML {*

    10 fun eqsubst_thm ctxt thms thm =

    11   let

    12     val goalstate = Goal.init (Thm.cprop_of thm)

    13     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of

    14       NONE => error "eqsubst_thm"

    15     | SOME th => cprem_of th 1

    16     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1

    17     val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');

    18     val cgoal = cterm_of (ProofContext.theory_of ctxt) goal

    19     val rt = Goal.prove_internal [] cgoal (fn _ => tac);

    20   in

    21     @{thm equal_elim_rule1} OF [rt, thm]

    22   end

    23 *}

    24 

    25 (* expects atomized definitions *)

    26 ML {*

    27 fun add_lower_defs_aux lthy thm =

    28   let

    29     val e1 = @{thm fun_cong} OF [thm];

    30     val f = eqsubst_thm lthy @{thms fun_map.simps} e1;

    31     val g = simp_ids f

    32   in

    33     (simp_ids thm) :: (add_lower_defs_aux lthy g)

    34   end

    35   handle _ => [simp_ids thm]

    36 *}

    37 

    38 ML {*

    39 fun add_lower_defs lthy def =

    40   let

    41     val def_pre_sym = symmetric def

    42     val def_atom = atomize_thm def_pre_sym

    43     val defs_all = add_lower_defs_aux lthy def_atom

    44   in

    45     map Thm.varifyT defs_all

    46   end

    47 *}

    48