Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Term5.thy
changeset 1287 8557af71724e
parent 1286 87894b5156f4
child 1288 0203cd5cfd6c 
--- a/Nominal/Term5.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -173,10 +173,13 @@
 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)))"
+  assumes a: "distinct [x, y]"
+  shows "(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 (simp add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp only: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
nominal2