|
1 (* Title: TFL/tfl.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 First part of main module. |
|
7 *) |
|
8 |
|
9 signature PRIM = |
|
10 sig |
|
11 val trace: bool ref |
|
12 type pattern |
|
13 val mk_functional: theory -> term list -> {functional: term, pats: pattern list} |
|
14 val wfrec_definition0: theory -> string -> term -> term -> theory * thm |
|
15 val post_definition: thm list -> theory * (thm * pattern list) -> |
|
16 {theory: theory, |
|
17 rules: thm, |
|
18 rows: int list, |
|
19 TCs: term list list, |
|
20 full_pats_TCs: (term * term list) list} |
|
21 val wfrec_eqns: theory -> xstring -> thm list -> term list -> |
|
22 {WFR: term, |
|
23 SV: term list, |
|
24 proto_def: term, |
|
25 extracta: (thm * term list) list, |
|
26 pats: pattern list} |
|
27 val lazyR_def: theory -> xstring -> thm list -> term list -> |
|
28 {theory: theory, |
|
29 rules: thm, |
|
30 R: term, |
|
31 SV: term list, |
|
32 full_pats_TCs: (term * term list) list, |
|
33 patterns : pattern list} |
|
34 val mk_induction: theory -> |
|
35 {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm |
|
36 val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory -> |
|
37 {rules: thm, induction: thm, TCs: term list list} -> |
|
38 {rules: thm, induction: thm, nested_tcs: thm list} |
|
39 end; |
|
40 |
|
41 structure Prim: PRIM = |
|
42 struct |
|
43 |
|
44 val trace = ref false; |
|
45 |
|
46 open BasisLibrary; |
|
47 |
|
48 structure R = Rules; |
|
49 structure S = USyntax; |
|
50 structure U = Utils; |
|
51 |
|
52 |
|
53 fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg}; |
|
54 |
|
55 val concl = #2 o R.dest_thm; |
|
56 val hyp = #1 o R.dest_thm; |
|
57 |
|
58 val list_mk_type = U.end_itlist (curry (op -->)); |
|
59 |
|
60 fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1)); |
|
61 |
|
62 fun front_last [] = raise TFL_ERR "front_last" "empty list" |
|
63 | front_last [x] = ([],x) |
|
64 | front_last (h::t) = |
|
65 let val (pref,x) = front_last t |
|
66 in |
|
67 (h::pref,x) |
|
68 end; |
|
69 |
|
70 |
|
71 (*--------------------------------------------------------------------------- |
|
72 * The next function is common to pattern-match translation and |
|
73 * proof of completeness of cases for the induction theorem. |
|
74 * |
|
75 * The curried function "gvvariant" returns a function to generate distinct |
|
76 * variables that are guaranteed not to be in names. The names of |
|
77 * the variables go u, v, ..., z, aa, ..., az, ... The returned |
|
78 * function contains embedded refs! |
|
79 *---------------------------------------------------------------------------*) |
|
80 fun gvvariant names = |
|
81 let val slist = ref names |
|
82 val vname = ref "u" |
|
83 fun new() = |
|
84 if !vname mem_string (!slist) |
|
85 then (vname := bump_string (!vname); new()) |
|
86 else (slist := !vname :: !slist; !vname) |
|
87 in |
|
88 fn ty => Free(new(), ty) |
|
89 end; |
|
90 |
|
91 |
|
92 (*--------------------------------------------------------------------------- |
|
93 * Used in induction theorem production. This is the simple case of |
|
94 * partitioning up pattern rows by the leading constructor. |
|
95 *---------------------------------------------------------------------------*) |
|
96 fun ipartition gv (constructors,rows) = |
|
97 let fun pfail s = raise TFL_ERR "partition.part" s |
|
98 fun part {constrs = [], rows = [], A} = rev A |
|
99 | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" |
|
100 | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" |
|
101 | part {constrs = c::crst, rows, A} = |
|
102 let val (Name,Ty) = dest_Const c |
|
103 val L = binder_types Ty |
|
104 val (in_group, not_in_group) = |
|
105 U.itlist (fn (row as (p::rst, rhs)) => |
|
106 fn (in_group,not_in_group) => |
|
107 let val (pc,args) = S.strip_comb p |
|
108 in if (#1(dest_Const pc) = Name) |
|
109 then ((args@rst, rhs)::in_group, not_in_group) |
|
110 else (in_group, row::not_in_group) |
|
111 end) rows ([],[]) |
|
112 val col_types = U.take type_of (length L, #1(hd in_group)) |
|
113 in |
|
114 part{constrs = crst, rows = not_in_group, |
|
115 A = {constructor = c, |
|
116 new_formals = map gv col_types, |
|
117 group = in_group}::A} |
|
118 end |
|
119 in part{constrs = constructors, rows = rows, A = []} |
|
120 end; |
|
121 |
|
122 |
|
123 |
|
124 (*--------------------------------------------------------------------------- |
|
125 * Each pattern carries with it a tag (i,b) where |
|
126 * i is the clause it came from and |
|
127 * b=true indicates that clause was given by the user |
|
128 * (or is an instantiation of a user supplied pattern) |
|
129 * b=false --> i = ~1 |
|
130 *---------------------------------------------------------------------------*) |
|
131 |
|
132 type pattern = term * (int * bool) |
|
133 |
|
134 fun pattern_map f (tm,x) = (f tm, x); |
|
135 |
|
136 fun pattern_subst theta = pattern_map (subst_free theta); |
|
137 |
|
138 val pat_of = fst; |
|
139 fun row_of_pat x = fst (snd x); |
|
140 fun given x = snd (snd x); |
|
141 |
|
142 (*--------------------------------------------------------------------------- |
|
143 * Produce an instance of a constructor, plus genvars for its arguments. |
|
144 *---------------------------------------------------------------------------*) |
|
145 fun fresh_constr ty_match colty gv c = |
|
146 let val (_,Ty) = dest_Const c |
|
147 val L = binder_types Ty |
|
148 and ty = body_type Ty |
|
149 val ty_theta = ty_match ty colty |
|
150 val c' = S.inst ty_theta c |
|
151 val gvars = map (S.inst ty_theta o gv) L |
|
152 in (c', gvars) |
|
153 end; |
|
154 |
|
155 |
|
156 (*--------------------------------------------------------------------------- |
|
157 * Goes through a list of rows and picks out the ones beginning with a |
|
158 * pattern with constructor = Name. |
|
159 *---------------------------------------------------------------------------*) |
|
160 fun mk_group Name rows = |
|
161 U.itlist (fn (row as ((prfx, p::rst), rhs)) => |
|
162 fn (in_group,not_in_group) => |
|
163 let val (pc,args) = S.strip_comb p |
|
164 in if ((#1 (Term.dest_Const pc) = Name) handle TERM _ => false) |
|
165 then (((prfx,args@rst), rhs)::in_group, not_in_group) |
|
166 else (in_group, row::not_in_group) end) |
|
167 rows ([],[]); |
|
168 |
|
169 (*--------------------------------------------------------------------------- |
|
170 * Partition the rows. Not efficient: we should use hashing. |
|
171 *---------------------------------------------------------------------------*) |
|
172 fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows" |
|
173 | partition gv ty_match |
|
174 (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) = |
|
175 let val fresh = fresh_constr ty_match colty gv |
|
176 fun part {constrs = [], rows, A} = rev A |
|
177 | part {constrs = c::crst, rows, A} = |
|
178 let val (c',gvars) = fresh c |
|
179 val (Name,Ty) = dest_Const c' |
|
180 val (in_group, not_in_group) = mk_group Name rows |
|
181 val in_group' = |
|
182 if (null in_group) (* Constructor not given *) |
|
183 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))] |
|
184 else in_group |
|
185 in |
|
186 part{constrs = crst, |
|
187 rows = not_in_group, |
|
188 A = {constructor = c', |
|
189 new_formals = gvars, |
|
190 group = in_group'}::A} |
|
191 end |
|
192 in part{constrs=constructors, rows=rows, A=[]} |
|
193 end; |
|
194 |
|
195 (*--------------------------------------------------------------------------- |
|
196 * Misc. routines used in mk_case |
|
197 *---------------------------------------------------------------------------*) |
|
198 |
|
199 fun mk_pat (c,l) = |
|
200 let val L = length (binder_types (type_of c)) |
|
201 fun build (prfx,tag,plist) = |
|
202 let val args = take (L,plist) |
|
203 and plist' = drop(L,plist) |
|
204 in (prfx,tag,list_comb(c,args)::plist') end |
|
205 in map build l end; |
|
206 |
|
207 fun v_to_prfx (prfx, v::pats) = (v::prfx,pats) |
|
208 | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx"; |
|
209 |
|
210 fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats) |
|
211 | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats"; |
|
212 |
|
213 |
|
214 (*---------------------------------------------------------------------------- |
|
215 * Translation of pattern terms into nested case expressions. |
|
216 * |
|
217 * This performs the translation and also builds the full set of patterns. |
|
218 * Thus it supports the construction of induction theorems even when an |
|
219 * incomplete set of patterns is given. |
|
220 *---------------------------------------------------------------------------*) |
|
221 |
|
222 fun mk_case ty_info ty_match usednames range_ty = |
|
223 let |
|
224 fun mk_case_fail s = raise TFL_ERR "mk_case" s |
|
225 val fresh_var = gvvariant usednames |
|
226 val divide = partition fresh_var ty_match |
|
227 fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row" |
|
228 | expand constructors ty (row as ((prfx, p::rst), rhs)) = |
|
229 if (is_Free p) |
|
230 then let val fresh = fresh_constr ty_match ty fresh_var |
|
231 fun expnd (c,gvs) = |
|
232 let val capp = list_comb(c,gvs) |
|
233 in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs) |
|
234 end |
|
235 in map expnd (map fresh constructors) end |
|
236 else [row] |
|
237 fun mk{rows=[],...} = mk_case_fail"no rows" |
|
238 | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *) |
|
239 ([(prfx,tag,[])], tm) |
|
240 | mk{path=[], rows = _::_} = mk_case_fail"blunder" |
|
241 | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} = |
|
242 mk{path = path, |
|
243 rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst} |
|
244 | mk{path = u::rstp, rows as ((_, p::_), _)::_} = |
|
245 let val (pat_rectangle,rights) = ListPair.unzip rows |
|
246 val col0 = map(hd o #2) pat_rectangle |
|
247 in |
|
248 if (forall is_Free col0) |
|
249 then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e) |
|
250 (ListPair.zip (col0, rights)) |
|
251 val pat_rectangle' = map v_to_prfx pat_rectangle |
|
252 val (pref_patl,tm) = mk{path = rstp, |
|
253 rows = ListPair.zip (pat_rectangle', |
|
254 rights')} |
|
255 in (map v_to_pats pref_patl, tm) |
|
256 end |
|
257 else |
|
258 let val pty as Type (ty_name,_) = type_of p |
|
259 in |
|
260 case (ty_info ty_name) |
|
261 of None => mk_case_fail("Not a known datatype: "^ty_name) |
|
262 | Some{case_const,constructors} => |
|
263 let |
|
264 val case_const_name = #1(dest_Const case_const) |
|
265 val nrows = List.concat (map (expand constructors pty) rows) |
|
266 val subproblems = divide(constructors, pty, range_ty, nrows) |
|
267 val groups = map #group subproblems |
|
268 and new_formals = map #new_formals subproblems |
|
269 and constructors' = map #constructor subproblems |
|
270 val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows}) |
|
271 (ListPair.zip (new_formals, groups)) |
|
272 val rec_calls = map mk news |
|
273 val (pat_rect,dtrees) = ListPair.unzip rec_calls |
|
274 val case_functions = map S.list_mk_abs |
|
275 (ListPair.zip (new_formals, dtrees)) |
|
276 val types = map type_of (case_functions@[u]) @ [range_ty] |
|
277 val case_const' = Const(case_const_name, list_mk_type types) |
|
278 val tree = list_comb(case_const', case_functions@[u]) |
|
279 val pat_rect1 = List.concat |
|
280 (ListPair.map mk_pat (constructors', pat_rect)) |
|
281 in (pat_rect1,tree) |
|
282 end |
|
283 end end |
|
284 in mk |
|
285 end; |
|
286 |
|
287 |
|
288 (* Repeated variable occurrences in a pattern are not allowed. *) |
|
289 fun FV_multiset tm = |
|
290 case (S.dest_term tm) |
|
291 of S.VAR{Name,Ty} => [Free(Name,Ty)] |
|
292 | S.CONST _ => [] |
|
293 | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand |
|
294 | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda"; |
|
295 |
|
296 fun no_repeat_vars thy pat = |
|
297 let fun check [] = true |
|
298 | check (v::rst) = |
|
299 if mem_term (v,rst) then |
|
300 raise TFL_ERR "no_repeat_vars" |
|
301 (quote (#1 (dest_Free v)) ^ |
|
302 " occurs repeatedly in the pattern " ^ |
|
303 quote (string_of_cterm (Thry.typecheck thy pat))) |
|
304 else check rst |
|
305 in check (FV_multiset pat) |
|
306 end; |
|
307 |
|
308 fun dest_atom (Free p) = p |
|
309 | dest_atom (Const p) = p |
|
310 | dest_atom _ = raise TFL_ERR "dest_atom" "function name not an identifier"; |
|
311 |
|
312 fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q); |
|
313 |
|
314 local fun mk_functional_err s = raise TFL_ERR "mk_functional" s |
|
315 fun single [_$_] = |
|
316 mk_functional_err "recdef does not allow currying" |
|
317 | single [f] = f |
|
318 | single fs = |
|
319 (*multiple function names?*) |
|
320 if length (gen_distinct same_name fs) < length fs |
|
321 then mk_functional_err |
|
322 "The function being declared appears with multiple types" |
|
323 else mk_functional_err |
|
324 (Int.toString (length fs) ^ |
|
325 " distinct function names being declared") |
|
326 in |
|
327 fun mk_functional thy clauses = |
|
328 let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses |
|
329 handle TERM _ => raise TFL_ERR "mk_functional" |
|
330 "recursion equations must use the = relation") |
|
331 val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) |
|
332 val atom = single (gen_distinct (op aconv) funcs) |
|
333 val (fname,ftype) = dest_atom atom |
|
334 val dummy = map (no_repeat_vars thy) pats |
|
335 val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, |
|
336 map (fn (t,i) => (t,(i,true))) (enumerate R)) |
|
337 val names = foldr add_term_names (R,[]) |
|
338 val atype = type_of(hd pats) |
|
339 and aname = variant names "a" |
|
340 val a = Free(aname,atype) |
|
341 val ty_info = Thry.match_info thy |
|
342 val ty_match = Thry.match_type thy |
|
343 val range_ty = type_of (hd R) |
|
344 val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty |
|
345 {path=[a], rows=rows} |
|
346 val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts |
|
347 handle Match => mk_functional_err "error in pattern-match translation" |
|
348 val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1 |
|
349 val finals = map row_of_pat patts2 |
|
350 val originals = map (row_of_pat o #2) rows |
|
351 val dummy = case (originals\\finals) |
|
352 of [] => () |
|
353 | L => mk_functional_err |
|
354 ("The following clauses are redundant (covered by preceding clauses): " ^ |
|
355 commas (map (fn i => Int.toString (i + 1)) L)) |
|
356 in {functional = Abs(Sign.base_name fname, ftype, |
|
357 abstract_over (atom, |
|
358 absfree(aname,atype, case_tm))), |
|
359 pats = patts2} |
|
360 end end; |
|
361 |
|
362 |
|
363 (*---------------------------------------------------------------------------- |
|
364 * |
|
365 * PRINCIPLES OF DEFINITION |
|
366 * |
|
367 *---------------------------------------------------------------------------*) |
|
368 |
|
369 |
|
370 (*For Isabelle, the lhs of a definition must be a constant.*) |
|
371 fun mk_const_def sign (Name, Ty, rhs) = |
|
372 Sign.infer_types sign (K None) (K None) [] false |
|
373 ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT) |
|
374 |> #1; |
|
375 |
|
376 (*Make all TVars available for instantiation by adding a ? to the front*) |
|
377 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts) |
|
378 | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort) |
|
379 | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort); |
|
380 |
|
381 local val f_eq_wfrec_R_M = |
|
382 #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY)))) |
|
383 val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M |
|
384 val (fname,_) = dest_Free f |
|
385 val (wfrec,_) = S.strip_comb rhs |
|
386 in |
|
387 fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) = |
|
388 let val def_name = if Name<>fid then |
|
389 raise TFL_ERR "wfrec_definition0" |
|
390 ("Expected a definition of " ^ |
|
391 quote fid ^ " but found one of " ^ |
|
392 quote Name) |
|
393 else Name ^ "_def" |
|
394 val wfrec_R_M = map_term_types poly_tvars |
|
395 (wfrec $ map_term_types poly_tvars R) |
|
396 $ functional |
|
397 val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M) |
|
398 val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy |
|
399 in (thy', def) end; |
|
400 end; |
|
401 |
|
402 |
|
403 |
|
404 (*--------------------------------------------------------------------------- |
|
405 * This structure keeps track of congruence rules that aren't derived |
|
406 * from a datatype definition. |
|
407 *---------------------------------------------------------------------------*) |
|
408 fun extraction_thms thy = |
|
409 let val {case_rewrites,case_congs} = Thry.extract_info thy |
|
410 in (case_rewrites, case_congs) |
|
411 end; |
|
412 |
|
413 |
|
414 (*--------------------------------------------------------------------------- |
|
415 * Pair patterns with termination conditions. The full list of patterns for |
|
416 * a definition is merged with the TCs arising from the user-given clauses. |
|
417 * There can be fewer clauses than the full list, if the user omitted some |
|
418 * cases. This routine is used to prepare input for mk_induction. |
|
419 *---------------------------------------------------------------------------*) |
|
420 fun merge full_pats TCs = |
|
421 let fun insert (p,TCs) = |
|
422 let fun insrt ((x as (h,[]))::rst) = |
|
423 if (p aconv h) then (p,TCs)::rst else x::insrt rst |
|
424 | insrt (x::rst) = x::insrt rst |
|
425 | insrt[] = raise TFL_ERR "merge.insert" "pattern not found" |
|
426 in insrt end |
|
427 fun pass ([],ptcl_final) = ptcl_final |
|
428 | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl) |
|
429 in |
|
430 pass (TCs, map (fn p => (p,[])) full_pats) |
|
431 end; |
|
432 |
|
433 |
|
434 fun givens pats = map pat_of (filter given pats); |
|
435 |
|
436 fun post_definition meta_tflCongs (theory, (def, pats)) = |
|
437 let val tych = Thry.typecheck theory |
|
438 val f = #lhs(S.dest_eq(concl def)) |
|
439 val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def |
|
440 val pats' = filter given pats |
|
441 val given_pats = map pat_of pats' |
|
442 val rows = map row_of_pat pats' |
|
443 val WFR = #ant(S.dest_imp(concl corollary)) |
|
444 val R = #Rand(S.dest_comb WFR) |
|
445 val corollary' = R.UNDISCH corollary (* put WF R on assums *) |
|
446 val corollaries = map (fn pat => R.SPEC (tych pat) corollary') |
|
447 given_pats |
|
448 val (case_rewrites,context_congs) = extraction_thms theory |
|
449 val corollaries' = map(rewrite_rule case_rewrites) corollaries |
|
450 val extract = R.CONTEXT_REWRITE_RULE |
|
451 (f, [R], cut_apply, meta_tflCongs@context_congs) |
|
452 val (rules, TCs) = ListPair.unzip (map extract corollaries') |
|
453 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules |
|
454 val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) |
|
455 val rules1 = R.LIST_CONJ(map mk_cond_rule rules0) |
|
456 in |
|
457 {theory = theory, |
|
458 rules = rules1, |
|
459 rows = rows, |
|
460 full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), |
|
461 TCs = TCs} |
|
462 end; |
|
463 |
|
464 |
|
465 (*--------------------------------------------------------------------------- |
|
466 * Perform the extraction without making the definition. Definition and |
|
467 * extraction commute for the non-nested case. (Deferred recdefs) |
|
468 * |
|
469 * The purpose of wfrec_eqns is merely to instantiate the recursion theorem |
|
470 * and extract termination conditions: no definition is made. |
|
471 *---------------------------------------------------------------------------*) |
|
472 |
|
473 fun wfrec_eqns thy fid tflCongs eqns = |
|
474 let val {lhs,rhs} = S.dest_eq (hd eqns) |
|
475 val (f,args) = S.strip_comb lhs |
|
476 val (fname,fty) = dest_atom f |
|
477 val (SV,a) = front_last args (* SV = schematic variables *) |
|
478 val g = list_comb(f,SV) |
|
479 val h = Free(fname,type_of g) |
|
480 val eqns1 = map (subst_free[(g,h)]) eqns |
|
481 val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns1 |
|
482 val given_pats = givens pats |
|
483 (* val f = Free(Name,Ty) *) |
|
484 val Type("fun", [f_dty, f_rty]) = Ty |
|
485 val dummy = if Name<>fid then |
|
486 raise TFL_ERR "wfrec_eqns" |
|
487 ("Expected a definition of " ^ |
|
488 quote fid ^ " but found one of " ^ |
|
489 quote Name) |
|
490 else () |
|
491 val (case_rewrites,context_congs) = extraction_thms thy |
|
492 val tych = Thry.typecheck thy |
|
493 val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY |
|
494 val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 |
|
495 val R = Free (variant (foldr add_term_names (eqns,[])) Rname, |
|
496 Rtype) |
|
497 val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0 |
|
498 val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) |
|
499 val dummy = |
|
500 if !trace then |
|
501 writeln ("ORIGINAL PROTO_DEF: " ^ |
|
502 Sign.string_of_term (Theory.sign_of thy) proto_def) |
|
503 else () |
|
504 val R1 = S.rand WFR |
|
505 val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM) |
|
506 val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats |
|
507 val corollaries' = map (rewrite_rule case_rewrites) corollaries |
|
508 fun extract X = R.CONTEXT_REWRITE_RULE |
|
509 (f, R1::SV, cut_apply, tflCongs@context_congs) X |
|
510 in {proto_def = proto_def, |
|
511 SV=SV, |
|
512 WFR=WFR, |
|
513 pats=pats, |
|
514 extracta = map extract corollaries'} |
|
515 end; |
|
516 |
|
517 |
|
518 (*--------------------------------------------------------------------------- |
|
519 * Define the constant after extracting the termination conditions. The |
|
520 * wellfounded relation used in the definition is computed by using the |
|
521 * choice operator on the extracted conditions (plus the condition that |
|
522 * such a relation must be wellfounded). |
|
523 *---------------------------------------------------------------------------*) |
|
524 |
|
525 fun lazyR_def thy fid tflCongs eqns = |
|
526 let val {proto_def,WFR,pats,extracta,SV} = |
|
527 wfrec_eqns thy fid tflCongs eqns |
|
528 val R1 = S.rand WFR |
|
529 val f = #lhs(S.dest_eq proto_def) |
|
530 val (extractants,TCl) = ListPair.unzip extracta |
|
531 val dummy = if !trace |
|
532 then (writeln "Extractants = "; |
|
533 prths extractants; |
|
534 ()) |
|
535 else () |
|
536 val TCs = foldr (gen_union (op aconv)) (TCl, []) |
|
537 val full_rqt = WFR::TCs |
|
538 val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} |
|
539 val R'abs = S.rand R' |
|
540 val proto_def' = subst_free[(R1,R')] proto_def |
|
541 val dummy = if !trace then writeln ("proto_def' = " ^ |
|
542 Sign.string_of_term |
|
543 (Theory.sign_of thy) proto_def') |
|
544 else () |
|
545 val {lhs,rhs} = S.dest_eq proto_def' |
|
546 val (c,args) = S.strip_comb lhs |
|
547 val (Name,Ty) = dest_atom c |
|
548 val defn = mk_const_def (Theory.sign_of thy) |
|
549 (Name, Ty, S.list_mk_abs (args,rhs)) |
|
550 val (theory, [def0]) = |
|
551 thy |
|
552 |> PureThy.add_defs_i false |
|
553 [Thm.no_attributes (fid ^ "_def", defn)] |
|
554 val def = freezeT def0; |
|
555 val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def) |
|
556 else () |
|
557 (* val fconst = #lhs(S.dest_eq(concl def)) *) |
|
558 val tych = Thry.typecheck theory |
|
559 val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt |
|
560 (*lcp: a lot of object-logic inference to remove*) |
|
561 val baz = R.DISCH_ALL |
|
562 (U.itlist R.DISCH full_rqt_prop |
|
563 (R.LIST_CONJ extractants)) |
|
564 val dum = if !trace then writeln ("baz = " ^ string_of_thm baz) |
|
565 else () |
|
566 val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) |
|
567 val SV' = map tych SV; |
|
568 val SVrefls = map reflexive SV' |
|
569 val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x)) |
|
570 SVrefls def) |
|
571 RS meta_eq_to_obj_eq |
|
572 val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 |
|
573 val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) |
|
574 val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX) |
|
575 body_th |
|
576 in {theory = theory, R=R1, SV=SV, |
|
577 rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', |
|
578 full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), |
|
579 patterns = pats} |
|
580 end; |
|
581 |
|
582 |
|
583 |
|
584 (*---------------------------------------------------------------------------- |
|
585 * |
|
586 * INDUCTION THEOREM |
|
587 * |
|
588 *---------------------------------------------------------------------------*) |
|
589 |
|
590 |
|
591 (*------------------------ Miscellaneous function -------------------------- |
|
592 * |
|
593 * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n] |
|
594 * ----------------------------------------------------------- |
|
595 * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]), |
|
596 * ... |
|
597 * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] ) |
|
598 * |
|
599 * This function is totally ad hoc. Used in the production of the induction |
|
600 * theorem. The nchotomy theorem can have clauses that look like |
|
601 * |
|
602 * ?v1..vn. z = C vn..v1 |
|
603 * |
|
604 * in which the order of quantification is not the order of occurrence of the |
|
605 * quantified variables as arguments to C. Since we have no control over this |
|
606 * aspect of the nchotomy theorem, we make the correspondence explicit by |
|
607 * pairing the incoming new variable with the term it gets beta-reduced into. |
|
608 *---------------------------------------------------------------------------*) |
|
609 |
|
610 fun alpha_ex_unroll (xlist, tm) = |
|
611 let val (qvars,body) = S.strip_exists tm |
|
612 val vlist = #2(S.strip_comb (S.rhs body)) |
|
613 val plist = ListPair.zip (vlist, xlist) |
|
614 val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars |
|
615 handle Library.OPTION => sys_error |
|
616 "TFL fault [alpha_ex_unroll]: no correspondence" |
|
617 fun build ex [] = [] |
|
618 | build (_$rex) (v::rst) = |
|
619 let val ex1 = betapply(rex, v) |
|
620 in ex1 :: build ex1 rst |
|
621 end |
|
622 val (nex::exl) = rev (tm::build tm args) |
|
623 in |
|
624 (nex, ListPair.zip (args, rev exl)) |
|
625 end; |
|
626 |
|
627 |
|
628 |
|
629 (*---------------------------------------------------------------------------- |
|
630 * |
|
631 * PROVING COMPLETENESS OF PATTERNS |
|
632 * |
|
633 *---------------------------------------------------------------------------*) |
|
634 |
|
635 fun mk_case ty_info usednames thy = |
|
636 let |
|
637 val divide = ipartition (gvvariant usednames) |
|
638 val tych = Thry.typecheck thy |
|
639 fun tych_binding(x,y) = (tych x, tych y) |
|
640 fun fail s = raise TFL_ERR "mk_case" s |
|
641 fun mk{rows=[],...} = fail"no rows" |
|
642 | mk{path=[], rows = [([], (thm, bindings))]} = |
|
643 R.IT_EXISTS (map tych_binding bindings) thm |
|
644 | mk{path = u::rstp, rows as (p::_, _)::_} = |
|
645 let val (pat_rectangle,rights) = ListPair.unzip rows |
|
646 val col0 = map hd pat_rectangle |
|
647 val pat_rectangle' = map tl pat_rectangle |
|
648 in |
|
649 if (forall is_Free col0) (* column 0 is all variables *) |
|
650 then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)])) |
|
651 (ListPair.zip (rights, col0)) |
|
652 in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')} |
|
653 end |
|
654 else (* column 0 is all constructors *) |
|
655 let val Type (ty_name,_) = type_of p |
|
656 in |
|
657 case (ty_info ty_name) |
|
658 of None => fail("Not a known datatype: "^ty_name) |
|
659 | Some{constructors,nchotomy} => |
|
660 let val thm' = R.ISPEC (tych u) nchotomy |
|
661 val disjuncts = S.strip_disj (concl thm') |
|
662 val subproblems = divide(constructors, rows) |
|
663 val groups = map #group subproblems |
|
664 and new_formals = map #new_formals subproblems |
|
665 val existentials = ListPair.map alpha_ex_unroll |
|
666 (new_formals, disjuncts) |
|
667 val constraints = map #1 existentials |
|
668 val vexl = map #2 existentials |
|
669 fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b)) |
|
670 val news = map (fn (nf,rows,c) => {path = nf@rstp, |
|
671 rows = map (expnd c) rows}) |
|
672 (U.zip3 new_formals groups constraints) |
|
673 val recursive_thms = map mk news |
|
674 val build_exists = foldr |
|
675 (fn((x,t), th) => |
|
676 R.CHOOSE (tych x, R.ASSUME (tych t)) th) |
|
677 val thms' = ListPair.map build_exists (vexl, recursive_thms) |
|
678 val same_concls = R.EVEN_ORS thms' |
|
679 in R.DISJ_CASESL thm' same_concls |
|
680 end |
|
681 end end |
|
682 in mk |
|
683 end; |
|
684 |
|
685 |
|
686 fun complete_cases thy = |
|
687 let val tych = Thry.typecheck thy |
|
688 val ty_info = Thry.induct_info thy |
|
689 in fn pats => |
|
690 let val names = foldr add_term_names (pats,[]) |
|
691 val T = type_of (hd pats) |
|
692 val aname = Term.variant names "a" |
|
693 val vname = Term.variant (aname::names) "v" |
|
694 val a = Free (aname, T) |
|
695 val v = Free (vname, T) |
|
696 val a_eq_v = HOLogic.mk_eq(a,v) |
|
697 val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a) |
|
698 (R.REFL (tych a)) |
|
699 val th0 = R.ASSUME (tych a_eq_v) |
|
700 val rows = map (fn x => ([x], (th0,[]))) pats |
|
701 in |
|
702 R.GEN (tych a) |
|
703 (R.RIGHT_ASSOC |
|
704 (R.CHOOSE(tych v, ex_th0) |
|
705 (mk_case ty_info (vname::aname::names) |
|
706 thy {path=[v], rows=rows}))) |
|
707 end end; |
|
708 |
|
709 |
|
710 (*--------------------------------------------------------------------------- |
|
711 * Constructing induction hypotheses: one for each recursive call. |
|
712 * |
|
713 * Note. R will never occur as a variable in the ind_clause, because |
|
714 * to do so, it would have to be from a nested definition, and we don't |
|
715 * allow nested defns to have R variable. |
|
716 * |
|
717 * Note. When the context is empty, there can be no local variables. |
|
718 *---------------------------------------------------------------------------*) |
|
719 (* |
|
720 local infix 5 ==> |
|
721 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
|
722 in |
|
723 fun build_ih f P (pat,TCs) = |
|
724 let val globals = S.free_vars_lr pat |
|
725 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
|
726 fun dest_TC tm = |
|
727 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
|
728 val (R,y,_) = S.dest_relation R_y_pat |
|
729 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
|
730 in case cntxt |
|
731 of [] => (P_y, (tm,[])) |
|
732 | _ => let |
|
733 val imp = S.list_mk_conj cntxt ==> P_y |
|
734 val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) |
|
735 val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs |
|
736 in (S.list_mk_forall(locals,imp), (tm,locals)) end |
|
737 end |
|
738 in case TCs |
|
739 of [] => (S.list_mk_forall(globals, P$pat), []) |
|
740 | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) |
|
741 val ind_clause = S.list_mk_conj ihs ==> P$pat |
|
742 in (S.list_mk_forall(globals,ind_clause), TCs_locals) |
|
743 end |
|
744 end |
|
745 end; |
|
746 *) |
|
747 |
|
748 local infix 5 ==> |
|
749 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
|
750 in |
|
751 fun build_ih f (P,SV) (pat,TCs) = |
|
752 let val pat_vars = S.free_vars_lr pat |
|
753 val globals = pat_vars@SV |
|
754 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
|
755 fun dest_TC tm = |
|
756 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
|
757 val (R,y,_) = S.dest_relation R_y_pat |
|
758 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
|
759 in case cntxt |
|
760 of [] => (P_y, (tm,[])) |
|
761 | _ => let |
|
762 val imp = S.list_mk_conj cntxt ==> P_y |
|
763 val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) |
|
764 val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs |
|
765 in (S.list_mk_forall(locals,imp), (tm,locals)) end |
|
766 end |
|
767 in case TCs |
|
768 of [] => (S.list_mk_forall(pat_vars, P$pat), []) |
|
769 | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) |
|
770 val ind_clause = S.list_mk_conj ihs ==> P$pat |
|
771 in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals) |
|
772 end |
|
773 end |
|
774 end; |
|
775 |
|
776 (*--------------------------------------------------------------------------- |
|
777 * This function makes good on the promise made in "build_ih". |
|
778 * |
|
779 * Input is tm = "(!y. R y pat ==> P y) ==> P pat", |
|
780 * TCs = TC_1[pat] ... TC_n[pat] |
|
781 * thm = ih1 /\ ... /\ ih_n |- ih[pat] |
|
782 *---------------------------------------------------------------------------*) |
|
783 fun prove_case f thy (tm,TCs_locals,thm) = |
|
784 let val tych = Thry.typecheck thy |
|
785 val antc = tych(#ant(S.dest_imp tm)) |
|
786 val thm' = R.SPEC_ALL thm |
|
787 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
|
788 fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) |
|
789 fun mk_ih ((TC,locals),th2,nested) = |
|
790 R.GENL (map tych locals) |
|
791 (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2 |
|
792 else if S.is_imp (concl TC) then R.IMP_TRANS TC th2 |
|
793 else R.MP th2 TC) |
|
794 in |
|
795 R.DISCH antc |
|
796 (if S.is_imp(concl thm') (* recursive calls in this clause *) |
|
797 then let val th1 = R.ASSUME antc |
|
798 val TCs = map #1 TCs_locals |
|
799 val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o |
|
800 #2 o S.strip_forall) TCs |
|
801 val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs)) |
|
802 TCs_locals |
|
803 val th2list = map (U.C R.SPEC th1 o tych) ylist |
|
804 val nlist = map nested TCs |
|
805 val triples = U.zip3 TClist th2list nlist |
|
806 val Pylist = map mk_ih triples |
|
807 in R.MP thm' (R.LIST_CONJ Pylist) end |
|
808 else thm') |
|
809 end; |
|
810 |
|
811 |
|
812 (*--------------------------------------------------------------------------- |
|
813 * |
|
814 * x = (v1,...,vn) |- M[x] |
|
815 * --------------------------------------------- |
|
816 * ?v1 ... vn. x = (v1,...,vn) |- M[x] |
|
817 * |
|
818 *---------------------------------------------------------------------------*) |
|
819 fun LEFT_ABS_VSTRUCT tych thm = |
|
820 let fun CHOOSER v (tm,thm) = |
|
821 let val ex_tm = S.mk_exists{Bvar=v,Body=tm} |
|
822 in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm) |
|
823 end |
|
824 val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm)) |
|
825 val {lhs,rhs} = S.dest_eq veq |
|
826 val L = S.free_vars_lr rhs |
|
827 in #2 (U.itlist CHOOSER L (veq,thm)) end; |
|
828 |
|
829 |
|
830 (*---------------------------------------------------------------------------- |
|
831 * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)] |
|
832 * |
|
833 * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove |
|
834 * recursion induction (Rinduct) by proving the antecedent of Sinduct from |
|
835 * the antecedent of Rinduct. |
|
836 *---------------------------------------------------------------------------*) |
|
837 fun mk_induction thy {fconst, R, SV, pat_TCs_list} = |
|
838 let val tych = Thry.typecheck thy |
|
839 val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM) |
|
840 val (pats,TCsl) = ListPair.unzip pat_TCs_list |
|
841 val case_thm = complete_cases thy pats |
|
842 val domain = (type_of o hd) pats |
|
843 val Pname = Term.variant (foldr (foldr add_term_names) |
|
844 (pats::TCsl, [])) "P" |
|
845 val P = Free(Pname, domain --> HOLogic.boolT) |
|
846 val Sinduct = R.SPEC (tych P) Sinduction |
|
847 val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) |
|
848 val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list |
|
849 val (Rassums,TCl') = ListPair.unzip Rassums_TCl' |
|
850 val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums)) |
|
851 val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats |
|
852 val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) |
|
853 val proved_cases = map (prove_case fconst thy) tasks |
|
854 val v = Free (variant (foldr add_term_names (map concl proved_cases, [])) |
|
855 "v", |
|
856 domain) |
|
857 val vtyped = tych v |
|
858 val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats |
|
859 val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') |
|
860 (substs, proved_cases) |
|
861 val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1 |
|
862 val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases) |
|
863 val dc = R.MP Sinduct dant |
|
864 val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc))) |
|
865 val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty) |
|
866 val dc' = U.itlist (R.GEN o tych) vars |
|
867 (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc) |
|
868 in |
|
869 R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') |
|
870 end |
|
871 handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation"; |
|
872 |
|
873 |
|
874 |
|
875 |
|
876 (*--------------------------------------------------------------------------- |
|
877 * |
|
878 * POST PROCESSING |
|
879 * |
|
880 *---------------------------------------------------------------------------*) |
|
881 |
|
882 |
|
883 fun simplify_induction thy hth ind = |
|
884 let val tych = Thry.typecheck thy |
|
885 val (asl,_) = R.dest_thm ind |
|
886 val (_,tc_eq_tc') = R.dest_thm hth |
|
887 val tc = S.lhs tc_eq_tc' |
|
888 fun loop [] = ind |
|
889 | loop (asm::rst) = |
|
890 if (can (Thry.match_term thy asm) tc) |
|
891 then R.UNDISCH |
|
892 (R.MATCH_MP |
|
893 (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind)) |
|
894 hth) |
|
895 else loop rst |
|
896 in loop asl |
|
897 end; |
|
898 |
|
899 |
|
900 (*--------------------------------------------------------------------------- |
|
901 * The termination condition is an antecedent to the rule, and an |
|
902 * assumption to the theorem. |
|
903 *---------------------------------------------------------------------------*) |
|
904 fun elim_tc tcthm (rule,induction) = |
|
905 (R.MP rule tcthm, R.PROVE_HYP tcthm induction) |
|
906 |
|
907 |
|
908 fun postprocess{wf_tac, terminator, simplifier} theory {rules,induction,TCs} = |
|
909 let val tych = Thry.typecheck theory |
|
910 |
|
911 (*--------------------------------------------------------------------- |
|
912 * Attempt to eliminate WF condition. It's the only assumption of rules |
|
913 *---------------------------------------------------------------------*) |
|
914 val (rules1,induction1) = |
|
915 let val thm = R.prove(tych(HOLogic.mk_Trueprop |
|
916 (hd(#1(R.dest_thm rules)))), |
|
917 wf_tac) |
|
918 in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction) |
|
919 end handle U.ERR _ => (rules,induction); |
|
920 |
|
921 (*---------------------------------------------------------------------- |
|
922 * The termination condition (tc) is simplified to |- tc = tc' (there |
|
923 * might not be a change!) and then 3 attempts are made: |
|
924 * |
|
925 * 1. if |- tc = T, then eliminate it with eqT; otherwise, |
|
926 * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else |
|
927 * 3. replace tc by tc' in both the rules and the induction theorem. |
|
928 *---------------------------------------------------------------------*) |
|
929 |
|
930 fun print_thms s L = |
|
931 if !trace then writeln (cat_lines (s :: map string_of_thm L)) |
|
932 else (); |
|
933 |
|
934 fun print_cterms s L = |
|
935 if !trace then writeln (cat_lines (s :: map string_of_cterm L)) |
|
936 else ();; |
|
937 |
|
938 fun simplify_tc tc (r,ind) = |
|
939 let val tc1 = tych tc |
|
940 val _ = print_cterms "TC before simplification: " [tc1] |
|
941 val tc_eq = simplifier tc1 |
|
942 val _ = print_thms "result: " [tc_eq] |
|
943 in |
|
944 elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind) |
|
945 handle U.ERR _ => |
|
946 (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) |
|
947 (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), |
|
948 terminator))) |
|
949 (r,ind) |
|
950 handle U.ERR _ => |
|
951 (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), |
|
952 simplify_induction theory tc_eq ind)) |
|
953 end |
|
954 |
|
955 (*---------------------------------------------------------------------- |
|
956 * Nested termination conditions are harder to get at, since they are |
|
957 * left embedded in the body of the function (and in induction |
|
958 * theorem hypotheses). Our "solution" is to simplify them, and try to |
|
959 * prove termination, but leave the application of the resulting theorem |
|
960 * to a higher level. So things go much as in "simplify_tc": the |
|
961 * termination condition (tc) is simplified to |- tc = tc' (there might |
|
962 * not be a change) and then 2 attempts are made: |
|
963 * |
|
964 * 1. if |- tc = T, then return |- tc; otherwise, |
|
965 * 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else |
|
966 * 3. return |- tc = tc' |
|
967 *---------------------------------------------------------------------*) |
|
968 fun simplify_nested_tc tc = |
|
969 let val tc_eq = simplifier (tych (#2 (S.strip_forall tc))) |
|
970 in |
|
971 R.GEN_ALL |
|
972 (R.MATCH_MP Thms.eqT tc_eq |
|
973 handle U.ERR _ => |
|
974 (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) |
|
975 (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))), |
|
976 terminator)) |
|
977 handle U.ERR _ => tc_eq)) |
|
978 end |
|
979 |
|
980 (*------------------------------------------------------------------- |
|
981 * Attempt to simplify the termination conditions in each rule and |
|
982 * in the induction theorem. |
|
983 *-------------------------------------------------------------------*) |
|
984 fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm |
|
985 fun loop ([],extras,R,ind) = (rev R, ind, extras) |
|
986 | loop ((r,ftcs)::rst, nthms, R, ind) = |
|
987 let val tcs = #1(strip_imp (concl r)) |
|
988 val extra_tcs = gen_rems (op aconv) (ftcs, tcs) |
|
989 val extra_tc_thms = map simplify_nested_tc extra_tcs |
|
990 val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind) |
|
991 val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1 |
|
992 in loop(rst, nthms@extra_tc_thms, r2::R, ind1) |
|
993 end |
|
994 val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs) |
|
995 val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1) |
|
996 in |
|
997 {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras} |
|
998 end; |
|
999 |
|
1000 |
|
1001 end; |