720 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
720 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
721 unfolding eqvt_def Z_graph_def |
721 unfolding eqvt_def Z_graph_def |
722 apply (rule, perm_simp, rule) |
722 apply (rule, perm_simp, rule) |
723 oops |
723 oops |
724 |
724 |
725 text {* tests of functions containing if and case *} |
|
726 |
|
727 consts P :: "lam \<Rightarrow> bool" |
|
728 |
|
729 nominal_primrec |
|
730 A :: "lam => lam" |
|
731 where |
|
732 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
733 | "A (Var x) = (Var x)" |
|
734 | "A (App M N) = (if True then M else A N)" |
|
735 oops |
|
736 |
|
737 nominal_primrec |
|
738 C :: "lam => lam" |
|
739 where |
|
740 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
741 | "C (Var x) = (Var x)" |
|
742 | "C (App M N) = (if True then M else C N)" |
|
743 oops |
|
744 |
|
745 nominal_primrec |
|
746 A :: "lam => lam" |
|
747 where |
|
748 "A (Lam [x].M) = (Lam [x].M)" |
|
749 | "A (Var x) = (Var x)" |
|
750 | "A (App M N) = (if True then M else A N)" |
|
751 oops |
|
752 |
|
753 nominal_primrec |
|
754 B :: "lam => lam" |
|
755 where |
|
756 "B (Lam [x].M) = (Lam [x].M)" |
|
757 | "B (Var x) = (Var x)" |
|
758 | "B (App M N) = (if True then M else (B N))" |
|
759 unfolding eqvt_def |
|
760 unfolding B_graph_def |
|
761 apply(perm_simp) |
|
762 apply(rule allI) |
|
763 apply(rule refl) |
|
764 oops |
|
765 |
|
766 |
|
767 lemma test: |
725 lemma test: |
768 assumes "t = s" |
726 assumes "t = s" |
769 and "supp p \<sharp>* t" "supp p \<sharp>* x" |
727 and "supp p \<sharp>* t" "supp p \<sharp>* x" |
770 and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y" |
728 and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y" |
771 shows "x = y" |
729 shows "x = y" |
829 apply(simp del: Product_Type.prod.inject) |
787 apply(simp del: Product_Type.prod.inject) |
830 sorry |
788 sorry |
831 |
789 |
832 termination by lexicographic_order |
790 termination by lexicographic_order |
833 |
791 |
|
792 text {* tests of functions containing if and case *} |
|
793 |
|
794 consts P :: "lam \<Rightarrow> bool" |
|
795 |
|
796 nominal_primrec |
|
797 A :: "lam => lam" |
|
798 where |
|
799 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
800 | "A (Var x) = (Var x)" |
|
801 | "A (App M N) = (if True then M else A N)" |
|
802 oops |
|
803 |
|
804 nominal_primrec |
|
805 C :: "lam => lam" |
|
806 where |
|
807 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
808 | "C (Var x) = (Var x)" |
|
809 | "C (App M N) = (if True then M else C N)" |
|
810 oops |
|
811 |
|
812 nominal_primrec |
|
813 A :: "lam => lam" |
|
814 where |
|
815 "A (Lam [x].M) = (Lam [x].M)" |
|
816 | "A (Var x) = (Var x)" |
|
817 | "A (App M N) = (if True then M else A N)" |
|
818 oops |
|
819 |
|
820 nominal_primrec |
|
821 B :: "lam => lam" |
|
822 where |
|
823 "B (Lam [x].M) = (Lam [x].M)" |
|
824 | "B (Var x) = (Var x)" |
|
825 | "B (App M N) = (if True then M else (B N))" |
|
826 unfolding eqvt_def |
|
827 unfolding B_graph_def |
|
828 apply(perm_simp) |
|
829 apply(rule allI) |
|
830 apply(rule refl) |
|
831 oops |
|
832 |
834 end |
833 end |
835 |
834 |
836 |
835 |
837 |
836 |