# HG changeset patch # User Cezary Kaliszyk # Date 1267440048 -3600 # Node ID 87894b5156f41d357e77ef3c218f369e959c8ee2 # Parent e3ac56d3b7af75fe7843b3dd60bc1fc9d086feb1 Example that shows that current alpha is wrong. diff -r e3ac56d3b7af -r 87894b5156f4 Nominal/Term5.thy --- a/Nominal/Term5.thy Mon Mar 01 07:46:50 2010 +0100 +++ b/Nominal/Term5.thy Mon Mar 01 11:40:48 2010 +0100 @@ -172,6 +172,18 @@ apply (simp add: permute_trm5_lts fresh_star_def) done +lemma lets_ok3: + "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = + (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (subst alpha5_INJ) +apply (rule conjI) +apply (rule_tac x="(x \ y)" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +apply (rule_tac x="0 :: perm" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +done lemma lets_not_ok1: "x \ y \ (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \