author | oheimb |
Fri, 21 Nov 1997 11:57:58 +0100 | |
changeset 4264 | 5e21f41ccd21 |
parent 4188 | 1025a27b08f9 |
child 4448 | b587d40ad474 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/datatype.ML |
2 |
ID: $Id$ |
|
1668 | 3 |
Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker, |
4 |
Konrad Slind |
|
923 | 5 |
Copyright 1995 TU Muenchen |
6 |
*) |
|
7 |
||
4107 | 8 |
|
9 |
(** theory information about datatypes **) |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
10 |
|
4107 | 11 |
fun datatype_info_sg sg name = |
12 |
(case Symtab.lookup (ThyData.get_datatypes_sg sg, name) of |
|
13 |
Some info => info |
|
14 |
| None => error ("Unknown datatype " ^ quote name)); |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
15 |
|
4107 | 16 |
val datatype_info = datatype_info_sg o sign_of; |
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
17 |
|
4107 | 18 |
fun match_info thy name = |
19 |
let val {case_const, constructors, ...} = datatype_info thy name in |
|
20 |
{case_const = case_const, constructors = constructors} |
|
21 |
end; |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
22 |
|
4107 | 23 |
fun induct_info thy name = |
24 |
let val {constructors, nchotomy, ...} = datatype_info thy name in |
|
25 |
{constructors = constructors, nchotomy = nchotomy} |
|
26 |
end; |
|
27 |
||
28 |
(*retrieve information for all datatypes defined in a theory*) |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
29 |
fun extract_info thy = |
4107 | 30 |
let |
31 |
val infos = map snd (Symtab.dest (ThyData.get_datatypes thy)); |
|
32 |
val (congs, rewrites) = (map #case_cong infos, flat (map #case_rewrites infos)); |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
33 |
in {case_congs = congs, case_rewrites = rewrites} end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
34 |
|
4107 | 35 |
|
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
36 |
local |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
37 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
38 |
fun find_tname var Bi = |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
39 |
let val frees = map dest_Free (term_frees Bi) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
40 |
val params = Logic.strip_params Bi; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
41 |
in case assoc (frees@params, var) of |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
42 |
None => error("No such variable in subgoal: " ^ quote var) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
43 |
| Some(Type(tn,_)) => tn |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
44 |
| _ => error("Cannot induct on type of " ^ quote var) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
45 |
end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
46 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
47 |
fun infer_tname state sign i aterm = |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
48 |
let val (_, _, Bi, _) = dest_state (state, i) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
49 |
val params = Logic.strip_params Bi (*params of subgoal i*) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
50 |
val params = rev(rename_wrt_term Bi params) (*as they are printed*) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
51 |
val (types,sorts) = types_sorts state |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
52 |
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
53 |
| types'(ixn) = types ixn; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
54 |
val (ct,_) = read_def_cterm (sign,types',sorts) [] false |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
55 |
(aterm,TVar(("",0),[])); |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
56 |
in case #T(rep_cterm ct) of |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
57 |
Type(tn,_) => tn |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
58 |
| _ => error("Cannot induct on type of " ^ quote aterm) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
59 |
end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
60 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
61 |
in |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
62 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
63 |
(* generic induction tactic for datatypes *) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
64 |
fun induct_tac var i state = state |> |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
65 |
let val (_, _, Bi, _) = dest_state (state, i) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
66 |
val sign = #sign(rep_thm state) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
67 |
val tn = find_tname var Bi |
4107 | 68 |
val ind_tac = #induct_tac(datatype_info_sg sign tn) |
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
69 |
in ind_tac var i end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
70 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
71 |
(* generic exhaustion tactic for datatypes *) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
72 |
fun exhaust_tac aterm i state = state |> |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
73 |
let val sign = #sign(rep_thm state) |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
74 |
val tn = infer_tname state sign i aterm |
4107 | 75 |
val exh_tac = #exhaust_tac(datatype_info_sg sign tn) |
3615
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
76 |
in exh_tac aterm i end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
77 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
78 |
end; |
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
79 |
|
e5322197cfea
Moved some functions which used to be part of thy_data.ML
berghofe
parents:
3564
diff
changeset
|
80 |
|
3292 | 81 |
(* should go into Pure *) |
3538 | 82 |
fun ALLNEWSUBGOALS tac tacf i st0 = st0 |> |
83 |
(tac i THEN |
|
84 |
(fn st1 => st1 |> |
|
85 |
let val d = nprems_of st1 - nprems_of st0 |
|
86 |
in EVERY(map tacf ((i+d) downto i)) end)); |
|
923 | 87 |
|
88 |
(*used for constructor parameters*) |
|
89 |
datatype dt_type = dtVar of string | |
|
90 |
dtTyp of dt_type list * string | |
|
91 |
dtRek of dt_type list * string; |
|
92 |
||
93 |
structure Datatype = |
|
94 |
struct |
|
95 |
local |
|
96 |
||
97 |
val mysort = sort; |
|
98 |
open ThyParse HOLogic; |
|
99 |
exception Impossible; |
|
100 |
exception RecError of string; |
|
101 |
||
102 |
val is_dtRek = (fn dtRek _ => true | _ => false); |
|
103 |
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; |
|
104 |
||
105 |
(* ----------------------------------------------------------------------- *) |
|
106 |
(* Derivation of the primrec combinator application from the equations *) |
|
107 |
||
108 |
(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *) |
|
109 |
||
110 |
fun subst_apps (_,_) [] t = t |
|
111 |
| subst_apps (fname,rpos) pairs t = |
|
112 |
let |
|
113 |
fun subst (Abs(a,T,t)) = Abs(a,T,subst t) |
|
114 |
| subst (funct $ body) = |
|
1465 | 115 |
let val (f,b) = strip_comb (funct$body) |
116 |
in |
|
3945 | 117 |
if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname |
1465 | 118 |
then |
119 |
let val (ls,rest) = (take(rpos,b), drop(rpos,b)); |
|
120 |
val (xk,rs) = (hd rest,tl rest) |
|
121 |
handle LIST _ => raise RecError "not enough arguments \ |
|
122 |
\ in recursive application on rhs" |
|
923 | 123 |
in |
1465 | 124 |
(case assoc (pairs,xk) of |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset
|
125 |
None => list_comb(f, map subst b) |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset
|
126 |
| Some U => list_comb(U, map subst (ls @ rs))) |
1465 | 127 |
end |
128 |
else list_comb(f, map subst b) |
|
129 |
end |
|
923 | 130 |
| subst(t) = t |
131 |
in subst t end; |
|
132 |
||
133 |
(* abstract rhs *) |
|
134 |
||
135 |
fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) = |
|
2270 | 136 |
let val rargs = (map #1 o |
1465 | 137 |
(filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); |
923 | 138 |
val subs = map (fn (s,T) => (s,dummyT)) |
1465 | 139 |
(rev(rename_wrt_term rhs rargs)); |
923 | 140 |
val subst_rhs = subst_apps (fname,rpos) |
1465 | 141 |
(map Free rargs ~~ map Free subs) rhs; |
923 | 142 |
in |
143 |
list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) |
|
144 |
end; |
|
145 |
||
146 |
(* parsing the prim rec equations *) |
|
147 |
||
148 |
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs)) |
|
149 |
= (lhs, rhs) |
|
150 |
| dest_eq _ = raise RecError "not a proper equation"; |
|
151 |
||
152 |
fun dest_rec eq = |
|
153 |
let val (lhs,rhs) = dest_eq eq; |
|
154 |
val (name,args) = strip_comb lhs; |
|
155 |
val (ls',rest) = take_prefix is_Free args; |
|
156 |
val (middle,rs') = take_suffix is_Free rest; |
|
157 |
val rpos = length ls'; |
|
158 |
val (c,cargs') = strip_comb (hd middle) |
|
159 |
handle LIST "hd" => raise RecError "constructor missing"; |
|
160 |
val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs' |
|
1465 | 161 |
, map dest_Free rs') |
923 | 162 |
handle TERM ("dest_Free",_) => |
1465 | 163 |
raise RecError "constructor has illegal argument in pattern"; |
923 | 164 |
in |
165 |
if length middle > 1 then |
|
166 |
raise RecError "more than one non-variable in pattern" |
|
167 |
else if not(null(findrep (map fst (ls @ rs @ cargs)))) then |
|
168 |
raise RecError "repeated variable name in pattern" |
|
3945 | 169 |
else (Sign.base_name (fst(dest_Const name)) handle TERM _ => |
1465 | 170 |
raise RecError "function is not declared as constant in theory" |
3945 | 171 |
,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs) |
923 | 172 |
end; |
173 |
||
174 |
(* check function specified for all constructors and sort function terms *) |
|
175 |
||
176 |
fun check_and_sort (n,its) = |
|
177 |
if length its = n |
|
178 |
then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its) |
|
179 |
else raise error "Primrec definition error:\n\ |
|
180 |
\Please give an equation for every constructor"; |
|
181 |
||
182 |
(* translate rec equations into function arguments suitable for rec comb *) |
|
183 |
(* theory parameter needed for printing error messages *) |
|
184 |
||
185 |
fun trans_recs _ _ [] = error("No primrec equations.") |
|
186 |
| trans_recs thy cs' (eq1::eqs) = |
|
187 |
let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1 |
|
188 |
handle RecError s => |
|
1465 | 189 |
error("Primrec definition error: " ^ s ^ ":\n" |
190 |
^ " " ^ Sign.string_of_term (sign_of thy) eq1); |
|
923 | 191 |
val tcs = map (fn (_,c,T,_,_) => (c,T)) cs'; |
192 |
val cs = map fst tcs; |
|
193 |
fun trans_recs' _ [] = [] |
|
194 |
| trans_recs' cis (eq::eqs) = |
|
1465 | 195 |
let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; |
196 |
val tc = assoc(tcs,c); |
|
4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4184
diff
changeset
|
197 |
val i = 1 + find_index_eq c cs; |
1465 | 198 |
in |
199 |
if name <> name1 then |
|
200 |
raise RecError "function names inconsistent" |
|
201 |
else if rpos <> rpos1 then |
|
202 |
raise RecError "position of rec. argument inconsistent" |
|
203 |
else if i = 0 then |
|
204 |
raise RecError "illegal argument in pattern" |
|
205 |
else if i mem cis then |
|
206 |
raise RecError "constructor already occured as pattern " |
|
207 |
else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) |
|
208 |
:: trans_recs' (i::cis) eqs |
|
209 |
end |
|
210 |
handle RecError s => |
|
211 |
error("Primrec definition error\n" ^ s ^ "\n" |
|
212 |
^ " " ^ Sign.string_of_term (sign_of thy) eq); |
|
923 | 213 |
in ( name1, ls1 |
1465 | 214 |
, check_and_sort (length cs, trans_recs' [] (eq1::eqs))) |
923 | 215 |
end ; |
216 |
||
217 |
in |
|
218 |
fun add_datatype (typevars, tname, cons_list') thy = |
|
219 |
let |
|
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
220 |
val dummy = require_thy thy "Arith" "datatype definitions"; |
2880 | 221 |
|
923 | 222 |
fun typid(dtRek(_,id)) = id |
223 |
| typid(dtVar s) = implode (tl (explode s)) |
|
224 |
| typid(dtTyp(_,id)) = id; |
|
225 |
||
226 |
fun index_vnames(vn::vns,tab) = |
|
227 |
(case assoc(tab,vn) of |
|
228 |
None => if vn mem vns |
|
229 |
then (vn^"1") :: index_vnames(vns,(vn,2)::tab) |
|
230 |
else vn :: index_vnames(vns,tab) |
|
231 |
| Some(i) => (vn^(string_of_int i)) :: |
|
232 |
index_vnames(vns,(vn,i+1)::tab)) |
|
233 |
| index_vnames([],tab) = []; |
|
234 |
||
235 |
fun mk_var_names types = index_vnames(map typid types,[]); |
|
236 |
||
237 |
(*search for free type variables and convert recursive *) |
|
238 |
fun analyse_types (cons, types, syn) = |
|
1465 | 239 |
let fun analyse(t as dtVar v) = |
923 | 240 |
if t mem typevars then t |
241 |
else error ("Free type variable " ^ v ^ " on rhs.") |
|
1465 | 242 |
| analyse(dtTyp(typl,s)) = |
243 |
if tname <> s then dtTyp(analyses typl, s) |
|
923 | 244 |
else if typevars = typl then dtRek(typl, s) |
245 |
else error (s ^ " used in different ways") |
|
1465 | 246 |
| analyse(dtRek _) = raise Impossible |
247 |
and analyses ts = map analyse ts; |
|
248 |
in (cons, Syntax.const_name cons syn, analyses types, |
|
923 | 249 |
mk_var_names types, syn) |
250 |
end; |
|
251 |
||
252 |
(*test if all elements are recursive, i.e. if the type is empty*) |
|
253 |
||
254 |
fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = |
|
1465 | 255 |
not(forall (exists is_dtRek o #3) cs) orelse |
256 |
error("Empty datatype not allowed!"); |
|
923 | 257 |
|
258 |
val cons_list = map analyse_types cons_list'; |
|
259 |
val dummy = non_empty cons_list; |
|
260 |
val num_of_cons = length cons_list; |
|
261 |
||
262 |
(* Auxiliary functions to construct argument and equation lists *) |
|
263 |
||
264 |
(*generate 'var_n, ..., var_m'*) |
|
265 |
fun Args(var, delim, n, m) = |
|
1465 | 266 |
space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); |
923 | 267 |
|
268 |
fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns); |
|
269 |
||
270 |
(*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *) |
|
271 |
fun arg_eqs vns vns' = |
|
272 |
let fun mkeq(x,x') = x ^ "=" ^ x' |
|
2270 | 273 |
in space_implode " & " (ListPair.map mkeq (vns,vns')) end; |
923 | 274 |
|
275 |
(*Pretty printers for type lists; |
|
276 |
pp_typlist1: parentheses, pp_typlist2: brackets*) |
|
1279
f59b4f9f2cdc
All constants introduced by datatype now operate on class term explicitly.
nipkow
parents:
980
diff
changeset
|
277 |
fun pp_typ (dtVar s) = "(" ^ s ^ "::term)" |
923 | 278 |
| pp_typ (dtTyp (typvars, id)) = |
1465 | 279 |
if null typvars then id else (pp_typlist1 typvars) ^ id |
923 | 280 |
| pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id |
281 |
and |
|
1465 | 282 |
pp_typlist' ts = commas (map pp_typ ts) |
923 | 283 |
and |
1465 | 284 |
pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); |
923 | 285 |
|
286 |
fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); |
|
287 |
||
288 |
(* Generate syntax translation for case rules *) |
|
289 |
fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = |
|
1465 | 290 |
let val arity = length vns; |
291 |
val body = "z" ^ string_of_int(c_nr); |
|
292 |
val args1 = if arity=0 then "" |
|
293 |
else " " ^ Args ("y", " ", y_nr, y_nr+arity-1); |
|
294 |
val args2 = if arity=0 then "" |
|
295 |
else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) |
|
296 |
^ ". "; |
|
297 |
val (rest1,rest2) = |
|
298 |
if null cs then ("","") |
|
299 |
else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs |
|
300 |
in (" | " ^ h1, " " ^ h2) end; |
|
301 |
in (name ^ args1 ^ " => " ^ body ^ rest1, |
|
964 | 302 |
args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2) |
923 | 303 |
end |
304 |
| calc_xrules _ _ [] = raise Impossible; |
|
305 |
||
306 |
val xrules = |
|
1465 | 307 |
let val (first_part, scnd_part) = calc_xrules 1 1 cons_list |
3534 | 308 |
in [Syntax.ParsePrintRule (("logic", "case x of " ^ first_part), |
2031 | 309 |
("logic", tname ^ "_case " ^ scnd_part ^ " x"))] |
1465 | 310 |
end; |
923 | 311 |
|
312 |
(*type declarations for constructors*) |
|
313 |
fun const_type (id, _, typlist, _, syn) = |
|
1465 | 314 |
(id, |
315 |
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ |
|
316 |
pp_typlist1 typevars ^ tname, syn); |
|
923 | 317 |
|
318 |
||
319 |
fun assumpt (dtRek _ :: ts, v :: vs ,found) = |
|
1465 | 320 |
let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" |
321 |
in h ^ (assumpt (ts, vs, true)) end |
|
923 | 322 |
| assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) |
323 |
| assumpt ([], [], found) = if found then "|] ==>" else "" |
|
324 |
| assumpt _ = raise Impossible; |
|
325 |
||
326 |
fun t_inducting ((_, name, types, vns, _) :: cs) = |
|
1465 | 327 |
let |
328 |
val h = if null types then " P(" ^ name ^ ")" |
|
3842 | 329 |
else " !!" ^ (space_implode " " vns) ^ ". " ^ |
1465 | 330 |
(assumpt (types, vns, false)) ^ |
923 | 331 |
"P(" ^ C_exp name vns ^ ")"; |
1465 | 332 |
val rest = t_inducting cs; |
333 |
in if rest = "" then h else h ^ "; " ^ rest end |
|
923 | 334 |
| t_inducting [] = ""; |
335 |
||
336 |
fun t_induct cl typ_name = |
|
337 |
"[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; |
|
338 |
||
339 |
fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) = |
|
1465 | 340 |
let val h = if (length ts) > 0 |
341 |
then pp_typlist2(f ts) ^ "=>" |
|
342 |
else "" |
|
343 |
in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end |
|
923 | 344 |
| gen_typlist _ _ [] = ""; |
345 |
||
346 |
||
347 |
(* -------------------------------------------------------------------- *) |
|
1465 | 348 |
(* The case constant and rules *) |
349 |
||
923 | 350 |
val t_case = tname ^ "_case"; |
351 |
||
352 |
fun case_rule n (id, name, _, vns, _) = |
|
1465 | 353 |
let val args = if vns = [] then "" else " " ^ space_implode " " vns |
354 |
in (t_case ^ "_" ^ id, |
|
355 |
t_case ^ " " ^ Args("f", " ", 1, num_of_cons) |
|
356 |
^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args) |
|
357 |
end |
|
923 | 358 |
|
359 |
fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs |
|
360 |
| case_rules _ [] = []; |
|
361 |
||
362 |
val datatype_arity = length typevars; |
|
363 |
||
364 |
val types = [(tname, datatype_arity, NoSyn)]; |
|
365 |
||
366 |
val arities = |
|
367 |
let val term_list = replicate datatype_arity termS; |
|
368 |
in [(tname, term_list, termS)] |
|
1465 | 369 |
end; |
923 | 370 |
|
371 |
val datatype_name = pp_typlist1 typevars ^ tname; |
|
372 |
||
373 |
val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; |
|
374 |
||
375 |
val case_const = |
|
1465 | 376 |
(t_case, |
377 |
"[" ^ gen_typlist new_tvar_name I cons_list |
|
378 |
^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term", |
|
379 |
NoSyn); |
|
923 | 380 |
|
381 |
val rules_case = case_rules 1 cons_list; |
|
382 |
||
383 |
(* -------------------------------------------------------------------- *) |
|
1465 | 384 |
(* The prim-rec combinator *) |
923 | 385 |
|
386 |
val t_rec = tname ^ "_rec" |
|
387 |
||
388 |
(* adding type variables for dtRek types to end of list of dt_types *) |
|
389 |
||
390 |
fun add_reks ts = |
|
1465 | 391 |
ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); |
923 | 392 |
|
393 |
(* positions of the dtRek types in a list of dt_types, starting from 1 *) |
|
2270 | 394 |
fun rek_vars ts vns = map #2 (filter (is_dtRek o fst) (ts ~~ vns)) |
923 | 395 |
|
396 |
fun rec_rule n (id,name,ts,vns,_) = |
|
1465 | 397 |
let val args = opt_parens(space_implode ") (" vns) |
398 |
val fargs = opt_parens(Args("f", ") (", 1, num_of_cons)) |
|
399 |
fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")" |
|
400 |
val rargs = opt_parens(space_implode ") (" |
|
964 | 401 |
(map rarg (rek_vars ts vns))) |
1465 | 402 |
in |
403 |
(t_rec ^ "_" ^ id, |
|
404 |
t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f" |
|
405 |
^ string_of_int(n) ^ args ^ rargs) |
|
406 |
end |
|
923 | 407 |
|
408 |
fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs |
|
1465 | 409 |
| rec_rules _ [] = []; |
923 | 410 |
|
411 |
val rec_const = |
|
1465 | 412 |
(t_rec, |
413 |
"[" ^ (gen_typlist new_tvar_name add_reks cons_list) |
|
414 |
^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term", |
|
415 |
NoSyn); |
|
923 | 416 |
|
417 |
val rules_rec = rec_rules 1 cons_list |
|
418 |
||
419 |
(* -------------------------------------------------------------------- *) |
|
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
420 |
(* The size function *) |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
421 |
|
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
422 |
fun size_eqn(_,name,types,vns,_) = |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
423 |
let fun sum((T,vn)::args) = |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
424 |
if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args) |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
425 |
else sum args |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
426 |
| sum [] = "1" |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
427 |
val rhs = if exists is_dtRek types then sum(types~~vns) else "0" |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
428 |
in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end; |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
429 |
|
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
430 |
val size_eqns = map size_eqn cons_list; |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
431 |
|
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset
|
432 |
(* -------------------------------------------------------------------- *) |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
433 |
(* The split equation *) |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
434 |
|
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
435 |
local |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
436 |
val fs = map (fn i => "f"^(string_of_int i)) (1 upto num_of_cons); |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
437 |
|
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
438 |
fun split1case concl ((_,name,_,vns,_),fi) = |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
439 |
let val svns = " " ^ (space_implode " " vns); |
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
440 |
val quant = if concl then "!" else "?"; |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
441 |
val impl = if concl then " --> " else " & ~"; |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
442 |
val all = if null vns then "" else quant ^ svns ^ ". " |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
443 |
in "("^all^tname^"0 = "^C_exp name vns^impl^"P("^fi^svns^"))" end; |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
444 |
|
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
445 |
fun rhss concl = map (split1case concl) (cons_list ~~ fs); |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
446 |
fun rhs concl= space_implode(if concl then " & " else " | ")(rhss concl); |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
447 |
val lhs = "P(" ^ t_case ^ " " ^ (space_implode " " fs) ^" "^ tname^"0)" |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
448 |
in |
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
449 |
val split_eqn = lhs ^ " = (" ^ rhs true ^ ")" |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
450 |
val split_eqn_prem = lhs ^ " = ( ~ (" ^ rhs false ^ "))" |
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
451 |
end; |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
452 |
|
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
453 |
(* -------------------------------------------------------------------- *) |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset
|
454 |
|
923 | 455 |
val consts = |
1465 | 456 |
map const_type cons_list |
457 |
@ (if num_of_cons < dtK then [] |
|
458 |
else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) |
|
459 |
@ [case_const,rec_const]; |
|
923 | 460 |
|
461 |
||
462 |
fun Ci_ing ((id, name, _, vns, _) :: cs) = |
|
1465 | 463 |
if null vns then Ci_ing cs |
464 |
else let val vns' = variantlist(vns,vns) |
|
923 | 465 |
in ("inject_" ^ id, |
1465 | 466 |
"(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns') |
467 |
^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs) |
|
923 | 468 |
end |
1465 | 469 |
| Ci_ing [] = []; |
923 | 470 |
|
471 |
fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) = |
|
472 |
let val vns2' = variantlist(vns2,vns1) |
|
473 |
val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2' |
|
1465 | 474 |
in (id1 ^ "_not_" ^ id2, ax) end; |
923 | 475 |
|
476 |
fun Ci_neg1 [] = [] |
|
1465 | 477 |
| Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; |
923 | 478 |
|
479 |
fun suc_expr n = |
|
1465 | 480 |
if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; |
923 | 481 |
|
482 |
fun Ci_neg2() = |
|
1465 | 483 |
let val ord_t = tname ^ "_ord"; |
2270 | 484 |
val cis = ListPair.zip (cons_list, 0 upto (num_of_cons - 1)) |
1465 | 485 |
fun Ci_neg2equals ((id, name, _, vns, _), n) = |
486 |
let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n) |
|
487 |
in (ord_t ^ "_" ^ id, ax) end |
|
488 |
in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: |
|
489 |
(map Ci_neg2equals cis) |
|
490 |
end; |
|
923 | 491 |
|
492 |
val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list |
|
1465 | 493 |
else Ci_neg2(); |
923 | 494 |
|
495 |
val rules_inject = Ci_ing cons_list; |
|
496 |
||
497 |
val rule_induct = (tname ^ "_induct", t_induct cons_list tname); |
|
498 |
||
499 |
val rules = rule_induct :: |
|
1465 | 500 |
(rules_inject @ rules_distinct @ rules_case @ rules_rec); |
923 | 501 |
|
502 |
fun add_primrec eqns thy = |
|
1465 | 503 |
let val rec_comb = Const(t_rec,dummyT) |
504 |
val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns |
|
505 |
val (fname,ls,fns) = trans_recs thy cons_list teqns |
|
506 |
val rhs = |
|
507 |
list_abs_free |
|
508 |
(ls @ [(tname,dummyT)] |
|
509 |
,list_comb(rec_comb |
|
510 |
, fns @ map Bound (0 ::(length ls downto 1)))); |
|
923 | 511 |
val sg = sign_of thy; |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset
|
512 |
val defpair = (fname ^ "_" ^ tname ^ "_def", |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset
|
513 |
Logic.mk_equals (Const(fname,dummyT), rhs)) |
1465 | 514 |
val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; |
515 |
val varT = Type.varifyT T; |
|
3945 | 516 |
val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname)); |
4040
20f7471eedbf
PureThy.add_store_defs_i, PureThy.add_store_axioms;
wenzelm
parents:
4032
diff
changeset
|
517 |
in PureThy.add_store_defs_i [defpairT] thy end; |
923 | 518 |
|
1360 | 519 |
in |
3768 | 520 |
(thy |> Theory.add_types types |
521 |
|> Theory.add_arities arities |
|
522 |
|> Theory.add_consts consts |
|
523 |
|> Theory.add_trrules xrules |
|
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
524 |
|> PureThy.add_store_axioms rules, |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset
|
525 |
add_primrec, size_eqns, (split_eqn,split_eqn_prem)) |
923 | 526 |
end |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
527 |
|
3564
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
528 |
(*Warn if the (induction) variable occurs Free among the premises, which |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
529 |
usually signals a mistake. But calls the tactic either way!*) |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
530 |
fun occs_in_prems tacf a = |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
531 |
SUBGOAL (fn (Bi,i) => |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
532 |
(if exists (fn Free(a',_) => a=a') |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
533 |
(foldr add_term_frees (#2 (strip_context Bi), [])) |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
534 |
then warning "Induction variable occurs also among premises!" |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
535 |
else (); |
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
536 |
tacf a i)); |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
537 |
|
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
538 |
end; |
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
539 |
|
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
540 |
end; |
923 | 541 |
|
542 |
(* |
|
543 |
Informal description of functions used in datatype.ML for the Isabelle/HOL |
|
544 |
implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) |
|
545 |
||
546 |
* subst_apps (fname,rpos) pairs t: |
|
547 |
substitute the term |
|
548 |
fname(ls,xk,rs) |
|
549 |
by |
|
550 |
yk(ls,rs) |
|
551 |
in t for (xk,yk) in pairs, where rpos = length ls. |
|
552 |
Applied with : |
|
553 |
fname = function name |
|
554 |
rpos = position of recursive argument |
|
555 |
pairs = list of pairs (xk,yk), where |
|
556 |
xk are the rec. arguments of the constructor in the pattern, |
|
557 |
yk is a variable with name derived from xk |
|
558 |
t = rhs of equation |
|
559 |
||
560 |
* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) |
|
561 |
- filter recursive arguments from constructor arguments cargs, |
|
562 |
- perform substitutions on rhs, |
|
563 |
- derive list subs of new variable names yk for use in subst_apps, |
|
564 |
- abstract rhs with respect to cargs, subs, ls and rs. |
|
565 |
||
566 |
* dest_eq t |
|
567 |
destruct a term denoting an equation into lhs and rhs. |
|
568 |
||
569 |
* dest_req eq |
|
570 |
destruct an equation of the form |
|
571 |
name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs |
|
572 |
into |
|
573 |
- function name (name) |
|
574 |
- position of the first non-variable parameter (rpos) |
|
575 |
- the list of first rpos parameters (ls = [vl1..vlrpos]) |
|
576 |
- the constructor (fst( dest_Const c) = Ci) |
|
577 |
- the arguments of the constructor (cargs = [vi1..vin]) |
|
578 |
- the rest of the variables in the pattern (rs = [vr1..vrn]) |
|
579 |
- the right hand side of the equation (rhs). |
|
580 |
||
581 |
* check_and_sort (n,its) |
|
582 |
check that n = length its holds, and sort elements of its by |
|
583 |
first component. |
|
584 |
||
585 |
* trans_recs thy cs' (eq1::eqs) |
|
586 |
destruct eq1 into name1, rpos1, ls1, etc.. |
|
587 |
get constructor list with and without type (tcs resp. cs) from cs', |
|
588 |
for every equation: |
|
589 |
destruct it into (name,rpos,ls,c,cargs,rs,rhs) |
|
590 |
get typed constructor tc from c and tcs |
|
591 |
determine the index i of the constructor |
|
592 |
check function name and position of rec. argument by comparison |
|
593 |
with first equation |
|
594 |
check for repeated variable names in pattern |
|
595 |
derive function term f_i which is used as argument of the rec. combinator |
|
596 |
sort the terms f_i according to i and return them together |
|
597 |
with the function name and the parameter of the definition (ls). |
|
598 |
||
599 |
* Application: |
|
600 |
||
601 |
The rec. combinator is applied to the function terms resulting from |
|
602 |
trans_rec. This results in a function which takes the recursive arg. |
|
603 |
as first parameter and then the arguments corresponding to ls. The |
|
604 |
order of parameters is corrected by setting the rhs equal to |
|
605 |
||
606 |
list_abs_free |
|
1465 | 607 |
(ls @ [(tname,dummyT)] |
608 |
,list_comb(rec_comb |
|
609 |
, fns @ map Bound (0 ::(length ls downto 1)))); |
|
923 | 610 |
|
611 |
Note the de-Bruijn indices counting the number of lambdas between the |
|
612 |
variable and its binding. |
|
613 |
*) |
|
1668 | 614 |
|
615 |
||
616 |
||
617 |
(* ----------------------------------------------- *) |
|
618 |
(* The following has been written by Konrad Slind. *) |
|
619 |
||
620 |
||
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
621 |
(* type dtype_info is defined in simpdata.ML *) |
1668 | 622 |
|
623 |
signature Dtype_sig = |
|
624 |
sig |
|
625 |
val build_case_cong: Sign.sg -> thm list -> cterm |
|
626 |
val build_nchotomy: Sign.sg -> thm list -> cterm |
|
627 |
||
628 |
val prove_case_cong: thm -> thm list -> cterm -> thm |
|
1690 | 629 |
val prove_nchotomy: (string -> int -> tactic) -> cterm -> thm |
1668 | 630 |
|
631 |
val case_thms : Sign.sg -> thm list -> (string -> int -> tactic) |
|
632 |
-> {nchotomy:thm, case_cong:thm} |
|
633 |
||
4107 | 634 |
val build_record: theory * (string * string list) * (string -> int -> tactic) |
635 |
-> string * datatype_info |
|
636 |
val add_record: string * string list * (string -> int -> tactic) -> theory -> theory |
|
637 |
val add_datatype_info: string * datatype_info -> theory -> theory |
|
1668 | 638 |
end; |
639 |
||
640 |
||
641 |
(*--------------------------------------------------------------------------- |
|
642 |
* This structure is support for the Isabelle datatype package. It provides |
|
643 |
* entrypoints for 1) building and proving the case congruence theorem for |
|
644 |
* a datatype and 2) building and proving the "exhaustion" theorem for |
|
645 |
* a datatype (I have called this theorem "nchotomy" for no good reason). |
|
646 |
* |
|
647 |
* It also brings all these together in the function "build_record", which |
|
648 |
* is probably what will be used. |
|
649 |
* |
|
650 |
* Since these routines are required in order to support TFL, they have |
|
651 |
* been written so they will compile "stand-alone", i.e., in Isabelle-HOL |
|
652 |
* without any TFL code around. |
|
653 |
*---------------------------------------------------------------------------*) |
|
654 |
structure Dtype : Dtype_sig = |
|
655 |
struct |
|
656 |
||
657 |
exception DTYPE_ERR of {func:string, mesg:string}; |
|
658 |
||
659 |
(*--------------------------------------------------------------------------- |
|
660 |
* General support routines |
|
661 |
*---------------------------------------------------------------------------*) |
|
662 |
fun itlist f L base_value = |
|
663 |
let fun it [] = base_value |
|
664 |
| it (a::rst) = f a (it rst) |
|
665 |
in it L |
|
666 |
end; |
|
667 |
||
668 |
fun end_itlist f = |
|
669 |
let fun endit [] = raise DTYPE_ERR{func="end_itlist", mesg="list too short"} |
|
670 |
| endit alist = |
|
671 |
let val (base::ralist) = rev alist |
|
672 |
in itlist f (rev ralist) base end |
|
673 |
in endit |
|
674 |
end; |
|
675 |
||
676 |
fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]); |
|
677 |
||
678 |
||
679 |
(*--------------------------------------------------------------------------- |
|
680 |
* Miscellaneous Syntax manipulation |
|
681 |
*---------------------------------------------------------------------------*) |
|
682 |
val mk_var = Free; |
|
683 |
val mk_const = Const |
|
684 |
fun mk_comb(Rator,Rand) = Rator $ Rand; |
|
685 |
fun mk_abs(r as (Var((s,_),ty),_)) = Abs(s,ty,abstract_over r) |
|
686 |
| mk_abs(r as (Free(s,ty),_)) = Abs(s,ty,abstract_over r) |
|
687 |
| mk_abs _ = raise DTYPE_ERR{func="mk_abs", mesg="1st not a variable"}; |
|
688 |
||
689 |
fun dest_var(Var((s,i),ty)) = (s,ty) |
|
690 |
| dest_var(Free(s,ty)) = (s,ty) |
|
691 |
| dest_var _ = raise DTYPE_ERR{func="dest_var", mesg="not a variable"}; |
|
692 |
||
693 |
fun dest_const(Const p) = p |
|
694 |
| dest_const _ = raise DTYPE_ERR{func="dest_const", mesg="not a constant"}; |
|
695 |
||
696 |
fun dest_comb(t1 $ t2) = (t1,t2) |
|
697 |
| dest_comb _ = raise DTYPE_ERR{func = "dest_comb", mesg = "not a comb"}; |
|
698 |
val rand = #2 o dest_comb; |
|
699 |
val rator = #1 o dest_comb; |
|
700 |
||
701 |
fun dest_abs(a as Abs(s,ty,M)) = |
|
702 |
let val v = Free(s, ty) |
|
703 |
in (v, betapply (a,v)) end |
|
704 |
| dest_abs _ = raise DTYPE_ERR{func="dest_abs", mesg="not an abstraction"}; |
|
705 |
||
706 |
||
707 |
val bool = Type("bool",[]) |
|
708 |
and prop = Type("prop",[]); |
|
709 |
||
710 |
fun mk_eq(lhs,rhs) = |
|
711 |
let val ty = type_of lhs |
|
712 |
val c = mk_const("op =", ty --> ty --> bool) |
|
713 |
in list_comb(c,[lhs,rhs]) |
|
714 |
end |
|
715 |
||
716 |
fun dest_eq(Const("op =",_) $ M $ N) = (M, N) |
|
717 |
| dest_eq _ = raise DTYPE_ERR{func="dest_eq", mesg="not an equality"}; |
|
718 |
||
719 |
fun mk_disj(disj1,disj2) = |
|
720 |
let val c = Const("op |", bool --> bool --> bool) |
|
721 |
in list_comb(c,[disj1,disj2]) |
|
722 |
end; |
|
723 |
||
724 |
fun mk_forall (r as (Bvar,_)) = |
|
725 |
let val ty = type_of Bvar |
|
726 |
val c = Const("All", (ty --> bool) --> bool) |
|
727 |
in mk_comb(c, mk_abs r) |
|
728 |
end; |
|
729 |
||
730 |
fun mk_exists (r as (Bvar,_)) = |
|
731 |
let val ty = type_of Bvar |
|
732 |
val c = Const("Ex", (ty --> bool) --> bool) |
|
733 |
in mk_comb(c, mk_abs r) |
|
734 |
end; |
|
735 |
||
736 |
fun mk_prop (tm as Const("Trueprop",_) $ _) = tm |
|
737 |
| mk_prop tm = mk_comb(Const("Trueprop", bool --> prop),tm); |
|
738 |
||
739 |
fun drop_prop (Const("Trueprop",_) $ X) = X |
|
740 |
| drop_prop X = X; |
|
741 |
||
742 |
fun mk_all (r as (Bvar,_)) = mk_comb(all (type_of Bvar), mk_abs r); |
|
743 |
fun list_mk_all(V,t) = itlist(fn v => fn b => mk_all(v,b)) V t; |
|
744 |
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v,b)) V t; |
|
745 |
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1,tm)) |
|
746 |
||
747 |
||
748 |
fun dest_thm thm = |
|
749 |
let val {prop,hyps,...} = rep_thm thm |
|
750 |
in (map drop_prop hyps, drop_prop prop) |
|
751 |
end; |
|
752 |
||
753 |
val concl = #2 o dest_thm; |
|
754 |
||
755 |
||
756 |
(*--------------------------------------------------------------------------- |
|
757 |
* Names of all variables occurring in a term, including bound ones. These |
|
758 |
* are added into the second argument. |
|
3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset
|
759 |
*--------------------------------------------------------------------------- |
1668 | 760 |
fun add_term_names tm = |
761 |
let fun insert (x:string) = |
|
762 |
let fun canfind[] = [x] |
|
763 |
| canfind(alist as (y::rst)) = |
|
764 |
if (x<y) then x::alist |
|
765 |
else if (x=y) then y::rst |
|
766 |
else y::canfind rst |
|
767 |
in canfind end |
|
768 |
fun add (Free(s,_)) V = insert s V |
|
769 |
| add (Var((s,_),_)) V = insert s V |
|
770 |
| add (Abs(s,_,body)) V = add body (insert s V) |
|
771 |
| add (f$t) V = add t (add f V) |
|
772 |
| add _ V = V |
|
773 |
in add tm |
|
774 |
end; |
|
3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset
|
775 |
Why bound ones??? |
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset
|
776 |
*) |
1668 | 777 |
|
778 |
(*--------------------------------------------------------------------------- |
|
779 |
* We need to make everything free, so that we can put the term into a |
|
780 |
* goalstack, or submit it as an argument to prove_goalw_cterm. |
|
781 |
*---------------------------------------------------------------------------*) |
|
782 |
fun make_free_ty(Type(s,alist)) = Type(s,map make_free_ty alist) |
|
783 |
| make_free_ty(TVar((s,i),srt)) = TFree(s,srt) |
|
784 |
| make_free_ty x = x; |
|
785 |
||
786 |
fun make_free (Var((s,_),ty)) = Free(s,make_free_ty ty) |
|
787 |
| make_free (Abs(s,x,body)) = Abs(s,make_free_ty x, make_free body) |
|
788 |
| make_free (f$t) = (make_free f $ make_free t) |
|
789 |
| make_free (Const(s,ty)) = Const(s, make_free_ty ty) |
|
790 |
| make_free (Free(s,ty)) = Free(s, make_free_ty ty) |
|
791 |
| make_free b = b; |
|
792 |
||
793 |
||
794 |
(*--------------------------------------------------------------------------- |
|
795 |
* Structure of case congruence theorem looks like this: |
|
796 |
* |
|
797 |
* (M = M') |
|
798 |
* ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = f1' x1..xk)) |
|
799 |
* ==> ... |
|
800 |
* ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = fn' x1..xj)) |
|
801 |
* ==> |
|
802 |
* (ty_case f1..fn M = ty_case f1'..fn' m') |
|
803 |
* |
|
804 |
* The input is the list of rules for the case construct for the type, i.e., |
|
805 |
* that found in the "ty.cases" field of a theory where datatype "ty" is |
|
806 |
* defined. |
|
807 |
*---------------------------------------------------------------------------*) |
|
808 |
||
809 |
fun build_case_cong sign case_rewrites = |
|
810 |
let val clauses = map concl case_rewrites |
|
811 |
val clause1 = hd clauses |
|
812 |
val left = (#1 o dest_eq) clause1 |
|
813 |
val ty = type_of ((#2 o dest_comb) left) |
|
3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset
|
814 |
val varnames = foldr add_term_names (clauses, []) |
1668 | 815 |
val M = variant varnames "M" |
816 |
val Mvar = Free(M, ty) |
|
817 |
val M' = variant (M::varnames) M |
|
818 |
val M'var = Free(M', ty) |
|
819 |
fun mk_clause clause = |
|
820 |
let val (lhs,rhs) = dest_eq clause |
|
821 |
val func = (#1 o strip_comb) rhs |
|
822 |
val (constr,xbar) = strip_comb(rand lhs) |
|
823 |
val (Name,Ty) = dest_var func |
|
824 |
val func'name = variant (M::M'::varnames) (Name^"a") |
|
825 |
val func' = mk_var(func'name,Ty) |
|
826 |
in (func', list_mk_all |
|
827 |
(xbar, Logic.mk_implies |
|
828 |
(mk_prop(mk_eq(M'var, list_comb(constr,xbar))), |
|
829 |
mk_prop(mk_eq(list_comb(func, xbar), |
|
830 |
list_comb(func',xbar)))))) end |
|
831 |
val (funcs',clauses') = unzip (map mk_clause clauses) |
|
832 |
val lhsM = mk_comb(rator left, Mvar) |
|
833 |
val c = #1(strip_comb left) |
|
834 |
in |
|
835 |
cterm_of sign |
|
836 |
(make_free |
|
837 |
(Logic.list_implies(mk_prop(mk_eq(Mvar, M'var))::clauses', |
|
838 |
mk_prop(mk_eq(lhsM, list_comb(c,(funcs'@[M'var]))))))) |
|
839 |
end |
|
840 |
handle _ => raise DTYPE_ERR{func="build_case_cong",mesg="failed"}; |
|
841 |
||
842 |
||
843 |
(*--------------------------------------------------------------------------- |
|
844 |
* Proves the result of "build_case_cong". |
|
1897
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
845 |
* This one solves it a disjunct at a time, and builds the ss only once. |
1668 | 846 |
*---------------------------------------------------------------------------*) |
847 |
fun prove_case_cong nchotomy case_rewrites ctm = |
|
848 |
let val {sign,t,...} = rep_cterm ctm |
|
849 |
val (Const("==>",_) $ tm $ _) = t |
|
850 |
val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm |
|
851 |
val (Free(str,_)) = Ma |
|
852 |
val thm = prove_goalw_cterm[] ctm |
|
1897
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
853 |
(fn prems => |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
854 |
let val simplify = asm_simp_tac(HOL_ss addsimps (prems@case_rewrites)) |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
855 |
in [simp_tac (HOL_ss addsimps [hd prems]) 1, |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
856 |
cut_inst_tac [("x",str)] (nchotomy RS spec) 1, |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
857 |
REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1), |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
858 |
REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)] |
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset
|
859 |
end) |
1668 | 860 |
in standard (thm RS eq_reflection) |
861 |
end |
|
862 |
handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"}; |
|
863 |
||
864 |
||
865 |
(*--------------------------------------------------------------------------- |
|
866 |
* Structure of exhaustion theorem looks like this: |
|
867 |
* |
|
868 |
* !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj) |
|
869 |
* |
|
870 |
* As for "build_case_cong", the input is the list of rules for the case |
|
871 |
* construct (the case "rewrites"). |
|
872 |
*---------------------------------------------------------------------------*) |
|
873 |
fun build_nchotomy sign case_rewrites = |
|
874 |
let val clauses = map concl case_rewrites |
|
875 |
val C_ybars = map (rand o #1 o dest_eq) clauses |
|
3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset
|
876 |
val varnames = foldr add_term_names (C_ybars, []) |
1668 | 877 |
val vname = variant varnames "v" |
878 |
val ty = type_of (hd C_ybars) |
|
879 |
val v = mk_var(vname,ty) |
|
880 |
fun mk_disj C_ybar = |
|
881 |
let val ybar = #2(strip_comb C_ybar) |
|
882 |
in list_mk_exists(ybar, mk_eq(v,C_ybar)) |
|
883 |
end |
|
884 |
in |
|
885 |
cterm_of sign |
|
886 |
(make_free(mk_prop (mk_forall(v, list_mk_disj (map mk_disj C_ybars))))) |
|
887 |
end |
|
888 |
handle _ => raise DTYPE_ERR{func="build_nchotomy",mesg="failed"}; |
|
889 |
||
890 |
||
891 |
(*--------------------------------------------------------------------------- |
|
892 |
* Takes the induction tactic for the datatype, and the result from |
|
1690 | 893 |
* "build_nchotomy" |
894 |
* |
|
895 |
* !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj) |
|
896 |
* |
|
897 |
* and proves the theorem. The proof works along a diagonal: the nth |
|
898 |
* disjunct in the nth subgoal is easy to solve. Thus this routine depends |
|
899 |
* on the order of goals arising out of the application of the induction |
|
900 |
* tactic. A more general solution would have to use injectiveness and |
|
901 |
* distinctness rewrite rules. |
|
1668 | 902 |
*---------------------------------------------------------------------------*) |
1690 | 903 |
fun prove_nchotomy induct_tac ctm = |
904 |
let val (Const ("Trueprop",_) $ g) = #t(rep_cterm ctm) |
|
1668 | 905 |
val (Const ("All",_) $ Abs (v,_,_)) = g |
1690 | 906 |
(* For goal i, select the correct disjunct to attack, then prove it *) |
907 |
fun tac i 0 = (rtac disjI1 i ORELSE all_tac) THEN |
|
908 |
REPEAT (rtac exI i) THEN (rtac refl i) |
|
909 |
| tac i n = rtac disjI2 i THEN tac i (n-1) |
|
1668 | 910 |
in |
911 |
prove_goalw_cterm[] ctm |
|
912 |
(fn _ => [rtac allI 1, |
|
913 |
induct_tac v 1, |
|
1690 | 914 |
ALLGOALS (fn i => tac i (i-1))]) |
1668 | 915 |
end |
916 |
handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"}; |
|
917 |
||
3282
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
918 |
(*--------------------------------------------------------------------------- |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
919 |
* Turn nchotomy into exhaustion: |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
920 |
* [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |] |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
921 |
* ==> P |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
922 |
*---------------------------------------------------------------------------*) |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
923 |
fun mk_exhaust nchotomy = |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
924 |
let val tac = rtac impI 1 THEN |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
925 |
REPEAT(SOMEGOAL(eresolve_tac [disjE,exE])) |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
926 |
in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end; |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
927 |
|
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
928 |
(* find name of v in exhaustion: *) |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
929 |
fun exhaust_var thm = |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
930 |
let val _ $ ( _ $ Var((x,_),_) $ _ ) = |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
931 |
hd(Logic.strip_assums_hyp(hd(prems_of thm))) |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
932 |
in x end; |
1668 | 933 |
|
934 |
(*--------------------------------------------------------------------------- |
|
935 |
* Brings the preceeding functions together. |
|
936 |
*---------------------------------------------------------------------------*) |
|
937 |
fun case_thms sign case_rewrites induct_tac = |
|
1690 | 938 |
let val nchotomy = prove_nchotomy induct_tac |
939 |
(build_nchotomy sign case_rewrites) |
|
1668 | 940 |
val cong = prove_case_cong nchotomy case_rewrites |
941 |
(build_case_cong sign case_rewrites) |
|
942 |
in {nchotomy=nchotomy, case_cong=cong} |
|
943 |
end; |
|
944 |
||
1690 | 945 |
|
1668 | 946 |
(*--------------------------------------------------------------------------- |
947 |
* Tests |
|
948 |
* |
|
949 |
* |
|
950 |
Dtype.case_thms (sign_of List.thy) List.list.cases List.list.induct_tac; |
|
951 |
Dtype.case_thms (sign_of Prod.thy) [split] |
|
952 |
(fn s => res_inst_tac [("p",s)] PairE_lemma); |
|
953 |
Dtype.case_thms (sign_of Nat.thy) [nat_case_0, nat_case_Suc] nat_ind_tac; |
|
954 |
||
955 |
* |
|
956 |
*---------------------------------------------------------------------------*) |
|
957 |
||
958 |
||
959 |
(*--------------------------------------------------------------------------- |
|
960 |
* Given a theory and the name (and constructors) of a datatype declared in |
|
961 |
* an ancestor of that theory and an induction tactic for that datatype, |
|
962 |
* return the information that TFL needs. This should only be called once for |
|
963 |
* a datatype, because "build_record" proves various facts, and thus is slow. |
|
964 |
* It fails on the datatype of pairs, which must be included for TFL to work. |
|
965 |
* The test shows how to build the record for pairs. |
|
966 |
*---------------------------------------------------------------------------*) |
|
967 |
||
968 |
local fun mk_rw th = (th RS eq_reflection) handle _ => th |
|
969 |
fun get_fact thy s = (get_axiom thy s handle _ => get_thm thy s) |
|
970 |
in |
|
971 |
fun build_record (thy,(ty,cl),itac) = |
|
972 |
let val sign = sign_of thy |
|
3945 | 973 |
val intern_const = Sign.intern_const sign; |
974 |
fun const s = |
|
975 |
let val s' = intern_const s |
|
976 |
in Const(s', the (Sign.const_type sign s')) end |
|
1668 | 977 |
val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl |
978 |
val {nchotomy,case_cong} = case_thms sign case_rewrites itac |
|
3282
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
979 |
val exhaustion = mk_exhaust nchotomy |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
980 |
val exh_var = exhaust_var exhaustion; |
3292 | 981 |
fun exhaust_tac a = |
982 |
ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion) |
|
983 |
(rotate_tac ~1); |
|
3564
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset
|
984 |
val induct_tac = Datatype.occs_in_prems itac |
1668 | 985 |
in |
986 |
(ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl, |
|
987 |
case_const = const (ty^"_case"), |
|
988 |
case_rewrites = map mk_rw case_rewrites, |
|
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset
|
989 |
induct_tac = induct_tac, |
1668 | 990 |
nchotomy = nchotomy, |
3282
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
991 |
exhaustion = exhaustion, |
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset
|
992 |
exhaust_tac = exhaust_tac, |
1668 | 993 |
case_cong = case_cong}) |
994 |
end |
|
995 |
end; |
|
996 |
||
997 |
||
4107 | 998 |
fun add_datatype_info info thy = thy |> |
999 |
ThyData.put_datatypes (Symtab.update (info, ThyData.get_datatypes thy)); |
|
1000 |
||
1001 |
fun add_record (ty, cl, itac) thy = thy |> |
|
1002 |
add_datatype_info (build_record (thy, (ty, cl), itac)); |
|
1003 |
||
1004 |
||
1005 |
||
1006 |
||
1668 | 1007 |
(*--------------------------------------------------------------------------- |
1008 |
* Test |
|
1009 |
* |
|
1010 |
* |
|
1011 |
map Dtype.build_record |
|
1012 |
[(Nat.thy, ("nat",["0", "Suc"]), nat_ind_tac), |
|
1013 |
(List.thy,("list",["[]", "#"]), List.list.induct_tac)] |
|
1014 |
@ |
|
1015 |
[let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] |
|
1016 |
(fn s => res_inst_tac [("p",s)] PairE_lemma) |
|
1017 |
fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s)) |
|
1018 |
in ("*", |
|
1019 |
{constructors = [const "Pair"], |
|
1020 |
case_const = const "split", |
|
1021 |
case_rewrites = [split RS eq_reflection], |
|
1022 |
case_cong = #case_cong prod_case_thms, |
|
1023 |
nchotomy = #nchotomy prod_case_thms}) end]; |
|
1024 |
||
1025 |
* |
|
1026 |
*---------------------------------------------------------------------------*) |
|
1027 |
||
1028 |
end; |