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