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