author | wenzelm |
Wed, 04 Apr 2007 00:11:03 +0200 | |
changeset 22578 | b0eb5652f210 |
parent 20548 | 8ef25fe585a8 |
permissions | -rw-r--r-- |
19835 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
2 |
(* Title: Pure/IsaPlanner/isand.ML |
|
3 |
ID: $Id$ |
|
4 |
Author: Lucas Dixon, University of Edinburgh |
|
5 |
lucas.dixon@ed.ac.uk |
|
6 |
Updated: 26 Apr 2005 |
|
7 |
Date: 6 Aug 2004 |
|
8 |
*) |
|
9 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
10 |
(* DESCRIPTION: |
|
11 |
||
12 |
Natural Deduction tools |
|
13 |
||
14 |
For working with Isabelle theorems in a natural detuction style. |
|
15 |
ie, not having to deal with meta level quantified varaibles, |
|
16 |
instead, we work with newly introduced frees, and hide the |
|
17 |
"all"'s, exporting results from theorems proved with the frees, to |
|
18 |
solve the all cases of the previous goal. This allows resolution |
|
19 |
to do proof search normally. |
|
20 |
||
21 |
Note: A nice idea: allow exporting to solve any subgoal, thus |
|
22 |
allowing the interleaving of proof, or provide a structure for the |
|
23 |
ordering of proof, thus allowing proof attempts in parrell, but |
|
24 |
recording the order to apply things in. |
|
25 |
||
26 |
THINK: are we really ok with our varify name w.r.t the prop - do |
|
27 |
we also need to avoid names in the hidden hyps? What about |
|
28 |
unification contraints in flex-flex pairs - might they also have |
|
29 |
extra free vars? |
|
30 |
*) |
|
31 |
||
32 |
signature ISA_ND = |
|
33 |
sig |
|
34 |
||
35 |
(* export data *) |
|
36 |
datatype export = export of |
|
37 |
{gth: Thm.thm, (* initial goal theorem *) |
|
38 |
sgid: int, (* subgoal id which has been fixed etc *) |
|
39 |
fixes: Thm.cterm list, (* frees *) |
|
40 |
assumes: Thm.cterm list} (* assumptions *) |
|
41 |
val fixes_of_exp : export -> Thm.cterm list |
|
42 |
val export_back : export -> Thm.thm -> Thm.thm Seq.seq |
|
43 |
val export_solution : export -> Thm.thm -> Thm.thm |
|
44 |
val export_solutions : export list * Thm.thm -> Thm.thm |
|
45 |
||
46 |
(* inserting meta level params for frees in the conditions *) |
|
47 |
val allify_conditions : |
|
48 |
(Term.term -> Thm.cterm) -> |
|
49 |
(string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list |
|
50 |
val allify_conditions' : |
|
51 |
(string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list |
|
52 |
val assume_allified : |
|
53 |
theory -> (string * Term.sort) list * (string * Term.typ) list |
|
54 |
-> Term.term -> (Thm.cterm * Thm.thm) |
|
55 |
||
56 |
(* meta level fixed params (i.e. !! vars) *) |
|
57 |
val fix_alls_in_term : Term.term -> Term.term * Term.term list |
|
58 |
val fix_alls_term : int -> Term.term -> Term.term * Term.term list |
|
59 |
val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list |
|
60 |
val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list |
|
61 |
val fix_alls : int -> Thm.thm -> Thm.thm * export |
|
62 |
||
63 |
(* meta variables in types and terms *) |
|
64 |
val fix_tvars_to_tfrees_in_terms |
|
65 |
: string list (* avoid these names *) |
|
66 |
-> Term.term list -> |
|
67 |
(((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *) |
|
68 |
val fix_vars_to_frees_in_terms |
|
69 |
: string list (* avoid these names *) |
|
70 |
-> Term.term list -> |
|
71 |
(((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *) |
|
72 |
val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm |
|
73 |
val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm |
|
74 |
val fix_vars_and_tvars : |
|
75 |
Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm |
|
76 |
val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm |
|
77 |
val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm |
|
78 |
val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm |
|
79 |
val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm |
|
80 |
val unfix_frees_and_tfrees : |
|
81 |
(Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm |
|
82 |
||
83 |
(* assumptions/subgoals *) |
|
84 |
val assume_prems : |
|
85 |
int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list |
|
86 |
val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) |
|
87 |
val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export |
|
88 |
val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list |
|
89 |
val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list |
|
90 |
||
91 |
(* abstracts cterms (vars) to locally meta-all bounds *) |
|
92 |
val prepare_goal_export : string list * Thm.cterm list -> Thm.thm |
|
93 |
-> int * Thm.thm |
|
94 |
val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq |
|
95 |
val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) |
|
96 |
end |
|
97 |
||
98 |
||
99 |
structure IsaND |
|
100 |
: ISA_ND |
|
101 |
= struct |
|
102 |
||
103 |
(* Solve *some* subgoal of "th" directly by "sol" *) |
|
104 |
(* Note: this is probably what Markus ment to do upon export of a |
|
105 |
"show" but maybe he used RS/rtac instead, which would wrongly lead to |
|
106 |
failing if there are premices to the shown goal. |
|
107 |
||
108 |
given: |
|
109 |
sol : Thm.thm = [| Ai... |] ==> Ci |
|
110 |
th : Thm.thm = |
|
111 |
[| ... [| Ai... |] ==> Ci ... |] ==> G |
|
112 |
results in: |
|
113 |
[| ... [| Ai-1... |] ==> Ci-1 |
|
114 |
[| Ai+1... |] ==> Ci+1 ... |
|
115 |
|] ==> G |
|
116 |
i.e. solves some subgoal of th that is identical to sol. |
|
117 |
*) |
|
118 |
fun solve_with sol th = |
|
119 |
let fun solvei 0 = Seq.empty |
|
120 |
| solvei i = |
|
19861 | 121 |
Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1)) |
19835 | 122 |
in |
123 |
solvei (Thm.nprems_of th) |
|
124 |
end; |
|
125 |
||
126 |
||
127 |
(* Given ctertmify function, (string,type) pairs capturing the free |
|
128 |
vars that need to be allified in the assumption, and a theorem with |
|
129 |
assumptions possibly containing the free vars, then we give back the |
|
130 |
assumptions allified as hidden hyps. |
|
131 |
||
132 |
Given: x |
|
133 |
th: A vs ==> B vs |
|
134 |
Results in: "B vs" [!!x. A x] |
|
135 |
*) |
|
136 |
fun allify_conditions ctermify Ts th = |
|
137 |
let |
|
138 |
val premts = Thm.prems_of th; |
|
139 |
||
140 |
fun allify_prem_var (vt as (n,ty),t) = |
|
141 |
(Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) |
|
142 |
||
143 |
fun allify_prem Ts p = foldr allify_prem_var p Ts |
|
144 |
||
145 |
val cTs = map (ctermify o Free) Ts |
|
146 |
val cterm_asms = map (ctermify o allify_prem Ts) premts |
|
147 |
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms |
|
148 |
in |
|
149 |
(Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms) |
|
150 |
end; |
|
151 |
||
152 |
fun allify_conditions' Ts th = |
|
22578 | 153 |
allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th; |
19835 | 154 |
|
155 |
(* allify types *) |
|
156 |
fun allify_typ ts ty = |
|
157 |
let |
|
158 |
fun trec (x as (TFree (s,srt))) = |
|
159 |
(case Library.find_first (fn (s2,srt2) => s = s2) ts |
|
160 |
of NONE => x |
|
161 |
| SOME (s2,_) => TVar ((s,0),srt)) |
|
162 |
(* Maybe add in check here for bad sorts? |
|
163 |
if srt = srt2 then TVar ((s,0),srt) |
|
164 |
else raise ("thaw_typ", ts, ty) *) |
|
165 |
| trec (Type (s,typs)) = Type (s, map trec typs) |
|
166 |
| trec (v as TVar _) = v; |
|
167 |
in trec ty end; |
|
168 |
||
169 |
(* implicit types and term *) |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20071
diff
changeset
|
170 |
fun allify_term_typs ty = Term.map_types (allify_typ ty); |
19835 | 171 |
|
172 |
(* allified version of term, given frees to allify over. Note that we |
|
173 |
only allify over the types on the given allified cterm, we can't do |
|
174 |
this for the theorem as we are not allowed type-vars in the hyp. *) |
|
175 |
(* FIXME: make the allified term keep the same conclusion as it |
|
176 |
started with, rather than a strictly more general version (ie use |
|
177 |
instantiate with initial params we abstracted from, rather than |
|
178 |
forall_elim_vars. *) |
|
179 |
fun assume_allified sgn (tyvs,vs) t = |
|
180 |
let |
|
181 |
fun allify_var (vt as (n,ty),t) = |
|
182 |
(Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) |
|
183 |
fun allify Ts p = List.foldr allify_var p Ts |
|
184 |
||
185 |
val ctermify = Thm.cterm_of sgn; |
|
186 |
val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs |
|
187 |
val allified_term = t |> allify vs; |
|
188 |
val ct = ctermify allified_term; |
|
189 |
val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term); |
|
190 |
in (typ_allified_ct, |
|
191 |
Drule.forall_elim_vars 0 (Thm.assume ct)) end; |
|
192 |
||
193 |
||
194 |
(* change type-vars to fresh type frees *) |
|
195 |
fun fix_tvars_to_tfrees_in_terms names ts = |
|
196 |
let |
|
197 |
val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts); |
|
198 |
val tvars = List.foldr Term.add_term_tvars [] ts; |
|
199 |
val (names',renamings) = |
|
200 |
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset
|
201 |
let val n2 = Name.variant Ns n in |
19835 | 202 |
(n2::Ns, (tv, (n2,s))::Rs) |
203 |
end) (tfree_names @ names,[]) tvars; |
|
204 |
in renamings end; |
|
205 |
fun fix_tvars_to_tfrees th = |
|
206 |
let |
|
22578 | 207 |
val sign = Thm.theory_of_thm th; |
19835 | 208 |
val ctypify = Thm.ctyp_of sign; |
209 |
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
|
210 |
val renamings = fix_tvars_to_tfrees_in_terms |
|
211 |
[] ((Thm.prop_of th) :: tpairs); |
|
212 |
val crenamings = |
|
213 |
map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) |
|
214 |
renamings; |
|
215 |
val fixedfrees = map snd crenamings; |
|
216 |
in (fixedfrees, Thm.instantiate (crenamings, []) th) end; |
|
217 |
||
218 |
||
219 |
(* change type-free's to type-vars in th, skipping the ones in "ns" *) |
|
220 |
fun unfix_tfrees ns th = |
|
221 |
let |
|
222 |
val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns |
|
223 |
val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[])); |
|
224 |
in #2 (Thm.varifyT' skiptfrees th) end; |
|
225 |
||
226 |
(* change schematic/meta vars to fresh free vars, avoiding name clashes |
|
227 |
with "names" *) |
|
228 |
fun fix_vars_to_frees_in_terms names ts = |
|
229 |
let |
|
230 |
val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts); |
|
231 |
val Ns = List.foldr Term.add_term_names names ts; |
|
232 |
val (_,renamings) = |
|
233 |
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset
|
234 |
let val n2 = Name.variant Ns n in |
19835 | 235 |
(n2 :: Ns, (v, (n2,ty)) :: Rs) |
236 |
end) ((Ns,[]), vars); |
|
237 |
in renamings end; |
|
238 |
fun fix_vars_to_frees th = |
|
239 |
let |
|
22578 | 240 |
val ctermify = Thm.cterm_of (Thm.theory_of_thm th) |
19835 | 241 |
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
242 |
val renamings = fix_vars_to_frees_in_terms |
|
243 |
[] ([Thm.prop_of th] @ tpairs); |
|
244 |
val crenamings = |
|
245 |
map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) |
|
246 |
renamings; |
|
247 |
val fixedfrees = map snd crenamings; |
|
248 |
in (fixedfrees, Thm.instantiate ([], crenamings) th) end; |
|
249 |
||
250 |
fun fix_tvars_upto_idx ix th = |
|
251 |
let |
|
22578 | 252 |
val sgn = Thm.theory_of_thm th; |
19835 | 253 |
val ctypify = Thm.ctyp_of sgn |
254 |
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
|
255 |
val prop = (Thm.prop_of th); |
|
256 |
val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); |
|
257 |
val ctyfixes = |
|
258 |
map_filter |
|
259 |
(fn (v as ((s,i),ty)) => |
|
260 |
if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) |
|
261 |
else NONE) tvars; |
|
262 |
in Thm.instantiate (ctyfixes, []) th end; |
|
263 |
fun fix_vars_upto_idx ix th = |
|
264 |
let |
|
22578 | 265 |
val sgn = Thm.theory_of_thm th; |
19835 | 266 |
val ctermify = Thm.cterm_of sgn |
267 |
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
|
268 |
val prop = (Thm.prop_of th); |
|
269 |
val vars = map Term.dest_Var (List.foldr Term.add_term_vars |
|
270 |
[] (prop :: tpairs)); |
|
271 |
val cfixes = |
|
272 |
map_filter |
|
273 |
(fn (v as ((s,i),ty)) => |
|
274 |
if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) |
|
275 |
else NONE) vars; |
|
276 |
in Thm.instantiate ([], cfixes) th end; |
|
277 |
||
278 |
||
279 |
(* make free vars into schematic vars with index zero *) |
|
280 |
fun unfix_frees frees = |
|
281 |
apply (map (K (Drule.forall_elim_var 0)) frees) |
|
282 |
o Drule.forall_intr_list frees; |
|
283 |
||
284 |
(* fix term and type variables *) |
|
285 |
fun fix_vars_and_tvars th = |
|
286 |
let val (tvars, th') = fix_tvars_to_tfrees th |
|
287 |
val (vars, th'') = fix_vars_to_frees th' |
|
288 |
in ((vars, tvars), th'') end; |
|
289 |
||
290 |
(* implicit Thm.thm argument *) |
|
291 |
(* assumes: vars may contain fixed versions of the frees *) |
|
292 |
(* THINK: what if vs already has types varified? *) |
|
293 |
fun unfix_frees_and_tfrees (vs,tvs) = |
|
294 |
(unfix_tfrees tvs o unfix_frees vs); |
|
295 |
||
296 |
(* datatype to capture an exported result, ie a fix or assume. *) |
|
297 |
datatype export = |
|
298 |
export of {fixes : Thm.cterm list, (* fixed vars *) |
|
299 |
assumes : Thm.cterm list, (* hidden hyps/assumed prems *) |
|
300 |
sgid : int, |
|
301 |
gth : Thm.thm}; (* subgoal/goalthm *) |
|
302 |
||
303 |
fun fixes_of_exp (export rep) = #fixes rep; |
|
304 |
||
305 |
(* export the result of the new goal thm, ie if we reduced teh |
|
306 |
subgoal, then we get a new reduced subtgoal with the old |
|
307 |
all-quantified variables *) |
|
308 |
local |
|
309 |
||
310 |
(* allify puts in a meta level univ quantifier for a free variavble *) |
|
311 |
fun allify_term (v, t) = |
|
312 |
let val vt = #t (Thm.rep_cterm v) |
|
313 |
val (n,ty) = Term.dest_Free vt |
|
314 |
in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; |
|
315 |
||
316 |
fun allify_for_sg_term ctermify vs t = |
|
317 |
let val t_alls = foldr allify_term t vs; |
|
318 |
val ct_alls = ctermify t_alls; |
|
319 |
in |
|
320 |
(ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) |
|
321 |
end; |
|
322 |
(* lookup type of a free var name from a list *) |
|
323 |
fun lookupfree vs vn = |
|
324 |
case Library.find_first (fn (n,ty) => n = vn) vs of |
|
325 |
NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term") |
|
326 |
| SOME x => x; |
|
327 |
in |
|
328 |
fun export_back (export {fixes = vs, assumes = hprems, |
|
329 |
sgid = i, gth = gth}) newth = |
|
330 |
let |
|
22578 | 331 |
val sgn = Thm.theory_of_thm newth; |
19835 | 332 |
val ctermify = Thm.cterm_of sgn; |
333 |
||
334 |
val sgs = prems_of newth; |
|
335 |
val (sgallcts, sgthms) = |
|
336 |
Library.split_list (map (allify_for_sg_term ctermify vs) sgs); |
|
337 |
val minimal_newth = |
|
338 |
(Library.foldl (fn ( newth', sgthm) => |
|
339 |
Drule.compose_single (sgthm, 1, newth')) |
|
340 |
(newth, sgthms)); |
|
341 |
val allified_newth = |
|
342 |
minimal_newth |
|
343 |
|> Drule.implies_intr_list hprems |
|
344 |
|> Drule.forall_intr_list vs |
|
345 |
||
346 |
val newth' = Drule.implies_intr_list sgallcts allified_newth |
|
347 |
in |
|
348 |
bicompose false (false, newth', (length sgallcts)) i gth |
|
349 |
end; |
|
350 |
||
351 |
(* |
|
352 |
Given "vs" : names of free variables to abstract over, |
|
353 |
Given cterms : premices to abstract over (P1... Pn) in terms of vs, |
|
354 |
Given a thm of the form: |
|
355 |
P1 vs; ...; Pn vs ==> Goal(C vs) |
|
356 |
||
357 |
Gives back: |
|
358 |
(n, length of given cterms which have been allified |
|
359 |
[| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm |
|
360 |
*) |
|
361 |
(* note: C may contain further premices etc |
|
362 |
Note that cterms is the assumed facts, ie prems of "P1" that are |
|
363 |
reintroduced in allified form. |
|
364 |
*) |
|
365 |
fun prepare_goal_export (vs, cterms) th = |
|
366 |
let |
|
22578 | 367 |
val sgn = Thm.theory_of_thm th; |
19835 | 368 |
val ctermify = Thm.cterm_of sgn; |
369 |
||
370 |
val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th)) |
|
371 |
val cfrees = map (ctermify o Free o lookupfree allfrees) vs |
|
372 |
||
373 |
val sgs = prems_of th; |
|
374 |
val (sgallcts, sgthms) = |
|
375 |
Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); |
|
376 |
||
377 |
val minimal_th = |
|
378 |
Goal.conclude (Library.foldl (fn ( th', sgthm) => |
|
379 |
Drule.compose_single (sgthm, 1, th')) |
|
380 |
(th, sgthms)); |
|
381 |
||
382 |
val allified_th = |
|
383 |
minimal_th |
|
384 |
|> Drule.implies_intr_list cterms |
|
385 |
|> Drule.forall_intr_list cfrees |
|
386 |
||
387 |
val th' = Drule.implies_intr_list sgallcts allified_th |
|
388 |
in |
|
389 |
((length sgallcts), th') |
|
390 |
end; |
|
391 |
||
392 |
end; |
|
393 |
||
394 |
||
395 |
(* exporting function that takes a solution to the fixed/assumed goal, |
|
396 |
and uses this to solve the subgoal in the main theorem *) |
|
397 |
fun export_solution (export {fixes = cfvs, assumes = hcprems, |
|
398 |
sgid = i, gth = gth}) solth = |
|
399 |
let |
|
400 |
val solth' = |
|
401 |
solth |> Drule.implies_intr_list hcprems |
|
402 |
|> Drule.forall_intr_list cfvs |
|
403 |
in Drule.compose_single (solth', i, gth) end; |
|
404 |
||
405 |
fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs; |
|
406 |
||
407 |
||
408 |
(* fix parameters of a subgoal "i", as free variables, and create an |
|
409 |
exporting function that will use the result of this proved goal to |
|
410 |
show the goal in the original theorem. |
|
411 |
||
412 |
Note, an advantage of this over Isar is that it supports instantiation |
|
413 |
of unkowns in the earlier theorem, ie we can do instantiation of meta |
|
414 |
vars! |
|
415 |
||
416 |
avoids constant, free and vars names. |
|
417 |
||
418 |
loosely corresponds to: |
|
419 |
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm |
|
420 |
Result: |
|
421 |
("(As ==> SGi x') ==> (As ==> SGi x')" : thm, |
|
422 |
expf : |
|
423 |
("As ==> SGi x'" : thm) -> |
|
424 |
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) |
|
425 |
*) |
|
426 |
fun fix_alls_in_term alledt = |
|
427 |
let |
|
428 |
val t = Term.strip_all_body alledt; |
|
429 |
val alls = rev (Term.strip_all_vars alledt); |
|
430 |
val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) |
|
431 |
val names = Term.add_term_names (t,varnames); |
|
432 |
val fvs = map Free |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset
|
433 |
(Name.variant_list names (map fst alls) |
19835 | 434 |
~~ (map snd alls)); |
435 |
in ((subst_bounds (fvs,t)), fvs) end; |
|
436 |
||
437 |
fun fix_alls_term i t = |
|
438 |
let |
|
439 |
val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) |
|
440 |
val names = Term.add_term_names (t,varnames); |
|
441 |
val gt = Logic.get_goal t i; |
|
442 |
val body = Term.strip_all_body gt; |
|
443 |
val alls = rev (Term.strip_all_vars gt); |
|
444 |
val fvs = map Free |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset
|
445 |
(Name.variant_list names (map fst alls) |
19835 | 446 |
~~ (map snd alls)); |
447 |
in ((subst_bounds (fvs,body)), fvs) end; |
|
448 |
||
449 |
fun fix_alls_cterm i th = |
|
450 |
let |
|
22578 | 451 |
val ctermify = Thm.cterm_of (Thm.theory_of_thm th); |
19835 | 452 |
val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th); |
453 |
val cfvs = rev (map ctermify fvs); |
|
454 |
val ct_body = ctermify fixedbody |
|
455 |
in |
|
456 |
(ct_body, cfvs) |
|
457 |
end; |
|
458 |
||
459 |
fun fix_alls' i = |
|
460 |
(apfst Thm.trivial) o (fix_alls_cterm i); |
|
461 |
||
462 |
||
463 |
(* hide other goals *) |
|
464 |
(* note the export goal is rotated by (i - 1) and will have to be |
|
465 |
unrotated to get backto the originial position(s) *) |
|
466 |
fun hide_other_goals th = |
|
467 |
let |
|
468 |
(* tl beacuse fst sg is the goal we are interested in *) |
|
469 |
val cprems = tl (Drule.cprems_of th) |
|
470 |
val aprems = map Thm.assume cprems |
|
471 |
in |
|
472 |
(Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, |
|
473 |
cprems) |
|
474 |
end; |
|
475 |
||
476 |
(* a nicer version of the above that leaves only a single subgoal (the |
|
477 |
other subgoals are hidden hyps, that the exporter suffles about) |
|
478 |
namely the subgoal that we were trying to solve. *) |
|
479 |
(* loosely corresponds to: |
|
480 |
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm |
|
481 |
Result: |
|
482 |
("(As ==> SGi x') ==> SGi x'" : thm, |
|
483 |
expf : |
|
484 |
("SGi x'" : thm) -> |
|
485 |
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) |
|
486 |
*) |
|
487 |
fun fix_alls i th = |
|
488 |
let |
|
489 |
val (fixed_gth, fixedvars) = fix_alls' i th |
|
490 |
val (sml_gth, othergoals) = hide_other_goals fixed_gth |
|
491 |
in |
|
492 |
(sml_gth, export {fixes = fixedvars, |
|
493 |
assumes = othergoals, |
|
494 |
sgid = i, gth = th}) |
|
495 |
end; |
|
496 |
||
497 |
||
498 |
(* assume the premises of subgoal "i", this gives back a list of |
|
499 |
assumed theorems that are the premices of subgoal i, it also gives |
|
500 |
back a new goal thm and an exporter, the new goalthm is as the old |
|
501 |
one, but without the premices, and the exporter will use a proof of |
|
502 |
the new goalthm, possibly using the assumed premices, to shoe the |
|
503 |
orginial goal. |
|
504 |
||
505 |
Note: Dealing with meta vars, need to meta-level-all them in the |
|
506 |
shyps, which we can later instantiate with a specific value.... ? |
|
507 |
think about this... maybe need to introduce some new fixed vars and |
|
508 |
then remove them again at the end... like I do with rw_inst. |
|
509 |
||
510 |
loosely corresponds to: |
|
511 |
Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm |
|
512 |
Result: |
|
513 |
(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions |
|
514 |
"SGi ==> SGi" : thm, -- new goal |
|
515 |
"SGi" ["A0" ... "An"] : thm -> -- export function |
|
516 |
("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) |
|
517 |
*) |
|
518 |
fun assume_prems i th = |
|
519 |
let |
|
520 |
val t = (prop_of th); |
|
521 |
val gt = Logic.get_goal t i; |
|
522 |
val _ = case Term.strip_all_vars gt of [] => () |
|
523 |
| _ => error "assume_prems: goal has params" |
|
524 |
val body = gt; |
|
525 |
val prems = Logic.strip_imp_prems body; |
|
526 |
val concl = Logic.strip_imp_concl body; |
|
527 |
||
22578 | 528 |
val sgn = Thm.theory_of_thm th; |
19835 | 529 |
val ctermify = Thm.cterm_of sgn; |
530 |
val cprems = map ctermify prems; |
|
531 |
val aprems = map Thm.assume cprems; |
|
532 |
val gthi = Thm.trivial (ctermify concl); |
|
533 |
||
534 |
(* fun explortf thi = |
|
535 |
Drule.compose (Drule.implies_intr_list cprems thi, |
|
536 |
i, th) *) |
|
537 |
in |
|
538 |
(aprems, gthi, cprems) |
|
539 |
end; |
|
540 |
||
541 |
||
542 |
(* first fix the variables, then assume the assumptions *) |
|
543 |
(* loosely corresponds to: |
|
544 |
Given |
|
545 |
"[| SG0; ... |
|
546 |
!! xs. [| A0 xs; ... An xs |] ==> SGi xs; |
|
547 |
... SGm |] ==> G" : thm |
|
548 |
Result: |
|
549 |
(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions |
|
550 |
"SGi xs' ==> SGi xs'" : thm, -- new goal |
|
551 |
"SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function |
|
552 |
("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) |
|
553 |
*) |
|
554 |
||
555 |
(* Note: the fix_alls actually pulls through all the assumptions which |
|
556 |
means that the second export is not needed. *) |
|
557 |
fun fixes_and_assumes i th = |
|
558 |
let |
|
559 |
val (fixgth, exp1) = fix_alls i th |
|
560 |
val (assumps, goalth, _) = assume_prems 1 fixgth |
|
561 |
in |
|
562 |
(assumps, goalth, exp1) |
|
563 |
end; |
|
564 |
||
565 |
||
566 |
(* Fixme: allow different order of subgoals given to expf *) |
|
567 |
(* make each subgoal into a separate thm that needs to be proved *) |
|
568 |
(* loosely corresponds to: |
|
569 |
Given |
|
570 |
"[| SG0; ... SGm |] ==> G" : thm |
|
571 |
Result: |
|
572 |
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals |
|
573 |
["SG0", ..., "SGm"] : thm list -> -- export function |
|
574 |
"G" : thm) |
|
575 |
*) |
|
576 |
fun subgoal_thms th = |
|
577 |
let |
|
578 |
val t = (prop_of th); |
|
579 |
||
580 |
val prems = Logic.strip_imp_prems t; |
|
581 |
||
22578 | 582 |
val sgn = Thm.theory_of_thm th; |
19835 | 583 |
val ctermify = Thm.cterm_of sgn; |
584 |
||
585 |
val aprems = map (Thm.trivial o ctermify) prems; |
|
586 |
||
587 |
fun explortf premths = |
|
588 |
Drule.implies_elim_list th premths |
|
589 |
in |
|
590 |
(aprems, explortf) |
|
591 |
end; |
|
592 |
||
593 |
||
594 |
(* make all the premices of a theorem hidden, and provide an unhide |
|
595 |
function, that will bring them back out at a later point. This is |
|
596 |
useful if you want to get back these premices, after having used the |
|
597 |
theorem with the premices hidden *) |
|
598 |
(* loosely corresponds to: |
|
599 |
Given "As ==> G" : thm |
|
600 |
Result: ("G [As]" : thm, |
|
601 |
"G [As]" : thm -> "As ==> G" : thm |
|
602 |
*) |
|
603 |
fun hide_prems th = |
|
604 |
let |
|
605 |
val cprems = Drule.cprems_of th; |
|
606 |
val aprems = map Thm.assume cprems; |
|
607 |
(* val unhidef = Drule.implies_intr_list cprems; *) |
|
608 |
in |
|
609 |
(Drule.implies_elim_list th aprems, cprems) |
|
610 |
end; |
|
611 |
||
612 |
||
613 |
||
614 |
||
615 |
(* Fixme: allow different order of subgoals in exportf *) |
|
616 |
(* as above, but also fix all parameters in all subgoals, and uses |
|
617 |
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent |
|
618 |
subgoals. *) |
|
619 |
(* loosely corresponds to: |
|
620 |
Given |
|
621 |
"[| !! x0s. A0s x0s ==> SG0 x0s; |
|
622 |
...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm |
|
623 |
Result: |
|
624 |
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", |
|
625 |
... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals |
|
626 |
["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function |
|
627 |
"G" : thm) |
|
628 |
*) |
|
629 |
(* requires being given solutions! *) |
|
630 |
fun fixed_subgoal_thms th = |
|
631 |
let |
|
632 |
val (subgoals, expf) = subgoal_thms th; |
|
633 |
(* fun export_sg (th, exp) = exp th; *) |
|
634 |
fun export_sgs expfs solthms = |
|
635 |
expf (map2 (curry (op |>)) solthms expfs); |
|
636 |
(* expf (map export_sg (ths ~~ expfs)); *) |
|
637 |
in |
|
638 |
apsnd export_sgs (Library.split_list (map (apsnd export_solution o |
|
639 |
fix_alls 1) subgoals)) |
|
640 |
end; |
|
641 |
||
642 |
end; |