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