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