equal
deleted
inserted
replaced
1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Atoms" |
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" |
6 begin |
6 begin |
7 |
7 |
447 |
447 |
448 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl |
448 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl |
449 (main_parser >> nominal_datatype2_cmd) |
449 (main_parser >> nominal_datatype2_cmd) |
450 *} |
450 *} |
451 |
451 |
452 |
|
453 |
|
454 atom_decl name |
452 atom_decl name |
|
453 |
|
454 nominal_datatype lam = |
|
455 Var name |
|
456 | App lam lam |
|
457 | Lam x::name t::lam bind_set x in t |
|
458 | Let p::pt t::lam bind_set "bn p" in t |
|
459 and pt = |
|
460 P1 name |
|
461 | P2 pt pt |
|
462 binder |
|
463 bn::"pt \<Rightarrow> atom set" |
|
464 where |
|
465 "bn (P1 x) = {atom x}" |
|
466 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
|
467 |
455 |
468 |
456 nominal_datatype exp = |
469 nominal_datatype exp = |
457 EVar name |
470 EVar name |
458 | EUnit |
471 | EUnit |
459 | EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 |
472 | EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 |
505 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 |
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 |
506 |
519 |
507 |
520 |
508 (* some further tests *) |
521 (* some further tests *) |
509 |
522 |
510 nominal_datatype lam = |
523 nominal_datatype lam2 = |
511 Var "name" |
524 Var2 "name" |
512 | App "lam" "lam list" |
525 | App2 "lam2" "lam2 list" |
513 | Lam x::"name" t::"lam" bind x in t |
526 | Lam2 x::"name" t::"lam2" bind x in t |
514 |
527 |
515 nominal_datatype ty = |
528 nominal_datatype ty = |
516 Var "name" |
529 Var "name" |
517 | Fun "ty" "ty" |
530 | Fun "ty" "ty" |
518 |
531 |