diff -r 25c4223635f4 -r aa0c572a0718 Quot/Examples/Terms.thy
--- a/Quot/Examples/Terms.thy	Tue Jan 26 20:12:41 2010 +0100
+++ b/Quot/Examples/Terms.thy	Wed Jan 27 07:45:01 2010 +0100
@@ -194,7 +194,10 @@
 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::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> (fv_trm3 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>3 s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> 
+                      (fv_trm3 t - {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::name prm. (
          fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
@@ -207,4 +210,62 @@
 quotient_type qtrm3 = trm3 / alpha3
   by (rule alpha3_equivp)
 
+
+section {*** lam with indirect list recursion ***}
+
+datatype trm4 =
+  Vr4 "name"
+| Ap4 "trm4" "trm4 list"
+| Lm4 "name" "trm4"
+
+thm trm4.recs
+
+primrec
+  fv_trm4 and fv_trm4_list
+where
+  "fv_trm4 (Vr4 x) = {x}"
+| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
+| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {x}"
+| "fv_trm4_list ([]) = {}"
+| "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
+
+
+(* needs to be stated by the package *)
+(* there cannot be a clause for lists, as *) 
+(* permutations are  already defined in Nominal (also functions, options, and so on) *)
+overloading
+  perm_trm4 \<equiv> "perm :: 'x prm \<Rightarrow> trm4 \<Rightarrow> trm4"   (unchecked)
+begin
+
+primrec
+  perm_trm4 
+where
+  "perm_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
+| "perm_trm4 pi (Ap4 t ts) = Ap4 (perm_trm4 pi t) (pi \<bullet> ts)"
+| "perm_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (perm_trm4 pi t)"
+
 end
+
+inductive
+    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
+and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 
+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::name prm. (fv_trm4 t - {a} = fv_trm4 s - {b} \<and> 
+                      (fv_trm4 t - {a})\<sharp>* pi \<and> 
+                      (pi \<bullet> t) \<approx>4 s \<and> 
+                      (pi \<bullet> a) = b)
+       \<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)"
+
+lemma alpha4_equivp: "equivp alpha4" sorry
+lemma alpha4list_equivp: "equivp alpha4list" sorry
+
+quotient_type 
+  qtrm4 = trm4 / alpha4 and
+  qtrm4list = "trm4 list" / alpha4list
+  by (simp_all add: alpha4_equivp alpha4list_equivp)
+
+end