--- a/Quot/Nominal/Terms.thy	Wed Feb 03 13:00:37 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 14:15:07 2010 +0100
@@ -758,40 +758,135 @@
   lts = rlts / alphalts
   by (auto intro: alpha5_equivps)
 
-quotient_definition
-  "Vr5 :: name \<Rightarrow> trm5"
-as
-  "rVr5"
+text {* type schemes *} 
+datatype ty = 
+  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)"
 
-quotient_definition
-  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
-as
-  "rAp5"
+lemma pt_ty_zero:
+  fixes T::ty
+  shows "0 \<bullet> T = T"
+apply(induct T rule: ty.inducts)
+apply(simp_all)
+done
 
-quotient_definition
-  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
-as
-  "rLt5"
+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
 
-quotient_definition
-  "Lnil :: lts"
-as
-  "rLnil"
+end
+
+datatype tyS = 
+  All "name set" "ty" 
 
-quotient_definition
-  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
-as
-  "rLcons"
+instantiation
+  tyS :: pt
+begin
+
+primrec
+  permute_tyS 
+where
+  "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"
 
-quotient_definition
-   "fv_trm5 :: trm5 \<Rightarrow> atom set"
-as
-  "rfv_trm5"
+lemma pt_tyS_zero:
+  fixes T::tyS
+  shows "0 \<bullet> T = T"
+apply(induct T rule: tyS.inducts)
+apply(simp_all)
+done
 
-quotient_definition
-   "fv_ltr :: lts \<Rightarrow> atom set"
-as
-  "rfv_lts"
+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
 
 
+abbreviation
+  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
+
+primrec
+  rfv_ty
+where
+  "rfv_ty (Var n) = {atom n}"
+| "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"
+
+primrec
+  rfv_tyS
+where 
+  "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"
+
+inductive
+  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+where
+  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2)) 
+        \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+
+lemma
+  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+  using a
+  apply(clarify)
+  apply(erule alpha_tyS.cases)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(erule exE)
+  apply(erule conjE)+
+  apply(clarify)
+  apply(simp)
+  apply(simp add: fresh_star_def)
+  apply(auto)
+  done
+  
+
 end