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