equal
deleted
inserted
replaced
904 apply (simp only: alpha_gen) |
904 apply (simp only: alpha_gen) |
905 apply (simp add: permute_trm5_lts fresh_star_def) |
905 apply (simp add: permute_trm5_lts fresh_star_def) |
906 apply (simp add: insert_eqvt eqvts atom_eqvt) |
906 apply (simp add: insert_eqvt eqvts atom_eqvt) |
907 done |
907 done |
908 |
908 |
|
909 lemma lets_ok2: |
|
910 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
911 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
912 apply (subst alpha5_INJ) |
|
913 apply (simp add: alpha_gen) |
|
914 apply (simp add: permute_trm5_lts fresh_star_def) |
|
915 apply (rule allI) |
|
916 apply (subst alpha5_INJ) |
|
917 apply (subst alpha5_INJ) |
|
918 apply (subst alpha5_INJ) |
|
919 apply (simp add: insert_eqvt eqvts atom_eqvt) |
|
920 apply (subst alpha5_INJ(5)) |
|
921 apply (subst alpha5_INJ) |
|
922 apply (subst alpha5_INJ(5)) |
|
923 apply (subst alpha5_INJ) |
|
924 apply (rule impI)+ |
|
925 apply (simp) |
|
926 done |
|
927 |
909 text {* type schemes *} |
928 text {* type schemes *} |
910 datatype ty = |
929 datatype ty = |
911 Var "name" |
930 Var "name" |
912 | Fun "ty" "ty" |
931 | Fun "ty" "ty" |
913 |
932 |