author | wenzelm |
Sat, 28 Mar 2009 17:53:33 +0100 | |
changeset 30763 | 6976521b4263 |
parent 30757 | 2d2076300185 |
child 31794 | 71af1fd6a5e4 |
permissions | -rw-r--r-- |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/obtain.ML |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
3 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
4 |
The 'obtain' and 'guess' language elements -- generalized existence at |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
5 |
the level of proof texts: 'obtain' involves a proof that certain |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
6 |
fixes/assumes may be introduced into the present context; 'guess' is |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
7 |
similar, but derives these elements from the course of reasoning! |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
8 |
|
9468 | 9 |
<chain_facts> |
18870 | 10 |
obtain x where "A x" <proof> == |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
11 |
|
18870 | 12 |
have "!!thesis. (!!x. A x ==> thesis) ==> thesis" |
12970 | 13 |
proof succeed |
9468 | 14 |
fix thesis |
18870 | 15 |
assume that [intro?]: "!!x. A x ==> thesis" |
16 |
<chain_facts> |
|
17 |
show thesis |
|
18 |
apply (insert that) |
|
19 |
<proof> |
|
12970 | 20 |
qed |
18870 | 21 |
fix x assm <<obtain_export>> "A x" |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
22 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
23 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
24 |
<chain_facts> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
25 |
guess x <proof body> <proof end> == |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
26 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
27 |
{ |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
28 |
fix thesis |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
29 |
<chain_facts> have "PROP ?guess" |
18870 | 30 |
apply magic -- {* turns goal into "thesis ==> #thesis" *} |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
31 |
<proof body> |
18870 | 32 |
apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into |
33 |
"#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
34 |
<proof end> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
35 |
} |
18870 | 36 |
fix x assm <<obtain_export>> "A x" |
8094 | 37 |
*) |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
38 |
|
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
39 |
signature OBTAIN = |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
40 |
sig |
21229 | 41 |
val thatN: string |
29581 | 42 |
val obtain: string -> (binding * string option * mixfix) list -> |
30211 | 43 |
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state |
29581 | 44 |
val obtain_i: string -> (binding * typ option * mixfix) list -> |
30211 | 45 |
(Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state |
20308 | 46 |
val result: (Proof.context -> tactic) -> thm list -> Proof.context -> |
47 |
(cterm list * thm list) * Proof.context |
|
29581 | 48 |
val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
49 |
val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
50 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
51 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
52 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
53 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
54 |
|
18670 | 55 |
(** obtain_export **) |
56 |
||
18870 | 57 |
(* |
18897 | 58 |
[x, A x] |
59 |
: |
|
60 |
B |
|
61 |
-------- |
|
62 |
B |
|
18870 | 63 |
*) |
21686 | 64 |
fun eliminate_term ctxt xs tm = |
65 |
let |
|
66 |
val vs = map (dest_Free o Thm.term_of) xs; |
|
67 |
val bads = Term.fold_aterms (fn t as Free v => |
|
68 |
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm []; |
|
69 |
val _ = null bads orelse |
|
70 |
error ("Result contains obtained parameters: " ^ |
|
24920 | 71 |
space_implode " " (map (Syntax.string_of_term ctxt) bads)); |
21686 | 72 |
in tm end; |
73 |
||
74 |
fun eliminate fix_ctxt rule xs As thm = |
|
9468 | 75 |
let |
20308 | 76 |
val thy = ProofContext.theory_of fix_ctxt; |
9468 | 77 |
|
21686 | 78 |
val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm); |
20308 | 79 |
val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse |
80 |
error "Conclusion in obtained context must be object-logic judgment"; |
|
81 |
||
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21686
diff
changeset
|
82 |
val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt; |
20308 | 83 |
val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm')); |
9468 | 84 |
in |
20308 | 85 |
((Drule.implies_elim_list thm' (map Thm.assume prems) |
86 |
|> Drule.implies_intr_list (map Drule.norm_hhf_cterm As) |
|
87 |
|> Drule.forall_intr_list xs) |
|
88 |
COMP rule) |
|
89 |
|> Drule.implies_intr_list prems |
|
90 |
|> singleton (Variable.export ctxt' fix_ctxt) |
|
9468 | 91 |
end; |
92 |
||
21686 | 93 |
fun obtain_export ctxt rule xs _ As = |
94 |
(eliminate ctxt rule xs As, eliminate_term ctxt xs); |
|
95 |
||
9468 | 96 |
|
97 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
98 |
(** obtain **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
99 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
100 |
fun bind_judgment ctxt name = |
18670 | 101 |
let |
20308 | 102 |
val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt; |
18670 | 103 |
val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name); |
20308 | 104 |
in ((v, t), ctxt') end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
105 |
|
18897 | 106 |
val thatN = "that"; |
107 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
108 |
local |
8094 | 109 |
|
18897 | 110 |
fun gen_obtain prep_att prep_vars prep_propp |
111 |
name raw_vars raw_asms int state = |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
112 |
let |
9468 | 113 |
val _ = Proof.assert_forward_or_chain state; |
20308 | 114 |
val thy = Proof.theory_of state; |
115 |
val cert = Thm.cterm_of thy; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
116 |
val ctxt = Proof.context_of state; |
17357 | 117 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
118 |
|
8543 | 119 |
(*obtain vars*) |
19844 | 120 |
val (vars, vars_ctxt) = prep_vars raw_vars ctxt; |
30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30757
diff
changeset
|
121 |
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars; |
30585
6b2ba4666336
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
wenzelm
parents:
30242
diff
changeset
|
122 |
val xs = map (Name.of_binding o #1) vars; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
123 |
|
8543 | 124 |
(*obtain asms*) |
11890 | 125 |
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19300
diff
changeset
|
126 |
val asm_props = maps (map fst) proppss; |
18678 | 127 |
val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; |
10464 | 128 |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
129 |
val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
130 |
|
12970 | 131 |
(*obtain statements*) |
20085
c5d60752587f
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20004
diff
changeset
|
132 |
val thesisN = Name.variant xs AutoBind.thesisN; |
20308 | 133 |
val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN); |
9468 | 134 |
|
20308 | 135 |
val asm_frees = fold Term.add_frees asm_props []; |
136 |
val parms = xs |> map (fn x => |
|
137 |
let val x' = ProofContext.get_skolem fix_ctxt x |
|
138 |
in (x', the_default propT (AList.lookup (op =) asm_frees x')) end); |
|
10582 | 139 |
|
18897 | 140 |
val that_name = if name = "" then thatN else name; |
10582 | 141 |
val that_prop = |
20308 | 142 |
Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)) |
143 |
|> Library.curry Logic.list_rename_params xs; |
|
12970 | 144 |
val obtain_prop = |
145 |
Logic.list_rename_params ([AutoBind.thesisN], |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
146 |
Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
147 |
|
18124 | 148 |
fun after_qed _ = |
17357 | 149 |
Proof.local_qed (NONE, false) |
29383 | 150 |
#> `Proof.the_fact #-> (fn rule => |
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
151 |
Proof.fix_i vars |
29383 | 152 |
#> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
153 |
in |
8094 | 154 |
state |
9468 | 155 |
|> Proof.enter_forward |
30211 | 156 |
|> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
157 |
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
28965 | 158 |
|> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)] |
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
159 |
|> Proof.assume_i |
28965 | 160 |
[((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] |
16842 | 161 |
|> `Proof.the_facts |
17357 | 162 |
||> Proof.chain_facts chain_facts |
30211 | 163 |
||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false |
18907 | 164 |
|-> Proof.refine_insert |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
165 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
166 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
167 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
168 |
|
18728 | 169 |
val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp; |
17111 | 170 |
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; |
8094 | 171 |
|
172 |
end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
173 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
174 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
175 |
|
20308 | 176 |
(** tactical result **) |
177 |
||
178 |
fun check_result ctxt thesis th = |
|
179 |
(case Thm.prems_of th of |
|
180 |
[prem] => |
|
181 |
if Thm.concl_of th aconv thesis andalso |
|
182 |
Logic.strip_assums_concl prem aconv thesis then th |
|
183 |
else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th) |
|
184 |
| [] => error "Goal solved -- nothing guessed." |
|
185 |
| _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th)); |
|
186 |
||
187 |
fun result tac facts ctxt = |
|
188 |
let |
|
189 |
val thy = ProofContext.theory_of ctxt; |
|
190 |
val cert = Thm.cterm_of thy; |
|
191 |
||
192 |
val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt AutoBind.thesisN; |
|
193 |
val rule = |
|
194 |
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of |
|
195 |
NONE => raise THM ("Obtain.result: tactic failed", 0, facts) |
|
21605 | 196 |
| SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th))); |
20308 | 197 |
|
198 |
val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; |
|
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21686
diff
changeset
|
199 |
val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt; |
20308 | 200 |
val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; |
201 |
val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt'; |
|
202 |
val (prems, ctxt'') = |
|
203 |
Assumption.add_assms (obtain_export fix_ctxt obtain_rule params) |
|
204 |
(Drule.strip_imp_prems stmt) fix_ctxt; |
|
205 |
in ((params, prems), ctxt'') end; |
|
206 |
||
207 |
||
208 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
209 |
(** guess **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
210 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
211 |
local |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
212 |
|
20308 | 213 |
fun unify_params vars thesis_var raw_rule ctxt = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
214 |
let |
18678 | 215 |
val thy = ProofContext.theory_of ctxt; |
19978 | 216 |
val certT = Thm.ctyp_of thy; |
217 |
val cert = Thm.cterm_of thy; |
|
24920 | 218 |
val string_of_typ = Syntax.string_of_typ ctxt; |
219 |
val string_of_term = setmp show_types true (Syntax.string_of_term ctxt); |
|
17891 | 220 |
|
18678 | 221 |
fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
222 |
|
19978 | 223 |
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
19779 | 224 |
val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
225 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
226 |
val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
227 |
val m = length vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
228 |
val n = length params; |
19779 | 229 |
val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
230 |
|
19779 | 231 |
fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
232 |
handle Type.TUNIFY => |
|
233 |
err ("Failed to unify variable " ^ |
|
234 |
string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ |
|
235 |
string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; |
|
19978 | 236 |
val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params)) |
19779 | 237 |
(Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
238 |
val norm_type = Envir.norm_type tyenv; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
239 |
|
19978 | 240 |
val xs = map (apsnd norm_type o fst) vars; |
19779 | 241 |
val ys = map (apsnd norm_type) (Library.drop (m, params)); |
20085
c5d60752587f
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20004
diff
changeset
|
242 |
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; |
19978 | 243 |
val terms = map (Drule.mk_term o cert o Free) (xs @ ys'); |
19779 | 244 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
245 |
val instT = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
246 |
fold (Term.add_tvarsT o #2) params [] |
19978 | 247 |
|> map (TVar #> (fn T => (certT T, certT (norm_type T)))); |
20308 | 248 |
val closed_rule = rule |
249 |
|> Thm.forall_intr (cert (Free thesis_var)) |
|
250 |
|> Thm.instantiate (instT, []); |
|
17891 | 251 |
|
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21686
diff
changeset
|
252 |
val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt; |
19978 | 253 |
val vars' = |
254 |
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ |
|
255 |
(map snd vars @ replicate (length ys) NoSyn); |
|
20308 | 256 |
val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; |
19978 | 257 |
in ((vars', rule''), ctxt') end; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
258 |
|
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
259 |
fun inferred_type (binding, _, mx) ctxt = |
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
260 |
let |
30585
6b2ba4666336
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
wenzelm
parents:
30242
diff
changeset
|
261 |
val x = Name.of_binding binding; |
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
262 |
val (T, ctxt') = ProofContext.inferred_param x ctxt |
19779 | 263 |
in ((x, T, mx), ctxt') end; |
264 |
||
20004
e6d3f2b031e6
guess: proper context for polymorphic parameters;
wenzelm
parents:
19978
diff
changeset
|
265 |
fun polymorphic ctxt vars = |
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19844
diff
changeset
|
266 |
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
19779 | 267 |
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; |
18693 | 268 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
269 |
fun gen_guess prep_vars raw_vars int state = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
270 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
271 |
val _ = Proof.assert_forward_or_chain state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
272 |
val thy = Proof.theory_of state; |
20308 | 273 |
val cert = Thm.cterm_of thy; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
274 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
275 |
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
276 |
|
20308 | 277 |
val (thesis_var, thesis) = #1 (bind_judgment ctxt AutoBind.thesisN); |
20004
e6d3f2b031e6
guess: proper context for polymorphic parameters;
wenzelm
parents:
19978
diff
changeset
|
278 |
val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
279 |
|
19978 | 280 |
fun guess_context raw_rule state' = |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
281 |
let |
19978 | 282 |
val ((parms, rule), ctxt') = |
20308 | 283 |
unify_params vars thesis_var raw_rule (Proof.context_of state'); |
19978 | 284 |
val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt'; |
285 |
val ts = map (bind o Free o #1) parms; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
286 |
val ps = map dest_Free ts; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
287 |
val asms = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
288 |
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |
19585 | 289 |
|> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), [])); |
19779 | 290 |
val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
291 |
in |
19978 | 292 |
state' |
293 |
|> Proof.map_context (K ctxt') |
|
28965 | 294 |
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |
28080
4723eb2456ce
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
24920
diff
changeset
|
295 |
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i |
30211 | 296 |
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)]) |
30757
2d2076300185
replaced add_binds(_i) by bind_terms -- internal version only;
wenzelm
parents:
30585
diff
changeset
|
297 |
|> Proof.bind_terms AutoBind.no_facts |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
298 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
299 |
|
19779 | 300 |
val goal = Var (("guess", 0), propT); |
301 |
fun print_result ctxt' (k, [(s, [_, th])]) = |
|
302 |
ProofDisplay.print_results int ctxt' (k, [(s, [th])]); |
|
21605 | 303 |
val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #> |
20308 | 304 |
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); |
19779 | 305 |
fun after_qed [[_, res]] = |
29383 | 306 |
Proof.end_block #> guess_context (check_result ctxt thesis res); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
307 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
308 |
state |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
309 |
|> Proof.enter_forward |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
310 |
|> Proof.begin_block |
28965 | 311 |
|> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)] |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
312 |
|> Proof.chain_facts chain_facts |
19779 | 313 |
|> Proof.local_goal print_result (K I) (apsnd (rpair I)) |
30211 | 314 |
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])] |
20308 | 315 |
|> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
316 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
317 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
318 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
319 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
320 |
val guess = gen_guess ProofContext.read_vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
321 |
val guess_i = gen_guess ProofContext.cert_vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
322 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
323 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
324 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
325 |
end; |