562 |
562 |
563 thm permute_weird_raw.simps[no_vars] |
563 thm permute_weird_raw.simps[no_vars] |
564 thm alpha_weird_raw.intros[no_vars] |
564 thm alpha_weird_raw.intros[no_vars] |
565 thm fv_weird_raw.simps[no_vars] |
565 thm fv_weird_raw.simps[no_vars] |
566 |
566 |
567 (* example 6 from Terms.thy *) |
|
568 |
|
569 (* BV is not respectful, needs to fail*) |
|
570 (* |
|
571 nominal_datatype trm6 = |
|
572 Vr6 "name" |
|
573 | Lm6 x::"name" t::"trm6" bind x in t |
|
574 | Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right |
|
575 binder |
|
576 bv6 |
|
577 where |
|
578 "bv6 (Vr6 n) = {}" |
|
579 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t" |
|
580 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" |
|
581 *) |
|
582 |
|
583 (* example 7 from Terms.thy *) |
|
584 (* BV is not respectful, needs to fail*) |
|
585 (* |
|
586 nominal_datatype trm7 = |
|
587 Vr7 "name" |
|
588 | Lm7 l::"name" r::"trm7" bind l in r |
|
589 | Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r |
|
590 binder |
|
591 bv7 |
|
592 where |
|
593 "bv7 (Vr7 n) = {atom n}" |
|
594 | "bv7 (Lm7 n t) = bv7 t - {atom n}" |
|
595 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" |
|
596 *) |
|
597 |
|
598 (* example 8 from Terms.thy *) |
567 (* example 8 from Terms.thy *) |
599 |
568 |
600 (* Binding in a term under a bn, needs to fail *) |
569 (* Binding in a term under a bn, needs to fail *) |
601 (* |
570 (* |
602 nominal_datatype foo8 = |
571 nominal_datatype foo8 = |
609 bv8 |
578 bv8 |
610 where |
579 where |
611 "bv8 (Bar0 x) = {}" |
580 "bv8 (Bar0 x) = {}" |
612 | "bv8 (Bar1 v x b) = {atom v}" |
581 | "bv8 (Bar1 v x b) = {atom v}" |
613 *) |
582 *) |
614 (* example 9 from Terms.thy *) |
|
615 |
|
616 (* BV is not respectful, needs to fail*) |
|
617 (* |
|
618 nominal_datatype lam9 = |
|
619 Var9 "name" |
|
620 | Lam9 n::"name" l::"lam9" bind n in l |
|
621 and bla9 = |
|
622 Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s |
|
623 binder |
|
624 bv9 |
|
625 where |
|
626 "bv9 (Var9 x) = {}" |
|
627 | "bv9 (Lam9 x b) = {atom x}" |
|
628 *) |
|
629 |
583 |
630 (* Type schemes with separate datatypes *) |
584 (* Type schemes with separate datatypes *) |
631 nominal_datatype T = |
585 nominal_datatype T = |
632 TVar "name" |
586 TVar "name" |
633 | TFun "T" "T" |
587 | TFun "T" "T" |