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