# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265218130 -3600
# Node ID afedef46d3abb10dbe3f4b6eb7fb0f398194494c
# Parent  f81b506f62a78c075da1c9ecf4816a046937c263
More let-rec experiments

diff -r f81b506f62a7 -r afedef46d3ab Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 17:36:25 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 18:28:50 2010 +0100
@@ -902,6 +902,20 @@
 apply (simp add: permute_trm5_lts fresh_star_def)
 done
 
+lemma lets_ok2:
+  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ)
+apply (rule conjI)
+apply (rule_tac x="0 :: perm" in exI)
+apply (simp only: 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)
+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>
              (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
@@ -915,9 +929,27 @@
 apply (simp only: alpha5_INJ(1))
 done
 
+lemma distinct_helper:
+  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
+  apply auto
+  apply (erule alpha5.cases)
+  apply (simp_all only: rtrm5.distinct)
+  done
 
+lemma distinct_helper2:
+  shows "(Vr5 x) \<noteq> (Ap5 y z)"
+  by (lifting distinct_helper)
 
-
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ)
+apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
+apply (subst alpha5_INJ(5))
+apply (subst alpha5_INJ(5))
+apply (simp add: distinct_helper2)
+done
 
 text {* type schemes *} 
 datatype ty =