author  nipkow 
Mon, 09 Feb 1998 18:09:35 +0100  
changeset 4613  67a726003cf8 
parent 4545  4eadc8c2681b 
child 4874  c66a42846887 
permissions  rwrr 
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 

923  81 
(*used for constructor parameters*) 
82 
datatype dt_type = dtVar of string  

83 
dtTyp of dt_type list * string  

84 
dtRek of dt_type list * string; 

85 

86 
structure Datatype = 

87 
struct 

88 
local 

89 

90 
open ThyParse HOLogic; 

91 
exception Impossible; 

92 
exception RecError of string; 

93 

94 
val is_dtRek = (fn dtRek _ => true  _ => false); 

95 
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 

96 

97 
(*  *) 

98 
(* Derivation of the primrec combinator application from the equations *) 

99 

100 
(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *) 

101 

102 
fun subst_apps (_,_) [] t = t 

103 
 subst_apps (fname,rpos) pairs t = 

104 
let 

105 
fun subst (Abs(a,T,t)) = Abs(a,T,subst t) 

106 
 subst (funct $ body) = 

1465  107 
let val (f,b) = strip_comb (funct$body) 
108 
in 

3945  109 
if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname 
1465  110 
then 
111 
let val (ls,rest) = (take(rpos,b), drop(rpos,b)); 

112 
val (xk,rs) = (hd rest,tl rest) 

113 
handle LIST _ => raise RecError "not enough arguments \ 

114 
\ in recursive application on rhs" 

923  115 
in 
1465  116 
(case assoc (pairs,xk) of 
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset

117 
None => list_comb(f, map subst b) 
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset

118 
 Some U => list_comb(U, map subst (ls @ rs))) 
1465  119 
end 
120 
else list_comb(f, map subst b) 

121 
end 

923  122 
 subst(t) = t 
123 
in subst t end; 

124 

125 
(* abstract rhs *) 

126 

127 
fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) = 

2270  128 
let val rargs = (map #1 o 
1465  129 
(filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); 
923  130 
val subs = map (fn (s,T) => (s,dummyT)) 
1465  131 
(rev(rename_wrt_term rhs rargs)); 
923  132 
val subst_rhs = subst_apps (fname,rpos) 
1465  133 
(map Free rargs ~~ map Free subs) rhs; 
923  134 
in 
135 
list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) 

136 
end; 

137 

138 
(* parsing the prim rec equations *) 

139 

140 
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs)) 

141 
= (lhs, rhs) 

142 
 dest_eq _ = raise RecError "not a proper equation"; 

143 

144 
fun dest_rec eq = 

145 
let val (lhs,rhs) = dest_eq eq; 

146 
val (name,args) = strip_comb lhs; 

147 
val (ls',rest) = take_prefix is_Free args; 

148 
val (middle,rs') = take_suffix is_Free rest; 

149 
val rpos = length ls'; 

150 
val (c,cargs') = strip_comb (hd middle) 

151 
handle LIST "hd" => raise RecError "constructor missing"; 

152 
val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs' 

1465  153 
, map dest_Free rs') 
923  154 
handle TERM ("dest_Free",_) => 
1465  155 
raise RecError "constructor has illegal argument in pattern"; 
923  156 
in 
157 
if length middle > 1 then 

158 
raise RecError "more than one nonvariable in pattern" 

159 
else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 

160 
raise RecError "repeated variable name in pattern" 

3945  161 
else (Sign.base_name (fst(dest_Const name)) handle TERM _ => 
1465  162 
raise RecError "function is not declared as constant in theory" 
3945  163 
,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs) 
923  164 
end; 
165 

166 
(* check function specified for all constructors and sort function terms *) 

167 

168 
fun check_and_sort (n,its) = 

169 
if length its = n 

4545  170 
then map snd (Library.sort (int_ord o pairself #1) its) 
923  171 
else raise error "Primrec definition error:\n\ 
172 
\Please give an equation for every constructor"; 

173 

174 
(* translate rec equations into function arguments suitable for rec comb *) 

175 
(* theory parameter needed for printing error messages *) 

176 

177 
fun trans_recs _ _ [] = error("No primrec equations.") 

178 
 trans_recs thy cs' (eq1::eqs) = 

179 
let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1 

180 
handle RecError s => 

1465  181 
error("Primrec definition error: " ^ s ^ ":\n" 
182 
^ " " ^ Sign.string_of_term (sign_of thy) eq1); 

923  183 
val tcs = map (fn (_,c,T,_,_) => (c,T)) cs'; 
184 
val cs = map fst tcs; 

185 
fun trans_recs' _ [] = [] 

186 
 trans_recs' cis (eq::eqs) = 

1465  187 
let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
188 
val tc = assoc(tcs,c); 

4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4184
diff
changeset

189 
val i = 1 + find_index_eq c cs; 
1465  190 
in 
191 
if name <> name1 then 

192 
raise RecError "function names inconsistent" 

193 
else if rpos <> rpos1 then 

194 
raise RecError "position of rec. argument inconsistent" 

195 
else if i = 0 then 

196 
raise RecError "illegal argument in pattern" 

197 
else if i mem cis then 

198 
raise RecError "constructor already occured as pattern " 

199 
else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) 

200 
:: trans_recs' (i::cis) eqs 

201 
end 

202 
handle RecError s => 

203 
error("Primrec definition error\n" ^ s ^ "\n" 

204 
^ " " ^ Sign.string_of_term (sign_of thy) eq); 

923  205 
in ( name1, ls1 
1465  206 
, check_and_sort (length cs, trans_recs' [] (eq1::eqs))) 
923  207 
end ; 
208 

209 
in 

210 
fun add_datatype (typevars, tname, cons_list') thy = 

211 
let 

3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

212 
val dummy = require_thy thy "Arith" "datatype definitions"; 
2880  213 

923  214 
fun typid(dtRek(_,id)) = id 
215 
 typid(dtVar s) = implode (tl (explode s)) 

216 
 typid(dtTyp(_,id)) = id; 

217 

218 
fun index_vnames(vn::vns,tab) = 

219 
(case assoc(tab,vn) of 

220 
None => if vn mem vns 

221 
then (vn^"1") :: index_vnames(vns,(vn,2)::tab) 

222 
else vn :: index_vnames(vns,tab) 

223 
 Some(i) => (vn^(string_of_int i)) :: 

224 
index_vnames(vns,(vn,i+1)::tab)) 

225 
 index_vnames([],tab) = []; 

226 

227 
fun mk_var_names types = index_vnames(map typid types,[]); 

228 

229 
(*search for free type variables and convert recursive *) 

230 
fun analyse_types (cons, types, syn) = 

1465  231 
let fun analyse(t as dtVar v) = 
923  232 
if t mem typevars then t 
233 
else error ("Free type variable " ^ v ^ " on rhs.") 

1465  234 
 analyse(dtTyp(typl,s)) = 
235 
if tname <> s then dtTyp(analyses typl, s) 

923  236 
else if typevars = typl then dtRek(typl, s) 
237 
else error (s ^ " used in different ways") 

1465  238 
 analyse(dtRek _) = raise Impossible 
239 
and analyses ts = map analyse ts; 

240 
in (cons, Syntax.const_name cons syn, analyses types, 

923  241 
mk_var_names types, syn) 
242 
end; 

243 

244 
(*test if all elements are recursive, i.e. if the type is empty*) 

245 

246 
fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = 

1465  247 
not(forall (exists is_dtRek o #3) cs) orelse 
248 
error("Empty datatype not allowed!"); 

923  249 

250 
val cons_list = map analyse_types cons_list'; 

251 
val dummy = non_empty cons_list; 

252 
val num_of_cons = length cons_list; 

253 

254 
(* Auxiliary functions to construct argument and equation lists *) 

255 

256 
(*generate 'var_n, ..., var_m'*) 

257 
fun Args(var, delim, n, m) = 

1465  258 
space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); 
923  259 

260 
fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns); 

261 

262 
(*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *) 

263 
fun arg_eqs vns vns' = 

264 
let fun mkeq(x,x') = x ^ "=" ^ x' 

2270  265 
in space_implode " & " (ListPair.map mkeq (vns,vns')) end; 
923  266 

267 
(*Pretty printers for type lists; 

268 
pp_typlist1: parentheses, pp_typlist2: brackets*) 

1279
f59b4f9f2cdc
All constants introduced by datatype now operate on class term explicitly.
nipkow
parents:
980
diff
changeset

269 
fun pp_typ (dtVar s) = "(" ^ s ^ "::term)" 
923  270 
 pp_typ (dtTyp (typvars, id)) = 
1465  271 
if null typvars then id else (pp_typlist1 typvars) ^ id 
923  272 
 pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id 
273 
and 

1465  274 
pp_typlist' ts = commas (map pp_typ ts) 
923  275 
and 
1465  276 
pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); 
923  277 

278 
fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); 

279 

280 
(* Generate syntax translation for case rules *) 

281 
fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = 

1465  282 
let val arity = length vns; 
283 
val body = "z" ^ string_of_int(c_nr); 

284 
val args1 = if arity=0 then "" 

285 
else " " ^ Args ("y", " ", y_nr, y_nr+arity1); 

286 
val args2 = if arity=0 then "" 

287 
else "(% " ^ Args ("y", " ", y_nr, y_nr+arity1) 

288 
^ ". "; 

289 
val (rest1,rest2) = 

290 
if null cs then ("","") 

291 
else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs 

292 
in ("  " ^ h1, " " ^ h2) end; 

293 
in (name ^ args1 ^ " => " ^ body ^ rest1, 

964  294 
args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2) 
923  295 
end 
296 
 calc_xrules _ _ [] = raise Impossible; 

297 

298 
val xrules = 

1465  299 
let val (first_part, scnd_part) = calc_xrules 1 1 cons_list 
3534  300 
in [Syntax.ParsePrintRule (("logic", "case x of " ^ first_part), 
2031  301 
("logic", tname ^ "_case " ^ scnd_part ^ " x"))] 
1465  302 
end; 
923  303 

304 
(*type declarations for constructors*) 

305 
fun const_type (id, _, typlist, _, syn) = 

1465  306 
(id, 
307 
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ 

308 
pp_typlist1 typevars ^ tname, syn); 

923  309 

310 

311 
fun assumpt (dtRek _ :: ts, v :: vs ,found) = 

1465  312 
let val h = if found then ";P(" ^ v ^ ")" else "[ P(" ^ v ^ ")" 
313 
in h ^ (assumpt (ts, vs, true)) end 

923  314 
 assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) 
315 
 assumpt ([], [], found) = if found then "] ==>" else "" 

316 
 assumpt _ = raise Impossible; 

317 

318 
fun t_inducting ((_, name, types, vns, _) :: cs) = 

1465  319 
let 
320 
val h = if null types then " P(" ^ name ^ ")" 

3842  321 
else " !!" ^ (space_implode " " vns) ^ ". " ^ 
1465  322 
(assumpt (types, vns, false)) ^ 
923  323 
"P(" ^ C_exp name vns ^ ")"; 
1465  324 
val rest = t_inducting cs; 
325 
in if rest = "" then h else h ^ "; " ^ rest end 

923  326 
 t_inducting [] = ""; 
327 

328 
fun t_induct cl typ_name = 

329 
"[" ^ t_inducting cl ^ "] ==> P(" ^ typ_name ^ ")"; 

330 

331 
fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) = 

1465  332 
let val h = if (length ts) > 0 
333 
then pp_typlist2(f ts) ^ "=>" 

334 
else "" 

335 
in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end 

923  336 
 gen_typlist _ _ [] = ""; 
337 

338 

339 
(*  *) 

1465  340 
(* The case constant and rules *) 
341 

923  342 
val t_case = tname ^ "_case"; 
343 

344 
fun case_rule n (id, name, _, vns, _) = 

1465  345 
let val args = if vns = [] then "" else " " ^ space_implode " " vns 
346 
in (t_case ^ "_" ^ id, 

347 
t_case ^ " " ^ Args("f", " ", 1, num_of_cons) 

348 
^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args) 

349 
end 

923  350 

351 
fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs 

352 
 case_rules _ [] = []; 

353 

354 
val datatype_arity = length typevars; 

355 

356 
val types = [(tname, datatype_arity, NoSyn)]; 

357 

358 
val arities = 

359 
let val term_list = replicate datatype_arity termS; 

360 
in [(tname, term_list, termS)] 

1465  361 
end; 
923  362 

363 
val datatype_name = pp_typlist1 typevars ^ tname; 

364 

365 
val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; 

366 

367 
val case_const = 

1465  368 
(t_case, 
369 
"[" ^ gen_typlist new_tvar_name I cons_list 

370 
^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term", 

371 
NoSyn); 

923  372 

373 
val rules_case = case_rules 1 cons_list; 

374 

375 
(*  *) 

1465  376 
(* The primrec combinator *) 
923  377 

378 
val t_rec = tname ^ "_rec" 

379 

380 
(* adding type variables for dtRek types to end of list of dt_types *) 

381 

382 
fun add_reks ts = 

1465  383 
ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
923  384 

385 
(* positions of the dtRek types in a list of dt_types, starting from 1 *) 

2270  386 
fun rek_vars ts vns = map #2 (filter (is_dtRek o fst) (ts ~~ vns)) 
923  387 

388 
fun rec_rule n (id,name,ts,vns,_) = 

1465  389 
let val args = opt_parens(space_implode ") (" vns) 
390 
val fargs = opt_parens(Args("f", ") (", 1, num_of_cons)) 

391 
fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")" 

392 
val rargs = opt_parens(space_implode ") (" 

964  393 
(map rarg (rek_vars ts vns))) 
1465  394 
in 
395 
(t_rec ^ "_" ^ id, 

396 
t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f" 

397 
^ string_of_int(n) ^ args ^ rargs) 

398 
end 

923  399 

400 
fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 

1465  401 
 rec_rules _ [] = []; 
923  402 

403 
val rec_const = 

1465  404 
(t_rec, 
405 
"[" ^ (gen_typlist new_tvar_name add_reks cons_list) 

406 
^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term", 

407 
NoSyn); 

923  408 

409 
val rules_rec = rec_rules 1 cons_list 

410 

411 
(*  *) 

3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

412 
(* The size function *) 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

413 

da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

414 
fun size_eqn(_,name,types,vns,_) = 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

415 
let fun sum((T,vn)::args) = 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

416 
if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args) 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

417 
else sum args 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

418 
 sum [] = "1" 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

419 
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

420 
in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end; 
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 
val size_eqns = map size_eqn cons_list; 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

423 

da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3292
diff
changeset

424 
(*  *) 
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

425 
(* The split equation *) 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

426 

4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

427 
local 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

428 
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

429 

4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

430 
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

431 
let val svns = " " ^ (space_implode " " vns); 
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

432 
val quant = if concl then "!" else "?"; 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

433 
val impl = if concl then " > " else " & ~"; 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

434 
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

435 
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

436 

4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

437 
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

438 
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

439 
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

440 
in 
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

441 
val split_eqn = lhs ^ " = (" ^ rhs true ^ ")" 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

442 
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

443 
end; 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

444 

4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

445 
(*  *) 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
3979
diff
changeset

446 

923  447 
val consts = 
1465  448 
map const_type cons_list 
449 
@ (if num_of_cons < dtK then [] 

450 
else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) 

451 
@ [case_const,rec_const]; 

923  452 

453 

454 
fun Ci_ing ((id, name, _, vns, _) :: cs) = 

1465  455 
if null vns then Ci_ing cs 
456 
else let val vns' = variantlist(vns,vns) 

923  457 
in ("inject_" ^ id, 
1465  458 
"(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns') 
459 
^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs) 

923  460 
end 
1465  461 
 Ci_ing [] = []; 
923  462 

463 
fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) = 

464 
let val vns2' = variantlist(vns2,vns1) 

465 
val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2' 

1465  466 
in (id1 ^ "_not_" ^ id2, ax) end; 
923  467 

468 
fun Ci_neg1 [] = [] 

1465  469 
 Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; 
923  470 

471 
fun suc_expr n = 

1465  472 
if n=0 then "0" else "Suc(" ^ suc_expr(n1) ^ ")"; 
923  473 

474 
fun Ci_neg2() = 

1465  475 
let val ord_t = tname ^ "_ord"; 
2270  476 
val cis = ListPair.zip (cons_list, 0 upto (num_of_cons  1)) 
1465  477 
fun Ci_neg2equals ((id, name, _, vns, _), n) = 
478 
let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n) 

479 
in (ord_t ^ "_" ^ id, ax) end 

480 
in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: 

481 
(map Ci_neg2equals cis) 

482 
end; 

923  483 

484 
val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list 

1465  485 
else Ci_neg2(); 
923  486 

487 
val rules_inject = Ci_ing cons_list; 

488 

489 
val rule_induct = (tname ^ "_induct", t_induct cons_list tname); 

490 

491 
val rules = rule_induct :: 

1465  492 
(rules_inject @ rules_distinct @ rules_case @ rules_rec); 
923  493 

494 
fun add_primrec eqns thy = 

1465  495 
let val rec_comb = Const(t_rec,dummyT) 
496 
val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns 

497 
val (fname,ls,fns) = trans_recs thy cons_list teqns 

498 
val rhs = 

499 
list_abs_free 

500 
(ls @ [(tname,dummyT)] 

501 
,list_comb(rec_comb 

502 
, fns @ map Bound (0 ::(length ls downto 1)))); 

923  503 
val sg = sign_of thy; 
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset

504 
val defpair = (fname ^ "_" ^ tname ^ "_def", 
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1465
diff
changeset

505 
Logic.mk_equals (Const(fname,dummyT), rhs)) 
1465  506 
val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; 
507 
val varT = Type.varifyT T; 

3945  508 
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

509 
in PureThy.add_store_defs_i [defpairT] thy end; 
923  510 

1360  511 
in 
3768  512 
(thy > Theory.add_types types 
513 
> Theory.add_arities arities 

514 
> Theory.add_consts consts 

515 
> Theory.add_trrules xrules 

4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

516 
> PureThy.add_store_axioms rules, 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4107
diff
changeset

517 
add_primrec, size_eqns, (split_eqn,split_eqn_prem)) 
923  518 
end 
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

519 

3564
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

520 
(*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

521 
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

522 
fun occs_in_prems tacf a = 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

523 
SUBGOAL (fn (Bi,i) => 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

524 
(if exists (fn Free(a',_) => a=a') 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

525 
(foldr add_term_frees (#2 (strip_context Bi), [])) 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

526 
then warning "Induction variable occurs also among premises!" 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

527 
else (); 
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

528 
tacf a i)); 
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

529 

7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

530 
end; 
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

531 

7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

532 
end; 
923  533 

534 
(* 

535 
Informal description of functions used in datatype.ML for the Isabelle/HOL 

536 
implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) 

537 

538 
* subst_apps (fname,rpos) pairs t: 

539 
substitute the term 

540 
fname(ls,xk,rs) 

541 
by 

542 
yk(ls,rs) 

543 
in t for (xk,yk) in pairs, where rpos = length ls. 

544 
Applied with : 

545 
fname = function name 

546 
rpos = position of recursive argument 

547 
pairs = list of pairs (xk,yk), where 

548 
xk are the rec. arguments of the constructor in the pattern, 

549 
yk is a variable with name derived from xk 

550 
t = rhs of equation 

551 

552 
* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) 

553 
 filter recursive arguments from constructor arguments cargs, 

554 
 perform substitutions on rhs, 

555 
 derive list subs of new variable names yk for use in subst_apps, 

556 
 abstract rhs with respect to cargs, subs, ls and rs. 

557 

558 
* dest_eq t 

559 
destruct a term denoting an equation into lhs and rhs. 

560 

561 
* dest_req eq 

562 
destruct an equation of the form 

563 
name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs 

564 
into 

565 
 function name (name) 

566 
 position of the first nonvariable parameter (rpos) 

567 
 the list of first rpos parameters (ls = [vl1..vlrpos]) 

568 
 the constructor (fst( dest_Const c) = Ci) 

569 
 the arguments of the constructor (cargs = [vi1..vin]) 

570 
 the rest of the variables in the pattern (rs = [vr1..vrn]) 

571 
 the right hand side of the equation (rhs). 

572 

573 
* check_and_sort (n,its) 

574 
check that n = length its holds, and sort elements of its by 

575 
first component. 

576 

577 
* trans_recs thy cs' (eq1::eqs) 

578 
destruct eq1 into name1, rpos1, ls1, etc.. 

579 
get constructor list with and without type (tcs resp. cs) from cs', 

580 
for every equation: 

581 
destruct it into (name,rpos,ls,c,cargs,rs,rhs) 

582 
get typed constructor tc from c and tcs 

583 
determine the index i of the constructor 

584 
check function name and position of rec. argument by comparison 

585 
with first equation 

586 
check for repeated variable names in pattern 

587 
derive function term f_i which is used as argument of the rec. combinator 

588 
sort the terms f_i according to i and return them together 

589 
with the function name and the parameter of the definition (ls). 

590 

591 
* Application: 

592 

593 
The rec. combinator is applied to the function terms resulting from 

594 
trans_rec. This results in a function which takes the recursive arg. 

595 
as first parameter and then the arguments corresponding to ls. The 

596 
order of parameters is corrected by setting the rhs equal to 

597 

598 
list_abs_free 

1465  599 
(ls @ [(tname,dummyT)] 
600 
,list_comb(rec_comb 

601 
, fns @ map Bound (0 ::(length ls downto 1)))); 

923  602 

603 
Note the deBruijn indices counting the number of lambdas between the 

604 
variable and its binding. 

605 
*) 

1668  606 

607 

608 

609 
(*  *) 

610 
(* The following has been written by Konrad Slind. *) 

611 

612 

3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
2880
diff
changeset

613 
(* type dtype_info is defined in simpdata.ML *) 
1668  614 

615 
signature Dtype_sig = 

616 
sig 

617 
val build_case_cong: Sign.sg > thm list > cterm 

618 
val build_nchotomy: Sign.sg > thm list > cterm 

619 

620 
val prove_case_cong: thm > thm list > cterm > thm 

1690  621 
val prove_nchotomy: (string > int > tactic) > cterm > thm 
1668  622 

623 
val case_thms : Sign.sg > thm list > (string > int > tactic) 

624 
> {nchotomy:thm, case_cong:thm} 

625 

4107  626 
val build_record: theory * (string * string list) * (string > int > tactic) 
627 
> string * datatype_info 

628 
val add_record: string * string list * (string > int > tactic) > theory > theory 

629 
val add_datatype_info: string * datatype_info > theory > theory 

1668  630 
end; 
631 

632 

633 
(* 

634 
* This structure is support for the Isabelle datatype package. It provides 

635 
* entrypoints for 1) building and proving the case congruence theorem for 

636 
* a datatype and 2) building and proving the "exhaustion" theorem for 

637 
* a datatype (I have called this theorem "nchotomy" for no good reason). 

638 
* 

639 
* It also brings all these together in the function "build_record", which 

640 
* is probably what will be used. 

641 
* 

642 
* Since these routines are required in order to support TFL, they have 

643 
* been written so they will compile "standalone", i.e., in IsabelleHOL 

644 
* without any TFL code around. 

645 
**) 

646 
structure Dtype : Dtype_sig = 

647 
struct 

648 

649 
exception DTYPE_ERR of {func:string, mesg:string}; 

650 

651 
(* 

652 
* General support routines 

653 
**) 

654 
fun itlist f L base_value = 

655 
let fun it [] = base_value 

656 
 it (a::rst) = f a (it rst) 

657 
in it L 

658 
end; 

659 

660 
fun end_itlist f = 

661 
let fun endit [] = raise DTYPE_ERR{func="end_itlist", mesg="list too short"} 

662 
 endit alist = 

663 
let val (base::ralist) = rev alist 

664 
in itlist f (rev ralist) base end 

665 
in endit 

666 
end; 

667 

668 
fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]); 

669 

670 

671 
(* 

672 
* Miscellaneous Syntax manipulation 

673 
**) 

674 
val mk_var = Free; 

675 
val mk_const = Const 

676 
fun mk_comb(Rator,Rand) = Rator $ Rand; 

677 
fun mk_abs(r as (Var((s,_),ty),_)) = Abs(s,ty,abstract_over r) 

678 
 mk_abs(r as (Free(s,ty),_)) = Abs(s,ty,abstract_over r) 

679 
 mk_abs _ = raise DTYPE_ERR{func="mk_abs", mesg="1st not a variable"}; 

680 

681 
fun dest_var(Var((s,i),ty)) = (s,ty) 

682 
 dest_var(Free(s,ty)) = (s,ty) 

683 
 dest_var _ = raise DTYPE_ERR{func="dest_var", mesg="not a variable"}; 

684 

685 
fun dest_const(Const p) = p 

686 
 dest_const _ = raise DTYPE_ERR{func="dest_const", mesg="not a constant"}; 

687 

688 
fun dest_comb(t1 $ t2) = (t1,t2) 

689 
 dest_comb _ = raise DTYPE_ERR{func = "dest_comb", mesg = "not a comb"}; 

690 
val rand = #2 o dest_comb; 

691 
val rator = #1 o dest_comb; 

692 

693 
fun dest_abs(a as Abs(s,ty,M)) = 

694 
let val v = Free(s, ty) 

695 
in (v, betapply (a,v)) end 

696 
 dest_abs _ = raise DTYPE_ERR{func="dest_abs", mesg="not an abstraction"}; 

697 

698 

699 
val bool = Type("bool",[]) 

700 
and prop = Type("prop",[]); 

701 

702 
fun mk_eq(lhs,rhs) = 

703 
let val ty = type_of lhs 

704 
val c = mk_const("op =", ty > ty > bool) 

705 
in list_comb(c,[lhs,rhs]) 

706 
end 

707 

708 
fun dest_eq(Const("op =",_) $ M $ N) = (M, N) 

709 
 dest_eq _ = raise DTYPE_ERR{func="dest_eq", mesg="not an equality"}; 

710 

711 
fun mk_disj(disj1,disj2) = 

712 
let val c = Const("op ", bool > bool > bool) 

713 
in list_comb(c,[disj1,disj2]) 

714 
end; 

715 

716 
fun mk_forall (r as (Bvar,_)) = 

717 
let val ty = type_of Bvar 

718 
val c = Const("All", (ty > bool) > bool) 

719 
in mk_comb(c, mk_abs r) 

720 
end; 

721 

722 
fun mk_exists (r as (Bvar,_)) = 

723 
let val ty = type_of Bvar 

724 
val c = Const("Ex", (ty > bool) > bool) 

725 
in mk_comb(c, mk_abs r) 

726 
end; 

727 

728 
fun mk_prop (tm as Const("Trueprop",_) $ _) = tm 

729 
 mk_prop tm = mk_comb(Const("Trueprop", bool > prop),tm); 

730 

731 
fun drop_prop (Const("Trueprop",_) $ X) = X 

732 
 drop_prop X = X; 

733 

734 
fun mk_all (r as (Bvar,_)) = mk_comb(all (type_of Bvar), mk_abs r); 

735 
fun list_mk_all(V,t) = itlist(fn v => fn b => mk_all(v,b)) V t; 

736 
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v,b)) V t; 

737 
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1,tm)) 

738 

739 

740 
fun dest_thm thm = 

741 
let val {prop,hyps,...} = rep_thm thm 

742 
in (map drop_prop hyps, drop_prop prop) 

743 
end; 

744 

745 
val concl = #2 o dest_thm; 

746 

747 

748 
(* 

749 
* Names of all variables occurring in a term, including bound ones. These 

750 
* are added into the second argument. 

3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset

751 
* 
1668  752 
fun add_term_names tm = 
753 
let fun insert (x:string) = 

754 
let fun canfind[] = [x] 

755 
 canfind(alist as (y::rst)) = 

756 
if (x<y) then x::alist 

757 
else if (x=y) then y::rst 

758 
else y::canfind rst 

759 
in canfind end 

760 
fun add (Free(s,_)) V = insert s V 

761 
 add (Var((s,_),_)) V = insert s V 

762 
 add (Abs(s,_,body)) V = add body (insert s V) 

763 
 add (f$t) V = add t (add f V) 

764 
 add _ V = V 

765 
in add tm 

766 
end; 

3265
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset

767 
Why bound ones??? 
8358e19d0d4c
Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents:
3197
diff
changeset

768 
*) 
1668  769 

770 
(* 

771 
* We need to make everything free, so that we can put the term into a 

772 
* goalstack, or submit it as an argument to prove_goalw_cterm. 

773 
**) 

774 
fun make_free_ty(Type(s,alist)) = Type(s,map make_free_ty alist) 

775 
 make_free_ty(TVar((s,i),srt)) = TFree(s,srt) 

776 
 make_free_ty x = x; 

777 

778 
fun make_free (Var((s,_),ty)) = Free(s,make_free_ty ty) 

779 
 make_free (Abs(s,x,body)) = Abs(s,make_free_ty x, make_free body) 

780 
 make_free (f$t) = (make_free f $ make_free t) 

781 
 make_free (Const(s,ty)) = Const(s, make_free_ty ty) 

782 
 make_free (Free(s,ty)) = Free(s, make_free_ty ty) 

783 
 make_free b = b; 

784 

785 

786 
(* 

787 
* Structure of case congruence theorem looks like this: 

788 
* 

789 
* (M = M') 

790 
* ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = f1' x1..xk)) 

791 
* ==> ... 

792 
* ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = fn' x1..xj)) 

793 
* ==> 

794 
* (ty_case f1..fn M = ty_case f1'..fn' m') 

795 
* 

796 
* The input is the list of rules for the case construct for the type, i.e., 

797 
* that found in the "ty.cases" field of a theory where datatype "ty" is 

798 
* defined. 

799 
**) 

800 

801 
fun build_case_cong sign case_rewrites = 

802 
let val clauses = map concl case_rewrites 

803 
val clause1 = hd clauses 

804 
val left = (#1 o dest_eq) clause1 

805 
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

806 
val varnames = foldr add_term_names (clauses, []) 
1668  807 
val M = variant varnames "M" 
808 
val Mvar = Free(M, ty) 

809 
val M' = variant (M::varnames) M 

810 
val M'var = Free(M', ty) 

811 
fun mk_clause clause = 

812 
let val (lhs,rhs) = dest_eq clause 

813 
val func = (#1 o strip_comb) rhs 

814 
val (constr,xbar) = strip_comb(rand lhs) 

815 
val (Name,Ty) = dest_var func 

816 
val func'name = variant (M::M'::varnames) (Name^"a") 

817 
val func' = mk_var(func'name,Ty) 

818 
in (func', list_mk_all 

819 
(xbar, Logic.mk_implies 

820 
(mk_prop(mk_eq(M'var, list_comb(constr,xbar))), 

821 
mk_prop(mk_eq(list_comb(func, xbar), 

822 
list_comb(func',xbar)))))) end 

823 
val (funcs',clauses') = unzip (map mk_clause clauses) 

824 
val lhsM = mk_comb(rator left, Mvar) 

825 
val c = #1(strip_comb left) 

826 
in 

827 
cterm_of sign 

828 
(make_free 

829 
(Logic.list_implies(mk_prop(mk_eq(Mvar, M'var))::clauses', 

830 
mk_prop(mk_eq(lhsM, list_comb(c,(funcs'@[M'var]))))))) 

831 
end 

832 
handle _ => raise DTYPE_ERR{func="build_case_cong",mesg="failed"}; 

833 

834 

835 
(* 

836 
* Proves the result of "build_case_cong". 

1897
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset

837 
* This one solves it a disjunct at a time, and builds the ss only once. 
1668  838 
**) 
839 
fun prove_case_cong nchotomy case_rewrites ctm = 

840 
let val {sign,t,...} = rep_cterm ctm 

841 
val (Const("==>",_) $ tm $ _) = t 

842 
val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm 

843 
val (Free(str,_)) = Ma 

844 
val thm = prove_goalw_cterm[] ctm 

1897
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset

845 
(fn prems => 
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset

846 
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

847 
in [simp_tac (HOL_ss addsimps [hd prems]) 1, 
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset

848 
cut_inst_tac [("x",str)] (nchotomy RS spec) 1, 
71e51870cc9a
Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents:
1810
diff
changeset

849 
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

850 
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

851 
end) 
1668  852 
in standard (thm RS eq_reflection) 
853 
end 

854 
handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"}; 

855 

856 

857 
(* 

858 
* Structure of exhaustion theorem looks like this: 

859 
* 

860 
* !v. (EX y1..yi. v = C1 y1..yi)  ...  (EX y1..yj. v = Cn y1..yj) 

861 
* 

862 
* As for "build_case_cong", the input is the list of rules for the case 

863 
* construct (the case "rewrites"). 

864 
**) 

865 
fun build_nchotomy sign case_rewrites = 

866 
let val clauses = map concl case_rewrites 

867 
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

868 
val varnames = foldr add_term_names (C_ybars, []) 
1668  869 
val vname = variant varnames "v" 
870 
val ty = type_of (hd C_ybars) 

871 
val v = mk_var(vname,ty) 

872 
fun mk_disj C_ybar = 

873 
let val ybar = #2(strip_comb C_ybar) 

874 
in list_mk_exists(ybar, mk_eq(v,C_ybar)) 

875 
end 

876 
in 

877 
cterm_of sign 

878 
(make_free(mk_prop (mk_forall(v, list_mk_disj (map mk_disj C_ybars))))) 

879 
end 

880 
handle _ => raise DTYPE_ERR{func="build_nchotomy",mesg="failed"}; 

881 

882 

883 
(* 

884 
* Takes the induction tactic for the datatype, and the result from 

1690  885 
* "build_nchotomy" 
886 
* 

887 
* !v. (EX y1..yi. v = C1 y1..yi)  ...  (EX y1..yj. v = Cn y1..yj) 

888 
* 

889 
* and proves the theorem. The proof works along a diagonal: the nth 

890 
* disjunct in the nth subgoal is easy to solve. Thus this routine depends 

891 
* on the order of goals arising out of the application of the induction 

892 
* tactic. A more general solution would have to use injectiveness and 

893 
* distinctness rewrite rules. 

1668  894 
**) 
1690  895 
fun prove_nchotomy induct_tac ctm = 
896 
let val (Const ("Trueprop",_) $ g) = #t(rep_cterm ctm) 

1668  897 
val (Const ("All",_) $ Abs (v,_,_)) = g 
1690  898 
(* For goal i, select the correct disjunct to attack, then prove it *) 
899 
fun tac i 0 = (rtac disjI1 i ORELSE all_tac) THEN 

900 
REPEAT (rtac exI i) THEN (rtac refl i) 

901 
 tac i n = rtac disjI2 i THEN tac i (n1) 

1668  902 
in 
903 
prove_goalw_cterm[] ctm 

904 
(fn _ => [rtac allI 1, 

905 
induct_tac v 1, 

1690  906 
ALLGOALS (fn i => tac i (i1))]) 
1668  907 
end 
908 
handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"}; 

909 

3282
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

910 
(* 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

911 
* Turn nchotomy into exhaustion: 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

912 
* [ !!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

913 
* ==> P 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

914 
**) 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

915 
fun mk_exhaust nchotomy = 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

916 
let val tac = rtac impI 1 THEN 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

917 
REPEAT(SOMEGOAL(eresolve_tac [disjE,exE])) 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

918 
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

919 

c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

920 
(* find name of v in exhaustion: *) 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

921 
fun exhaust_var thm = 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

922 
let val _ $ ( _ $ Var((x,_),_) $ _ ) = 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

923 
hd(Logic.strip_assums_hyp(hd(prems_of thm))) 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

924 
in x end; 
1668  925 

926 
(* 

927 
* Brings the preceeding functions together. 

928 
**) 

929 
fun case_thms sign case_rewrites induct_tac = 

1690  930 
let val nchotomy = prove_nchotomy induct_tac 
931 
(build_nchotomy sign case_rewrites) 

1668  932 
val cong = prove_case_cong nchotomy case_rewrites 
933 
(build_case_cong sign case_rewrites) 

934 
in {nchotomy=nchotomy, case_cong=cong} 

935 
end; 

936 

1690  937 

1668  938 
(* 
939 
* Tests 

940 
* 

941 
* 

942 
Dtype.case_thms (sign_of List.thy) List.list.cases List.list.induct_tac; 

943 
Dtype.case_thms (sign_of Prod.thy) [split] 

944 
(fn s => res_inst_tac [("p",s)] PairE_lemma); 

945 
Dtype.case_thms (sign_of Nat.thy) [nat_case_0, nat_case_Suc] nat_ind_tac; 

946 

947 
* 

948 
**) 

949 

950 

951 
(* 

952 
* Given a theory and the name (and constructors) of a datatype declared in 

953 
* an ancestor of that theory and an induction tactic for that datatype, 

954 
* return the information that TFL needs. This should only be called once for 

955 
* a datatype, because "build_record" proves various facts, and thus is slow. 

956 
* It fails on the datatype of pairs, which must be included for TFL to work. 

957 
* The test shows how to build the record for pairs. 

958 
**) 

959 

960 
local fun mk_rw th = (th RS eq_reflection) handle _ => th 

961 
fun get_fact thy s = (get_axiom thy s handle _ => get_thm thy s) 

962 
in 

963 
fun build_record (thy,(ty,cl),itac) = 

964 
let val sign = sign_of thy 

3945  965 
val intern_const = Sign.intern_const sign; 
966 
fun const s = 

967 
let val s' = intern_const s 

968 
in Const(s', the (Sign.const_type sign s')) end 

1668  969 
val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl 
970 
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

971 
val exhaustion = mk_exhaust nchotomy 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

972 
val exh_var = exhaust_var exhaustion; 
4613  973 
fun exhaust_tac a = (res_inst_tac [(exh_var,a)] exhaustion) 
974 
THEN_ALL_NEW (rotate_tac ~1); 

3564
f886dbd91ee5
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents:
3538
diff
changeset

975 
val induct_tac = Datatype.occs_in_prems itac 
1668  976 
in 
977 
(ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl, 

978 
case_const = const (ty^"_case"), 

979 
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

980 
induct_tac = induct_tac, 
1668  981 
nchotomy = nchotomy, 
3282
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

982 
exhaustion = exhaustion, 
c31e6239d4c9
Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents:
3265
diff
changeset

983 
exhaust_tac = exhaust_tac, 
1668  984 
case_cong = case_cong}) 
985 
end 

986 
end; 

987 

988 

4107  989 
fun add_datatype_info info thy = thy > 
990 
ThyData.put_datatypes (Symtab.update (info, ThyData.get_datatypes thy)); 

991 

992 
fun add_record (ty, cl, itac) thy = thy > 

993 
add_datatype_info (build_record (thy, (ty, cl), itac)); 

994 

995 

996 

997 

1668  998 
(* 
999 
* Test 

1000 
* 

1001 
* 

1002 
map Dtype.build_record 

1003 
[(Nat.thy, ("nat",["0", "Suc"]), nat_ind_tac), 

1004 
(List.thy,("list",["[]", "#"]), List.list.induct_tac)] 

1005 
@ 

1006 
[let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 

1007 
(fn s => res_inst_tac [("p",s)] PairE_lemma) 

1008 
fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s)) 

1009 
in ("*", 

1010 
{constructors = [const "Pair"], 

1011 
case_const = const "split", 

1012 
case_rewrites = [split RS eq_reflection], 

1013 
case_cong = #case_cong prod_case_thms, 

1014 
nchotomy = #nchotomy prod_case_thms}) end]; 

1015 

1016 
* 

1017 
**) 

1018 

1019 
end; 