|
1 theory Thm_inst |
|
2 imports Term_pat |
|
3 begin |
|
4 |
|
5 section {* Monad for theorem instantiation based on bindings in proof contexts *} |
|
6 |
|
7 subsection {* Implementation *} |
|
8 |
|
9 ML {* |
|
10 local |
|
11 fun read_termTs ctxt schematic ts Ts = |
|
12 let |
|
13 val ts' = |
|
14 map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts |
|
15 |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt) |
|
16 |> Variable.polymorphic ctxt; |
|
17 val Ts' = map Term.fastype_of ts'; |
|
18 val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty; |
|
19 in (ts', map (apsnd snd) (Vartab.dest tyenv)) end; |
|
20 |
|
21 fun make_inst f v = |
|
22 let |
|
23 val t = Var v; |
|
24 val t' = f t; |
|
25 in if t aconv t' then NONE else SOME (t, t') end; |
|
26 |
|
27 |
|
28 fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi)); |
|
29 |
|
30 fun the_type vars (xi: indexname) = |
|
31 (case AList.lookup (op =) vars xi of |
|
32 SOME T => T |
|
33 | NONE => error_var "No such variable in theorem: " xi); |
|
34 |
|
35 fun instantiate inst = |
|
36 Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #> |
|
37 Envir.beta_norm; |
|
38 |
|
39 fun make_instT f v = |
|
40 let |
|
41 val T = TVar v; |
|
42 val T' = f T; |
|
43 in if T = T' then NONE else SOME (T, T') end; |
|
44 |
|
45 fun read_insts ctxt term_insts (tvars, vars) = |
|
46 let |
|
47 val thy = Proof_Context.theory_of ctxt; |
|
48 val cert = Thm.cterm_of thy; |
|
49 val certT = Thm.ctyp_of thy; |
|
50 |
|
51 |
|
52 (* type instantiations *) |
|
53 |
|
54 val instT1 = Term_Subst.instantiateT []; |
|
55 val vars1 = map (apsnd instT1) vars; |
|
56 |
|
57 |
|
58 (* term instantiations *) |
|
59 |
|
60 val (xs, ts) = split_list term_insts; |
|
61 val Ts = map (the_type vars1) xs; |
|
62 val (ts, inferred) = read_termTs ctxt false ts Ts; |
|
63 |
|
64 val instT2 = Term.typ_subst_TVars inferred; |
|
65 val vars2 = map (apsnd instT2) vars1; |
|
66 val inst2 = instantiate (xs ~~ ts); |
|
67 |
|
68 |
|
69 (* result *) |
|
70 |
|
71 val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; |
|
72 val inst_vars = map_filter (make_inst inst2) vars2; |
|
73 in |
|
74 (map (pairself certT) inst_tvars, map (pairself cert) inst_vars) |
|
75 end |
|
76 |
|
77 val add_used = |
|
78 (Thm.fold_terms o fold_types o fold_atyps) |
|
79 (fn TFree (a, _) => insert (op =) a |
|
80 | TVar ((a, _), _) => insert (op =) a |
|
81 | _ => I) |
|
82 |
|
83 fun term_instantiate ctxt term_insts thm = |
|
84 let |
|
85 val ctxt' = ctxt |
|
86 |> Variable.declare_thm thm |
|
87 |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); |
|
88 (* FIXME !? *) |
|
89 val tvars = Thm.fold_terms Term.add_tvars thm []; |
|
90 val vars = Thm.fold_terms Term.add_vars thm []; |
|
91 val insts = read_insts ctxt' term_insts (tvars, vars); |
|
92 in |
|
93 Drule.instantiate_normalize insts thm |
|
94 |> Rule_Cases.save thm |
|
95 end |
|
96 |
|
97 in |
|
98 fun ctxt_instantiate ctxt thm = let |
|
99 val binds = Variable.binds_of ctxt |
|
100 val vars = Thm.fold_terms Term.add_vars thm [] |> map fst |
|
101 val inst = map_filter ( Vartab.lookup_key binds) vars |> map (apsnd snd) |
|
102 val thm' = term_instantiate ctxt inst thm |
|
103 in thm' end |
|
104 |
|
105 fun thm_instM thm = |
|
106 liftM (lift (m0M (fn ctxt => |
|
107 returnM (ctxt_instantiate ctxt thm) |
|
108 )) |> exnM err_trans) |
|
109 |
|
110 end |
|
111 *} |
|
112 |
|
113 subsection {* Examples *} |
|
114 |
|
115 lemma h: "x = x \<and> y = y" |
|
116 by simp |
|
117 |
|
118 ML {* |
|
119 val ctxt = @{context} |
|
120 val t = ctxt_instantiate ctxt @{thm h} |> prop_of |
|
121 *} |
|
122 |
|
123 ML {* |
|
124 val t = [((), @{context})] |> @{match "?x"} @{term "[]::nat list"} |-- |
|
125 @{match "?y"} @{term "1::nat"} |-- |
|
126 thm_instM @{thm h} |
|
127 *} |
|
128 |
|
129 end |
|
130 |