2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 "Abs" "Perm" "Nominal2_FSet" |
3 "Abs" "Perm" "Nominal2_FSet" |
4 begin |
4 begin |
5 |
5 |
6 ML {* |
6 ML {* |
|
7 (* binding modes *) |
|
8 |
7 datatype bmodes = |
9 datatype bmodes = |
8 BEmy of int |
10 BEmy of int |
9 | BLst of ((term option * int) list) * (int list) |
11 | BLst of ((term option * int) list) * (int list) |
10 | BSet of ((term option * int) list) * (int list) |
12 | BSet of ((term option * int) list) * (int list) |
11 | BRes of ((term option * int) list) * (int list) |
13 | BRes of ((term option * int) list) * (int list) |
241 map2 fv_constr constrs bclausess |
243 map2 fv_constr constrs bclausess |
242 end |
244 end |
243 *} |
245 *} |
244 |
246 |
245 ML {* |
247 ML {* |
246 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy = |
248 fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy = |
247 let |
249 let |
248 val thy = ProofContext.theory_of lthy; |
250 val thy = ProofContext.theory_of lthy; |
249 val {descr as dt_descr, sorts, ...} = dt_info; |
|
250 |
251 |
251 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
252 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
252 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
253 val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; |
253 val fv_frees = map Free (fv_names ~~ fv_types); |
254 val fv_frees = map Free (fv_names ~~ fv_types); |
254 |
255 |
|
256 (* free variables for the bn-functions *) |
255 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
257 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
256 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
258 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
257 |
259 |
|
260 |
258 val fv_bns = map snd bn_fvbn; |
261 val fv_bns = map snd bn_fvbn; |
259 val fv_nums = 0 upto (length fv_frees - 1) |
262 val fv_nums = 0 upto (length fv_frees - 1) |
260 |
263 |
261 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums); |
264 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums); |
262 |
265 |