src/HOL/Nominal/Examples/Fsub.thy

 text {* Typing contexts are represented as lists that ``grow" on the left; we
   thereby deviating from the convention in the POPLmark-paper. The lists contain
   pairs of type-variables and types (this is sufficient for Part 1A). *}
 
 text {* In order to state validity-conditions for typing-contexts, the notion of
-  a @{text "domain"} of a typing-context is handy. *}
+  a @{text "dom"} of a typing-context is handy. *}
 
 nominal_primrec
   "tyvrs_of" :: "binding \<Rightarrow> tyvrs set"
 where
   "tyvrs_of (VarB  x y) = {}"

   "vrs_of (VarB  x y) = {x}"
 | "vrs_of (TVarB x y) = {}"
 by auto
 
 consts
-  "ty_domain" :: "env \<Rightarrow> tyvrs set"
+  "ty_dom" :: "env \<Rightarrow> tyvrs set"
 primrec
-  "ty_domain [] = {}"
-  "ty_domain (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_domain \<Gamma>)" 
+  "ty_dom [] = {}"
+  "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
 
 consts
-  "trm_domain" :: "env \<Rightarrow> vrs set"
+  "trm_dom" :: "env \<Rightarrow> vrs set"
 primrec
-  "trm_domain [] = {}"
-  "trm_domain (X#\<Gamma>) = (vrs_of X)\<union>(trm_domain \<Gamma>)" 
+  "trm_dom [] = {}"
+  "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
 
 lemma vrs_of_eqvt[eqvt]:
   fixes pi ::"tyvrs prm"
   and   pi'::"vrs   prm"
   shows "pi \<bullet>(tyvrs_of x) = tyvrs_of (pi\<bullet>x)"
   and   "pi'\<bullet>(tyvrs_of x) = tyvrs_of (pi'\<bullet>x)"
   and   "pi \<bullet>(vrs_of x)   = vrs_of   (pi\<bullet>x)"
   and   "pi'\<bullet>(vrs_of x)   = vrs_of   (pi'\<bullet>x)"
 by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts)
 
-lemma domains_eqvt[eqvt]:
+lemma doms_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
   and   pi'::"vrs prm"
-  shows "pi \<bullet>(ty_domain \<Gamma>)  = ty_domain  (pi\<bullet>\<Gamma>)"
-  and   "pi'\<bullet>(ty_domain \<Gamma>)  = ty_domain  (pi'\<bullet>\<Gamma>)"
-  and   "pi \<bullet>(trm_domain \<Gamma>) = trm_domain (pi\<bullet>\<Gamma>)"
-  and   "pi'\<bullet>(trm_domain \<Gamma>) = trm_domain (pi'\<bullet>\<Gamma>)"
+  shows "pi \<bullet>(ty_dom \<Gamma>)  = ty_dom  (pi\<bullet>\<Gamma>)"
+  and   "pi'\<bullet>(ty_dom \<Gamma>)  = ty_dom  (pi'\<bullet>\<Gamma>)"
+  and   "pi \<bullet>(trm_dom \<Gamma>) = trm_dom (pi\<bullet>\<Gamma>)"
+  and   "pi'\<bullet>(trm_dom \<Gamma>) = trm_dom (pi'\<bullet>\<Gamma>)"
 by (induct \<Gamma>) (simp_all add: eqvts)
 
 lemma finite_vrs:
   shows "finite (tyvrs_of x)"
   and   "finite (vrs_of x)"
 by (nominal_induct rule:binding.strong_induct, auto)
  
-lemma finite_domains:
-  shows "finite (ty_domain \<Gamma>)"
-  and   "finite (trm_domain \<Gamma>)"
+lemma finite_doms:
+  shows "finite (ty_dom \<Gamma>)"
+  and   "finite (trm_dom \<Gamma>)"
 by (induct \<Gamma>, auto simp add: finite_vrs)
 
-lemma ty_domain_supp:
-  shows "(supp (ty_domain  \<Gamma>)) = (ty_domain  \<Gamma>)"
-  and   "(supp (trm_domain \<Gamma>)) = (trm_domain \<Gamma>)"
-by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_domains)+
-
-lemma ty_domain_inclusion:
+lemma ty_dom_supp:
+  shows "(supp (ty_dom  \<Gamma>)) = (ty_dom  \<Gamma>)"
+  and   "(supp (trm_dom \<Gamma>)) = (trm_dom \<Gamma>)"
+by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+
+
+lemma ty_dom_inclusion:
   assumes a: "(TVarB X T)\<in>set \<Gamma>" 
-  shows "X\<in>(ty_domain \<Gamma>)"
+  shows "X\<in>(ty_dom \<Gamma>)"
 using a by (induct \<Gamma>, auto)
 
 lemma ty_binding_existence:
   assumes "X \<in> (tyvrs_of a)"
   shows "\<exists>T.(TVarB X T=a)"
   using assms
 by (nominal_induct a rule: binding.strong_induct, auto)
 
-lemma ty_domain_existence:
-  assumes a: "X\<in>(ty_domain \<Gamma>)" 
+lemma ty_dom_existence:
+  assumes a: "X\<in>(ty_dom \<Gamma>)" 
   shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
   using a 
   apply (induct \<Gamma>, auto) 
   apply (subgoal_tac "\<exists>T.(TVarB X T=a)")
   apply (auto)
   apply (auto simp add: ty_binding_existence)
 done
 
-lemma domains_append:
-  shows "ty_domain (\<Gamma>@\<Delta>) = ((ty_domain \<Gamma>) \<union> (ty_domain \<Delta>))"
-  and   "trm_domain (\<Gamma>@\<Delta>) = ((trm_domain \<Gamma>) \<union> (trm_domain \<Delta>))"
+lemma doms_append:
+  shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
+  and   "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
   by (induct \<Gamma>, auto)
 
 lemma ty_vrs_prm_simp:
   fixes pi::"vrs prm"
   and   S::"ty"
   shows "pi\<bullet>S = S"
 by (induct S rule: ty.induct) (auto simp add: calc_atm)
 
-lemma fresh_ty_domain_cons:
+lemma fresh_ty_dom_cons:
   fixes X::"tyvrs"
-  shows "X\<sharp>(ty_domain (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_domain \<Gamma>))"
+  shows "X\<sharp>(ty_dom (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_dom \<Gamma>))"
   apply (nominal_induct rule:binding.strong_induct)
   apply (auto)
   apply (simp add: fresh_def supp_def eqvts)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)
+  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
   apply (simp add: fresh_def supp_def eqvts)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)+
+  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+
   done
 
 lemma tyvrs_fresh:
   fixes   X::"tyvrs"
   assumes "X \<sharp> a" 

   apply (nominal_induct a rule:binding.strong_induct)
   apply (auto)
   apply (fresh_guess)+
 done
 
-lemma fresh_domain:
+lemma fresh_dom:
   fixes X::"tyvrs"
   assumes a: "X\<sharp>\<Gamma>" 
-  shows "X\<sharp>(ty_domain \<Gamma>)"
+  shows "X\<sharp>(ty_dom \<Gamma>)"
 using a
 apply(induct \<Gamma>)
 apply(simp add: fresh_set_empty) 
-apply(simp only: fresh_ty_domain_cons)
+apply(simp only: fresh_ty_dom_cons)
 apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) 
 done
 
 text {* Not all lists of type @{typ "env"} are well-formed. One condition
   requires that in @{term "TVarB X S#\<Gamma>"} all free variables of @{term "S"} must be 
-  in the @{term "ty_domain"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"} 
+  in the @{term "ty_dom"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"} 
   in @{term "\<Gamma>"}. The set of free variables of @{term "S"} is the 
   @{text "support"} of @{term "S"}. *}
 
 constdefs
   "closed_in" :: "ty \<Rightarrow> env \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
-  "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_domain \<Gamma>)"
+  "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_dom \<Gamma>)"
 
 lemma closed_in_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"

   fixes x::"vrs"
   and   T::"ty"
   shows "x \<sharp> T"
 by (simp add: fresh_def supp_def ty_vrs_prm_simp)
 
-lemma ty_domain_vrs_prm_simp:
+lemma ty_dom_vrs_prm_simp:
   fixes pi::"vrs prm"
   and   \<Gamma>::"env"
-  shows "(ty_domain (pi\<bullet>\<Gamma>)) = (ty_domain \<Gamma>)"
+  shows "(ty_dom (pi\<bullet>\<Gamma>)) = (ty_dom \<Gamma>)"
   apply(induct \<Gamma>) 
   apply (simp add: eqvts)
   apply(simp add:  tyvrs_vrs_prm_simp)
 done
 
 lemma closed_in_eqvt'[eqvt]:
   fixes pi::"vrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
 using a
-by (simp add: closed_in_def ty_domain_vrs_prm_simp  ty_vrs_prm_simp)
+by (simp add: closed_in_def ty_dom_vrs_prm_simp  ty_vrs_prm_simp)
 
 lemma fresh_vrs_of: 
   fixes x::"vrs"
   shows "x\<sharp>vrs_of b = x\<sharp>b"
   by (nominal_induct b rule: binding.strong_induct)
     (simp_all add: fresh_singleton [OF pt_vrs_inst at_vrs_inst] fresh_set_empty ty_vrs_fresh fresh_atm)
 
-lemma fresh_trm_domain: 
+lemma fresh_trm_dom: 
   fixes x::"vrs"
-  shows "x\<sharp> trm_domain \<Gamma> = x\<sharp>\<Gamma>"
+  shows "x\<sharp> trm_dom \<Gamma> = x\<sharp>\<Gamma>"
   by (induct \<Gamma>)
     (simp_all add: fresh_set_empty fresh_list_cons
      fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
-     finite_domains finite_vrs fresh_vrs_of fresh_list_nil)
-
-lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_domain \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
-  by (auto simp add: closed_in_def fresh_def ty_domain_supp)
+     finite_doms finite_vrs fresh_vrs_of fresh_list_nil)
+
+lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
+  by (auto simp add: closed_in_def fresh_def ty_dom_supp)
 
 text {* Now validity of a context is a straightforward inductive definition. *}
   
 inductive
   valid_rel :: "env \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
 where
   valid_nil[simp]:   "\<turnstile> [] ok"
-| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_domain  \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (TVarB X T#\<Gamma>) ok"
-| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_domain \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (VarB  x T#\<Gamma>) ok"
+| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_dom  \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (TVarB X T#\<Gamma>) ok"
+| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (VarB  x T#\<Gamma>) ok"
 
 equivariance valid_rel
 
 declare binding.inject [simp add]
 declare trm.inject     [simp add]
 
-inductive_cases validE[elim]: "\<turnstile> (TVarB X T#\<Gamma>) ok" "\<turnstile> (VarB  x T#\<Gamma>) ok" "\<turnstile> (b#\<Gamma>) ok" 
+inductive_cases validE[elim]: 
+  "\<turnstile> (TVarB X T#\<Gamma>) ok" 
+  "\<turnstile> (VarB  x T#\<Gamma>) ok" 
+  "\<turnstile> (b#\<Gamma>) ok" 
 
 declare binding.inject [simp del]
 declare trm.inject     [simp del]
 
 lemma validE_append:

   and     b: "S closed_in \<Gamma>"
   shows "\<turnstile> (\<Delta>@(TVarB X S)#\<Gamma>) ok"
 using a b
 proof(induct \<Delta>)
   case Nil
-  then show ?case by (auto elim: validE intro: valid_cons simp add: domains_append closed_in_def)
+  then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def)
 next
   case (Cons a \<Gamma>')
   then show ?case 
     by (nominal_induct a rule:binding.strong_induct)
-       (auto elim: validE intro!: valid_cons simp add: domains_append closed_in_def)
+       (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def)
 qed
 
 text {* Well-formed contexts have a unique type-binding for a type-variable. *} 
 
 lemma uniqueness_of_ctxt:

 using a b c
 proof (induct)
   case (valid_consT \<Gamma> X' T')
   moreover
   { fix \<Gamma>'::"env"
-    assume a: "X'\<sharp>(ty_domain \<Gamma>')" 
+    assume a: "X'\<sharp>(ty_dom \<Gamma>')" 
     have "\<not>(\<exists>T.(TVarB X' T)\<in>(set \<Gamma>'))" using a 
     proof (induct \<Gamma>')
       case (Cons Y \<Gamma>')
       thus "\<not> (\<exists>T.(TVarB X' T)\<in>set(Y#\<Gamma>'))"
-	by (simp add:  fresh_ty_domain_cons 
+	by (simp add:  fresh_ty_dom_cons 
                        fresh_fin_union[OF pt_tyvrs_inst  at_tyvrs_inst fs_tyvrs_inst]  
-                       finite_vrs finite_domains, 
+                       finite_vrs finite_doms, 
             auto simp add: fresh_atm fresh_singleton [OF pt_tyvrs_inst at_tyvrs_inst])
     qed (simp)
   }
   ultimately show "T=S" by (auto simp add: binding.inject)
 qed (auto)

 using a b c
 proof (induct)
   case (valid_cons \<Gamma> x' T')
   moreover
   { fix \<Gamma>'::"env"
-    assume a: "x'\<sharp>(trm_domain \<Gamma>')" 
+    assume a: "x'\<sharp>(trm_dom \<Gamma>')" 
     have "\<not>(\<exists>T.(VarB x' T)\<in>(set \<Gamma>'))" using a 
     proof (induct \<Gamma>')
       case (Cons y \<Gamma>')
       thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))" 
 	by (simp add:  fresh_fin_union[OF pt_vrs_inst  at_vrs_inst fs_vrs_inst]  
-                       finite_vrs finite_domains, 
+                       finite_vrs finite_doms, 
             auto simp add: fresh_atm fresh_singleton [OF pt_vrs_inst at_vrs_inst])
     qed (simp)
   }
   ultimately show "T=S" by (auto simp add: binding.inject)
 qed (auto)

   subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_ \<mapsto> _]\<^sub>\<tau>" [300, 0, 0] 300)
 where
   "(Tvar X)[Y \<mapsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)"
 | "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top"
 | "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>"
-| "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>X<:T\<^isub>1. T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>)"
+| "X\<sharp>(Y,T,T\<^isub>1) \<Longrightarrow> (\<forall>X<:T\<^isub>1. T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>)"
   apply (finite_guess)+
   apply (rule TrueI)+
   apply (simp add: abs_fresh)
   apply (fresh_guess)+
   done

   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma type_subst_fresh:
   fixes X::"tyvrs"
-  assumes "X \<sharp> T" and "X \<sharp> P"
-  shows   "X \<sharp> T[Y \<mapsto> P]\<^sub>\<tau>"
+  assumes "X\<sharp>T" and "X\<sharp>P"
+  shows   "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>"
 using assms
 by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
    (auto simp add: abs_fresh)
 
 lemma fresh_type_subst_fresh:

     shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
 using assms 
 by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
    (auto simp add: fresh_atm abs_fresh fresh_nat) 
 
-lemma type_subst_identity: "X \<sharp> T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
+lemma type_subst_identity: 
+  "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
   by (nominal_induct T avoiding: X U rule: ty.strong_induct)
     (simp_all add: fresh_atm abs_fresh)
 
 lemma type_substitution_lemma:  
-  "X \<noteq> Y \<Longrightarrow> X \<sharp> L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
+  "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
   by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct)
     (auto simp add: type_subst_fresh type_subst_identity)
 
 lemma type_subst_rename:
-  "Y \<sharp> T \<Longrightarrow> ([(Y, X)] \<bullet> T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
+  "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X Y U rule: ty.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux)
 
 nominal_primrec
   subst_tyb :: "binding \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> binding" ("_[_ \<mapsto> _]\<^sub>b" [100,100,100] 100)

 | "(VarB  X U)[Y \<mapsto> T]\<^sub>b =  VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
 by auto
 
 lemma binding_subst_fresh:
   fixes X::"tyvrs"
-  assumes "X \<sharp> a"
-  and     "X \<sharp> P"
-  shows "X \<sharp> a[Y \<mapsto> P]\<^sub>b"
+  assumes "X\<sharp>a"
+  and     "X\<sharp>P"
+  shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b"
 using assms
 by (nominal_induct a rule: binding.strong_induct)
    (auto simp add: type_subst_fresh)
 
 lemma binding_subst_identity: 
-  shows "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
+  shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
 by (induct B rule: binding.induct)
    (simp_all add: fresh_atm type_subst_identity)
 
 consts 
   subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)

 "([])[Y \<mapsto> T]\<^sub>e= []"
 "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
 
 lemma ctxt_subst_fresh':
   fixes X::"tyvrs"
-  assumes "X \<sharp> \<Gamma>"
-  and     "X \<sharp> P"
-  shows   "X \<sharp> \<Gamma>[Y \<mapsto> P]\<^sub>e"
+  assumes "X\<sharp>\<Gamma>"
+  and     "X\<sharp>P"
+  shows   "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e"
 using assms
 by (induct \<Gamma>)
    (auto simp add: fresh_list_cons binding_subst_fresh)
 
 lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
 lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
-lemma ctxt_subst_identity: "X \<sharp> \<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
+lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
   by (induct \<Gamma>) (simp_all add: fresh_list_cons binding_subst_identity)
 
 lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<mapsto> T]\<^sub>e = \<Delta>[X \<mapsto> T]\<^sub>e @ \<Gamma>[X \<mapsto> T]\<^sub>e"
   by (induct \<Delta>) simp_all
 

 apply(simp add: abs_fresh)+
 apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
 done
 
 lemma subst_trm_fresh_tyvar:
-  "(X::tyvrs) \<sharp> t \<Longrightarrow> X \<sharp> u \<Longrightarrow> X \<sharp> t[x \<mapsto> u]"
+  fixes X::"tyvrs"
+  shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (auto simp add: trm.fresh abs_fresh)
 
-lemma subst_trm_fresh_var: "x \<sharp> u \<Longrightarrow> x \<sharp> t[x \<mapsto> u]"
+lemma subst_trm_fresh_var: 
+  "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_atm ty_vrs_fresh)
 
 lemma subst_trm_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 

   shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma subst_trm_rename:
-  "y \<sharp> t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
+  "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x y u rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh)
 
 nominal_primrec (freshness_context: "T2::ty")
   subst_trm_ty :: "trm \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> trm"  ("_[_ \<mapsto>\<^sub>\<tau> _]" [300, 0, 0] 300)

 apply(simp add: type_subst_fresh)
 apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
 done
 
 lemma subst_trm_ty_fresh:
-  "(X::tyvrs) \<sharp> t \<Longrightarrow> X \<sharp> T \<Longrightarrow> X \<sharp> t[Y \<mapsto>\<^sub>\<tau> T]"
+  fixes X::"tyvrs"
+  shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: Y T rule: trm.strong_induct)
     (auto simp add: abs_fresh type_subst_fresh)
 
 lemma subst_trm_ty_fresh':
-  "X \<sharp> T \<Longrightarrow> X \<sharp> t[X \<mapsto>\<^sub>\<tau> T]"
+  "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm)
 
 lemma subst_trm_ty_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 

   shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
      (perm_simp add: fresh_left subst_eqvt')+
 
 lemma subst_trm_ty_rename:
-  "Y \<sharp> t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
+  "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
   by (nominal_induct t avoiding: X Y U rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename)
 
 section {* Subtyping-Relation *}
 

 
 inductive 
   subtype_of :: "env \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
 where
   SA_Top[intro]:    "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-| SA_refl_TVar[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
+| SA_refl_TVar[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_dom \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
 | SA_trans_TVar[intro]:    "\<lbrakk>(TVarB X S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T"
 | SA_arrow[intro]:  "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^isub>1 \<rightarrow> S\<^isub>2) <: (T\<^isub>1 \<rightarrow> T\<^isub>2)" 
 | SA_all[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"
 
 lemma subtype_implies_ok:

   have "S closed_in \<Gamma>" by fact
   ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp
 next
   case (SA_trans_TVar X S \<Gamma> T)
   have "(TVarB X S)\<in>set \<Gamma>" by fact
-  hence "X \<in> ty_domain \<Gamma>" by (rule ty_domain_inclusion)
+  hence "X \<in> ty_dom \<Gamma>" by (rule ty_dom_inclusion)
   hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
   moreover
   have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
   hence "T closed_in \<Gamma>" by force
   ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp

   assumes a1: "\<Gamma> \<turnstile> S <: T"
   and     a2: "X\<sharp>\<Gamma>"
   shows "X\<sharp>S \<and> X\<sharp>T"  
 proof -
   from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
-  with a2 have "X\<sharp>ty_domain(\<Gamma>)" by (simp add: fresh_domain)
+  with a2 have "X\<sharp>ty_dom(\<Gamma>)" by (simp add: fresh_dom)
   moreover
   from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
-  hence "supp S \<subseteq> ((supp (ty_domain \<Gamma>))::tyvrs set)" 
-    and "supp T \<subseteq> ((supp (ty_domain \<Gamma>))::tyvrs set)" by (simp_all add: ty_domain_supp closed_in_def)
+  hence "supp S \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" 
+    and "supp T \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def)
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
 qed
 
-lemma valid_ty_domain_fresh:
+lemma valid_ty_dom_fresh:
   fixes X::"tyvrs"
   assumes valid: "\<turnstile> \<Gamma> ok"
-  shows "X\<sharp>(ty_domain \<Gamma>) = X\<sharp>\<Gamma>" 
+  shows "X\<sharp>(ty_dom \<Gamma>) = X\<sharp>\<Gamma>" 
   using valid
   apply induct
   apply (simp add: fresh_list_nil fresh_set_empty)
   apply (simp_all add: binding.fresh fresh_list_cons
-     fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains fresh_atm)
+     fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm)
   apply (auto simp add: closed_in_fresh)
   done
 
 equivariance subtype_of
 
 nominal_inductive subtype_of
   apply (simp_all add: abs_fresh)
-  apply (fastsimp simp add: valid_ty_domain_fresh dest: subtype_implies_ok)
+  apply (fastsimp simp add: valid_ty_dom_fresh dest: subtype_implies_ok)
   apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
   done
 
 section {* Reflexivity of Subtyping *}
 

 proof(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
   case (Forall X T\<^isub>1 T\<^isub>2)
   have ih_T\<^isub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact 
   have ih_T\<^isub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
   have fresh_cond: "X\<sharp>\<Gamma>" by fact
-  hence fresh_ty_domain: "X\<sharp>(ty_domain \<Gamma>)" by (simp add: fresh_domain)
+  hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
   have "(\<forall>X<:T\<^isub>2. T\<^isub>1) closed_in \<Gamma>" by fact
   hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((TVarB  X T\<^isub>2)#\<Gamma>)" 
     by (auto simp add: closed_in_def ty.supp abs_supp)
   have ok: "\<turnstile> \<Gamma> ok" by fact  
-  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_domain by simp
+  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp
   have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
   moreover
   have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp
   ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^isub>2. T\<^isub>1) <: (\<forall>X<:T\<^isub>2. T\<^isub>1)" using fresh_cond 
     by (simp add: subtype_of.SA_all)

 apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
   --{* Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   an explicit definition for @{text "closed_in_def"}. *}
 apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec)
-apply(force dest: fresh_domain simp add: closed_in_def)
+apply(force dest: fresh_dom simp add: closed_in_def)
 done
 
 section {* Weakening *}
 
 text {* In order to prove weakening we introduce the notion of a type-context extending 

 
 constdefs 
   extends :: "env \<Rightarrow> env \<Rightarrow> bool" ("_ extends _" [100,100] 100)
   "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>"
 
-lemma extends_ty_domain:
+lemma extends_ty_dom:
   assumes a: "\<Delta> extends \<Gamma>"
-  shows "ty_domain \<Gamma> \<subseteq> ty_domain \<Delta>"
+  shows "ty_dom \<Gamma> \<subseteq> ty_dom \<Delta>"
   using a 
   apply (auto simp add: extends_def)
-  apply (drule ty_domain_existence)
-  apply (force simp add: ty_domain_inclusion)
+  apply (drule ty_dom_existence)
+  apply (force simp add: ty_dom_inclusion)
   done
 
 lemma extends_closed:
   assumes a1: "T closed_in \<Gamma>"
   and     a2: "\<Delta> extends \<Gamma>"
   shows "T closed_in \<Delta>"
   using a1 a2
-  by (auto dest: extends_ty_domain simp add: closed_in_def)
+  by (auto dest: extends_ty_dom simp add: closed_in_def)
 
 lemma extends_memb:
   assumes a: "\<Delta> extends \<Gamma>"
   and b: "(TVarB X T) \<in> set \<Gamma>"
   shows "(TVarB X T) \<in> set \<Delta>"

   moreover
   have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp
   ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force
 next
   case (SA_refl_TVar \<Gamma> X)
-  have lh_drv_prem: "X \<in> ty_domain \<Gamma>" by fact
+  have lh_drv_prem: "X \<in> ty_dom \<Gamma>" by fact
   have "\<turnstile> \<Delta> ok" by fact
   moreover
   have "\<Delta> extends \<Gamma>" by fact
-  hence "X \<in> ty_domain \<Delta>" using lh_drv_prem by (force dest: extends_ty_domain)
+  hence "X \<in> ty_dom \<Delta>" using lh_drv_prem by (force dest: extends_ty_dom)
   ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force
 next 
   case (SA_arrow \<Gamma> T\<^isub>1 S\<^isub>1 S\<^isub>2 T\<^isub>2) thus "\<Delta> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by blast
 next
   case (SA_all \<Gamma> T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2)
   have fresh_cond: "X\<sharp>\<Delta>" by fact
-  hence fresh_domain: "X\<sharp>(ty_domain \<Delta>)" by (simp add: fresh_domain)
+  hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
   have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
-  hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force   
+  hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover 
   have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   ultimately have "((TVarB X T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 

   shows "\<Delta> \<turnstile> S <: T"
   using a b c 
 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
   case (SA_all \<Gamma> T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2)
   have fresh_cond: "X\<sharp>\<Delta>" by fact
-  hence fresh_domain: "X\<sharp>(ty_domain \<Delta>)" by (simp add: fresh_domain)
+  hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
   have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
-  hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force   
+  hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover
   have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   ultimately have "((TVarB X T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp 
   ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)" using ok by (force intro: SA_all)
-qed (blast intro: extends_closed extends_memb dest: extends_ty_domain)+
+qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+
 
 section {* Transitivity and Narrowing *}
 
 text {* Some inversion lemmas that are needed in the transitivity and narrowing proof.*}
 

 inductive_cases S_ArrowE_left: "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" 
 
 declare ty.inject [simp del]
 
 lemma S_ForallE_left:
-  shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<rbrakk>
+  shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1; X\<sharp>T\<rbrakk>
          \<Longrightarrow> T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = (\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)"
-  apply(frule subtype_implies_ok)
-  apply(ind_cases "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T")
-  apply(auto simp add: ty.inject alpha)
-  apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI)
-  apply(rule conjI)
-  apply(rule sym)
-  apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-  apply(rule pt_tyvrs3)
-  apply(simp)
-  apply(rule at_ds5[OF at_tyvrs_inst])
-  apply(rule conjI)
-  apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm)
-  apply(drule_tac \<Gamma>="((TVarB Xa T\<^isub>1)#\<Gamma>)" in  subtype_implies_closed)+
-  apply(simp add: closed_in_def)
-  apply(drule fresh_domain)+
-  apply(simp add: fresh_def)
-  apply(subgoal_tac "X \<notin> (insert Xa (ty_domain \<Gamma>))")(*A*)
-  apply(force)
-  (*A*)apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domains(1)])
-  (* 2nd conjunct *)apply(frule_tac X="X" in subtype_implies_fresh)
-  apply(assumption)
-  apply (frule_tac \<Gamma>="TVarB Xa T\<^isub>1 # \<Gamma>" in subtype_implies_ok)
-  apply (erule validE)
-  apply (simp add: valid_ty_domain_fresh)
-  apply(drule_tac X="Xa" in subtype_implies_fresh)
-  apply(assumption)
-  apply(drule_tac pi="[(X,Xa)]" in subtype_of.eqvt(2))
-  apply(simp add: calc_atm)
-  apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-  done
+apply(erule subtype_of.strong_cases[where X="X"])
+apply(auto simp add: abs_fresh ty.inject alpha)
+done
 
 text {* Next we prove the transitivity and narrowing for the subtyping-relation. 
 The POPLmark-paper says the following:
 
 \begin{quote}

 lemma 
   shows subtype_transitivity: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 
   and subtype_narrow: "(\<Delta>@[(TVarB X Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N"
 proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
   case (less Q)
-    --{* \begin{minipage}[t]{0.9\textwidth}
-    First we mention the induction hypotheses of the outer induction for later
-    reference:\end{minipage}*}
   have IH_trans:  
     "\<And>Q' \<Gamma> S T. \<lbrakk>size_ty Q' < size_ty Q; \<Gamma>\<turnstile>S<:Q'; \<Gamma>\<turnstile>Q'<:T\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>S<:T" by fact
   have IH_narrow:
     "\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(TVarB X Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk> 
     \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N" by fact
-    --{* \begin{minipage}[t]{0.9\textwidth}
-    We proceed with the transitivity proof as an auxiliary lemma, because it needs 
-    to be referenced in the narrowing proof.\end{minipage}*}
-  have transitivity_aux:
-    "\<And>\<Gamma> S T. \<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
-  proof - 
-    fix \<Gamma>' S' T
-    assume "\<Gamma>' \<turnstile> S' <: Q" --{* left-hand derivation *}
-      and  "\<Gamma>' \<turnstile> Q <: T"  --{* right-hand derivation *}
-    thus "\<Gamma>' \<turnstile> S' <: T"
-    proof (nominal_induct \<Gamma>' S' Q\<equiv>Q rule: subtype_of.strong_induct) 
+
+  { fix \<Gamma> S T
+    have "\<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T" 
+    proof (induct \<Gamma> S Q\<equiv>Q rule: subtype_of.induct) 
       case (SA_Top \<Gamma> S) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S <: Top"}, giving
-	us @{term "\<turnstile> \<Gamma> ok"} and @{term "S closed_in \<Gamma>"}. This case is straightforward, 
-	because the right-hand derivation must be of the form @{term "\<Gamma> \<turnstile> Top <: Top"} 
-	giving us the equation @{term "T = Top"}.\end{minipage}*}
-      hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
-      hence T_inst: "T = Top" by (auto elim: S_TopE)
+      then have rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
+      then have T_inst: "T = Top" by (auto elim: S_TopE)
       from `\<turnstile> \<Gamma> ok` and `S closed_in \<Gamma>`
-      have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
-      thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
+      have "\<Gamma> \<turnstile> S <: Top" by auto
+      then show "\<Gamma> \<turnstile> S <: T" using T_inst by simp 
     next
       case (SA_trans_TVar Y U \<Gamma>) 
-	-- {* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> Tvar Y <: Q"} 
-	with @{term "S = Tvar Y"}. We have therefore @{term "(Y,U)"} 
-	is in @{term "\<Gamma>"} and by inner induction hypothesis that @{term "\<Gamma> \<turnstile> U <: T"}. 
-	By @{text "S_Var"} follows @{term "\<Gamma> \<turnstile> Tvar Y <: T"}.\end{minipage}*}
-      hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
+      then have IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
       have "(TVarB Y U) \<in> set \<Gamma>" by fact
-      with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by (simp add: subtype_of.SA_trans_TVar)
+      with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by auto
     next
       case (SA_refl_TVar \<Gamma> X) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-        In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(Tvar X) <: (Tvar X)"} with
-        @{term "Q=Tvar X"}. The goal then follows immediately from the right-hand 
-	derivation.\end{minipage}*}
-      thus "\<Gamma> \<turnstile> Tvar X <: T" by simp
+      then show "\<Gamma> \<turnstile> Tvar X <: T" by simp
     next
       case (SA_arrow \<Gamma> Q\<^isub>1 S\<^isub>1 S\<^isub>2 Q\<^isub>2) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: Q\<^isub>1 \<rightarrow> Q\<^isub>2"} with
-        @{term "S\<^isub>1\<rightarrow>S\<^isub>2=S"} and @{term "Q\<^isub>1\<rightarrow>Q\<^isub>2=Q"}. We know that the @{text "size_ty"} of 
-	@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
-	so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. 
-	We also have the sub-derivations  @{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "\<Gamma>\<turnstile>S\<^isub>2<:Q\<^isub>2"}.
-	The right-hand derivation is @{term "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T"}. There exist types 
-	@{text "T\<^isub>1,T\<^isub>2"} such that @{term "T=Top \<or> T=T\<^isub>1\<rightarrow>T\<^isub>2"}. The @{term "Top"}-case is 
-	straightforward once we know @{term "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. 
-	In the other case we have the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "\<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"}. 
-	Using the outer induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"} 
-	and @{term "\<Gamma>\<turnstile>S\<^isub>2<:T\<^isub>2"}. By rule @{text "S_Arrow"} follows @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"},
-	which is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>"}.\end{minipage}*}
-      hence rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
+      then have rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
       from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q` 
       have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
       have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact      
       from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
-	by (auto elim: S_ArrowE_left)  
+	by (auto elim: S_ArrowE_left)
       moreover
       have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in \<Gamma>" 
 	using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
       hence "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
       moreover
       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
       moreover
-      { assume "\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"
+      { assume "\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1 \<and> \<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2"
 	then obtain T\<^isub>1 T\<^isub>2 
 	  where T_inst: "T = T\<^isub>1 \<rightarrow> T\<^isub>2" 
 	  and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
 	  and   rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
 	from IH_trans[of "Q\<^isub>1"] 
 	have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
 	moreover
 	from IH_trans[of "Q\<^isub>2"] 
 	have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
-	ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by (simp add: subtype_of.SA_arrow)
-	hence "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
+	ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
+	then have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
       }
       ultimately show "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" by blast
     next
       case (SA_all \<Gamma> Q\<^isub>1 S\<^isub>1 X S\<^isub>2 Q\<^isub>2) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:Q\<^isub>1. Q\<^isub>2)"} with 
-	@{term "(\<forall>X<:S\<^isub>1. S\<^isub>2)=S"} and @{term "(\<forall>X<:Q\<^isub>1. Q\<^isub>2)=Q"}. We therefore have the sub-derivations  
-	@{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "((TVarB X Q\<^isub>1)#\<Gamma>)\<turnstile>S\<^isub>2<:Q\<^isub>2"}. Since @{term "X"} is a binder, we
-	assume that it is sufficiently fresh; in particular we have the freshness conditions
-	@{term "X\<sharp>\<Gamma>"} and @{term "X\<sharp>Q\<^isub>1"} (these assumptions are provided by the strong 
-	induction-rule @{text "subtype_of_induct"}). We know that the @{text "size_ty"} of 
-	@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
-	so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. 
-	The right-hand derivation is @{term "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T"}. Since @{term "X\<sharp>\<Gamma>"} 
-	and @{term "X\<sharp>Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that 
-	@{term "T=Top \<or> T=(\<forall>X<:T\<^isub>1. T\<^isub>2)"}. The @{term "Top"}-case is straightforward once we know 
-	@{term "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. In the other case we have 
-	the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "((TVarB X T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"}. Using the outer 
-	induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"}. From the outer 
-	induction for narrowing we get @{term "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using again 
-	induction for transitivity we obtain @{term "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. By rule 
-	@{text "S_Forall"} and the freshness condition @{term "X\<sharp>\<Gamma>"} follows 
-	@{term "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"}, which is @{term "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T\<^isub>"}.
-	\end{minipage}*}
-      hence rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp
+      then have rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp
       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
       have lh_drv_prm\<^isub>2: "((TVarB X Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
-      then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_domain_fresh)
-      then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" using lh_drv_prm\<^isub>1 by (simp_all add: subtype_implies_fresh)
-      from `(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q` 
-      have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " using fresh_cond by auto
+      then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh)
+      then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" "X\<sharp>T" using rh_drv lh_drv_prm\<^isub>1 
+	by (simp_all add: subtype_implies_fresh)
       from rh_drv 
-      have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=(\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
+      have "T = Top \<or> 
+          (\<exists>T\<^isub>1 T\<^isub>2. T = (\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2)" 
 	using fresh_cond by (simp add: S_ForallE_left)
       moreover
       have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in ((TVarB X Q\<^isub>1)#\<Gamma>)" 
 	using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
-      hence "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
+      then have "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
       moreover
       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
       moreover
       { assume "\<exists>T\<^isub>1 T\<^isub>2. T=(\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"
 	then obtain T\<^isub>1 T\<^isub>2 
 	  where T_inst: "T = (\<forall>X<:T\<^isub>1. T\<^isub>2)" 
 	  and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" 
 	  and   rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
+	have "(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q" by fact 
+	then have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" 
+	  using fresh_cond by auto
 	from IH_trans[of "Q\<^isub>1"] 
 	have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast
 	moreover
 	from IH_narrow[of "Q\<^isub>1" "[]"] 
 	have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>1\<^isub>2_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp

 	  using fresh_cond by (simp add: subtype_of.SA_all)
 	hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" using T_inst by simp
       }
       ultimately show "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" by blast
     qed
-  qed
+  } note transitivity_lemma = this  
 
   { --{* The transitivity proof is now by the auxiliary lemma. *}
     case 1 
     from `\<Gamma> \<turnstile> S <: Q` and `\<Gamma> \<turnstile> Q <: T`
-    show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux) 
+    show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma) 
   next 
-    --{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N"}. *}
     case 2
-    from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` --{* left-hand derivation *}
-      and `\<Gamma> \<turnstile> P<:Q` --{* right-hand derivation *}
+    from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` 
+      and `\<Gamma> \<turnstile> P<:Q` 
     show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 
-    proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of.strong_induct) 
-      case (SA_Top _ S \<Delta> \<Gamma> X)
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> S <: Top"}. We show
-	that the context @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} is ok and that @{term S} is closed in 
-	@{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. Then we can apply the @{text "S_Top"}-rule.\end{minipage}*}
-      hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
+    proof (induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
+      case (SA_Top _ S \<Gamma> X \<Delta>)
+      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
 	and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
       have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
       hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
       with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
       moreover
       from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
-	by (simp add: closed_in_def domains_append)
+	by (simp add: closed_in_def doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
     next
-      case (SA_trans_TVar Y S _ N \<Delta> \<Gamma> X) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} and
-	by inner induction hypothesis we have @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"}. We therefore 
-	know that the contexts @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"} and @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} are ok, and that 
-	@{term "(Y,S)"} is in @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. We need to show that 
-	@{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N"}  holds. In case @{term "X\<noteq>Y"} we know that 
-	@{term "(Y,S)"} is in @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} and can use the inner induction hypothesis 
-	and rule @{text "S_Var"} to conclude. In case @{term "X=Y"} we can infer that 
-	@{term "S=Q"}; moreover we have that  @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>"} and therefore 
-	by @{text "weakening"} that @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we 
-	obtain then @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule 
-	@{text "S_Var"}.\end{minipage}*}
-      hence IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
+      case (SA_trans_TVar Y S _ N \<Gamma> X \<Delta>) 
+      then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
 	and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
 	and rh_drv: "\<Gamma> \<turnstile> P<:Q"
 	and ok\<^isub>Q: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok)
-      hence ok\<^isub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) 
+      then have ok\<^isub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) 
       show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N"
       proof (cases "X=Y")
 	case False
 	have "X\<noteq>Y" by fact
 	hence "(TVarB Y S)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" using lh_drv_prm by (simp add:binding.inject)

 	hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt)
 	hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
 	moreover
 	have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
 	hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
-	ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_aux) 
-	thus "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by (simp only: subtype_of.SA_trans_TVar)
+	ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma) 
+	then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
       qed
     next
-      case (SA_refl_TVar _ Y \<Delta> \<Gamma> X)
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y"} and we
-	therefore know that @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"} is ok and that @{term "Y"} is in 
-	the domain of @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. We therefore know that @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} is ok
-	and that @{term Y} is in the domain of @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. We can conclude by applying 
-	rule @{text "S_Refl"}.\end{minipage}*}
-      hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
-	and lh_drv_prm\<^isub>2: "Y \<in> ty_domain (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
+      case (SA_refl_TVar _ Y \<Gamma> X \<Delta>)
+      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
+	and lh_drv_prm\<^isub>2: "Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
       have "\<Gamma> \<turnstile> P <: Q" by fact
       hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
       with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
       moreover
-      from lh_drv_prm\<^isub>2 have "Y \<in> ty_domain (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: domains_append)
+      from lh_drv_prm\<^isub>2 have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
     next
-      case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Delta> \<Gamma> X) 
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2"} 
-	and the proof is trivial.\end{minipage}*}
-      thus "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
+      case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>) 
+      then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
     next
-      case (SA_all \<Gamma>' T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Delta> \<Gamma> X)
-	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)"}
-	and therfore we know that the binder @{term Y} is fresh for @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. By
-	the inner induction hypothesis we have that @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"} and 
-	@{term "((TVarB Y T\<^isub>1)#\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. Since @{term P} is a subtype of @{term Q}
-	we can infer that @{term Y} is fresh for @{term P} and thus also fresh for 
-	@{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. We can then conclude by applying rule @{text "S_Forall"}.
-	\end{minipage}*}
-      hence rh_drv: "\<Gamma> \<turnstile> P <: Q"
-	and IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" 
-	and "TVarB Y T\<^isub>1 # \<Gamma>' = ((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X Q] @ \<Gamma>" by auto
-      moreover have " \<lbrakk>\<Gamma>\<turnstile>P<:Q; TVarB Y T\<^isub>1 # \<Gamma>' = ((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X Q] @ \<Gamma>\<rbrakk> \<Longrightarrow> (((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X P] @ \<Gamma>)\<turnstile>S\<^isub>2<:T\<^isub>2" by fact
-      ultimately have IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X P] @ \<Gamma>)\<turnstile>S\<^isub>2<:T\<^isub>2" by auto
-      with IH_inner\<^isub>1 IH_inner\<^isub>2 
-      show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by (simp add: subtype_of.SA_all)
+      case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
+      from SA_all(2,4,5,6)
+      have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" 
+	and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" by force+
+      then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by auto
     qed
   } 
 qed
 
 section {* Typing *}

   T_Var[intro]: "\<lbrakk> VarB x T \<in> set \<Gamma>; \<turnstile> \<Gamma> ok \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | T_App[intro]: "\<lbrakk> \<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot> t\<^isub>2 : T\<^isub>2"
 | T_Abs[intro]: "\<lbrakk> VarB x T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> T\<^isub>2"
 | T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 | T_TAbs[intro]:"\<lbrakk> TVarB X T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1. t\<^isub>2) : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
-| T_TApp[intro]:"\<lbrakk> X \<sharp> (\<Gamma>, t\<^isub>1, T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
+| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
 
 equivariance typing
 
 lemma better_T_TApp:
   assumes H1: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T11. T12)"

   assumes "\<Gamma> \<turnstile> t : T"
   shows   "\<turnstile> \<Gamma> ok"
 using assms by (induct, auto)
 
 nominal_inductive typing
-by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain type_subst_fresh
-    simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_domain_fresh fresh_trm_domain)
+by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
+    simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom)
 
 lemma ok_imp_VarB_closed_in:
   assumes ok: "\<turnstile> \<Gamma> ok"
   shows "VarB x T \<in> set \<Gamma> \<Longrightarrow> T closed_in \<Gamma>" using ok
   by induct (auto simp add: binding.inject closed_in_def)
 
 lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
-lemma ty_domain_subst: "ty_domain (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_domain \<Gamma>"
+lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: tyvrs_of_subst)
 
 lemma vrs_of_subst: "vrs_of (B[X \<mapsto> T]\<^sub>b) = vrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
-lemma trm_domain_subst: "trm_domain (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_domain \<Gamma>"
+lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: vrs_of_subst)
 
 lemma subst_closed_in:
   "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)"
   apply (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
-  apply (simp add: closed_in_def ty.supp supp_atm domains_append ty_domain_subst)
+  apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst)
   apply blast
   apply (simp add: closed_in_def ty.supp)
   apply (simp add: closed_in_def ty.supp)
   apply (simp add: closed_in_def ty.supp abs_supp)
   apply (drule_tac x = X in meta_spec)
   apply (drule_tac x = U in meta_spec)
   apply (drule_tac x = "(TVarB tyvrs ty2) # \<Gamma>" in meta_spec)
-  apply (simp add: domains_append ty_domain_subst)
+  apply (simp add: doms_append ty_dom_subst)
   apply blast
   done
 
 lemmas subst_closed_in' = subst_closed_in [where \<Delta>="[]", simplified]
 

 inductive_cases eval_inv_auto[elim]: 
   "Var x \<longmapsto> t'" 
   "(\<lambda>x:T. t) \<longmapsto> t'" 
   "(\<lambda>X<:T. t) \<longmapsto> t'" 
 
-lemma ty_domain_cons:
-  shows "ty_domain (\<Gamma>@[VarB X Q]@\<Delta>) = ty_domain (\<Gamma>@\<Delta>)"
+lemma ty_dom_cons:
+  shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
 by (induct \<Gamma>, auto)
 
 lemma closed_in_cons: 
   assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
   shows "S closed_in (\<Gamma>@\<Delta>)"
-using assms ty_domain_cons closed_in_def by auto
+using assms ty_dom_cons closed_in_def by auto
 
 lemma closed_in_weaken: "T closed_in (\<Delta> @ \<Gamma>) \<Longrightarrow> T closed_in (\<Delta> @ B # \<Gamma>)"
-  by (auto simp add: closed_in_def domains_append)
+  by (auto simp add: closed_in_def doms_append)
 
 lemma closed_in_weaken': "T closed_in \<Gamma> \<Longrightarrow> T closed_in (\<Delta> @ \<Gamma>)"
-  by (auto simp add: closed_in_def domains_append)
+  by (auto simp add: closed_in_def doms_append)
 
 lemma valid_subst:
   assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok"
   and closed: "P closed_in \<Gamma>"
   shows "\<turnstile> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed

   apply assumption
   apply (erule validE)
   apply simp
   apply (rule valid_consT)
   apply assumption
-  apply (simp add: domains_append ty_domain_subst)
-  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)
+  apply (simp add: doms_append ty_dom_subst)
+  apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
   apply (rule_tac S=Q in subst_closed_in')
-  apply (simp add: closed_in_def domains_append ty_domain_subst)
-  apply (simp add: closed_in_def domains_append)
+  apply (simp add: closed_in_def doms_append ty_dom_subst)
+  apply (simp add: closed_in_def doms_append)
   apply blast
   apply simp
   apply (rule valid_cons)
   apply assumption
-  apply (simp add: domains_append trm_domain_subst)
+  apply (simp add: doms_append trm_dom_subst)
   apply (rule_tac S=Q in subst_closed_in')
-  apply (simp add: closed_in_def domains_append ty_domain_subst)
-  apply (simp add: closed_in_def domains_append)
+  apply (simp add: closed_in_def doms_append ty_dom_subst)
+  apply (simp add: closed_in_def doms_append)
   apply blast
   done
 
-lemma ty_domain_vrs:
-  shows "ty_domain (G @ [VarB x Q] @ D) = ty_domain (G @ D)"
+lemma ty_dom_vrs:
+  shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
 by (induct G, auto)
 
 lemma valid_cons':
   assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
   shows "\<turnstile> (\<Gamma> @ \<Delta>) ok"

     with valid_consT show ?thesis by simp
   next
     case (Cons b bs)
     with valid_consT
     have "\<turnstile> (bs @ \<Delta>) ok" by simp
-    moreover from Cons and valid_consT have "X \<sharp> ty_domain (bs @ \<Delta>)"
-      by (simp add: domains_append)
+    moreover from Cons and valid_consT have "X \<sharp> ty_dom (bs @ \<Delta>)"
+      by (simp add: doms_append)
     moreover from Cons and valid_consT have "T closed_in (bs @ \<Delta>)"
-      by (simp add: closed_in_def domains_append)
+      by (simp add: closed_in_def doms_append)
     ultimately have "\<turnstile> (TVarB X T # bs @ \<Delta>) ok"
       by (rule valid_rel.valid_consT)
     with Cons and valid_consT show ?thesis by simp
   qed
 next

     with valid_cons show ?thesis by simp
   next
     case (Cons b bs)
     with valid_cons
     have "\<turnstile> (bs @ \<Delta>) ok" by simp
-    moreover from Cons and valid_cons have "x \<sharp> trm_domain (bs @ \<Delta>)"
-      by (simp add: domains_append finite_domains
+    moreover from Cons and valid_cons have "x \<sharp> trm_dom (bs @ \<Delta>)"
+      by (simp add: doms_append finite_doms
 	fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst])
     moreover from Cons and valid_cons have "T closed_in (bs @ \<Delta>)"
-      by (simp add: closed_in_def domains_append)
+      by (simp add: closed_in_def doms_append)
     ultimately have "\<turnstile> (VarB x T # bs @ \<Delta>) ok"
       by (rule valid_rel.valid_cons)
     with Cons and valid_cons show ?thesis by simp
   qed
 qed

   then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (VarB y T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
     apply (rule valid_cons)
     apply (rule T_Abs)
-    apply (simp add: domains_append
+    apply (simp add: doms_append
       fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
       fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
-      finite_domains finite_vrs fresh_vrs_of T_Abs fresh_trm_domain)
+      finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom)
     apply (rule closed_in_weaken)
     apply (rule closed)
     done
   then have "\<turnstile> ((VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   then have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"

   then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
     apply (rule valid_consT)
     apply (rule T_TAbs)
-    apply (simp add: domains_append
+    apply (simp add: doms_append
       fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
       fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
-      finite_domains finite_vrs tyvrs_fresh T_TAbs fresh_domain)
+      finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom)
     apply (rule closed_in_weaken)
     apply (rule closed)
     done
   then have "\<turnstile> ((TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   then have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"

   ultimately show ?case using subtype_of.SA_Top by auto
 next
   case (SA_refl_TVar G X' G')
   then have "\<turnstile> (G' @ VarB x Q # \<Delta>) ok" by simp
   then have h1:"\<turnstile> (G' @ \<Delta>) ok" by (auto dest: valid_cons')
-  have "X' \<in> ty_domain (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
-  then have h2:"X' \<in> ty_domain (G' @ \<Delta>)" using ty_domain_vrs by auto
+  have "X' \<in> ty_dom (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
+  then have h2:"X' \<in> ty_dom (G' @ \<Delta>)" using ty_dom_vrs by auto
   show ?case using h1 h2 by auto
 next
   case (SA_all G T1 S1 X S2 T2 G')
   have ih1:"TVarB X T1 # G = (TVarB X T1 # G') @ VarB x Q # \<Delta> \<Longrightarrow> ((TVarB X T1 # G') @ \<Delta>)\<turnstile>S2<:T2" by fact
   then have h1:"(TVarB X T1 # (G' @ \<Delta>))\<turnstile>S2<:T2" using SA_all by auto

    moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening)
    ultimately show ?case by auto 
  next
    case (T_TAbs X T1 G t2 T2 x u D)
    from `TVarB X T1 # G \<turnstile> t2 : T2` have "X \<sharp> T1"
-     by (auto simp add: valid_ty_domain_fresh dest: typing_ok intro!: closed_in_fresh)
+     by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
    with `X \<sharp> u` and T_TAbs show ?case by fastsimp
  next
    case (T_TApp X G t1 T2 T11 T12 x u D)
    then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
    then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp

   show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
   proof (cases "X = Y")
     assume eq: "X = Y"
     from eq and SA_trans_TVar have "TVarB Y Q \<in> set G" by simp
     with G_ok have QS: "Q = S" using `TVarB Y S \<in> set G` by (rule uniqueness_of_ctxt)
-    from X\<Gamma>_ok have "X \<sharp> ty_domain \<Gamma>" and "Q closed_in \<Gamma>" by auto
+    from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
     then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
     note `\<Gamma>\<turnstile>P<:Q`
     moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
     moreover have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def)
     ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening)

 	by (rule ctxt_subst_mem_TVarB)
       then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
       with neq and ST show ?thesis by auto
     next
       assume Y: "TVarB Y S \<in> set \<Gamma>"
-      from X\<Gamma>_ok have "X \<sharp> ty_domain \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
-      then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_domain_fresh)
+      from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
+      then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
       with Y have "X \<sharp> S"
 	by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons)
       with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>"
 	by (simp add: type_subst_identity)
       moreover from Y have "TVarB Y S \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp

     assume "X = Y"
     with closed' and ok show ?thesis
       by (auto intro: subtype_reflexivity)
   next
     assume neq: "X \<noteq> Y"
-    with SA_refl_TVar have "Y \<in> ty_domain (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
-      by (simp add: ty_domain_subst domains_append)
+    with SA_refl_TVar have "Y \<in> ty_dom (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
+      by (simp add: ty_dom_subst doms_append)
     with neq and ok show ?thesis by auto
   qed
 next
   case (SA_arrow G T1 S1 S2 T2 X P D)
   then have h1:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   show ?case using subtype_of.SA_arrow h1 h2 by auto
 next
   case (SA_all G T1 S1 Y S2 T2 X P D)
-  then have Y: "Y \<sharp> ty_domain (D @ TVarB X Q # \<Gamma>)"
-    by (auto dest: subtype_implies_ok intro: fresh_domain)
+  then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
+    by (auto dest: subtype_implies_ok intro: fresh_dom)
   moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_closed)
   ultimately have S1: "Y \<sharp> S1" by (rule closed_in_fresh)
   from SA_all have "T1 closed_in (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_closed)

       by (rule ctxt_subst_mem_VarB)
     then show ?thesis by simp
   next
     assume x: "VarB x T \<in> set G"
     from T_Var have ok: "\<turnstile> G ok" by (auto dest: subtype_implies_ok)
-    then have "X \<sharp> ty_domain G" using T_Var by (auto dest: validE_append)
-    with ok have "X \<sharp> G" by (simp add: valid_ty_domain_fresh)
+    then have "X \<sharp> ty_dom G" using T_Var by (auto dest: validE_append)
+    with ok have "X \<sharp> G" by (simp add: valid_ty_dom_fresh)
     moreover from x have "VarB x T \<in> set (D' @ G)" by simp
     then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<mapsto> P]\<^sub>e)"
       by (rule ctxt_subst_mem_VarB)
     ultimately show ?thesis
       by (simp add: ctxt_subst_append ctxt_subst_identity)

 next
   case (T_Sub G' t S T X P D')
   then show ?case using substT_subtype by force
 next
   case (T_TAbs X' G' T1 t2 T2 X P D')
-  then have "X' \<sharp> ty_domain (D' @ TVarB X Q # G)"
+  then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
   and "G' closed_in (D' @ TVarB X Q # G)"
     by (auto dest: typing_ok)
   then have "X' \<sharp> G'" by (rule closed_in_fresh)
   with T_TAbs show ?case by force
 next
   case (T_TApp X' G' t1 T2 T11 T12 X P D')
-  then have "X' \<sharp> ty_domain (D' @ TVarB X Q # G)"
-    by (simp add: fresh_domain)
+  then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
+    by (simp add: fresh_dom)
   moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
     by (auto dest: subtype_implies_closed)
   ultimately have X': "X' \<sharp> T11" by (rule closed_in_fresh)
   from T_TApp have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<mapsto> P]\<^sub>\<tau>"
     by simp

   from T_Abs have "VarB y S # \<Gamma> \<turnstile> [(y, x)] \<bullet> s : T\<^isub>2"
     by (simp add: trm.inject alpha fresh_atm)
   then have "[(y, x)] \<bullet> (VarB y S # \<Gamma>) \<turnstile> [(y, x)] \<bullet> [(y, x)] \<bullet> s : [(y, x)] \<bullet> T\<^isub>2"
     by (rule typing.eqvt)
   moreover from T_Abs have "y \<sharp> \<Gamma>"
-    by (auto dest!: typing_ok simp add: fresh_trm_domain)
+    by (auto dest!: typing_ok simp add: fresh_trm_dom)
   ultimately have "VarB x S # \<Gamma> \<turnstile> s : T\<^isub>2" using T_Abs
     by (perm_simp add: ty_vrs_prm_simp)
   with ty1 show ?case using ty2 by (rule T_Abs)
 next
   case (T_Sub \<Gamma> t S T)

   and   "(TVarB X U # \<Gamma>) \<turnstile> S' <: U'"
   using H H' fresh
 proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct)
   case (T_TAbs Y T\<^isub>1 \<Gamma> t\<^isub>2 T\<^isub>2)
   from `TVarB Y T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2` have Y: "Y \<sharp> \<Gamma>"
-    by (auto dest!: typing_ok simp add: valid_ty_domain_fresh)
+    by (auto dest!: typing_ok simp add: valid_ty_dom_fresh)
   from `Y \<sharp> U'` and `Y \<sharp> X`
   have "(\<forall>X<:U. U') = (\<forall>Y<:U. [(Y, X)] \<bullet> U')"
     by (simp add: ty.inject alpha' fresh_atm)
   with T_TAbs have "\<Gamma> \<turnstile> (\<forall>Y<:S. T\<^isub>2) <: (\<forall>Y<:U. [(Y, X)] \<bullet> U')" by (simp add: trm.inject)
   then obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "(TVarB Y U # \<Gamma>) \<turnstile> T\<^isub>2 <: ([(Y, X)] \<bullet> U')" using T_TAbs Y

   proof (cases rule: eval.strong_cases [where X=X and x=x])
     case (E_TAbs T\<^isub>1\<^isub>1' T\<^isub>2' t\<^isub>1\<^isub>2)
     with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>1\<^isub>1'"
       by (simp_all add: trm.inject)
     moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>1\<^isub>1"
-      by (blast intro: closed_in_fresh fresh_domain dest: subtype_implies_closed)
+      by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
     ultimately obtain S'
       where "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
       and "(TVarB X T\<^isub>1\<^isub>1 # \<Gamma>) \<turnstile> S' <: T\<^isub>1\<^isub>2"
       by (rule TAbs_type') blast
     hence "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : T\<^isub>1\<^isub>2" by (rule T_Sub)