equal
deleted
inserted
replaced
1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "NewFv" |
5 "Perm" "NewFv" "NewAlpha" |
6 begin |
6 begin |
7 |
7 |
8 section{* Interface for nominal_datatype *} |
8 section{* Interface for nominal_datatype *} |
9 |
9 |
10 |
10 |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
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; |
277 val thy = Local_Theory.exit_global lthy2; |
278 val lthy3 = Theory_Target.init NONE thy; |
278 val lthy3 = Theory_Target.init NONE thy; |
279 |
279 |
280 val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
280 val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
281 in |
281 val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4; |
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
282 in |
|
283 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5) |
283 end |
284 end |
284 *} |
285 *} |
285 |
286 |
286 section {* Preparing and parsing of the specification *} |
287 section {* Preparing and parsing of the specification *} |
287 |
288 |
464 where |
465 where |
465 "bn (P1 x) = {atom x}" |
466 "bn (P1 x) = {atom x}" |
466 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
467 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
467 |
468 |
468 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps |
469 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps |
|
470 thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros |
469 |
471 |
470 nominal_datatype exp = |
472 nominal_datatype exp = |
471 EVar name |
473 EVar name |
472 | EUnit |
474 | EUnit |
473 | EPair q1::exp q2::exp |
475 | EPair q1::exp q2::exp |
514 typ pat_raw |
516 typ pat_raw |
515 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
517 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
516 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
518 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
517 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
519 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
518 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 |
520 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 |
|
521 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 |
519 |
522 |
520 nominal_datatype ty = |
523 nominal_datatype ty = |
521 Var "name" |
524 Var "name" |
522 | Fun "ty" "ty" |
525 | Fun "ty" "ty" |
523 |
526 |
524 nominal_datatype tys = |
527 nominal_datatype tys = |
525 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
528 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
526 thm fv_tys_raw.simps |
529 thm fv_tys_raw.simps |
|
530 thm alpha_tys_raw.intros |
527 |
531 |
528 (* some further tests *) |
532 (* some further tests *) |
529 |
533 |
530 nominal_datatype lam2 = |
534 nominal_datatype lam2 = |
531 Var2 "name" |
535 Var2 "name" |