1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "Equivp" "Rsp" "Lift" |
5 "Perm" "NewFv" |
6 begin |
6 begin |
7 |
7 |
8 section{* Interface for nominal_datatype *} |
8 section{* Interface for nominal_datatype *} |
9 |
9 |
10 |
10 |
46 (* main parser *) |
46 (* main parser *) |
47 val main_parser = |
47 val main_parser = |
48 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
48 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
49 |
49 |
50 end |
50 end |
51 *} |
|
52 |
|
53 ML {* |
|
54 datatype bmodes = |
|
55 BEmy of int |
|
56 | BLst of ((term option * int) list) * (int list) |
|
57 | BSet of ((term option * int) list) * (int list) |
|
58 | BRes of ((term option * int) list) * (int list) |
|
59 *} |
51 *} |
60 |
52 |
61 ML {* |
53 ML {* |
62 fun get_cnstrs dts = |
54 fun get_cnstrs dts = |
63 map (fn (_, _, _, constrs) => constrs) dts |
55 map (fn (_, _, _, constrs) => constrs) dts |
275 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
276 val {descr, sorts, ...} = dtinfo; |
268 val {descr, sorts, ...} = dtinfo; |
277 |
269 |
278 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
270 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
279 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
271 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
280 in |
272 |
281 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2) |
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 |
|
280 val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
|
281 in |
|
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
282 end |
283 end |
283 *} |
284 *} |
284 |
285 |
285 section {* Preparing and parsing of the specification *} |
286 section {* Preparing and parsing of the specification *} |
286 |
287 |
498 |
499 |
499 typ exp_raw |
500 typ exp_raw |
500 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
501 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
501 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
502 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
502 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
503 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
503 |
504 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 |
504 |
505 |
505 |
506 |
506 |
507 |
507 end |
508 |
508 |
509 end |
509 |
510 |
510 |
511 |
|
512 |