diff -r 59dc48db4a84 -r 1240d5eb275d Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 23 18:28:48 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 09:58:12 2010 +0100
@@ -5,50 +5,51 @@
 atom_decl name
 atom_decl ident
 
-datatype kind =
+datatype rkind =
     Type
-  | KPi "ty" "name" "kind"
-and ty =
+  | KPi "rty" "name" "rkind"
+and rty =
     TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" "name" "ty"
-and trm =
+  | TApp "rty" "rtrm"
+  | TPi "rty" "name" "rty"
+and rtrm =
     Const "ident"
   | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" "name" "trm"
+  | App "rtrm" "rtrm"
+  | Lam "rty" "name" "rtrm"
 
-instantiation kind and ty and trm :: pt
+
+instantiation rkind and rty and rtrm :: pt
 begin
 
 primrec
-    permute_kind
-and permute_ty
-and permute_trm
+    permute_rkind
+and permute_rty
+and permute_rtrm
 where
-  "permute_kind pi Type = Type"
-| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
-| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
-| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
-| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
-| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
-| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
-| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
-| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"
+  "permute_rkind pi Type = Type"
+| "permute_rkind pi (KPi t n k) = KPi (permute_rty pi t) (pi \<bullet> n) (permute_rkind pi k)"
+| "permute_rty pi (TConst i) = TConst (pi \<bullet> i)"
+| "permute_rty pi (TApp A M) = TApp (permute_rty pi A) (permute_rtrm pi M)"
+| "permute_rty pi (TPi A x B) = TPi (permute_rty pi A) (pi \<bullet> x) (permute_rty pi B)"
+| "permute_rtrm pi (Const i) = Const (pi \<bullet> i)"
+| "permute_rtrm pi (Var x) = Var (pi \<bullet> x)"
+| "permute_rtrm pi (App M N) = App (permute_rtrm pi M) (permute_rtrm pi N)"
+| "permute_rtrm pi (Lam A x M) = Lam (permute_rty pi A) (pi \<bullet> x) (permute_rtrm pi M)"
 
 lemma rperm_zero_ok:
-  "0 \<bullet> (x :: kind) = x"
-  "0 \<bullet> (y :: ty) = y"
-  "0 \<bullet> (z :: trm) = z"
-apply(induct x and y and z rule: kind_ty_trm.inducts)
+  "0 \<bullet> (x :: rkind) = x"
+  "0 \<bullet> (y :: rty) = y"
+  "0 \<bullet> (z :: rtrm) = z"
+apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
 apply(simp_all)
 done
 
 lemma rperm_plus_ok:
- "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
- "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
- "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
-apply(induct x and y and z rule: kind_ty_trm.inducts)
+ "(p + q) \<bullet> (x :: rkind) = p \<bullet> q \<bullet> x"
+ "(p + q) \<bullet> (y :: rty) = p \<bullet> q \<bullet> y"
+ "(p + q) \<bullet> (z :: rtrm) = p \<bullet> q \<bullet> z"
+apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
 apply(simp_all)
 done
 
@@ -60,120 +61,120 @@
 end
 
 (*
-setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *}
+setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
 local_setup {*
-  snd o define_fv_alpha "LFex.kind"
+  snd o define_fv_alpha "LFex.rkind"
   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 notation
-    alpha_kind  ("_ \<approx>ki _" [100, 100] 100)
-and alpha_ty    ("_ \<approx>ty _" [100, 100] 100)
-and alpha_trm   ("_ \<approx>tr _" [100, 100] 100)
-thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *}
+    alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
+and alpha_rty    ("_ \<approx>rty _" [100, 100] 100)
+and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
+thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
 thm alphas_inj
 
 lemma alphas_eqvt:
   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+  "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 sorry
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
-  (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}]
-     @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} 
-     @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj}
-     @{thms kind.distinct ty.distinct trm.distinct}
-     @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases}
+  (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
+     @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 
+     @{thms rkind.inject rty.inject rtrm.inject} @{thms alphas_inj}
+     @{thms rkind.distinct rty.distinct rtrm.distinct}
+     @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
      @{thms alphas_eqvt} ctxt)) ctxt)) *}
 thm alphas_equivp
 *)
 
 primrec
-    rfv_kind :: "kind \<Rightarrow> atom set"
-and rfv_ty   :: "ty \<Rightarrow> atom set"
-and rfv_trm  :: "trm \<Rightarrow> atom set"
+    rfv_rkind :: "rkind \<Rightarrow> atom set"
+and rfv_rty   :: "rty \<Rightarrow> atom set"
+and rfv_rtrm  :: "rtrm \<Rightarrow> atom set"
 where
-  "rfv_kind (Type) = {}"
-| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {atom i}"
-| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
-| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
-| "rfv_trm (Const i) = {atom i}"
-| "rfv_trm (Var x) = {atom x}"
-| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
-| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
+  "rfv_rkind (Type) = {}"
+| "rfv_rkind (KPi A x K) = (rfv_rty A) \<union> ((rfv_rkind K) - {atom x})"
+| "rfv_rty (TConst i) = {atom i}"
+| "rfv_rty (TApp A M) = (rfv_rty A) \<union> (rfv_rtrm M)"
+| "rfv_rty (TPi A x B) = (rfv_rty A) \<union> ((rfv_rty B) - {atom x})"
+| "rfv_rtrm (Const i) = {atom i}"
+| "rfv_rtrm (Var x) = {atom x}"
+| "rfv_rtrm (App M N) = (rfv_rtrm M) \<union> (rfv_rtrm N)"
+| "rfv_rtrm (Lam A x M) = (rfv_rty A) \<union> ((rfv_rtrm M) - {atom x})"
 
 inductive
-    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
-and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
+    arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)
+and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 where
   a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
-| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
-| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
-| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
+| a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
+| a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
+| a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
+| a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
+| a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
-lemma akind_aty_atrm_inj:
+lemma arkind_arty_artrm_inj:
   "(Type) \<approx>ki (Type) = True"
-  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
-  "(TConst i) \<approx>ty (TConst j) = (i = j)"
-  "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
-  "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
+  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K')))"
+  "(TConst i) \<approx>rty (TConst j) = (i = j)"
+  "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
+  "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))))"
   "(Const i) \<approx>tr (Const j) = (i = j)"
   "(Var x) \<approx>tr (Var y) = (x = y)"
   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
+  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))))"
 apply -
-apply (simp add: akind_aty_atrm.intros)
+apply (simp add: arkind_arty_artrm.intros)
 
-apply rule apply (erule akind.cases) apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule arkind.cases) apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule aty.cases) apply simp apply simp apply simp
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule arty.cases) apply simp apply simp apply simp
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule aty.cases) apply simp apply simp apply simp
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule arty.cases) apply simp apply simp apply simp
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule aty.cases) apply simp apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule arty.cases) apply simp apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 
-apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: akind_aty_atrm.intros)
+apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: arkind_arty_artrm.intros)
 done
 
 lemma rfv_eqvt[eqvt]:
-  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
-  "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
-  "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
-apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
+  "((pi\<bullet>rfv_rkind t1) = rfv_rkind (pi\<bullet>t1))"
+  "((pi\<bullet>rfv_rty t2) = rfv_rty (pi\<bullet>t2))"
+  "((pi\<bullet>rfv_rtrm t3) = rfv_rtrm (pi\<bullet>t3))"
+apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
 apply(simp_all add:  union_eqvt Diff_eqvt)
 apply(simp_all add: permute_set_eq atom_eqvt)
 done
 
 lemma alpha_eqvt:
   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+  "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
-apply(induct rule: akind_aty_atrm.inducts)
-apply (simp_all add: akind_aty_atrm.intros)
-apply (simp_all add: akind_aty_atrm_inj)
+apply(induct rule: arkind_arty_artrm.inducts)
+apply (simp_all add: arkind_arty_artrm.intros)
+apply (simp_all add: arkind_arty_artrm_inj)
 apply (rule alpha_gen_atom_eqvt)
 apply (simp add: rfv_eqvt)
 apply assumption
@@ -186,14 +187,14 @@
 done
 
 lemma al_refl:
-  fixes K::"kind" 
-  and   A::"ty"
-  and   M::"trm"
+  fixes K::"rkind" 
+  and   A::"rty"
+  and   M::"rtrm"
   shows "K \<approx>ki K"
-  and   "A \<approx>ty A"
+  and   "A \<approx>rty A"
   and   "M \<approx>tr M"
-  apply(induct K and A and M rule: kind_ty_trm.inducts)
-  apply(auto intro: akind_aty_atrm.intros)
+  apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
+  apply(auto intro: arkind_arty_artrm.intros)
   apply (rule a2)
   apply auto
   apply(rule_tac x="0" in exI)
@@ -209,13 +210,13 @@
   done
 
 lemma al_sym:
-  fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
+  fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
-  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
+  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A"
   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
-  apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
-  apply(simp_all add: akind_aty_atrm.intros)
-  apply (simp_all add: akind_aty_atrm_inj)
+  apply(induct K K' and A A' and M M' rule: arkind_arty_artrm.inducts)
+  apply(simp_all add: arkind_arty_artrm.intros)
+  apply (simp_all add: arkind_arty_artrm_inj)
   apply(erule alpha_gen_compose_sym)
   apply(erule alpha_eqvt)
   apply(erule alpha_gen_compose_sym)
@@ -225,44 +226,44 @@
   done
 
 lemma al_trans:
-  fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
+  fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
-  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
+  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A'' \<Longrightarrow> A \<approx>rty A''"
   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
-  apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
-  apply(simp_all add: akind_aty_atrm.intros)
-  apply(erule akind.cases)
-  apply(simp_all add: akind_aty_atrm.intros)
-  apply(simp add: akind_aty_atrm_inj)
+  apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: arkind_arty_artrm.inducts)
+  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(erule arkind.cases)
+  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(simp add: arkind_arty_artrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   apply(rotate_tac 4)
-  apply(erule aty.cases)
-  apply(simp_all add: akind_aty_atrm.intros)
+  apply(erule arty.cases)
+  apply(simp_all add: arkind_arty_artrm.intros)
   apply(rotate_tac 3)
-  apply(erule aty.cases)
-  apply(simp_all add: akind_aty_atrm.intros)
-  apply(simp add: akind_aty_atrm_inj)
+  apply(erule arty.cases)
+  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(simp add: arkind_arty_artrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   apply(rotate_tac 4)
-  apply(erule atrm.cases)
-  apply(simp_all add: akind_aty_atrm.intros)
+  apply(erule artrm.cases)
+  apply(simp_all add: arkind_arty_artrm.intros)
   apply(rotate_tac 3)
-  apply(erule atrm.cases)
-  apply(simp_all add: akind_aty_atrm.intros)
-  apply(simp add: akind_aty_atrm_inj)
+  apply(erule artrm.cases)
+  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(simp add: arkind_arty_artrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   done
 
 lemma alpha_equivps:
-  shows "equivp akind"
-  and   "equivp aty"
-  and   "equivp atrm"
+  shows "equivp arkind"
+  and   "equivp arty"
+  and   "equivp artrm"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(auto intro: al_refl al_sym al_trans)
@@ -274,108 +275,108 @@
   apply(auto intro: al_refl al_sym al_trans)
   done
 
-quotient_type KIND = kind / akind
+quotient_type RKIND = rkind / arkind
   by (rule alpha_equivps)
 
 quotient_type
-    TY = ty / aty and
-    TRM = trm / atrm
+    RTY = rty / arty and
+    RTRM = rtrm / artrm
   by (auto intro: alpha_equivps)
 
 quotient_definition
-   "TYP :: KIND"
+   "TYP :: RKIND"
 is
   "Type"
 
 quotient_definition
-   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+   "KPI :: RTY \<Rightarrow> name \<Rightarrow> RKIND \<Rightarrow> RKIND"
 is
   "KPi"
 
 quotient_definition
-   "TCONST :: ident \<Rightarrow> TY"
+   "TCONST :: ident \<Rightarrow> RTY"
 is
   "TConst"
 
 quotient_definition
-   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
+   "TAPP :: RTY \<Rightarrow> RTRM \<Rightarrow> RTY"
 is
   "TApp"
 
 quotient_definition
-   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+   "TPI :: RTY \<Rightarrow> name \<Rightarrow> RTY \<Rightarrow> RTY"
 is
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_definition
-   "CONS :: ident \<Rightarrow> TRM"
+   "CONS :: ident \<Rightarrow> RTRM"
 is
   "Const"
 
 quotient_definition
-   "VAR :: name \<Rightarrow> TRM"
+   "VAR :: name \<Rightarrow> RTRM"
 is
   "Var"
 
 quotient_definition
-   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+   "APP :: RTRM \<Rightarrow> RTRM \<Rightarrow> RTRM"
 is
   "App"
 
 quotient_definition
-   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+   "LAM :: RTY \<Rightarrow> name \<Rightarrow> RTRM \<Rightarrow> RTRM"
 is
   "Lam"
 
-(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
+(* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
 quotient_definition
-   "fv_kind :: KIND \<Rightarrow> atom set"
+   "fv_rkind :: RKIND \<Rightarrow> atom set"
 is
-  "rfv_kind"
+  "rfv_rkind"
 
 quotient_definition
-   "fv_ty :: TY \<Rightarrow> atom set"
+   "fv_rty :: RTY \<Rightarrow> atom set"
 is
-  "rfv_ty"
+  "rfv_rty"
 
 quotient_definition
-   "fv_trm :: TRM \<Rightarrow> atom set"
+   "fv_rtrm :: RTRM \<Rightarrow> atom set"
 is
-  "rfv_trm"
+  "rfv_rtrm"
 
 lemma alpha_rfv:
-  shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
-     (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
-     (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
-  apply(rule akind_aty_atrm.induct)
+  shows "(t \<approx>ki s \<longrightarrow> rfv_rkind t = rfv_rkind s) \<and>
+     (t1 \<approx>rty s1 \<longrightarrow> rfv_rty t1 = rfv_rty s1) \<and>
+     (t2 \<approx>tr s2 \<longrightarrow> rfv_rtrm t2 = rfv_rtrm s2)"
+  apply(rule arkind_arty_artrm.induct)
   apply(simp_all add: alpha_gen)
   done
 
 lemma perm_rsp[quot_respect]:
-  "(op = ===> akind ===> akind) permute permute"
-  "(op = ===> aty ===> aty) permute permute"
-  "(op = ===> atrm ===> atrm) permute permute"
+  "(op = ===> arkind ===> arkind) permute permute"
+  "(op = ===> arty ===> arty) permute permute"
+  "(op = ===> artrm ===> artrm) permute permute"
   by (simp_all add:alpha_eqvt)
 
 lemma tconst_rsp[quot_respect]: 
-  "(op = ===> aty) TConst TConst"
+  "(op = ===> arty) TConst TConst"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma tapp_rsp[quot_respect]: 
-  "(aty ===> atrm ===> aty) TApp TApp" 
+  "(arty ===> artrm ===> arty) TApp TApp" 
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma var_rsp[quot_respect]: 
-  "(op = ===> atrm) Var Var"
+  "(op = ===> artrm) Var Var"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma app_rsp[quot_respect]: 
-  "(atrm ===> atrm ===> atrm) App App"
+  "(artrm ===> artrm ===> artrm) App App"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma const_rsp[quot_respect]: 
-  "(op = ===> atrm) Const Const"
+  "(op = ===> artrm) Const Const"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
 lemma kpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> akind ===> akind) KPi KPi"
+  "(arty ===> op = ===> arkind ===> arkind) KPi KPi"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
   apply (rule a2) apply assumption
   apply (rule_tac x="0" in exI)
@@ -383,66 +384,66 @@
   done
 
 lemma tpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> aty ===> aty) TPi TPi"
+  "(arty ===> op = ===> arty ===> arty) TPi TPi"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
   apply (rule a5) apply assumption
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 lemma lam_rsp[quot_respect]: 
-  "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
+  "(arty ===> op = ===> artrm ===> artrm) Lam Lam"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
   apply (rule a9) apply assumption
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
-lemma rfv_ty_rsp[quot_respect]: 
-  "(aty ===> op =) rfv_ty rfv_ty"
+lemma rfv_rty_rsp[quot_respect]: 
+  "(arty ===> op =) rfv_rty rfv_rty"
   by (simp add: alpha_rfv)
-lemma rfv_kind_rsp[quot_respect]:
-  "(akind ===> op =) rfv_kind rfv_kind"
+lemma rfv_rkind_rsp[quot_respect]:
+  "(arkind ===> op =) rfv_rkind rfv_rkind"
   by (simp add: alpha_rfv)
-lemma rfv_trm_rsp[quot_respect]:
-  "(atrm ===> op =) rfv_trm rfv_trm"
+lemma rfv_rtrm_rsp[quot_respect]:
+  "(artrm ===> op =) rfv_rtrm rfv_rtrm"
   by (simp add: alpha_rfv)
 
-thm kind_ty_trm.induct
-lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]
+thm rkind_rty_rtrm.induct
+lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
 
-thm kind_ty_trm.inducts
-lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]
+thm rkind_rty_rtrm.inducts
+lemmas RKIND_RTY_RTRM_inducts = rkind_rty_rtrm.inducts[quot_lifted]
 
-instantiation KIND and TY and TRM :: pt
+instantiation RKIND and RTY and RTRM :: pt
 begin
 
 quotient_definition
-  "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
+  "permute_RKIND :: perm \<Rightarrow> RKIND \<Rightarrow> RKIND"
 is
-  "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
+  "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
 
 quotient_definition
-  "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
+  "permute_RTY :: perm \<Rightarrow> RTY \<Rightarrow> RTY"
 is
-  "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
+  "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
 
 quotient_definition
-  "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
+  "permute_RTRM :: perm \<Rightarrow> RTRM \<Rightarrow> RTRM"
 is
-  "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
+  "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
 
-lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
+lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
 
-lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
-apply (induct rule: KIND_TY_TRM_induct)
+lemma perm_zero_ok: "0 \<bullet> (x :: RKIND) = x \<and> 0 \<bullet> (y :: RTY) = y \<and> 0 \<bullet> (z :: RTRM) = z"
+apply (induct rule: RKIND_RTY_RTRM_induct)
 apply (simp_all)
 done
 
 lemma perm_add_ok:
-  "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
-  "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
-  "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
-apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
+  "((p + q) \<bullet> (x1 :: RKIND) = (p \<bullet> q \<bullet> x1))"
+  "((p + q) \<bullet> (x2 :: RTY) = p \<bullet> q \<bullet> x2)"
+  "((p + q) \<bullet> (x3 :: RTRM) = p \<bullet> q \<bullet> x3)"
+apply (induct x1 and x2 and x3 rule: RKIND_RTY_RTRM_inducts)
 apply (simp_all)
 done
 
@@ -453,22 +454,22 @@
 
 end
 
-lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]
+lemmas fv_rkind_rty_rtrm = rfv_rkind_rfv_rty_rfv_rtrm.simps[quot_lifted]
 
 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
-lemma supp_kind_ty_trm_easy:
+lemma supp_rkind_rty_rtrm_easy:
  "supp TYP = {}"
  "supp (TCONST i) = {atom i}"
  "supp (TAPP A M) = supp A \<union> supp M"
  "supp (CONS i) = {atom i}"
  "supp (VAR x) = {atom x}"
  "supp (APP M N) = supp M \<union> supp N"
-apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)
+apply (simp_all add: supp_def permute_ktt RKIND_RTY_RTRM_INJECT)
 apply (simp_all only: supp_at_base[simplified supp_def])
 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 done
@@ -476,7 +477,7 @@
 lemma supp_bind:
   "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
   "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
-  "(supp (atom na, (ty, trm))) supports (LAM ty na trm)"
+  "(supp (atom na, (ty, rtrm))) supports (LAM ty na rtrm)"
 apply(simp_all add: supports_def)
 apply(fold fresh_def)
 apply(simp_all add: fresh_Pair swap_fresh_fresh)
@@ -491,12 +492,12 @@
 apply(simp_all add: fresh_atom)
 done
 
-lemma KIND_TY_TRM_fs:
-  "finite (supp (x\<Colon>KIND))"
-  "finite (supp (y\<Colon>TY))"
-  "finite (supp (z\<Colon>TRM))"
-apply(induct x and y and z rule: KIND_TY_TRM_inducts)
-apply(simp_all add: supp_kind_ty_trm_easy)
+lemma RKIND_RTY_RTRM_fs:
+  "finite (supp (x\<Colon>RKIND))"
+  "finite (supp (y\<Colon>RTY))"
+  "finite (supp (z\<Colon>RTRM))"
+apply(induct x and y and z rule: RKIND_RTY_RTRM_inducts)
+apply(simp_all add: supp_rkind_rty_rtrm_easy)
 apply(rule supports_finite)
 apply(rule supp_bind(1))
 apply(simp add: supp_Pair supp_atom)
@@ -508,38 +509,38 @@
 apply(simp add: supp_Pair supp_atom)
 done
 
-instance KIND and TY and TRM :: fs
+instance RKIND and RTY and RTRM :: fs
 apply(default)
-apply(simp_all only: KIND_TY_TRM_fs)
+apply(simp_all only: RKIND_RTY_RTRM_fs)
 done
 
 lemma supp_fv:
- "supp t1 = fv_kind t1"
- "supp t2 = fv_ty t2"
- "supp t3 = fv_trm t3"
-apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
-apply (simp_all add: supp_kind_ty_trm_easy)
-apply (simp_all add: fv_kind_ty_trm)
-apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
+ "supp t1 = fv_rkind t1"
+ "supp t2 = fv_rty t2"
+ "supp t3 = fv_rtrm t3"
+apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts)
+apply (simp_all add: supp_rkind_rty_rtrm_easy)
+apply (simp_all add: fv_rkind_rty_rtrm)
+apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
-apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: RKIND_RTY_RTRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
+apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
-apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: RKIND_RTY_RTRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
+apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
-apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: RKIND_RTY_RTRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
@@ -548,12 +549,12 @@
 
 (* Not needed anymore *)
 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
-apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)
+apply (simp add: permute_set_eq supp_def Abs_eq_iff RKIND_RTY_RTRM_INJECT)
 apply (simp add: alpha_gen supp_fv)
 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
 done
 
-lemma supp_kind_ty_trm:
+lemma supp_rkind_rty_rtrm:
  "supp TYP = {}"
  "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
  "supp (TCONST i) = {atom i}"
@@ -563,8 +564,8 @@
  "supp (VAR x) = {atom x}"
  "supp (APP M N) = supp M \<union> supp N"
  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
-apply (simp_all only: supp_kind_ty_trm_easy)
-apply (simp_all only: supp_fv fv_kind_ty_trm)
+apply (simp_all only: supp_rkind_rty_rtrm_easy)
+apply (simp_all only: supp_fv fv_rkind_rty_rtrm)
 done
 
 end