Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Example that shows that current alpha is wrong.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 01 Mar 2010 11:40:48 +0100
changeset 1286 87894b5156f4
parent 1285 e3ac56d3b7af
child 1287 8557af71724e
Example that shows that current alpha is wrong.
Nominal/Term5.thy file | annotate | diff | comparison | revisions 
--- 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 \<leftrightarrow> 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 \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
nominal2