603 apply rule |
603 apply rule |
604 apply simp |
604 apply simp |
605 oops (* can this be defined ? *) |
605 oops (* can this be defined ? *) |
606 (* Yes, if "sub" is a constant. *) |
606 (* Yes, if "sub" is a constant. *) |
607 |
607 |
608 |
608 text {* Working Examples *} |
609 text {* tests of functions containing if and case *} |
|
610 |
|
611 consts P :: "lam \<Rightarrow> bool" |
|
612 |
|
613 nominal_primrec |
|
614 A :: "lam => lam" |
|
615 where |
|
616 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
617 | "A (Var x) = (Var x)" |
|
618 | "A (App M N) = (if True then M else A N)" |
|
619 oops |
|
620 |
|
621 nominal_primrec |
|
622 C :: "lam => lam" |
|
623 where |
|
624 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
625 | "C (Var x) = (Var x)" |
|
626 | "C (App M N) = (if True then M else C N)" |
|
627 oops |
|
628 |
609 |
629 nominal_primrec |
610 nominal_primrec |
630 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
611 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
631 where |
612 where |
632 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
613 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
644 done |
625 done |
645 |
626 |
646 termination |
627 termination |
647 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
628 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
648 |
629 |
|
630 nominal_primrec |
|
631 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
|
632 where |
|
633 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
|
634 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
|
635 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
|
636 oops |
|
637 |
|
638 nominal_primrec |
|
639 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
640 where |
|
641 "CPS (Var x) k = Var x" |
|
642 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
|
643 oops |
|
644 |
|
645 consts b :: name |
|
646 nominal_primrec |
|
647 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
648 where |
|
649 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
650 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
|
651 unfolding eqvt_def Z_graph_def |
|
652 apply (rule, perm_simp, rule) |
|
653 oops |
|
654 |
|
655 text {* tests of functions containing if and case *} |
|
656 |
|
657 consts P :: "lam \<Rightarrow> bool" |
|
658 |
|
659 nominal_primrec |
|
660 A :: "lam => lam" |
|
661 where |
|
662 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
663 | "A (Var x) = (Var x)" |
|
664 | "A (App M N) = (if True then M else A N)" |
|
665 oops |
|
666 |
|
667 nominal_primrec |
|
668 C :: "lam => lam" |
|
669 where |
|
670 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
671 | "C (Var x) = (Var x)" |
|
672 | "C (App M N) = (if True then M else C N)" |
|
673 oops |
|
674 |
649 nominal_primrec |
675 nominal_primrec |
650 A :: "lam => lam" |
676 A :: "lam => lam" |
651 where |
677 where |
652 "A (Lam [x].M) = (Lam [x].M)" |
678 "A (Lam [x].M) = (Lam [x].M)" |
653 | "A (Var x) = (Var x)" |
679 | "A (Var x) = (Var x)" |
665 apply(perm_simp) |
691 apply(perm_simp) |
666 apply(rule allI) |
692 apply(rule allI) |
667 apply(rule refl) |
693 apply(rule refl) |
668 oops |
694 oops |
669 |
695 |
670 text {* "HO" functions *} |
|
671 |
|
672 nominal_primrec |
|
673 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
|
674 where |
|
675 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
|
676 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
|
677 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
|
678 oops |
|
679 |
|
680 nominal_primrec |
|
681 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
682 where |
|
683 "CPS (Var x) k = Var x" |
|
684 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
|
685 oops |
|
686 |
|
687 (* Problem: nominal_primrec generates non-quantified free variable "x" *) |
|
688 consts b :: name |
|
689 nominal_primrec |
|
690 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
691 where |
|
692 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
693 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
|
694 unfolding eqvt_def Z_graph_def |
|
695 apply (rule, perm_simp, rule) |
|
696 oops |
|
697 |
|
698 |
|
699 |
|
700 |
|
701 |
|
702 |
|
703 |
|
704 |
|
705 end |
696 end |
706 |
697 |
707 |
698 |
708 |
699 |