# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268755892 -3600
# Node ID 9cb619aa933c50f2e70185dd8d3dbe049aace268
# Parent  91fe914e1befa35d69610653e5ba4c70adaa76ff
Alpha is wrong.

diff -r 91fe914e1bef -r 9cb619aa933c Nominal/Term5.thy
--- a/Nominal/Term5.thy	Tue Mar 16 16:51:06 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 17:11:32 2010 +0100
@@ -157,9 +157,10 @@
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
   "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
-  "(alpha_rbv5 0 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
+  "(alpha_rbv5 p b c \<Longrightarrow> fv_rbv5 (p \<bullet> b) = fv_rbv5 c)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
   apply(simp_all add: eqvts)
+  thm alpha5_inj
   apply(simp add: alpha_gen)
   apply(clarify)
   apply(simp)
@@ -232,6 +233,16 @@
 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
+lemma lets_bla:
+  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
+apply (simp only: alpha5_INJ)
+apply (simp only: bv5)
+apply simp
+apply (rule_tac x="(z \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
+done
+
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
 thm alpha5_INJ