equal
deleted
inserted
replaced
497 bp :: "pat \<Rightarrow> atom set" |
497 bp :: "pat \<Rightarrow> atom set" |
498 where |
498 where |
499 "bp (PVar x) = {atom x}" |
499 "bp (PVar x) = {atom x}" |
500 | "bp (PUnit) = {}" |
500 | "bp (PUnit) = {}" |
501 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
501 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
502 |
502 thm alpha_exp_raw_alpha_pat_raw.intros |
503 thm quot_respect |
503 |
504 (* example 6 from Peter Sewell's bestiary *) |
504 (* example 6 from Peter Sewell's bestiary *) |
505 nominal_datatype exp6 = |
505 nominal_datatype exp6 = |
506 EVar name |
506 EVar name |
507 | EPair exp6 exp6 |
507 | EPair exp6 exp6 |
508 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
508 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
514 bp6 :: "pat6 \<Rightarrow> atom set" |
514 bp6 :: "pat6 \<Rightarrow> atom set" |
515 where |
515 where |
516 "bp6 (PVar' x) = {atom x}" |
516 "bp6 (PVar' x) = {atom x}" |
517 | "bp6 (PUnit') = {}" |
517 | "bp6 (PUnit') = {}" |
518 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
518 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
|
519 thm alpha_exp6_raw_alpha_pat6_raw.intros |
519 |
520 |
520 (* example 7 from Peter Sewell's bestiary *) |
521 (* example 7 from Peter Sewell's bestiary *) |
521 nominal_datatype exp7 = |
522 nominal_datatype exp7 = |
522 EVar name |
523 EVar name |
523 | EUnit |
524 | EUnit |
533 b7s :: "lrbs \<Rightarrow> atom set" |
534 b7s :: "lrbs \<Rightarrow> atom set" |
534 where |
535 where |
535 "b7 (Assign x e) = {atom x}" |
536 "b7 (Assign x e) = {atom x}" |
536 | "b7s (Single a) = b7 a" |
537 | "b7s (Single a) = b7 a" |
537 | "b7s (More a as) = (b7 a) \<union> (b7s as)" |
538 | "b7s (More a as) = (b7 a) \<union> (b7s as)" |
|
539 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros |
538 |
540 |
539 (* example 8 from Peter Sewell's bestiary *) |
541 (* example 8 from Peter Sewell's bestiary *) |
540 nominal_datatype exp8 = |
542 nominal_datatype exp8 = |
541 EVar name |
543 EVar name |
542 | EUnit |
544 | EUnit |
570 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
572 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
571 | "b_fnclauses (S fc) = (b_fnclause fc)" |
573 | "b_fnclauses (S fc) = (b_fnclause fc)" |
572 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
574 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
573 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" |
575 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" |
574 | "b_fnclause (K x pat exp8) = {atom x}" |
576 | "b_fnclause (K x pat exp8) = {atom x}" |
|
577 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros |
575 |
578 |
576 |
579 |
577 |
580 |
578 |
581 |
579 (* example 9 from Peter Sewell's bestiary *) |
582 (* example 9 from Peter Sewell's bestiary *) |