172 ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}

   172 ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} 

   173 

   173          @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}

   174 

   174 

   175 ML {*

   176   mk_REGULARIZE_goal @{context} 

   177     @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}

   178     @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}

   179   |> Syntax.string_of_term @{context}

   180   |> writeln

   181 *}

   182 

   183 lemma procedure: 

   184   assumes a: "A"

   185   and     b: "A \<Longrightarrow> B"

   186   and     c: "B = C"

   187   and     d: "C = D"

   188   shows   "D"

   189   using a b c d

   190   by simp

   191 

   192 ML {* 

   193 fun procedure_inst ctxt rtrm qtrm =

   194 let

   195   val thy = ProofContext.theory_of ctxt

   196   val rtrm' = HOLogic.dest_Trueprop rtrm

   197   val qtrm' = HOLogic.dest_Trueprop qtrm

   198 in

   199   Drule.instantiate' [] 

   200     [SOME (cterm_of thy rtrm'), 

   201      SOME (cterm_of thy (Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm'))),

   202      SOME (cterm_of thy (Syntax.check_term ctxt (inj_REPABS ctxt (rtrm', qtrm'))))] 

   203   @{thm procedure}

   204 end

   205 

   206 fun procedure_tac rthm =

   207   Subgoal.FOCUS (fn {context, concl, ...} =>

   208     let

   209       val rthm' = atomize_thm rthm

   210       val rule = procedure_inst context (prop_of rthm') (term_of concl)

   211     in

   212       EVERY1 [rtac rule, rtac rthm']

   213     end)

   214 *}

   215 

   216 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"

   217 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})

   218 sorry