--- a/Quot/Nominal/Terms.thy	Wed Feb 17 13:54:35 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 17 13:56:31 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm"
 begin
 
 atom_decl name
@@ -39,46 +39,7 @@
 | "rfv_bp (BVr x) = {atom x}"
 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
 
-(* needs to be stated by the package *)
-instantiation 
-  rtrm1 and bp :: pt
-begin
-
-primrec
-  permute_rtrm1 and permute_bp
-where
-  "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"
-| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
-| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"
-| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
-| "permute_bp pi (BUnit) = BUnit"
-| "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"
-| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"
-
-lemma pt_rtrm1_bp_zero:
-  fixes t::rtrm1
-  and   b::bp
-  shows "0 \<bullet> t = t"
-  and   "0 \<bullet> b = b"
-apply(induct t and b rule: rtrm1_bp.inducts)
-apply(simp_all)
-done
-
-lemma pt_rtrm1_bp_plus:
-  fixes t::rtrm1
-  and   b::bp
-  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: rtrm1_bp.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)
-done
-
-end
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
 
 inductive
   alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
@@ -340,45 +301,7 @@
 | "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
-  rtrm2 and rassign :: pt
-begin
-
-primrec
-  permute_rtrm2 and permute_rassign
-where
-  "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_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: rtrm2_rassign.inducts)
-apply(simp_all)
-done
-
-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: rtrm2_rassign.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)
-done
-
-
-end
+setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
 
 inductive
   alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
@@ -434,46 +357,7 @@
 | "fv_assigns (ANil) = {}"
 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"
 
-(* needs to be stated by the package *)
-instantiation
- trm3 and assigns :: pt
-begin
-
-primrec
-  permute_trm3 and permute_assigns
-where
-  "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
-| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
-| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
-| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
-| "permute_assigns pi (ANil) = ANil"
-| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"
-
-lemma pt_trm3_assigns_zero:
-  fixes t::trm3
-  and   b::assigns
-  shows "0 \<bullet> t = t"
-  and   "0 \<bullet> b = b"
-apply(induct t and b rule: trm3_assigns.inducts)
-apply(simp_all)
-done
-
-lemma pt_trm3_assigns_plus:
-  fixes t::trm3
-  and   b::assigns
-  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: trm3_assigns.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
-done
-
-
-end
+setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
 
 inductive
   alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
@@ -519,49 +403,9 @@
 | "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 *) 
+(* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
-instantiation
-  trm4 :: pt
-begin
-
-(* does not work yet *)
-primrec
-  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_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
+setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
 
 (* "repairing" of the permute function *)
 lemma repaired:
@@ -616,43 +460,8 @@
 | "rfv_lts (rLnil) = {}"
 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
 
-instantiation
-  rtrm5 and rlts :: pt
-begin
-
-primrec
-  permute_rtrm5 and permute_rlts
-where
-  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
-| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
-| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
-| "permute_rlts pi (rLnil) = rLnil"
-| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
-
-lemma pt_rtrm5_zero:
-  fixes t::rtrm5
-  and   l::rlts
-  shows "0 \<bullet> t = t"
-  and   "0 \<bullet> l = l"
-apply(induct t and l rule: rtrm5_rlts.inducts)
-apply(simp_all)
-done
-
-lemma pt_rtrm5_plus:
-  fixes t::rtrm5
-  and   l::rlts
-  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
-  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
-apply(induct t and l rule: rtrm5_rlts.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
-done
-
-end
+setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
+print_theorems
 
 inductive
   alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
@@ -946,37 +755,8 @@
 | "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}"
 | "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 l"
 
-instantiation
-  rtrm6 :: pt
-begin
-
-primrec
-  permute_rtrm6
-where
-  "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \<bullet> a)"
-| "permute_rtrm6 pi (rLm6 n t) = rLm6 (pi \<bullet> n) (permute_rtrm6 pi t)"
-| "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
-
-lemma pt_rtrm6_zero:
-  fixes t::rtrm6
-  shows "0 \<bullet> t = t"
-apply(induct t)
-apply(simp_all)
-done
-
-lemma pt_rtrm6_plus:
-  fixes t::rtrm6
-  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
-apply(induct t)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus)
-done
-
-end
+setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
+print_theorems
 
 inductive
   alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
@@ -1134,37 +914,8 @@
 | "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}"
 | "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \<union> (rfv_trm7 r - rbv7 l)"
 
-instantiation
-  rtrm7 :: pt
-begin
-
-primrec
-  permute_rtrm7
-where
-  "permute_rtrm7 pi (rVr7 a) = rVr7 (pi \<bullet> a)"
-| "permute_rtrm7 pi (rLm7 a t) = rLm7 (pi \<bullet> a) (permute_rtrm7 pi t)"
-| "permute_rtrm7 pi (rLt7 t1 t2) = rLt7 (permute_rtrm7 pi t1) (permute_rtrm7 pi t2)"
-
-lemma pt_rtrm7_zero:
-  fixes t::rtrm7
-  shows "0 \<bullet> t = t"
-apply(induct t)
-apply(simp_all)
-done
-
-lemma pt_rtrm7_plus:
-  fixes t::rtrm7
-  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
-apply(induct t)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_rtrm7_zero pt_rtrm7_plus)
-done
-
-end
+setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
+print_theorems
 
 inductive
   alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
@@ -1216,21 +967,8 @@
 | "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"
 print_theorems
 
-instantiation
-  rfoo8 and rbar8 :: pt
-begin
-
-primrec
-  permute_rfoo8 and permute_rbar8
-where
-  "permute_rfoo8 pi (Foo0 a) = Foo0 (pi \<bullet> a)"
-| "permute_rfoo8 pi (Foo1 b t) = Foo1 (permute_rbar8 pi b) (permute_rfoo8 pi t)"
-| "permute_rbar8 pi (Bar0 a) = Bar0 (pi \<bullet> a)"
-| "permute_rbar8 pi (Bar1 v x t) = Bar1 (pi \<bullet> v) (pi \<bullet> x) (permute_rbar8 pi t)"
-
-instance sorry
-
-end
+setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
+print_theorems
 
 inductive
   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
@@ -1286,20 +1024,8 @@
 | "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})"
 | "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \<union> rfv_lam9 l"
 
-instantiation
-  rlam9 and rbla9 :: pt
-begin
-
-primrec
-  permute_rlam9 and permute_rbla9
-where
-  "permute_rlam9 pi (Var9 a) = Var9 (pi \<bullet> a)"
-| "permute_rlam9 pi (Lam9 b t) = Lam9 (pi \<bullet> b) (permute_rlam9 pi t)"
-| "permute_rbla9 pi (Bla9 l r) = Bla9 (permute_rlam9 pi l) (permute_rlam9 pi r)"
-
-instance sorry
-
-end
+setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
+print_theorems
 
 inductive
   alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
@@ -1380,70 +1106,14 @@
   Var "name" 
 | Fun "ty" "ty"
 
-instantiation
-  ty :: pt
-begin
-
-primrec
-  permute_ty 
-where
-  "permute_ty pi (Var a) = Var (pi \<bullet> a)"
-| "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"
-
-lemma pt_ty_zero:
-  fixes T::ty
-  shows "0 \<bullet> T = T"
-apply(induct T rule: ty.inducts)
-apply(simp_all)
-done
-
-lemma pt_ty_plus:
-  fixes T::ty
-  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
-apply(induct T rule: ty.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_ty_zero pt_ty_plus)
-done
-
-end
+setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
+print_theorems
 
 datatype tyS = 
   All "name set" "ty" 
 
-instantiation
-  tyS :: pt
-begin
-
-primrec
-  permute_tyS 
-where
-  "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"
-
-lemma pt_tyS_zero:
-  fixes T::tyS
-  shows "0 \<bullet> T = T"
-apply(induct T rule: tyS.inducts)
-apply(simp_all)
-done
-
-lemma pt_tyS_plus:
-  fixes T::tyS
-  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
-apply(induct T rule: tyS.inducts)
-apply(simp_all)
-done
-
-instance
-apply default
-apply(simp_all add: pt_tyS_zero pt_tyS_plus)
-done
-
-end
-
+setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
+print_theorems
 
 abbreviation
   "atoms xs \<equiv> {atom x| x. x \<in> xs}"