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