equal
deleted
inserted
replaced
862 apply(simp del: Product_Type.prod.inject) |
862 apply(simp del: Product_Type.prod.inject) |
863 oops |
863 oops |
864 |
864 |
865 lemma abs_same_binder: |
865 lemma abs_same_binder: |
866 fixes t ta s sa :: "_ :: fs" |
866 fixes t ta s sa :: "_ :: fs" |
867 assumes "sort_of (atom x) = sort_of (atom y)" |
867 and x y::"'a::at" |
868 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa |
868 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa |
869 \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)" |
869 \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)" |
870 by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair) |
870 by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair) |
871 |
871 |
872 nominal_primrec |
872 nominal_primrec |
905 |
905 |
906 text {* tests of functions containing if and case *} |
906 text {* tests of functions containing if and case *} |
907 |
907 |
908 consts P :: "lam \<Rightarrow> bool" |
908 consts P :: "lam \<Rightarrow> bool" |
909 |
909 |
|
910 (* |
910 nominal_primrec |
911 nominal_primrec |
911 A :: "lam => lam" |
912 A :: "lam => lam" |
912 where |
913 where |
913 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
914 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
914 | "A (Var x) = (Var x)" |
915 | "A (Var x) = (Var x)" |
941 unfolding B_graph_def |
942 unfolding B_graph_def |
942 apply(perm_simp) |
943 apply(perm_simp) |
943 apply(rule allI) |
944 apply(rule allI) |
944 apply(rule refl) |
945 apply(rule refl) |
945 oops |
946 oops |
946 |
947 *) |
947 end |
948 end |
948 |
949 |
949 |
950 |
950 |
951 |