diff -r ae73578feb64 -r 9348581d7d92 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:44:38 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:47:41 2010 +0100
@@ -70,73 +70,73 @@
      @{thms alpha_eqvt} ctxt)) ctxt)) *}
 thm alpha_equivps
 
-quotient_type RKIND = rkind / alpha_rkind
+quotient_type kind = rkind / alpha_rkind
   by (rule alpha_equivps)
 
 quotient_type
-    RTY = rty / alpha_rty and
-    RTRM = rtrm / alpha_rtrm
+    ty = rty / alpha_rty and
+    trm = rtrm / alpha_rtrm
   by (auto intro: alpha_equivps)
 
 quotient_definition
-   "TYP :: RKIND"
+   "TYP :: kind"
 is
   "Type"
 
 quotient_definition
-   "KPI :: RTY \<Rightarrow> name \<Rightarrow> RKIND \<Rightarrow> RKIND"
+   "KPI :: ty \<Rightarrow> name \<Rightarrow> kind \<Rightarrow> kind"
 is
   "KPi"
 
 quotient_definition
-   "TCONST :: ident \<Rightarrow> RTY"
+   "TCONST :: ident \<Rightarrow> ty"
 is
   "TConst"
 
 quotient_definition
-   "TAPP :: RTY \<Rightarrow> RTRM \<Rightarrow> RTY"
+   "TAPP :: ty \<Rightarrow> trm \<Rightarrow> ty"
 is
   "TApp"
 
 quotient_definition
-   "TPI :: RTY \<Rightarrow> name \<Rightarrow> RTY \<Rightarrow> RTY"
+   "TPI :: ty \<Rightarrow> name \<Rightarrow> ty \<Rightarrow> ty"
 is
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_definition
-   "CONS :: ident \<Rightarrow> RTRM"
+   "CONS :: ident \<Rightarrow> trm"
 is
   "Const"
 
 quotient_definition
-   "VAR :: name \<Rightarrow> RTRM"
+   "VAR :: name \<Rightarrow> trm"
 is
   "Var"
 
 quotient_definition
-   "APP :: RTRM \<Rightarrow> RTRM \<Rightarrow> RTRM"
+   "APP :: trm \<Rightarrow> trm \<Rightarrow> trm"
 is
   "App"
 
 quotient_definition
-   "LAM :: RTY \<Rightarrow> name \<Rightarrow> RTRM \<Rightarrow> RTRM"
+   "LAM :: ty \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
 is
   "Lam"
 
 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
 quotient_definition
-   "fv_kind :: RKIND \<Rightarrow> atom set"
+   "fv_kind :: kind \<Rightarrow> atom set"
 is
   "fv_rkind"
 
 quotient_definition
-   "fv_ty :: RTY \<Rightarrow> atom set"
+   "fv_ty :: ty \<Rightarrow> atom set"
 is
   "fv_rty"
 
 quotient_definition
-   "fv_trm :: RTRM \<Rightarrow> atom set"
+   "fv_trm :: trm \<Rightarrow> atom set"
 is
   "fv_rtrm"
 
@@ -204,41 +204,41 @@
   by (simp add: alpha_rfv)
 
 thm rkind_rty_rtrm.induct
-lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
+lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
 
 thm rkind_rty_rtrm.inducts
-lemmas RKIND_RTY_RTRM_inducts = rkind_rty_rtrm.inducts[quot_lifted]
+lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
 
-instantiation RKIND and RTY and RTRM :: pt
+instantiation kind and ty and trm :: pt
 begin
 
 quotient_definition
-  "permute_RKIND :: perm \<Rightarrow> RKIND \<Rightarrow> RKIND"
+  "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
 is
   "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
 
 quotient_definition
-  "permute_RTY :: perm \<Rightarrow> RTY \<Rightarrow> RTY"
+  "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
 is
   "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
 
 quotient_definition
-  "permute_RTRM :: perm \<Rightarrow> RTRM \<Rightarrow> RTRM"
+  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
 is
   "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
 
 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
 
-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)
+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)
 apply (simp_all)
 done
 
 lemma perm_add_ok:
-  "((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)
+  "((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)
 apply (simp_all)
 done
 
@@ -249,9 +249,9 @@
 
 end
 
-lemmas ALPHA_RKIND_ALPHA_RTY_ALPHA_RTRM_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemmas RKIND_RTY_RTRM_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
@@ -265,7 +265,7 @@
  "supp (VAR x) = {atom x}"
  "supp (APP M N) = supp M \<union> supp N"
 apply (simp_all add: supp_def permute_ktt)
-apply (simp_all only: RKIND_RTY_RTRM_INJECT)
+apply (simp_all only: kind_ty_trm_INJECT)
 apply (simp_all only: supp_at_base[simplified supp_def])
 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 done
@@ -288,11 +288,11 @@
 apply(simp_all add: fresh_atom)
 done
 
-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)
+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_rkind_rty_rtrm_easy)
 apply(rule supports_finite)
 apply(rule supp_bind(1))
@@ -305,22 +305,22 @@
 apply(simp add: supp_Pair supp_atom)
 done
 
-instance RKIND and RTY and RTRM :: fs
+instance kind and ty and trm :: fs
 apply(default)
-apply(simp_all only: RKIND_RTY_RTRM_fs)
+apply(simp_all only: kind_ty_trm_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: RKIND_RTY_RTRM_inducts)
+apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)
 apply (simp_all add: supp_rkind_rty_rtrm_easy)
 apply (simp_all add: fv_kind_ty_trm)
 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: RKIND_RTY_RTRM_INJECT)
+apply(simp add: kind_ty_trm_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)
@@ -328,7 +328,7 @@
 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: RKIND_RTY_RTRM_INJECT)
+apply(simp add: kind_ty_trm_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)
@@ -336,7 +336,7 @@
 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: RKIND_RTY_RTRM_INJECT)
+apply(simp add: kind_ty_trm_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)
@@ -345,7 +345,7 @@
 
 (* 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 RKIND_RTY_RTRM_INJECT)
+apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT)
 apply (simp add: alpha_gen supp_fv)
 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
 done