equal
deleted
inserted
replaced
900 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
900 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
901 apply (simp only: alpha_gen) |
901 apply (simp only: alpha_gen) |
902 apply (simp add: permute_trm5_lts fresh_star_def) |
902 apply (simp add: permute_trm5_lts fresh_star_def) |
903 done |
903 done |
904 |
904 |
|
905 lemma lets_ok2: |
|
906 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
907 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
908 apply (subst alpha5_INJ) |
|
909 apply (rule conjI) |
|
910 apply (rule_tac x="0 :: perm" in exI) |
|
911 apply (simp only: alpha_gen) |
|
912 apply (simp add: permute_trm5_lts fresh_star_def) |
|
913 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
914 apply (simp only: alpha_gen) |
|
915 apply (simp add: permute_trm5_lts fresh_star_def) |
|
916 done |
|
917 |
|
918 |
905 lemma lets_not_ok1: |
919 lemma lets_not_ok1: |
906 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
920 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
907 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
921 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
908 apply (subst alpha5_INJ(3)) |
922 apply (subst alpha5_INJ(3)) |
909 apply(clarify) |
923 apply(clarify) |
913 apply(clarify) |
927 apply(clarify) |
914 apply (simp add: alpha5_INJ(2)) |
928 apply (simp add: alpha5_INJ(2)) |
915 apply (simp only: alpha5_INJ(1)) |
929 apply (simp only: alpha5_INJ(1)) |
916 done |
930 done |
917 |
931 |
918 |
932 lemma distinct_helper: |
919 |
933 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
920 |
934 apply auto |
|
935 apply (erule alpha5.cases) |
|
936 apply (simp_all only: rtrm5.distinct) |
|
937 done |
|
938 |
|
939 lemma distinct_helper2: |
|
940 shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
941 by (lifting distinct_helper) |
|
942 |
|
943 lemma lets_nok: |
|
944 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
945 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
946 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
947 apply (subst alpha5_INJ) |
|
948 apply (simp only: alpha_gen permute_trm5_lts fresh_star_def) |
|
949 apply (subst alpha5_INJ(5)) |
|
950 apply (subst alpha5_INJ(5)) |
|
951 apply (simp add: distinct_helper2) |
|
952 done |
921 |
953 |
922 text {* type schemes *} |
954 text {* type schemes *} |
923 datatype ty = |
955 datatype ty = |
924 Var "name" |
956 Var "name" |
925 | Fun "ty" "ty" |
957 | Fun "ty" "ty" |