Theory Renaming_Auto

theory Renaming_Auto
  imports
    Renaming
    ZF.Finite
    ZF.List
keywords
  "rename" :: thy_decl % "ML"
and
  "simple_rename" :: thy_decl % "ML"
and
  "src"
and
  "tgt"
abbrevs
  "simple_rename" = ""

begin

lemmas app_fun = apply_iff[THEN iffD1]
lemmas nat_succI = nat_succ_iff[THEN iffD2]
ML_file‹Utils.ml›
ML_file‹Renaming_ML.ml›
ML‹
  open Renaming_ML

  fun renaming_def mk_ren name from to ctxt =
    let val to = to |> Syntax.read_term ctxt
        val from = from |> Syntax.read_term ctxt
        val (tc_lemma,action_lemma,fvs,r) = mk_ren from to ctxt
        val (tc_lemma,action_lemma) = (fix_vars tc_lemma fvs ctxt , fix_vars action_lemma fvs ctxt)
        val ren_fun_name = Binding.name (name ^ "_fn")
        val ren_fun_def =  Binding.name (name ^ "_fn_def")
        val ren_thm = Binding.name (name ^ "_thm")
    in
      Local_Theory.note   ((ren_thm, []), [tc_lemma,action_lemma]) ctxt |> snd |>
      Local_Theory.define ((ren_fun_name, NoSyn), ((ren_fun_def, []), r)) |> snd      
  end;
›

ML‹
local

  val ren_parser = Parse.position (Parse.string --
      (Parse.$$$ "src" |-- Parse.string --| Parse.$$$ "tgt" -- Parse.string));

  val _ =
   Outer_Syntax.local_theory \<^command_keyword>‹rename› "ML setup for synthetic definitions"
     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def sum_rename name from to ))

  val _ =
   Outer_Syntax.local_theory \<^command_keyword>‹simple_rename› "ML setup for synthetic definitions"
     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def ren_thm name from to ))

in
end
›
end