--- a/Quot/Nominal/Terms.thy	Tue Feb 09 11:22:34 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 12:22:00 2010 +0100
@@ -388,8 +388,10 @@
   a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
-| a4: "(\<exists>pi. (((bv2 bt), t) \<approx>gen alpha2 fv_rtrm2 pi ((bv2 bs), s))) \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
-| a5: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rAs a t \<approx>2a rAs b s"
+| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
+        \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
+        \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
+| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
 
 lemma alpha2_equivp:
   "equivp alpha2"
@@ -403,6 +405,7 @@
   by (auto intro: alpha2_equivp)
 
 
+
 section {*** lets with many assignments ***}
 
 datatype trm3 =
@@ -474,25 +477,28 @@
 
 inductive
   alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
+and
+  alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
 where
   a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and> 
-             (fv_trm3 t - {atom a})\<sharp>* pi \<and> 
-             (pi \<bullet> t) \<approx>3 s \<and> 
-             (pi \<bullet> a) = b)
-       \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-| a4: "\<exists>pi. (
-         fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
-         (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
-         pi \<bullet> t1 = t2      (* \<and> (pi \<bullet> b1 = b2)  *)
-       ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
+| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
+        \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
+        \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
+| a5: "ANil \<approx>3a ANil"
+| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
 
-lemma alpha3_equivp: "equivp alpha3" 
+lemma alpha3_equivp:
+  "equivp alpha3"
+  "equivp alpha3a"
   sorry
 
-quotient_type qtrm3 = trm3 / alpha3
-  by (rule alpha3_equivp)
+quotient_type
+  qtrm3 = trm3 / alpha3
+and
+  qassigns = assigns / alpha3a
+  by (auto intro: alpha3_equivp)
 
 
 section {*** lam with indirect list recursion ***}
@@ -516,7 +522,7 @@
 
 (* needs to be stated by the package *)
 (* there cannot be a clause for lists, as *) 
-(* permuteutations are  already defined in Nominal (also functions, options, and so on) *)
+(* permutations are  already defined in Nominal (also functions, options, and so on) *)
 instantiation
   trm4 :: pt
 begin
@@ -574,11 +580,7 @@
 where
   a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
-| a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and> 
-            (fv_trm4 t - {atom a})\<sharp>* pi \<and> 
-            (pi \<bullet> t) \<approx>4 s \<and> 
-            (pi \<bullet> a) = b)
-       \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
 | a5: "[] \<approx>4list []"
 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
 
@@ -741,6 +743,47 @@
 as
   "rbv5"
 
+lemma rbv5_eqvt:
+  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+sorry
+
+lemma rfv_trm5_eqvt:
+  "pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)"
+sorry
+
+lemma rfv_lts_eqvt:
+  "pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)"
+sorry
+
+lemma alpha5_eqvt:
+  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
+  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
+  apply(induct rule: alpha5_alphalts.inducts)
+  apply (simp_all add: alpha5_inj)
+  apply (erule exE)+
+  apply(unfold alpha_gen)
+  apply (erule conjE)+
+  apply (rule conjI)
+  apply (rule_tac x="x \<bullet> pi" in exI)
+  apply (rule conjI)
+  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+  apply (subst permute_eqvt[symmetric])
+  apply (simp)
+  apply (rule_tac x="x \<bullet> pia" in exI)
+  apply (rule conjI)
+  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+  apply (subst permute_eqvt[symmetric])
+  apply (simp)
+  done
+
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
   "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
@@ -748,27 +791,32 @@
   apply(simp_all add: alpha_gen)
   done
 
-lemma [quot_respect]:
-"(op = ===> alpha5 ===> alpha5) permute permute"
-"(op = ===> alphalts ===> alphalts) permute permute"
-"(op = ===> alpha5) rVr5 rVr5"
-"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
-"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
-"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
-"(alphalts ===> op =) rfv_lts rfv_lts"
-"(alphalts ===> op =) rbv5 rbv5"
-sorry
-
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
-apply(induct rule: alpha5_alphalts.inducts(2))
-apply(simp_all)
-done
+  apply(induct rule: alpha5_alphalts.inducts(2))
+  apply(simp_all)
+  done
 
+lemma [quot_respect]:
+  "(alphalts ===> op =) rfv_lts rfv_lts"
+  "(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+  "(alphalts ===> op =) rbv5 rbv5"
+  "(op = ===> alpha5) rVr5 rVr5"
+  "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+  "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+  "(op = ===> alpha5 ===> alpha5) permute permute"
+  "(op = ===> alphalts ===> alphalts) permute permute"
+  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
+  apply (auto)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  done
 
-lemma 
+lemma
   shows "(alphalts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)