--- 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