diff -r 8441b4b2469d -r a69ec3f3f535 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 15:20:40 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 15:20:52 2010 +0100
@@ -316,99 +316,103 @@
 
 section {*** lets with single assignments ***}
 
-datatype trm2 =
-  Vr2 "name"
-| Ap2 "trm2" "trm2"
-| Lm2 "name" "trm2"
-| Lt2 "assign" "trm2"
-and assign =
-  As "name" "trm2"
+datatype rtrm2 =
+  rVr2 "name"
+| rAp2 "rtrm2" "rtrm2"
+| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
+| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
+and rassign =
+  rAs "name" "rtrm2"
 
 (* to be given by the user *)
 primrec 
-  bv2
+  rbv2
 where
-  "bv2 (As x t) = {atom x}"
+  "rbv2 (rAs x t) = {atom x}"
 
 (* needs to be calculated by the package *)
 primrec
-  fv_trm2 and fv_assign
+  fv_rtrm2 and fv_rassign
 where
-  "fv_trm2 (Vr2 x) = {atom x}"
-| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
-| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
-| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
-| "fv_assign (As x t) = (fv_trm2 t)"
+  "fv_rtrm2 (rVr2 x) = {atom x}"
+| "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"
+| "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"
+| "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"
+| "fv_rassign (rAs x t) = fv_rtrm2 t"
 
 (* needs to be stated by the package *)
-instantiation 
-  trm2 and assign :: pt
+instantiation
+  rtrm2 and rassign :: pt
 begin
 
 primrec
-  permute_trm2 and permute_assign
+  permute_rtrm2 and permute_rassign
 where
-  "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
-| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
-| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
-| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
-| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+  "permute_rtrm2 pi (rVr2 a) = rVr2 (pi \<bullet> a)"
+| "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)"
+| "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \<bullet> a) (permute_rtrm2 pi t)"
+| "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)"
+| "permute_rassign pi (rAs a t) = rAs (pi \<bullet> a) (permute_rtrm2 pi t)"
 
-lemma pt_trm2_assign_zero:
-  fixes t::trm2
-  and   b::assign
+lemma pt_rtrm2_rassign_zero:
+  fixes t::rtrm2
+  and   b::rassign
   shows "0 \<bullet> t = t"
   and   "0 \<bullet> b = b"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
 
-lemma pt_trm2_assign_plus:
-  fixes t::trm2
-  and   b::assign
+lemma pt_rtrm2_rassign_plus:
+  fixes t::rtrm2
+  and   b::rassign
   shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
   and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
 
 instance
 apply default
-apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)
 done
 
 
 end
 
 inductive
-  alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+  alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+and
+  alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
-| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> 
-            (fv_trm2 t - {atom a})\<sharp>* pi \<and> 
-            (pi \<bullet> t) \<approx>2 s \<and> 
-            (pi \<bullet> a) = b)
-       \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
-| a4: "\<exists>pi. (
-         fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
-         (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
-         pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)
-       ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
+  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: "\<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" 
+lemma alpha2_equivp:
+  "equivp alpha2"
+  "equivp alpha2a"
   sorry
 
-quotient_type qtrm2 = trm2 / alpha2
-  by (rule alpha2_equivp)
+quotient_type
+  trm2 = rtrm2 / alpha2
+and
+  assign = rassign / alpha2a
+  by (auto intro: alpha2_equivp)
+
+
 
 section {*** lets with many assignments ***}
 
 datatype trm3 =
   Vr3 "name"
 | Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3"
-| Lt3 "assigns" "trm3"
+| Lm3 "name" "trm3" --"bind (name) in (trm3)"
+| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
 and assigns =
   ANil
 | ACons "name" "trm3" "assigns"
@@ -473,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 ***}
@@ -499,7 +506,7 @@
 datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4"
+| Lm4 "name" "trm4"  --"bind (name) in (trm)"
 
 thm trm4.recs
 
@@ -515,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
@@ -573,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)"
 
@@ -593,7 +596,7 @@
 datatype rtrm5 =
   rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
 and rlts =
   rLnil
 | rLcons "name" "rtrm5" "rlts"
@@ -740,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)"
@@ -747,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)