author | oheimb |
Wed, 12 Nov 1997 12:34:43 +0100 | |
changeset 4206 | 688050e83d89 |
parent 4204 | 7b15e7eee982 |
child 4225 | 3d9e551bc5a6 |
permissions | -rw-r--r-- |
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 = |
|
39 |
name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" -- |
|
40 |
repeat1 ((name --$$ "::" -- typ) >> mk_pair) |
|
4001 | 41 |
>> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
3980 | 42 |
|
43 |
||
923 | 44 |
(** (co)inductive **) |
45 |
||
46 |
(*co is either "" or "Co"*) |
|
47 |
fun inductive_decl co = |
|
48 |
let |
|
49 |
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |
|
50 |
if Syntax.is_identifier s then "op " ^ s else "_"; |
|
51 |
fun mk_params (((recs, ipairs), monos), con_defs) = |
|
52 |
let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs) |
|
53 |
and srec_tms = mk_list recs |
|
54 |
and sintrs = mk_big_list (map snd ipairs) |
|
3194 | 55 |
val intrnl_name = big_rec_name ^ "_Intrnl" |
923 | 56 |
in |
57 |
(";\n\n\ |
|
3194 | 58 |
\structure " ^ intrnl_name ^ " =\n\ |
923 | 59 |
\ struct\n\ |
60 |
\ val _ = writeln \"" ^ co ^ |
|
61 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
62 |
\ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) " |
923 | 63 |
^ srec_tms ^ "\n\ |
64 |
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" |
|
65 |
^ sintrs ^ "\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
66 |
\ end;\n\n\ |
923 | 67 |
\val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
3194 | 68 |
intrnl_name ^ ".rec_tms, " ^ |
69 |
intrnl_name ^ ".intr_tms)" |
|
923 | 70 |
, |
71 |
"structure " ^ big_rec_name ^ " =\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
72 |
\ let\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
73 |
\ val _ = writeln \"Proofs for " ^ co ^ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
74 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
923 | 75 |
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ |
3194 | 76 |
\\t (open " ^ intrnl_name ^ "\n\ |
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
77 |
\\t val thy\t\t= thy\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
78 |
\\t val monos\t\t= " ^ monos ^ "\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
79 |
\\t val con_defs\t\t= " ^ con_defs ^ ");\n\n\ |
1465 | 80 |
\ in\n\ |
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
81 |
\ struct\n\ |
923 | 82 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ |
83 |
\ open Result\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
84 |
\ end\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
85 |
\ end;\n\n\ |
3194 | 86 |
\structure " ^ intrnl_name ^ " = struct end;\n\n" |
923 | 87 |
) |
88 |
end |
|
89 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
3403 | 90 |
fun optstring s = optional (s $$-- string >> trim) "[]" |
923 | 91 |
in |
1788 | 92 |
repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs" |
923 | 93 |
>> mk_params |
94 |
end; |
|
95 |
||
96 |
||
97 |
||
98 |
(** datatype **) |
|
99 |
||
100 |
local |
|
101 |
(* FIXME err -> add_datatype *) |
|
102 |
fun mk_cons cs = |
|
103 |
(case duplicates (map (fst o fst) cs) of |
|
104 |
[] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs |
|
105 |
| dups => error ("Duplicate constructors: " ^ commas_quote dups)); |
|
106 |
||
107 |
(*generate names of distinctiveness axioms*) |
|
108 |
fun mk_distinct_rules cs tname = |
|
109 |
let |
|
110 |
val uqcs = map (fn ((s, _), _) => strip_quotes s) cs; |
|
111 |
(*combine all constructor names with all others w/o duplicates*) |
|
112 |
fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2)); |
|
113 |
fun neg1 [] = [] |
|
114 |
| neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs; |
|
115 |
in |
|
116 |
if length uqcs < dtK then neg1 uqcs |
|
117 |
else quote (tname ^ "_ord_distinct") :: |
|
118 |
map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs |
|
119 |
end; |
|
120 |
||
121 |
fun mk_rules tname cons pre = " map (get_axiom thy) " ^ |
|
3194 | 122 |
mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons); |
923 | 123 |
|
1668 | 124 |
(*generate string for calling add_datatype and build_record*) |
923 | 125 |
fun mk_params ((ts, tname), cons) = |
4184
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset
|
126 |
"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
|
127 |
\ Datatype.add_datatype\n" |
923 | 128 |
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\ |
4106 | 129 |
\val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\ |
130 |
\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
|
131 |
\ (\"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
|
132 |
\structure " ^ tname ^ " =\n\ |
923 | 133 |
\struct\n\ |
134 |
\ val inject = map (get_axiom thy) " ^ |
|
135 |
mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s)) |
|
136 |
(filter_out (null o snd o fst) cons)) ^ ";\n\ |
|
137 |
\ val distinct = " ^ |
|
138 |
(if length cons < dtK then "let val distinct' = " else "") ^ |
|
139 |
"map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^ |
|
140 |
(if length cons < dtK then |
|
141 |
" in distinct' @ (map (fn t => sym COMP (t RS contrapos))\ |
|
142 |
\ distinct') end" |
|
143 |
else "") ^ ";\n\ |
|
144 |
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ |
|
145 |
\ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\ |
|
146 |
\ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\ |
|
147 |
\ val simps = inject @ distinct @ cases @ recs;\n\ |
|
148 |
\ 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
|
149 |
\end;\n\ |
4106 | 150 |
\val thy = thy |> Dtype.add_record " ^ |
151 |
mk_triple |
|
152 |
("Sign.intern_tycon (sign_of thy) " ^ quote tname, |
|
153 |
mk_list (map (fst o fst) cons), |
|
154 |
tname ^ ".induct_tac") ^ ";\n\ |
|
155 |
\val dummy = context thy;\n\ |
|
2930 | 156 |
\val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\ |
157 |
\val dummy = AddIffs " ^ tname ^ ".inject;\n\ |
|
158 |
\val dummy = " ^ |
|
159 |
(if length cons < dtK then "AddIffs " else "Addsimps ") ^ |
|
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
160 |
tname ^ ".distinct;\n\ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
161 |
\val dummy = Addsimps(map (fn (_,eqn) =>\n\ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
162 |
\ 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
|
163 |
"] 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
|
164 |
\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
|
165 |
\ (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
|
166 |
^ quote tname ^ ")) \""^tname^"0\" 1,\n\ |
23a09f2fd687
Each datatype t now proves a theorem split_t_case_prem
nipkow
parents:
4106
diff
changeset
|
167 |
\ ALLGOALS Asm_simp_tac]);\n\ |
4204 | 168 |
\val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\ |
4106 | 169 |
\ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) " |
170 |
^ quote tname ^ ")) \""^tname^"0\" 1,\n\ |
|
171 |
\ ALLGOALS Asm_simp_tac]);\n\ |
|
172 |
\val thy = thy\n"; |
|
173 |
||
4032
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset
|
174 |
(* |
4b1c69d8b767
For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents:
4001
diff
changeset
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
*) |
923 | 182 |
|
183 |
(*parsers*) |
|
184 |
val tvars = type_args >> map (cat "dtVar"); |
|
1316 | 185 |
|
186 |
val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) || |
|
187 |
type_var >> cat "dtVar"; |
|
188 |
||
1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
189 |
fun complex_typ toks = |
1316 | 190 |
let val typ = simple_typ || "(" $$-- complex_typ --$$ ")"; |
191 |
val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")"; |
|
192 |
in |
|
193 |
(typ -- repeat (ident>>quote) >> |
|
194 |
(foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) || |
|
195 |
"(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >> |
|
196 |
(fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^ |
|
197 |
mk_pair (brackets x, y)) (commas fst, ids))) toks |
|
198 |
end; |
|
199 |
||
977
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset
|
200 |
val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); |
923 | 201 |
val constructor = name -- opt_typs -- opt_mixfix; |
202 |
in |
|
203 |
val datatype_decl = |
|
204 |
tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params; |
|
205 |
end; |
|
206 |
||
207 |
||
208 |
||
209 |
(** primrec **) |
|
210 |
||
2922 | 211 |
(*recursion equations have user-supplied names*) |
1845 | 212 |
fun mk_primrec_decl_1 ((fname, tname), axms) = |
923 | 213 |
let |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
214 |
(*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
|
215 |
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
|
216 |
|
923 | 217 |
fun mk_prove (name, eqn) = |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
218 |
"val " ^ name ^ " = store_thm (" ^ quote name |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
219 |
^ ", prove_goalw thy [get_def thy " |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
220 |
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\ |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
221 |
\ (fn _ => [Simp_tac 1]));"; |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
222 |
|
923 | 223 |
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
2922 | 224 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs |
225 |
, |
|
226 |
cat_lines (map mk_prove axms) |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
227 |
^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
228 |
end; |
923 | 229 |
|
2922 | 230 |
(*recursion equations have no names*) |
1845 | 231 |
fun mk_primrec_decl_2 ((fname, tname), axms) = |
232 |
let |
|
233 |
(*Isolate type name from the structure's identifier it may be stored in*) |
|
234 |
val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); |
|
235 |
||
236 |
fun mk_prove eqn = |
|
237 |
"prove_goalw thy [get_def thy " |
|
238 |
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \ |
|
239 |
\(fn _ => [Simp_tac 1])"; |
|
240 |
||
241 |
val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms); |
|
2922 | 242 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs |
243 |
, |
|
1845 | 244 |
"val dummy = Addsimps " ^ |
245 |
brackets(space_implode ",\n" (map mk_prove axms)) ^ ";") |
|
246 |
end; |
|
247 |
||
2922 | 248 |
(*function name, argument type and either (name,axiom) pairs or just axioms*) |
923 | 249 |
val primrec_decl = |
1845 | 250 |
(name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) || |
251 |
(name -- long_id -- repeat1 string >> mk_primrec_decl_2) ; |
|
923 | 252 |
|
253 |
||
254 |
||
2922 | 255 |
|
256 |
(** rec: interface to Slind's TFL **) |
|
257 |
||
258 |
||
3194 | 259 |
(*fname: name of function being defined; rel: well-founded relation*) |
3456 | 260 |
fun mk_rec_decl ((((fname, rel), congs), ss), axms) = |
2922 | 261 |
let val fid = trim fname |
3194 | 262 |
val intrnl_name = fid ^ "_Intrnl" |
2922 | 263 |
in |
264 |
(";\n\n\ |
|
3194 | 265 |
\val _ = writeln \"Recursive function " ^ fid ^ "\"\n\ |
266 |
\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
|
267 |
quote fid ^ " " ^ |
3194 | 268 |
rel ^ "\n" ^ mk_big_list axms ^ ";\n\ |
2922 | 269 |
\val thy = thy" |
270 |
, |
|
3194 | 271 |
"structure " ^ fid ^ " =\n\ |
272 |
\ struct\n\ |
|
273 |
\ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\ |
|
274 |
\ val {rules, induct, tcs} = \n\ |
|
3456 | 275 |
\ \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\ |
276 |
\ \t\t (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\ |
|
3194 | 277 |
\ end;\n\ |
278 |
\val pats_" ^ intrnl_name ^ " = ();\n") |
|
2922 | 279 |
end; |
280 |
||
3403 | 281 |
val rec_decl = (name -- string -- |
3456 | 282 |
optional ("congs" $$-- string >> trim) "[]" -- |
4091 | 283 |
optional ("simpset" $$-- string >> trim) "simpset()" -- |
3403 | 284 |
repeat1 string >> mk_rec_decl) ; |
2922 | 285 |
|
286 |
||
287 |
||
3622 | 288 |
(** augment thy syntax **) |
923 | 289 |
|
3622 | 290 |
in |
923 | 291 |
|
3622 | 292 |
val _ = ThySyn.add_syntax |
293 |
["intrs", "monos", "con_defs", "congs", "simpset", "|"] |
|
1475 | 294 |
[axm_section "typedef" "|> Typedef.add_typedef" typedef_decl, |
3980 | 295 |
(section "record" "|> Record.add_record" record_decl), |
923 | 296 |
("inductive", inductive_decl ""), |
297 |
("coinductive", inductive_decl "Co"), |
|
4106 | 298 |
(section "datatype" "" datatype_decl), |
2922 | 299 |
("primrec", primrec_decl), |
300 |
("recdef", rec_decl)]; |
|
923 | 301 |
|
302 |
end; |