468 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps |
468 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps |
469 |
469 |
470 nominal_datatype exp = |
470 nominal_datatype exp = |
471 EVar name |
471 EVar name |
472 | EUnit |
472 | EUnit |
473 | EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 |
473 | EPair q1::exp q2::exp |
474 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e l |
474 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e l |
475 |
475 |
476 and fnclause = |
476 and fnclause = |
477 K x::name p::pat f::exp bind_res "b_pat p" in f |
477 K x::name p::pat f::exp bind_res "b_pat p" in f |
478 |
478 |
479 and fnclauses = |
479 and fnclauses = |
480 S fnclause |
480 S fnclause |
481 | ORs fnclause fnclauses |
481 | ORs fnclause fnclauses |
482 |
482 |
491 PVar name |
491 PVar name |
492 | PUnit |
492 | PUnit |
493 | PPair pat pat |
493 | PPair pat pat |
494 |
494 |
495 binder |
495 binder |
496 b_lrbs :: "lrbs \<Rightarrow> atom set" and |
496 b_lrbs :: "lrbs \<Rightarrow> atom list" and |
497 b_pat :: "pat \<Rightarrow> atom set" and |
497 b_pat :: "pat \<Rightarrow> atom set" and |
498 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
498 b_fnclauses :: "fnclauses \<Rightarrow> atom list" and |
499 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
499 b_fnclause :: "fnclause \<Rightarrow> atom list" and |
500 b_lrb :: "lrb \<Rightarrow> atom set" |
500 b_lrb :: "lrb \<Rightarrow> atom list" |
501 |
501 |
502 where |
502 where |
503 "b_lrbs (Single l) = b_lrb l" |
503 "b_lrbs (Single l) = b_lrb l" |
504 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls" |
504 | "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)" |
505 | "b_pat (PVar x) = {atom x}" |
505 | "b_pat (PVar x) = {atom x}" |
506 | "b_pat (PUnit) = {}" |
506 | "b_pat (PUnit) = {}" |
507 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
507 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
508 | "b_fnclauses (S fc) = (b_fnclause fc)" |
508 | "b_fnclauses (S fc) = (b_fnclause fc)" |
509 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
509 | "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" |
510 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
510 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
511 | "b_fnclause (K x pat exp) = {atom x}" |
511 | "b_fnclause (K x pat exp) = [atom x]" |
512 |
512 |
513 |
513 typ exp_raw |
514 typ exp_raw |
514 typ pat_raw |
515 typ pat_raw |
|
516 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
515 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
517 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
516 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
518 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_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 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 |
520 |
519 |
|
520 nominal_datatype ty = |
|
521 Var "name" |
|
522 | Fun "ty" "ty" |
|
523 |
|
524 nominal_datatype tys = |
|
525 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
|
526 thm fv_tys_raw.simps |
521 |
527 |
522 (* some further tests *) |
528 (* some further tests *) |
523 |
529 |
524 nominal_datatype lam2 = |
530 nominal_datatype lam2 = |
525 Var2 "name" |
531 Var2 "name" |
526 | App2 "lam2" "lam2 list" |
532 | App2 "lam2" "lam2 list" |
527 | Lam2 x::"name" t::"lam2" bind x in t |
533 | Lam2 x::"name" t::"lam2" bind x in t |
528 |
534 |
529 nominal_datatype ty = |
535 |
530 Var "name" |
536 |
531 | Fun "ty" "ty" |
537 |
532 |
538 end |
533 nominal_datatype tys = |
539 |
534 All xs::"name fset" ty::"ty_raw" bind xs in ty |
540 |
535 |
541 |
536 |
|
537 |
|
538 end |
|
539 |
|
540 |
|
541 |
|