--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Thm_inst.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,130 @@
+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
+