theory Thm_inst

imports Term_pat

begin

section {* Monad for theorem instantiation based on bindings in proof contexts *}

subsection {* Implementation *}

ML {*

local

fun read_termTs ctxt schematic ts Ts =

  let

    val ts' =

      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts

      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)

      |> Variable.polymorphic ctxt;

    val Ts' = map Term.fastype_of ts';

    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;

  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;

fun make_inst f v =

  let

    val t = Var v;

    val t' = f t;

  in if t aconv t' then NONE else SOME (t, t') end;

fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));

fun the_type vars (xi: indexname) =

  (case AList.lookup (op =) vars xi of

    SOME T => T

  | NONE => error_var "No such variable in theorem: " xi);

fun instantiate inst =

  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>

  Envir.beta_norm;

fun make_instT f v =

  let

    val T = TVar v;

    val T' = f T;

  in if T = T' then NONE else SOME (T, T') end;

fun read_insts ctxt term_insts (tvars, vars) =

  let

    val thy = Proof_Context.theory_of ctxt;

    val cert = Thm.cterm_of thy;

    val certT = Thm.ctyp_of thy;

    (* type instantiations *)

    val instT1 = Term_Subst.instantiateT [];

    val vars1 = map (apsnd instT1) vars;

    (* term instantiations *)

    val (xs, ts) = split_list term_insts;

    val Ts = map (the_type vars1) xs;

    val (ts, inferred) = read_termTs ctxt false ts Ts;

    val instT2 = Term.typ_subst_TVars inferred;

    val vars2 = map (apsnd instT2) vars1;

    val inst2 = instantiate (xs ~~ ts);

    (* result *)

    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;

    val inst_vars = map_filter (make_inst inst2) vars2;

  in

    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)

  end

  val add_used =

  (Thm.fold_terms o fold_types o fold_atyps)

    (fn TFree (a, _) => insert (op =) a

      | TVar ((a, _), _) => insert (op =) a

      | _ => I)

fun term_instantiate ctxt term_insts thm =

  let

    val ctxt' = ctxt

      |> Variable.declare_thm thm

      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); 

                 (* FIXME !? *)

    val tvars = Thm.fold_terms Term.add_tvars thm [];

    val vars = Thm.fold_terms Term.add_vars thm [];

    val insts = read_insts ctxt' term_insts (tvars, vars);

  in

    Drule.instantiate_normalize insts thm

    |> Rule_Cases.save thm

  end

in

  fun ctxt_instantiate ctxt thm = let

     val binds = Variable.binds_of ctxt

     val vars = Thm.fold_terms Term.add_vars thm [] |> map fst

     val inst = map_filter ( Vartab.lookup_key binds) vars |> map (apsnd snd)

     val thm' = term_instantiate ctxt inst thm 

  in thm' end

  fun thm_instM thm = 

   liftM (lift (m0M (fn ctxt =>

    returnM (ctxt_instantiate ctxt thm)

   )) |> exnM err_trans)

end

*}

subsection {* Examples *}

lemma h: "x = x \<and> y = y"

  by simp

ML {*

  val ctxt = @{context}

  val t = ctxt_instantiate ctxt @{thm h} |> prop_of

*}

ML {*

  val t =   [((), @{context})] |> @{match "?x"} @{term "[]::nat list"} |--

                                  @{match "?y"} @{term "1::nat"} |--

                                  thm_instM @{thm h}

*}

end