author  oheimb 
Thu, 08 Jan 1998 18:09:47 +0100  
changeset 4536  74f7c556fd90 
parent 4226  38c91213f26b 
child 4873  b5999638979e 
permissions  rwrr 
923  1 
(* Title: HOL/thy_syntax.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm 

4 

5 
Additional theory file sections for HOL. 

6 
*) 

7 

8 
(*the kind of distinctiveness axioms depends on number of constructors*) 

2930  9 
val dtK = 7; (* FIXME rename?, move? *) 
923  10 

3622  11 

12 
local 

923  13 

14 
open ThyParse; 

15 

16 

1475  17 
(** typedef **) 
923  18 

1475  19 
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) = 
923  20 
let 
21 
val name' = if_none opt_name t; 

22 
val name = strip_quotes name'; 

23 
in 

24 
(cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt], 

25 
[name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse", 

26 
"Abs_" ^ name ^ "_inverse"]) 

27 
end; 

28 

1475  29 
val typedef_decl = 
923  30 
optional ("(" $$ name $$ ")" >> Some) None  
31 
type_args  name  opt_infix $$ "="  string  opt_witness 

1475  32 
>> mk_typedef_decl; 
923  33 

34 

35 

3980  36 
(** record **) 
37 

38 
val record_decl = 

4225  39 
(type_args  name >> (mk_pair o apfst mk_list)) $$ "=" 
4226  40 
 optional (typ $$ "+" >> (parens o cat "Some")) "None" 
4225  41 
 repeat1 ((name $$ "::"  typ) >> mk_pair) 
4001  42 
>> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); 
3980  43 

44 

923  45 
(** (co)inductive **) 
46 

47 
(*co is either "" or "Co"*) 

48 
fun inductive_decl co = 

49 
let 

50 
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) 

51 
if Syntax.is_identifier s then "op " ^ s else "_"; 

52 
fun mk_params (((recs, ipairs), monos), con_defs) = 

53 
let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs) 

54 
and srec_tms = mk_list recs 

55 
and sintrs = mk_big_list (map snd ipairs) 

3194  56 
val intrnl_name = big_rec_name ^ "_Intrnl" 
923  57 
in 
58 
(";\n\n\ 

3194  59 
\structure " ^ intrnl_name ^ " =\n\ 
923  60 
\ struct\n\ 
61 
\ val _ = writeln \"" ^ co ^ 

62 
"Inductive definition " ^ big_rec_name ^ "\"\n\ 

1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

63 
\ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) " 
923  64 
^ srec_tms ^ "\n\ 
65 
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" 

66 
^ sintrs ^ "\n\ 

1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

67 
\ end;\n\n\ 
923  68 
\val thy = thy > " ^ co ^ "Ind.add_fp_def_i \n (" ^ 
3194  69 
intrnl_name ^ ".rec_tms, " ^ 
70 
intrnl_name ^ ".intr_tms)" 

923  71 
, 
72 
"structure " ^ big_rec_name ^ " =\n\ 

1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

73 
\ let\n\ 
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

74 
\ val _ = writeln \"Proofs for " ^ co ^ 
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

75 
"Inductive definition " ^ big_rec_name ^ "\"\n\ 
923  76 
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ 
3194  77 
\\t (open " ^ intrnl_name ^ "\n\ 
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

78 
\\t val thy\t\t= thy\n\ 
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

79 
\\t val monos\t\t= " ^ monos ^ "\n\ 
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

80 
\\t val con_defs\t\t= " ^ con_defs ^ ");\n\n\ 
1465  81 
\ in\n\ 
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

82 
\ struct\n\ 
923  83 
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ 
84 
\ open Result\n\ 

1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

85 
\ end\n\ 
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset

86 
\ end;\n\n\ 
3194  87 
\structure " ^ intrnl_name ^ " = struct end;\n\n" 
923  88 
) 
89 
end 

90 
val ipairs = "intrs" $$ repeat1 (ident  !! string) 

3403  91 
fun optstring s = optional (s $$ string >> trim) "[]" 
923  92 
in 
1788  93 
repeat1 name  ipairs  optstring "monos"  optstring "con_defs" 
923  94 
>> mk_params 
95 
end; 

96 

97 

98 

99 
(** datatype **) 

100 

101 
local 

102 
(* FIXME err > add_datatype *) 

103 
fun mk_cons cs = 

104 
(case duplicates (map (fst o fst) cs) of 

105 
[] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs 

106 
 dups => error ("Duplicate constructors: " ^ commas_quote dups)); 

107 

108 
(*generate names of distinctiveness axioms*) 

109 
fun mk_distinct_rules cs tname = 

110 
let 

111 
val uqcs = map (fn ((s, _), _) => strip_quotes s) cs; 

112 
(*combine all constructor names with all others w/o duplicates*) 

113 
fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2)); 

114 
fun neg1 [] = [] 

115 
 neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs; 

116 
in 

117 
if length uqcs < dtK then neg1 uqcs 

118 
else quote (tname ^ "_ord_distinct") :: 

119 
map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs 

120 
end; 

121 

122 
fun mk_rules tname cons pre = " map (get_axiom thy) " ^ 

3194  123 
mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons); 
923  124 

1668  125 
(*generate string for calling add_datatype and build_record*) 
923  126 
fun mk_params ((ts, tname), cons) = 
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset

127 
"val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\ 
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

128 
\ Datatype.add_datatype\n" 
923  129 
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\ 
4106  130 
\val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\ 
131 
\val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\ 

3665
3b44fac767f6
Added Larry's test for preventing a datatype shadowing a theory.
nipkow
parents:
3622
diff
changeset

132 
\ (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\ 
3b44fac767f6
Added Larry's test for preventing a datatype shadowing a theory.
nipkow
parents:
3622
diff
changeset

133 
\structure " ^ tname ^ " =\n\ 
923  134 
\struct\n\ 
135 
\ val inject = map (get_axiom thy) " ^ 

136 
mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s)) 

137 
(filter_out (null o snd o fst) cons)) ^ ";\n\ 

138 
\ val distinct = " ^ 

139 
(if length cons < dtK then "let val distinct' = " else "") ^ 

140 
"map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^ 

141 
(if length cons < dtK then 

142 
" in distinct' @ (map (fn t => sym COMP (t RS contrapos))\ 

143 
\ distinct') end" 

144 
else "") ^ ";\n\ 

145 
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ 

146 
\ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\ 

147 
\ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\ 

148 
\ val simps = inject @ distinct @ cases @ recs;\n\ 

149 
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

150 
\end;\n\ 
4106  151 
\val thy = thy > Dtype.add_record " ^ 
152 
mk_triple 

153 
("Sign.intern_tycon (sign_of thy) " ^ quote tname, 

154 
mk_list (map (fst o fst) cons), 

155 
tname ^ ".induct_tac") ^ ";\n\ 

156 
\val dummy = context thy;\n\ 

2930  157 
\val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\ 
158 
\val dummy = AddIffs " ^ tname ^ ".inject;\n\ 

159 
\val dummy = " ^ 

160 
(if length cons < dtK then "AddIffs " else "Addsimps ") ^ 

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

161 
tname ^ ".distinct;\n\ 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset

162 
\val dummy = Addsimps(map (fn (_,eqn) =>\n\ 
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset

163 
\ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^ 
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

164 
"] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\ 
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset

165 
\val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\ 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset

166 
\ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) " 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset

167 
^ quote tname ^ ")) \""^tname^"0\" 1,\n\ 
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset

168 
\ ALLGOALS Asm_simp_tac]);\n\ 
4204  169 
\val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\ 
4106  170 
\ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) " 
171 
^ quote tname ^ ")) \""^tname^"0\" 1,\n\ 

4536  172 
\ ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\ 
4106  173 
\val thy = thy\n"; 
174 

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

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

176 
The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

177 
is a hack. Ideally I would just write exhaust_tac, but the latter extracts the 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

178 
specific exhaustion tactic from the theory associated with the proof 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

179 
state. However, the exhaustion tactic for the current datatype has only just 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

180 
been added to !datatypes (a few lines above) but is not yet associated with 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

181 
the theory. Hope this can be simplified in the future. 
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset

182 
*) 
923  183 

184 
(*parsers*) 

185 
val tvars = type_args >> map (cat "dtVar"); 

1316  186 

187 
val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote)  

188 
type_var >> cat "dtVar"; 

189 

1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset

190 
fun complex_typ toks = 
1316  191 
let val typ = simple_typ  "(" $$ complex_typ $$ ")"; 
192 
val typ2 = complex_typ  "(" $$ complex_typ $$ ")"; 

193 
in 

194 
(typ  repeat (ident>>quote) >> 

195 
(foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y)))  

196 
"(" $$ !! (list1 typ2) $$ ")"  !! (repeat1 (ident>>quote)) >> 

197 
(fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^ 

198 
mk_pair (brackets x, y)) (commas fst, ids))) toks 

199 
end; 

200 

977
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset

201 
val opt_typs = repeat (simple_typ  ("(" $$ complex_typ $$ ")")); 
923  202 
val constructor = name  opt_typs  opt_mixfix; 
203 
in 

204 
val datatype_decl = 

205 
tvars  ident $$ "="  enum1 "" constructor >> mk_params; 

206 
end; 

207 

208 

209 

210 
(** primrec **) 

211 

2922  212 
(*recursion equations have usersupplied names*) 
1845  213 
fun mk_primrec_decl_1 ((fname, tname), axms) = 
923  214 
let 
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset

215 
(*Isolate type name from the structure's identifier it may be stored in*) 
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset

216 
val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); 
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset

217 

923  218 
fun mk_prove (name, eqn) = 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

219 
"val " ^ name ^ " = store_thm (" ^ quote name 
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset

220 
^ ", prove_goalw thy [get_def thy " 
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset

221 
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\ 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

222 
\ (fn _ => [Simp_tac 1]));"; 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

223 

923  224 
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); 
2922  225 
in ("> " ^ tname ^ "_add_primrec " ^ axs 
226 
, 

227 
cat_lines (map mk_prove axms) 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

228 
^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset

229 
end; 
923  230 

2922  231 
(*recursion equations have no names*) 
1845  232 
fun mk_primrec_decl_2 ((fname, tname), axms) = 
233 
let 

234 
(*Isolate type name from the structure's identifier it may be stored in*) 

235 
val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); 

236 

237 
fun mk_prove eqn = 

238 
"prove_goalw thy [get_def thy " 

239 
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \ 

240 
\(fn _ => [Simp_tac 1])"; 

241 

242 
val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms); 

2922  243 
in ("> " ^ tname ^ "_add_primrec " ^ axs 
244 
, 

1845  245 
"val dummy = Addsimps " ^ 
246 
brackets(space_implode ",\n" (map mk_prove axms)) ^ ";") 

247 
end; 

248 

2922  249 
(*function name, argument type and either (name,axiom) pairs or just axioms*) 
923  250 
val primrec_decl = 
1845  251 
(name  long_id  repeat1 (ident  string) >> mk_primrec_decl_1)  
252 
(name  long_id  repeat1 string >> mk_primrec_decl_2) ; 

923  253 

254 

255 

2922  256 

257 
(** rec: interface to Slind's TFL **) 

258 

259 

3194  260 
(*fname: name of function being defined; rel: wellfounded relation*) 
3456  261 
fun mk_rec_decl ((((fname, rel), congs), ss), axms) = 
2922  262 
let val fid = trim fname 
3194  263 
val intrnl_name = fid ^ "_Intrnl" 
2922  264 
in 
265 
(";\n\n\ 

3194  266 
\val _ = writeln \"Recursive function " ^ fid ^ "\"\n\ 
267 
\val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 

3345
4d888ddd6284
Now recdef checks the name of the function being defined.
paulson
parents:
3308
diff
changeset

268 
quote fid ^ " " ^ 
3194  269 
rel ^ "\n" ^ mk_big_list axms ^ ";\n\ 
2922  270 
\val thy = thy" 
271 
, 

3194  272 
"structure " ^ fid ^ " =\n\ 
273 
\ struct\n\ 

274 
\ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\ 

275 
\ val {rules, induct, tcs} = \n\ 

3456  276 
\ \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\ 
277 
\ \t\t (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\ 

3194  278 
\ end;\n\ 
279 
\val pats_" ^ intrnl_name ^ " = ();\n") 

2922  280 
end; 
281 

3403  282 
val rec_decl = (name  string  
3456  283 
optional ("congs" $$ string >> trim) "[]"  
4091  284 
optional ("simpset" $$ string >> trim) "simpset()"  
3403  285 
repeat1 string >> mk_rec_decl) ; 
2922  286 

287 

288 

3622  289 
(** augment thy syntax **) 
923  290 

3622  291 
in 
923  292 

3622  293 
val _ = ThySyn.add_syntax 
294 
["intrs", "monos", "con_defs", "congs", "simpset", ""] 

1475  295 
[axm_section "typedef" "> Typedef.add_typedef" typedef_decl, 
3980  296 
(section "record" "> Record.add_record" record_decl), 
923  297 
("inductive", inductive_decl ""), 
298 
("coinductive", inductive_decl "Co"), 

4106  299 
(section "datatype" "" datatype_decl), 
2922  300 
("primrec", primrec_decl), 
301 
("recdef", rec_decl)]; 

923  302 

303 
end; 