# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263691455 -3600
# Node ID 2468c0f2b2762c76ae8eff1a9d97458adb480ede
# Parent  fe506cb64093d75180f5fdea5e7b999a5289a65d
added permutation functions for the raw calculi

diff -r fe506cb64093 -r 2468c0f2b276 Quot/Examples/Terms.thy
--- a/Quot/Examples/Terms.thy	Sat Jan 16 04:23:27 2010 +0100
+++ b/Quot/Examples/Terms.thy	Sun Jan 17 02:24:15 2010 +0100
@@ -4,7 +4,10 @@
 
 atom_decl name
 
-text {*** lets with binding patterns ***}
+text {* primrec seems to be genarally faster than fun *}
+
+section {*** lets with binding patterns ***}
+
 datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
@@ -16,7 +19,7 @@
 | BPr "bp" "bp"
 
 (* to be given by the user *)
-fun 
+primrec 
   bv1
 where
   "bv1 (BUnit) = {}"
@@ -24,7 +27,7 @@
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
 
 (* needs to be calculated by the package *)
-fun 
+primrec 
   fv_trm1 and fv_bp
 where
   "fv_trm1 (Vr1 x) = {x}"
@@ -35,7 +38,28 @@
 | "fv_bp (BVr x) = {x}"
 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"
 
-text {*** lets with single assignments ***}
+(* needs to be stated by the package *)
+overloading
+  perm_trm1 \<equiv> "perm :: 'x prm \<Rightarrow> trm1 \<Rightarrow> trm1"   (unchecked)
+  perm_bp \<equiv> "perm :: 'x prm \<Rightarrow> bp \<Rightarrow> bp" (unchecked)
+begin
+
+primrec
+  perm_trm1 and perm_bp
+where
+  "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)"
+| "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)"
+| "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)"
+| "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)"
+| "perm_bp pi (BUnit) = BUnit"
+| "perm_bp pi (BVr a) = BVr (pi \<bullet> a)"
+| "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)"
+
+end
+
+
+section {*** lets with single assignments ***}
+
 datatype trm2 =
   Vr2 "name"
 | Ap2 "trm2" "trm2"
@@ -45,13 +69,13 @@
   As "name" "trm2"
 
 (* to be given by the user *)
-fun 
+primrec 
   bv2
 where
   "bv2 (As x t) = {x}"
 
 (* needs to be calculated by the package *)
-fun 
+primrec
   fv_trm2 and fv_assign
 where
   "fv_trm2 (Vr2 x) = {x}"
@@ -60,8 +84,26 @@
 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
 | "fv_assign (As x t) = (fv_trm2 t)"
 
+(* needs to be stated by the package *)
+overloading
+  perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2"   (unchecked)
+  perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked)
+begin
 
-text {*** lets with many assignments ***}
+primrec
+  perm_trm2 and perm_assign
+where
+  "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
+| "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)"
+| "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)"
+| "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)"
+| "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)"
+
+end
+
+
+section {*** lets with many assignments ***}
+
 datatype trm3 =
   Vr3 "name"
 | Ap3 "trm3" "trm3"
@@ -72,13 +114,13 @@
 | ACons "name" "trm3" "assigns"
 
 (* to be given by the user *)
-fun 
+primrec 
   bv3
 where
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)"
 
-fun 
+primrec
   fv_trm3 and fv_assigns
 where
   "fv_trm3 (Vr3 x) = {x}"
@@ -88,4 +130,23 @@
 | "fv_assigns (ANil) = {}"
 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"
 
+(* needs to be stated by the package *)
+overloading
+  perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3"   (unchecked)
+  perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked)
+begin
+
+primrec
+  perm_trm3 and perm_assigns
+where
+  "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
+| "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)"
+| "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)"
+| "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)"
+| "perm_assigns pi (ANil) = ANil"
+| "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)"
+
+end
+
+
 end
\ No newline at end of file