# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264597542 -3600
# Node ID caed1462c951f05f7f6f812c8c033548e7ceebb5
# Parent  fd2493ae3df2321fd66d075d324353ffd1cb9bbc
completely ported

diff -r fd2493ae3df2 -r caed1462c951 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Jan 27 12:19:21 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Jan 27 14:05:42 2010 +0100
@@ -309,24 +309,60 @@
 
 (* does not work yet *)
 primrec
-  permute_trm4 
+  permute_trm4  and permute_trm4_list
 where
   "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
-| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute pi ts)"
+| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
+| "permute_trm4_list pi ([]) = []"
+| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"
+
+lemma pt_trm4_list_zero:
+  fixes t::trm4
+  and   ts::"trm4 list"
+  shows "0 \<bullet> t = t"
+  and   "permute_trm4_list 0 ts = ts"
+apply(induct t and ts rule: trm4.inducts)
+apply(simp_all)
+done
+
+lemma pt_trm4_list_plus:
+  fixes t::trm4
+  and   ts::"trm4 list"
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+  and   "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
+apply(induct t and ts rule: trm4.inducts)
+apply(simp_all)
+done
+
+
+instance
+apply(default)
+apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
+done
 
 end
 
+(* "repairing" of the permute function *)
+lemma repaired:
+  fixes ts::"trm4 list"
+  shows "permute_trm4_list p ts = p \<bullet> ts"
+  apply(induct ts)
+  apply(simp_all)
+  done
+
+thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+
 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)
+| 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"
 | a5: "[] \<approx>4list []"
 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
@@ -339,4 +375,6 @@
   qtrm4list = "trm4 list" / alpha4list
   by (simp_all add: alpha4_equivp alpha4list_equivp)
 
+
+
 end