# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265214985 -3600
# Node ID f81b506f62a78c075da1c9ecf4816a046937c263
# Parent  a9135d300fbfc1556cd8de487e53e773dd494d32
proposal for an alpha equivalence

diff -r a9135d300fbf -r f81b506f62a7 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 15:17:29 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 17:36:25 2010 +0100
@@ -714,9 +714,8 @@
 where
   a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
-| a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
-             (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
-              (pi \<bullet> (rbv5 l1) = rbv5 l2))
+| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2)); 
+        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
         \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
 | a4: "rLnil \<approx>l rLnil"
 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
@@ -726,11 +725,10 @@
 lemma alpha5_inj:
   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
-  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
-         (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
-         (pi \<bullet> (rbv5 l1) = rbv5 l2)))"
+  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2))) \<and>
+         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))))"
   "rLnil \<approx>l rLnil"
-  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
+  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
 apply -
 apply (simp_all add: alpha5_alphalts.intros)
 apply rule
@@ -803,10 +801,6 @@
   "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
   apply(induct rule: alpha5_alphalts.inducts)
   apply(simp_all add: alpha_gen)
-  apply(erule conjE)+
-  apply(erule exE)
-  apply(erule conjE)+
-  apply simp
   done
 
 lemma [quot_respect]:
@@ -828,11 +822,11 @@
 apply(simp_all)
 done
 
+
 lemma 
   shows "(alphalts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)
 
-
 instantiation trm5 and lts :: pt
 begin
 
@@ -875,11 +869,10 @@
   "((Vr5 a) = (Vr5 b)) = (a = b)"
   "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
   "(Lt5 l1 t1 = Lt5 l2 t2) =
-     (\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and>
-            (bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and>
-            (pi \<bullet> (bv5 l1) = bv5 l2)))"
+     ((\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2))) \<and>
+      (\<exists>pi. ((bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2))))"
   "Lnil = Lnil"
-  "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)"
+  "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (n1 = n2 \<and> ls1 = ls2 \<and> t1 = t2)"
 unfolding alpha_gen
 apply(lifting alpha5_inj[unfolded alpha_gen])
 done
@@ -900,31 +893,32 @@
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (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="(x \<leftrightarrow> y)" in exI)
 apply (simp only: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: insert_eqvt eqvts atom_eqvt)
 done
 
-lemma lets_ok2:
+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)))"
-apply (subst alpha5_INJ)
+             (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (subst alpha5_INJ(3))
+apply(clarify)
 apply (simp add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule allI)
-apply (subst alpha5_INJ)
-apply (subst alpha5_INJ)
-apply (subst alpha5_INJ)
-apply (simp add: insert_eqvt eqvts atom_eqvt)
-apply (subst alpha5_INJ(5))
-apply (subst alpha5_INJ)
-apply (subst alpha5_INJ(5))
-apply (subst alpha5_INJ)
-apply (rule impI)+
-apply (simp)
+apply (simp add: alpha5_INJ(5))
+apply(clarify)
+apply (simp add: alpha5_INJ(2))
+apply (simp only: alpha5_INJ(1))
 done
 
+
+
+
+
 text {* type schemes *} 
 datatype ty = 
   Var "name"