theory simproc_test imports Main 
keywords "mydef":: thy_decl
begin


definition "MyDef a \<equiv> 1 + a"

ML{*


fun mydef_cterm_simproc ctxt cterm = 
  let
    val _ = writeln ("simproc");
    val th = @{thm MyDef_def};
  in
    SOME th
  end;
*}

ML{*
  val ctxt = @{context};

fun mydef_make_simproc ctxt =
    Simplifier.make_simproc ctxt "MyDef" {lhss = [@{term "(MyDef x)"}], proc = fn _ => (fn _ => mydef_cterm_simproc ctxt), identifier = []}
*}

ML{*
  val ctxt = @{context} addsimprocs [mydef_make_simproc @{context}];
  val T = Simplifier.rewrite ctxt @{cterm "id (MyDef (id 5))"};
*}

ML{*

fun simulink_definition_only_aux prep (raw_var, raw_spec) int lthy =
  let
    val ((vars, [((raw_name, atts), prop)]), get_pos) = fst (prep (the_list raw_var) [raw_spec] lthy);
    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
    val var as (b, _) = (Binding.make (x, get_pos x), NoSyn)
    val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
    val const_name = b;
    val ((lhs, (_, raw_th)), lthy2) = lthy
      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));

    val th = prove lthy2 raw_th;
    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);

    val ([(def_name, [th'])], lthy4) = lthy3
      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
  in 
    (lthy4, th, th', lhs, prop, def_name, const_name)
  end;

  fun simulink_definition_only raw_spec (int:bool) lthy = simulink_definition_only_aux Specification.read_free_spec (NONE, raw_spec) int lthy;
*}

lemma eq_equiv_tran_a: "a = b \<Longrightarrow> b \<equiv> c \<Longrightarrow> a = c"
  by simp

ML{*
fun mydef_gen_def (raw_spec) int lthy =
  let
    val (lthy', th, th', lhs, prop, def_name, const_name) = simulink_definition_only (raw_spec) int lthy;

    val lthy_simp = lthy' addsimprocs [mydef_make_simproc lthy'];

    val gen_simp_term =  Thm.dest_arg (Thm.dest_arg (Thm.cprop_of th'))

    val gen_simp_th = Simplifier.rewrite lthy_simp gen_simp_term

    val spec_simp_th = @{thm eq_equiv_tran_a} OF [th, gen_simp_th]
    val vars = Variable.add_free_names lthy' (Thm.prop_of spec_simp_th) [];
    val spec_simp_th' = Thm.generalize ([], vars) ((Thm.maxidx_of spec_simp_th) + 1) spec_simp_th

    val name_sc_c = (Binding.name ((Binding.name_of const_name) ^ "_simp"));
    val ([(_, [_])], lthy_out) = lthy' |> Local_Theory.notes [((name_sc_c, []), [([spec_simp_th'], [])])];


  in ((lhs, (def_name, th')), lthy_out) end;

*}


ML{*
  val parse_mydef = (Parse_Spec.opt_thm_name ":" -- Parse.prop);
  val _ =
    Outer_Syntax.local_theory' @{command_keyword mydef} "mydef definition"
      (parse_mydef >> (fn args => snd oo mydef_gen_def args));
*}


  mydef "tt = id (MyDef (id 5))"

  thm tt_simp

end