1941
|
1 |
theory NewParser
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2 |
imports "../Nominal-General/Nominal2_Base"
|
1941
|
3 |
"../Nominal-General/Nominal2_Eqvt"
|
|
4 |
"../Nominal-General/Nominal2_Supp"
|
1992
|
5 |
"Perm" "NewFv" "NewAlpha"
|
1941
|
6 |
begin
|
|
7 |
|
|
8 |
section{* Interface for nominal_datatype *}
|
|
9 |
|
|
10 |
|
|
11 |
ML {*
|
|
12 |
(* nominal datatype parser *)
|
|
13 |
local
|
|
14 |
structure P = OuterParse;
|
|
15 |
structure S = Scan
|
|
16 |
|
|
17 |
fun triple1 ((x, y), z) = (x, y, z)
|
|
18 |
fun triple2 (x, (y, z)) = (x, y, z)
|
|
19 |
fun tuple ((x, y, z), u) = (x, y, z, u)
|
|
20 |
fun tswap (((x, y), z), u) = (x, y, u, z)
|
|
21 |
in
|
|
22 |
|
|
23 |
val _ = OuterKeyword.keyword "bind"
|
|
24 |
val _ = OuterKeyword.keyword "bind_set"
|
|
25 |
val _ = OuterKeyword.keyword "bind_res"
|
|
26 |
|
1943
|
27 |
val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
|
1941
|
28 |
|
|
29 |
val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res"
|
|
30 |
|
|
31 |
val bind_clauses =
|
|
32 |
P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
|
|
33 |
|
|
34 |
val cnstr_parser =
|
1943
|
35 |
P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
|
1941
|
36 |
|
|
37 |
(* datatype parser *)
|
|
38 |
val dt_parser =
|
|
39 |
(P.type_args -- P.binding -- P.opt_mixfix >> triple1) --
|
1943
|
40 |
(P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
|
1941
|
41 |
|
|
42 |
(* binding function parser *)
|
|
43 |
val bnfun_parser =
|
1944
|
44 |
S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
|
1941
|
45 |
|
|
46 |
(* main parser *)
|
|
47 |
val main_parser =
|
1944
|
48 |
P.and_list1 dt_parser -- bnfun_parser >> triple2
|
1941
|
49 |
|
|
50 |
end
|
|
51 |
*}
|
|
52 |
|
|
53 |
ML {*
|
|
54 |
fun get_cnstrs dts =
|
|
55 |
map (fn (_, _, _, constrs) => constrs) dts
|
|
56 |
|
|
57 |
fun get_typed_cnstrs dts =
|
|
58 |
flat (map (fn (_, bn, _, constrs) =>
|
|
59 |
(map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
|
|
60 |
|
|
61 |
fun get_cnstr_strs dts =
|
|
62 |
map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
|
|
63 |
|
|
64 |
fun get_bn_fun_strs bn_funs =
|
|
65 |
map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
|
|
66 |
*}
|
|
67 |
|
|
68 |
ML {*
|
|
69 |
fun add_primrec_wrapper funs eqs lthy =
|
|
70 |
if null funs then (([], []), lthy)
|
|
71 |
else
|
|
72 |
let
|
|
73 |
val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
|
|
74 |
val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
|
|
75 |
in
|
|
76 |
Primrec.add_primrec funs' eqs' lthy
|
|
77 |
end
|
|
78 |
*}
|
|
79 |
|
|
80 |
ML {*
|
|
81 |
fun add_datatype_wrapper dt_names dts =
|
|
82 |
let
|
|
83 |
val conf = Datatype.default_config
|
|
84 |
in
|
|
85 |
Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)
|
|
86 |
end
|
|
87 |
*}
|
|
88 |
|
1944
|
89 |
|
|
90 |
text {* Infrastructure for adding "_raw" to types and terms *}
|
|
91 |
|
1941
|
92 |
ML {*
|
|
93 |
fun add_raw s = s ^ "_raw"
|
|
94 |
fun add_raws ss = map add_raw ss
|
|
95 |
fun raw_bind bn = Binding.suffix_name "_raw" bn
|
|
96 |
|
|
97 |
fun replace_str ss s =
|
|
98 |
case (AList.lookup (op=) ss s) of
|
|
99 |
SOME s' => s'
|
|
100 |
| NONE => s
|
|
101 |
|
|
102 |
fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
|
|
103 |
| replace_typ ty_ss T = T
|
|
104 |
|
|
105 |
fun raw_dts ty_ss dts =
|
|
106 |
let
|
|
107 |
fun raw_dts_aux1 (bind, tys, mx) =
|
|
108 |
(raw_bind bind, map (replace_typ ty_ss) tys, mx)
|
|
109 |
|
|
110 |
fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
|
|
111 |
(ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
|
|
112 |
in
|
|
113 |
map raw_dts_aux2 dts
|
|
114 |
end
|
|
115 |
|
|
116 |
fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
|
|
117 |
| replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
|
|
118 |
| replace_aterm trm_ss trm = trm
|
|
119 |
|
|
120 |
fun replace_term trm_ss ty_ss trm =
|
|
121 |
trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss)
|
|
122 |
*}
|
|
123 |
|
|
124 |
ML {*
|
|
125 |
fun rawify_dts dt_names dts dts_env =
|
|
126 |
let
|
|
127 |
val raw_dts = raw_dts dts_env dts
|
|
128 |
val raw_dt_names = add_raws dt_names
|
|
129 |
in
|
|
130 |
(raw_dt_names, raw_dts)
|
|
131 |
end
|
|
132 |
*}
|
|
133 |
|
|
134 |
ML {*
|
|
135 |
fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
|
|
136 |
let
|
|
137 |
val bn_funs' = map (fn (bn, ty, mx) =>
|
|
138 |
(raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
|
|
139 |
|
|
140 |
val bn_eqs' = map (fn (attr, trm) =>
|
|
141 |
(attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
|
|
142 |
in
|
|
143 |
(bn_funs', bn_eqs')
|
|
144 |
end
|
|
145 |
*}
|
|
146 |
|
|
147 |
ML {*
|
|
148 |
fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses =
|
|
149 |
let
|
|
150 |
fun rawify_bnds bnds =
|
|
151 |
map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
|
|
152 |
|
|
153 |
fun rawify_bclause (BEmy n) = BEmy n
|
|
154 |
| rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys)
|
|
155 |
| rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys)
|
|
156 |
| rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys)
|
|
157 |
in
|
|
158 |
map (map (map rawify_bclause)) bclauses
|
|
159 |
end
|
|
160 |
*}
|
|
161 |
|
1942
d3b89f6c086a
added a comment about a function where I am not sure who wrote it.
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
text {* What does the prep_bn code do? Cezary's Function? *}
|
1941
|
163 |
|
|
164 |
ML {*
|
|
165 |
fun strip_bn_fun t =
|
|
166 |
case t of
|
|
167 |
Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
|
|
168 |
| Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
|
|
169 |
| Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
|
|
170 |
(i, NONE) :: strip_bn_fun y
|
|
171 |
| Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
|
|
172 |
(i, NONE) :: strip_bn_fun y
|
|
173 |
| Const (@{const_name bot}, _) => []
|
|
174 |
| Const (@{const_name Nil}, _) => []
|
|
175 |
| (f as Free _) $ Bound i => [(i, SOME f)]
|
|
176 |
| _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
|
|
177 |
*}
|
|
178 |
|
|
179 |
ML {*
|
|
180 |
fun find [] _ = error ("cannot find element")
|
|
181 |
| find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
|
|
182 |
*}
|
|
183 |
|
|
184 |
ML {*
|
|
185 |
fun prep_bn dt_names dts eqs =
|
|
186 |
let
|
|
187 |
fun aux eq =
|
|
188 |
let
|
|
189 |
val (lhs, rhs) = eq
|
|
190 |
|> strip_qnt_body "all"
|
|
191 |
|> HOLogic.dest_Trueprop
|
|
192 |
|> HOLogic.dest_eq
|
|
193 |
val (bn_fun, [cnstr]) = strip_comb lhs
|
|
194 |
val (_, ty) = dest_Free bn_fun
|
|
195 |
val (ty_name, _) = dest_Type (domain_type ty)
|
|
196 |
val dt_index = find_index (fn x => x = ty_name) dt_names
|
|
197 |
val (cnstr_head, cnstr_args) = strip_comb cnstr
|
|
198 |
val rhs_elements = strip_bn_fun rhs
|
|
199 |
val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
|
|
200 |
in
|
|
201 |
(dt_index, (bn_fun, (cnstr_head, included)))
|
|
202 |
end
|
|
203 |
fun order dts i ts =
|
|
204 |
let
|
|
205 |
val dt = nth dts i
|
|
206 |
val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
|
|
207 |
val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
|
|
208 |
in
|
|
209 |
map (find ts') cts
|
|
210 |
end
|
|
211 |
|
|
212 |
val unordered = AList.group (op=) (map aux eqs)
|
|
213 |
val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered
|
|
214 |
val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered'
|
|
215 |
in
|
|
216 |
ordered
|
|
217 |
end
|
|
218 |
*}
|
|
219 |
|
|
220 |
|
|
221 |
ML {*
|
|
222 |
fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
|
|
223 |
let
|
|
224 |
val thy = ProofContext.theory_of lthy
|
|
225 |
val thy_name = Context.theory_name thy
|
|
226 |
|
|
227 |
val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
|
|
228 |
val dt_full_names = map (Long_Name.qualify thy_name) dt_names
|
|
229 |
val dt_full_names' = add_raws dt_full_names
|
|
230 |
val dts_env = dt_full_names ~~ dt_full_names'
|
|
231 |
|
|
232 |
val cnstrs = get_cnstr_strs dts
|
|
233 |
val cnstrs_ty = get_typed_cnstrs dts
|
|
234 |
val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
|
|
235 |
val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
|
|
236 |
(Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
|
|
237 |
val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
|
|
238 |
|
|
239 |
val bn_fun_strs = get_bn_fun_strs bn_funs
|
|
240 |
val bn_fun_strs' = add_raws bn_fun_strs
|
|
241 |
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
|
|
242 |
val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
|
|
243 |
(bn_fun_strs ~~ bn_fun_strs')
|
|
244 |
|
|
245 |
val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
|
|
246 |
|
|
247 |
val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
|
|
248 |
|
|
249 |
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
|
|
250 |
|
|
251 |
val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
|
|
252 |
in
|
|
253 |
lthy
|
|
254 |
|> add_datatype_wrapper raw_dt_names raw_dts
|
|
255 |
||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
|
|
256 |
||>> pair raw_bclauses
|
|
257 |
||>> pair raw_bns
|
|
258 |
end
|
|
259 |
*}
|
|
260 |
|
|
261 |
ML {*
|
|
262 |
fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
|
|
263 |
let
|
1945
|
264 |
val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
|
1941
|
265 |
raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
|
|
266 |
|
1945
|
267 |
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
|
|
268 |
val {descr, sorts, ...} = dtinfo;
|
|
269 |
|
|
270 |
val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
|
|
271 |
Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
|
1960
|
272 |
|
|
273 |
val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
|
|
274 |
fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
|
|
275 |
val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
|
|
276 |
val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
|
|
277 |
val thy = Local_Theory.exit_global lthy2;
|
|
278 |
val lthy3 = Theory_Target.init NONE thy;
|
|
279 |
|
1996
|
280 |
val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
|
|
281 |
val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) =
|
|
282 |
define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
|
1941
|
283 |
in
|
1992
|
284 |
((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
|
1941
|
285 |
end
|
|
286 |
*}
|
|
287 |
|
|
288 |
section {* Preparing and parsing of the specification *}
|
|
289 |
|
|
290 |
ML {*
|
|
291 |
(* parsing the datatypes and declaring *)
|
|
292 |
(* constructors in the local theory *)
|
|
293 |
fun prepare_dts dt_strs lthy =
|
|
294 |
let
|
|
295 |
val thy = ProofContext.theory_of lthy
|
|
296 |
|
|
297 |
fun mk_type full_tname tvrs =
|
|
298 |
Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)
|
|
299 |
|
|
300 |
fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) =
|
|
301 |
let
|
|
302 |
val tys = map (Syntax.read_typ lthy o snd) anno_tys
|
|
303 |
val ty = mk_type full_tname tvs
|
|
304 |
in
|
|
305 |
((cname, tys ---> ty, mx), (cname, tys, mx))
|
|
306 |
end
|
|
307 |
|
|
308 |
fun prep_dt (tvs, tname, mx, cnstrs) =
|
|
309 |
let
|
|
310 |
val full_tname = Sign.full_name thy tname
|
|
311 |
val (cnstrs', cnstrs'') =
|
|
312 |
split_list (map (prep_cnstr full_tname tvs) cnstrs)
|
|
313 |
in
|
|
314 |
(cnstrs', (tvs, tname, mx, cnstrs''))
|
|
315 |
end
|
|
316 |
|
|
317 |
val (cnstrs, dts) = split_list (map prep_dt dt_strs)
|
|
318 |
in
|
|
319 |
lthy
|
|
320 |
|> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
|
|
321 |
|> pair dts
|
|
322 |
end
|
|
323 |
*}
|
|
324 |
|
|
325 |
ML {*
|
|
326 |
(* parsing the binding function specification and *)
|
|
327 |
(* declaring the functions in the local theory *)
|
|
328 |
fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
|
|
329 |
let
|
|
330 |
val ((bn_funs, bn_eqs), _) =
|
|
331 |
Specification.read_spec bn_fun_strs bn_eq_strs lthy
|
|
332 |
|
|
333 |
fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
|
|
334 |
|
|
335 |
val bn_funs' = map prep_bn_fun bn_funs
|
|
336 |
in
|
|
337 |
lthy
|
|
338 |
|> Local_Theory.theory (Sign.add_consts_i bn_funs')
|
|
339 |
|> pair (bn_funs', bn_eqs)
|
|
340 |
end
|
|
341 |
*}
|
|
342 |
|
|
343 |
text {* associates every SOME with the index in the list; drops NONEs *}
|
|
344 |
ML {*
|
|
345 |
fun indexify xs =
|
|
346 |
let
|
|
347 |
fun mapp _ [] = []
|
|
348 |
| mapp i (NONE :: xs) = mapp (i + 1) xs
|
|
349 |
| mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs
|
|
350 |
in
|
|
351 |
mapp 0 xs
|
|
352 |
end
|
|
353 |
|
|
354 |
fun index_lookup xs x =
|
|
355 |
case AList.lookup (op=) xs x of
|
|
356 |
SOME x => x
|
|
357 |
| NONE => error ("Cannot find " ^ x ^ " as argument annotation.");
|
|
358 |
*}
|
|
359 |
|
|
360 |
ML {*
|
|
361 |
fun prepare_bclauses dt_strs lthy =
|
|
362 |
let
|
|
363 |
val annos_bclauses =
|
|
364 |
get_cnstrs dt_strs
|
|
365 |
|> map (map (fn (_, antys, _, bns) => (map fst antys, bns)))
|
|
366 |
|
|
367 |
fun prep_binder env bn_str =
|
|
368 |
case (Syntax.read_term lthy bn_str) of
|
|
369 |
Free (x, _) => (NONE, index_lookup env x)
|
|
370 |
| Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
|
|
371 |
| _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
|
|
372 |
|
|
373 |
fun prep_body env bn_str = index_lookup env bn_str
|
|
374 |
|
|
375 |
fun prep_mode "bind" = BLst
|
|
376 |
| prep_mode "bind_set" = BSet
|
|
377 |
| prep_mode "bind_res" = BRes
|
|
378 |
|
|
379 |
fun prep_bclause env (mode, binders, bodies) =
|
|
380 |
let
|
|
381 |
val binders' = map (prep_binder env) binders
|
|
382 |
val bodies' = map (prep_body env) bodies
|
|
383 |
in
|
|
384 |
prep_mode mode (binders', bodies')
|
|
385 |
end
|
|
386 |
|
|
387 |
fun prep_bclauses (annos, bclause_strs) =
|
|
388 |
let
|
|
389 |
val env = indexify annos (* for every label, associate the index *)
|
|
390 |
in
|
|
391 |
map (prep_bclause env) bclause_strs
|
|
392 |
end
|
|
393 |
in
|
|
394 |
map (map prep_bclauses) annos_bclauses
|
|
395 |
end
|
|
396 |
*}
|
|
397 |
|
1943
|
398 |
text {*
|
|
399 |
adds an empty binding clause for every argument
|
|
400 |
that is not already part of a binding clause
|
|
401 |
*}
|
|
402 |
|
1941
|
403 |
ML {*
|
|
404 |
fun included i bcs =
|
|
405 |
let
|
|
406 |
fun incl (BEmy j) = i = j
|
|
407 |
| incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
|
|
408 |
| incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
|
|
409 |
| incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
|
|
410 |
in
|
|
411 |
exists incl bcs
|
|
412 |
end
|
|
413 |
*}
|
|
414 |
|
|
415 |
ML {*
|
|
416 |
fun complete dt_strs bclauses =
|
|
417 |
let
|
|
418 |
val args =
|
|
419 |
get_cnstrs dt_strs
|
|
420 |
|> map (map (fn (_, antys, _, _) => length antys))
|
|
421 |
|
|
422 |
fun complt n bcs =
|
|
423 |
let
|
|
424 |
fun add bcs i = (if included i bcs then [] else [BEmy i])
|
|
425 |
in
|
|
426 |
bcs @ (flat (map_range (add bcs) n))
|
|
427 |
end
|
|
428 |
in
|
|
429 |
map2 (map2 complt) args bclauses
|
|
430 |
end
|
|
431 |
*}
|
|
432 |
|
|
433 |
ML {*
|
|
434 |
fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
|
|
435 |
let
|
|
436 |
fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
|
|
437 |
val lthy0 =
|
|
438 |
Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
|
1944
|
439 |
val (dts, lthy1) = prepare_dts dt_strs lthy0
|
|
440 |
val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
|
1941
|
441 |
val bclauses = prepare_bclauses dt_strs lthy2
|
|
442 |
val bclauses' = complete dt_strs bclauses
|
|
443 |
in
|
|
444 |
nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd
|
|
445 |
end
|
|
446 |
|
|
447 |
|
|
448 |
(* Command Keyword *)
|
|
449 |
|
|
450 |
val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
|
|
451 |
(main_parser >> nominal_datatype2_cmd)
|
|
452 |
*}
|
|
453 |
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
454 |
atom_decl name
|
1941
|
455 |
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
456 |
nominal_datatype lam =
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
457 |
Var name
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
458 |
| App lam lam
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
459 |
| Lam x::name t::lam bind_set x in t
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
460 |
| Let p::pt t::lam bind_set "bn p" in t
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
461 |
and pt =
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
462 |
P1 name
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
463 |
| P2 pt pt
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
464 |
binder
|
1981
|
465 |
bn::"pt \<Rightarrow> atom set"
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
466 |
where
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
467 |
"bn (P1 x) = {atom x}"
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
468 |
| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
469 |
|
1981
|
470 |
thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
|
1992
|
471 |
thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
|
1941
|
472 |
|
|
473 |
nominal_datatype exp =
|
|
474 |
EVar name
|
|
475 |
| EUnit
|
1988
|
476 |
| EPair q1::exp q2::exp
|
1941
|
477 |
| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l
|
|
478 |
|
|
479 |
and fnclause =
|
1988
|
480 |
K x::name p::pat f::exp bind_res "b_pat p" in f
|
1941
|
481 |
|
|
482 |
and fnclauses =
|
|
483 |
S fnclause
|
|
484 |
| ORs fnclause fnclauses
|
|
485 |
|
|
486 |
and lrb =
|
|
487 |
Clause fnclauses
|
|
488 |
|
|
489 |
and lrbs =
|
|
490 |
Single lrb
|
|
491 |
| More lrb lrbs
|
|
492 |
|
|
493 |
and pat =
|
|
494 |
PVar name
|
|
495 |
| PUnit
|
|
496 |
| PPair pat pat
|
|
497 |
|
|
498 |
binder
|
1988
|
499 |
b_lrbs :: "lrbs \<Rightarrow> atom list" and
|
1941
|
500 |
b_pat :: "pat \<Rightarrow> atom set" and
|
1988
|
501 |
b_fnclauses :: "fnclauses \<Rightarrow> atom list" and
|
|
502 |
b_fnclause :: "fnclause \<Rightarrow> atom list" and
|
|
503 |
b_lrb :: "lrb \<Rightarrow> atom list"
|
1941
|
504 |
|
|
505 |
where
|
|
506 |
"b_lrbs (Single l) = b_lrb l"
|
1988
|
507 |
| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)"
|
1941
|
508 |
| "b_pat (PVar x) = {atom x}"
|
|
509 |
| "b_pat (PUnit) = {}"
|
|
510 |
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
|
|
511 |
| "b_fnclauses (S fc) = (b_fnclause fc)"
|
1988
|
512 |
| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)"
|
1941
|
513 |
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
|
1988
|
514 |
| "b_fnclause (K x pat exp) = [atom x]"
|
1941
|
515 |
|
1988
|
516 |
typ exp_raw
|
|
517 |
typ pat_raw
|
1941
|
518 |
thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
|
|
519 |
thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
|
1945
|
520 |
thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
|
1960
|
521 |
thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
|
2006
|
522 |
thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros[no_vars]
|
1945
|
523 |
|
1988
|
524 |
nominal_datatype ty =
|
|
525 |
Var "name"
|
|
526 |
| Fun "ty" "ty"
|
|
527 |
|
|
528 |
nominal_datatype tys =
|
|
529 |
All xs::"name fset" ty::"ty_raw" bind_res xs in ty
|
|
530 |
thm fv_tys_raw.simps
|
1992
|
531 |
thm alpha_tys_raw.intros
|
1941
|
532 |
|
1964
|
533 |
(* some further tests *)
|
|
534 |
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
535 |
nominal_datatype lam2 =
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
536 |
Var2 "name"
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
537 |
| App2 "lam2" "lam2 list"
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
538 |
| Lam2 x::"name" t::"lam2" bind x in t
|
1964
|
539 |
|
|
540 |
|
1941
|
541 |
|
|
542 |
|
|
543 |
end
|
|
544 |
|
|
545 |
|
|
546 |
|