author | wenzelm |
Fri, 28 Oct 2005 22:28:12 +0200 | |
changeset 18040 | c67505cdecad |
parent 17974 | 5b54db4a44ee |
child 18124 | a310c78298f9 |
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 |
ID: $Id$ |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
4 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
5 |
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
|
6 |
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
|
7 |
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
|
8 |
similar, but derives these elements from the course of reasoning! |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
9 |
|
9468 | 10 |
<chain_facts> |
11 |
obtain x where "P x" <proof> == |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
12 |
|
12970 | 13 |
have "!!thesis. (!!x. P x ==> thesis) ==> thesis" |
14 |
proof succeed |
|
9468 | 15 |
fix thesis |
12970 | 16 |
assume that [intro?]: "!!x. P x ==> thesis" |
17 |
<chain_facts> show thesis <proof (insert that)> |
|
18 |
qed |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
19 |
fix x assm (obtained) "P x" |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
20 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
21 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
22 |
<chain_facts> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
23 |
guess x <proof body> <proof end> == |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
24 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
25 |
{ |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
26 |
fix thesis |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
27 |
<chain_facts> have "PROP ?guess" |
17974 | 28 |
apply magic -- {* turns goal into "thesis ==> Goal thesis" *} |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
29 |
<proof body> |
17974 | 30 |
apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> Goal thesis" into |
31 |
"Goal ((!!x. P 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
|
32 |
<proof end> |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
33 |
} |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
34 |
fix x assm (obtained) "P x" |
8094 | 35 |
*) |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
36 |
|
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
37 |
signature OBTAIN = |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
38 |
sig |
11890 | 39 |
val obtain: (string list * string option) list -> |
17111 | 40 |
((string * Attrib.src list) * (string * (string list * string list)) list) list |
17357 | 41 |
-> bool -> Proof.state -> Proof.state |
11890 | 42 |
val obtain_i: (string list * typ option) list -> |
43 |
((string * Proof.context attribute list) * (term * (term list * term list)) list) list |
|
17357 | 44 |
-> bool -> Proof.state -> Proof.state |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
45 |
val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state Seq.seq |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
46 |
val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
47 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
48 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
49 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
50 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
51 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
52 |
(** export_obtained **) |
8094 | 53 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
54 |
fun export_obtained state parms rule cprops thm = |
9468 | 55 |
let |
17111 | 56 |
val {thy, prop, maxidx, ...} = Thm.rep_thm thm; |
57 |
val cparms = map (Thm.cterm_of thy) parms; |
|
9468 | 58 |
|
59 |
val thm' = thm |
|
18040
c67505cdecad
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17974
diff
changeset
|
60 |
|> Drule.implies_intr_protected cprops |
9468 | 61 |
|> Drule.forall_intr_list cparms |
62 |
|> Drule.forall_elim_vars (maxidx + 1); |
|
18040
c67505cdecad
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17974
diff
changeset
|
63 |
val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI); |
9468 | 64 |
|
65 |
val concl = Logic.strip_assums_concl prop; |
|
66 |
val bads = parms inter (Term.term_frees concl); |
|
67 |
in |
|
68 |
if not (null bads) then |
|
9481 | 69 |
raise Proof.STATE ("Conclusion contains obtained parameters: " ^ |
12055 | 70 |
space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
71 |
else if not (ObjectLogic.is_judgment thy concl) then |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
72 |
raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state) |
9468 | 73 |
else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule |
74 |
end; |
|
75 |
||
76 |
||
77 |
||
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
78 |
(** obtain **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
79 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
80 |
fun bind_judgment ctxt name = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
81 |
let val (t as _ $ Free v) = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
82 |
ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
83 |
|> ProofContext.bind_skolem ctxt [name] |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
84 |
in (v, t) end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
85 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
86 |
local |
8094 | 87 |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
88 |
val thatN = "that"; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
89 |
|
17357 | 90 |
fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
91 |
let |
9468 | 92 |
val _ = Proof.assert_forward_or_chain state; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
93 |
val ctxt = Proof.context_of state; |
17357 | 94 |
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
|
95 |
|
8543 | 96 |
(*obtain vars*) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
97 |
val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
98 |
val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars; |
15570 | 99 |
val xs = List.concat (map fst vars); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
100 |
|
8543 | 101 |
(*obtain asms*) |
11890 | 102 |
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
15570 | 103 |
val asm_props = List.concat (map (map fst) proppss); |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
104 |
val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss; |
10464 | 105 |
|
10582 | 106 |
val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
107 |
|
12970 | 108 |
(*obtain statements*) |
16606 | 109 |
val thesisN = Term.variant xs AutoBind.thesisN; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
110 |
val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN; |
9468 | 111 |
|
10582 | 112 |
fun occs_var x = Library.get_first (fn t => |
113 |
ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; |
|
114 |
val raw_parms = map occs_var xs; |
|
15570 | 115 |
val parms = List.mapPartial I raw_parms; |
10582 | 116 |
val parm_names = |
15570 | 117 |
List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs); |
10582 | 118 |
|
119 |
val that_prop = |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
120 |
Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis)) |
10582 | 121 |
|> Library.curry Logic.list_rename_params (map #2 parm_names); |
12970 | 122 |
val obtain_prop = |
123 |
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
|
124 |
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
|
125 |
|
17357 | 126 |
fun after_qed _ _ = |
127 |
Proof.local_qed (NONE, false) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
128 |
#> Seq.map (`Proof.the_fact #-> (fn rule => |
17357 | 129 |
Proof.fix_i vars |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
130 |
#> Proof.assm_i (K (export_obtained state parms rule)) asms)); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
131 |
in |
8094 | 132 |
state |
9468 | 133 |
|> Proof.enter_forward |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
134 |
|> Proof.have_i NONE (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
135 |
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd |
15531 | 136 |
|> Proof.fix_i [([thesisN], NONE)] |
137 |
|> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])] |
|
16842 | 138 |
|> `Proof.the_facts |
17357 | 139 |
||> Proof.chain_facts chain_facts |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
140 |
||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false |
17357 | 141 |
|-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
142 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
143 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
144 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
145 |
|
17111 | 146 |
val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp; |
147 |
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; |
|
8094 | 148 |
|
149 |
end; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
150 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
151 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
152 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
153 |
(** guess **) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
154 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
155 |
local |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
156 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
157 |
fun match_params state vars rule = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
158 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
159 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
160 |
val thy = Proof.theory_of state; |
17891 | 161 |
val string_of_typ = ProofContext.string_of_typ ctxt; |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
162 |
val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt); |
17891 | 163 |
|
164 |
fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state); |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
165 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
166 |
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
|
167 |
val m = length vars; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
168 |
val n = length params; |
17891 | 169 |
val _ = conditional (m > n) |
170 |
(fn () => 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
|
171 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
172 |
fun match ((x, SOME T), (y, U)) tyenv = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
173 |
((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH => |
17891 | 174 |
err ("Failed to match variable " ^ |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
175 |
string_of_term (Free (x, T)) ^ " against parameter " ^ |
17891 | 176 |
string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
177 |
| match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
178 |
val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
179 |
val ys = Library.drop (m, params); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
180 |
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
|
181 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
182 |
val xs' = xs |> map (apsnd norm_type); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
183 |
val ys' = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
184 |
map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~ |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
185 |
map (norm_type o snd) ys; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
186 |
val instT = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
187 |
fold (Term.add_tvarsT o #2) params [] |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
188 |
|> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T)))); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
189 |
val rule' = rule |> Thm.instantiate (instT, []); |
17891 | 190 |
|
191 |
val tvars = Drule.tvars_of rule'; |
|
192 |
val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule'); |
|
193 |
val _ = |
|
194 |
if null tvars andalso null vars then () |
|
195 |
else err ("Illegal schematic variable(s) " ^ |
|
196 |
commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule'; |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
197 |
in (xs' @ ys', rule') end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
198 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
199 |
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
|
200 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
201 |
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
|
202 |
val thy = Proof.theory_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
203 |
val ctxt = Proof.context_of state; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
204 |
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
|
205 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
206 |
val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
207 |
val varss = #1 (fold_map prep_vars raw_vars ctxt); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
208 |
val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss); |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
209 |
|
17974 | 210 |
fun check_result th = |
211 |
(case Thm.prems_of th of |
|
212 |
[prem] => |
|
213 |
if Thm.concl_of th aconv thesis andalso |
|
214 |
Logic.strip_assums_concl prem aconv thesis then () |
|
215 |
else raise Proof.STATE ("Guessed a different clause:\n" ^ |
|
216 |
ProofContext.string_of_thm ctxt th, state) |
|
217 |
| [] => raise Proof.STATE ("Goal solved -- nothing guessed.", state) |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
218 |
| _ => raise Proof.STATE ("Guess split into several cases:\n" ^ |
17974 | 219 |
ProofContext.string_of_thm ctxt th, state)); |
17891 | 220 |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
221 |
fun guess_context raw_rule = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
222 |
let |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
223 |
val (parms, rule) = match_params state vars raw_rule; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
224 |
val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
225 |
val ps = map dest_Free ts; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
226 |
val asms = |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
227 |
Logic.strip_assums_hyp (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
|
228 |
|> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], []))); |
17974 | 229 |
val _ = conditional (null asms) (fn () => |
230 |
raise Proof.STATE ("Trivial result -- nothing guessed", state)); |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
231 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
232 |
Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
233 |
#> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)] |
17974 | 234 |
#> Proof.add_binds_i AutoBind.no_facts |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
235 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
236 |
|
18040
c67505cdecad
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17974
diff
changeset
|
237 |
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect)); |
17974 | 238 |
fun after_qed _ [[res]] = |
239 |
(check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context)); |
|
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
240 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
241 |
state |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
242 |
|> Proof.enter_forward |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
243 |
|> Proof.begin_block |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
244 |
|> Proof.fix_i [([AutoBind.thesisN], NONE)] |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
245 |
|> Proof.chain_facts chain_facts |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
246 |
|> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I)) |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
247 |
"guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])] |
17974 | 248 |
|> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |
17858
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
249 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
250 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
251 |
in |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
252 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
253 |
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
|
254 |
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
|
255 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
256 |
end; |
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
257 |
|
bc4db8cfd92f
added 'guess', which derives the obtained context from the course of reasoning;
wenzelm
parents:
17357
diff
changeset
|
258 |
end; |