more

Author: Andrei Popescu

thys/POPLmark/POPLmark_1A.thy

@@ -5,8 +5,8 @@ begin
 (********************* Actual formalization ************************)
 
 lemma ty_refl: "\<lbrakk>wf \<Gamma> ; T closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T <: T"
-proof (binder_induction T arbitrary: \<Gamma> avoiding: "dom \<Gamma>" rule: Type.strong_induct)
-  case (TyVar x \<Gamma>)
+proof (binder_induction T arbitrary: \<Gamma> avoiding: "dom \<Gamma>" rule: sftypeP.strong_induct)
+  case (TVr x \<Gamma>)
   then show ?case by blast
 qed (auto simp: Diff_single_insert SA_All wf_Cons)
 
@@ -83,24 +83,22 @@ proof (induction \<Delta>)
   then show ?case unfolding 1 using Cons 2 by auto
 qed auto
 
-(* todo for A: look at this and the next *)
-(* TODO: Automatically derive these from strong induction *)
 lemma SA_AllE1[consumes 2, case_names SA_Trans_TVar SA_All]:
   assumes "\<Gamma> \<turnstile> \<forall>X<:S\<^sub>1. S\<^sub>2 <: T" "X \<notin> dom \<Gamma>"
     and Top: "\<And>\<Gamma>. \<lbrakk>wf \<Gamma>; \<forall>X<:S\<^sub>1. S\<^sub>2 closed_in \<Gamma> \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) Top"
     and Forall: "\<And>\<Gamma> T\<^sub>1 T\<^sub>2. \<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) (\<forall>X<:T\<^sub>1 . T\<^sub>2)"
   shows "R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) T"
 using assms(1,2) proof (binder_induction \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T avoiding: \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T rule: ty.strong_induct)
   case (SA_All \<Gamma> T\<^sub>1 R\<^sub>1 Y R\<^sub>2 T\<^sub>2)
-  have 1: "\<forall>Y<:T\<^sub>1 . T\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) T\<^sub>2"
+  have 1: "\<forall>Y<:T\<^sub>1 . T\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) T\<^sub>2"
     apply (rule Forall_swap)
     using SA_All(6,9) well_scoped(2) by fastforce
-  have fresh: "X \<notin> FFVars_Type T\<^sub>1"
+  have fresh: "X \<notin> FFVars_sftypeP T\<^sub>1"
     by (meson SA_All(4,9) in_mono well_scoped(1))
-  have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) Type_inject(3) by blast
-  have x: "\<forall>Y<:S\<^sub>1. R\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) R\<^sub>2"
+  have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) sftypeP_inject(3) by blast
+  have x: "\<forall>Y<:S\<^sub>1. R\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) R\<^sub>2"
     apply (rule Forall_swap)
-    by (metis (no_types, lifting) SA_All(8) assms(1,2) in_mono sup.bounded_iff Type.set(4) well_scoped(1))
+    by (metis (no_types, lifting) SA_All(8) assms(1,2) in_mono sup.bounded_iff sftypeP.set(4) well_scoped(1))
   show ?case unfolding 1
     apply (rule Forall)
     using same SA_All(4) apply simp
@@ -120,27 +118,27 @@ qed (auto simp: Top)
 
 lemma SA_AllE2[consumes 2, case_names SA_Trans_TVar SA_All]:
   assumes "\<Gamma> \<turnstile> S <: \<forall>X<:T\<^sub>1. T\<^sub>2" "X \<notin> dom \<Gamma>"
-    and TyVar: "\<And>\<Gamma> x U. \<lbrakk> x<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: \<forall> X <: T\<^sub>1 . T\<^sub>2 ; R \<Gamma> U (\<forall>X<:T\<^sub>1. T\<^sub>2) \<rbrakk> \<Longrightarrow> R \<Gamma> (TyVar x) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
+    and TVr: "\<And>\<Gamma> x U. \<lbrakk> x<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: \<forall> X <: T\<^sub>1 . T\<^sub>2 ; R \<Gamma> U (\<forall>X<:T\<^sub>1. T\<^sub>2) \<rbrakk> \<Longrightarrow> R \<Gamma> (TVr x) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
     and Forall: "\<And>\<Gamma> S\<^sub>1 S\<^sub>2. \<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
   shows "R \<Gamma> S (\<forall>X<:T\<^sub>1. T\<^sub>2)"
 using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^sub>2" avoiding: \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^sub>2" rule: ty.strong_induct)
   case (SA_All \<Gamma> R\<^sub>1 S\<^sub>1 Y S\<^sub>2 R\<^sub>2)
-  have 1: "\<forall>Y<:S\<^sub>1. S\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) S\<^sub>2"
+  have 1: "\<forall>Y<:S\<^sub>1. S\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) S\<^sub>2"
     apply (rule Forall_swap)
     using SA_All(6,9) well_scoped(1) by fastforce
   have fresh: "X \<notin> dom \<Gamma>" "Y \<notin> dom \<Gamma>"
     using SA_All(9) apply blast
     by (metis SA_All(6) fst_conv wf_ConsE wf_context)
-  have fresh2: "X \<notin> FFVars_Type T\<^sub>1" "Y \<notin> FFVars_Type T\<^sub>1"
-     apply (metis SA_All(4,8) in_mono fresh(1) Type_inject(3) well_scoped(1))
-    by (metis SA_All(4,8) in_mono fresh(2) Type_inject(3) well_scoped(1))
-  have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) Type_inject(3) by blast
-  have x: "\<forall>Y<:T\<^sub>1 . R\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) R\<^sub>2"
+  have fresh2: "X \<notin> FFVars_sftypeP T\<^sub>1" "Y \<notin> FFVars_sftypeP T\<^sub>1"
+     apply (metis SA_All(4,8) in_mono fresh(1) sftypeP_inject(3) well_scoped(1))
+    by (metis SA_All(4,8) in_mono fresh(2) sftypeP_inject(3) well_scoped(1))
+  have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) sftypeP_inject(3) by blast
+  have x: "\<forall>Y<:T\<^sub>1 . R\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) R\<^sub>2"
     apply (rule Forall_swap)
-    by (metis SA_All(8) Un_iff assms(1,2) in_mono Type.set(4) well_scoped(2))
+    by (metis SA_All(8) Un_iff assms(1,2) in_mono sftypeP.set(4) well_scoped(2))
   show ?case unfolding 1
     apply (rule Forall)
-     apply (metis SA_All(4,8) Type_inject(3))
+     apply (metis SA_All(4,8) sftypeP_inject(3))
     apply (rule iffD2[OF arg_cong3[OF _ refl, of _ _ _ _ ty], rotated -1])
       apply (rule ty.equiv)
        apply (rule bij_swap supp_swap_bound infinite_var)+
@@ -151,9 +149,9 @@ using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^
      apply (rule arg_cong3[of _ _ _ _ _ _ extend])
     using fresh apply (metis bij_swap SA_All(4) Un_iff context_map_cong_id fun_upd_apply id_apply infinite_var supp_swap_bound wf_FFVars wf_context)
       apply simp
-    using fresh2 unfolding same apply (metis bij_swap fun_upd_apply id_apply infinite_var supp_swap_bound Type.rrename_cong_ids)
+    using fresh2 unfolding same apply (metis bij_swap fun_upd_apply id_apply infinite_var supp_swap_bound sftypeP.rrename_cong_ids)
     using SA_All(8) x Forall_inject_same unfolding same by simp
-qed (auto simp: TyVar)
+qed (auto simp: TVr)
 
 lemma ty_transitivity : "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   and ty_narrowing : "\<lbrakk> (\<Gamma> ,, X <: Q),, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
@@ -162,25 +160,25 @@ proof -
     ty_trans: "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   and ty_narrow: "\<lbrakk> (\<Gamma>,, X <: Q),, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q ; wf (\<Gamma>,, X <: R,, \<Delta>) ; 
     M closed_in (\<Gamma>,, X <: R,, \<Delta>) ; N closed_in (\<Gamma>,, X <: R,, \<Delta>) \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
-  proof (binder_induction Q arbitrary: \<Gamma> \<Delta> S T M N X R avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: Type.strong_induct)
-    case (TyVar Y \<Gamma> \<Delta> S T M N X R)
+  proof (binder_induction Q arbitrary: \<Gamma> \<Delta> S T M N X R avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: sftypeP.strong_induct)
+    case (TVr Y \<Gamma> \<Delta> S T M N X R)
     {
       fix \<Gamma> S T
-      show ty_trans: "\<Gamma> \<turnstile> S <: TyVar Y \<Longrightarrow> \<Gamma> \<turnstile> TyVar Y <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
-        by (induction \<Gamma> S "TyVar Y" rule: ty.induct) auto
+      show ty_trans: "\<Gamma> \<turnstile> S <: TVr Y \<Longrightarrow> \<Gamma> \<turnstile> TVr Y <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
+        by (induction \<Gamma> S "TVr Y" rule: ty.induct) auto
     } note ty_trans = this
     {
       case 2
       then show ?case
-      proof (binder_induction "\<Gamma>,, X <: TyVar Y,, \<Delta>" M N arbitrary: \<Delta> avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: ty.strong_induct)
+      proof (binder_induction "\<Gamma>,, X <: TVr Y,, \<Delta>" M N arbitrary: \<Delta> avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: ty.strong_induct)
         case (SA_Trans_TVar Z U T \<Delta>')
         show ?case
         proof (cases "X = Z")
           case True
-          then have u: "U = TyVar Y" using SA_Trans_TVar(1,2) context_determ wf_context by blast
-          have "TyVar Y closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
-          then have "\<Gamma>,, Z <: R ,, \<Delta>' \<turnstile> TyVar Y <: T" using SA_Trans_TVar True u by auto
-          moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: TyVar Y" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
+          then have u: "U = TVr Y" using SA_Trans_TVar(1,2) context_determ wf_context by blast
+          have "TVr Y closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
+          then have "\<Gamma>,, Z <: R ,, \<Delta>' \<turnstile> TVr Y <: T" using SA_Trans_TVar True u by auto
+          moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: TVr Y" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
             by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
           ultimately have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: T" using ty_trans by blast
           then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
@@ -254,7 +252,7 @@ proof -
           then show ?thesis by (meson left(1,3) ty.SA_Arrow ty.SA_Top well_scoped(1))
         next
           case right: (SA_Arrow U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2)
-          then show ?thesis using left by (metis Fun(1,3) SA_Arrow Type_inject(2))
+          then show ?thesis using left by (metis Fun(1,3) SA_Arrow sftypeP_inject(2))
         qed auto
       qed auto
     } note ty_trans = this
@@ -396,10 +394,10 @@ proof -
 qed
 
 theorem ty_transitivity2: "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
-proof (binder_induction Q arbitrary: \<Gamma> S T avoiding: "dom \<Gamma>" rule: Type.strong_induct)
-  case (TyVar x \<Gamma> S T)
+proof (binder_induction Q arbitrary: \<Gamma> S T avoiding: "dom \<Gamma>" rule: sftypeP.strong_induct)
+  case (TVr x \<Gamma> S T)
   then show ?case
-    by (induction \<Gamma> S "TyVar x") auto
+    by (induction \<Gamma> S "TVr x") auto
 next
   case (Fun x1 x2 \<Gamma> S T)
   from Fun(4,3) show ?case
@@ -413,8 +411,8 @@ next
       case (SA_Arrow \<Gamma> U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2)
       show ?case
         apply (rule ty.SA_Arrow)
-         apply (metis Fun(1) SA_Arrow(1,5,6,8) Type_inject(2))
-        by (metis Fun(2) SA_Arrow(3,5,7,8) Type_inject(2))
+         apply (metis Fun(1) SA_Arrow(1,5,6,8) sftypeP_inject(2))
+        by (metis Fun(2) SA_Arrow(3,5,7,8) sftypeP_inject(2))
     qed auto
   qed auto
 next
@@ -437,9 +435,9 @@ next
   qed blast
 qed auto
 
-(*
+
 corollary ty_narrowing2: "\<lbrakk> \<Gamma>,, X <: Q,, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q \<rbrakk> \<Longrightarrow> \<Gamma>,, X <: R,, \<Delta> \<turnstile> M <: N"
   using ty_narrowing_aux ty_transitivity2 by blast
-*)
+
 
 end

thys/POPLmark/SystemFSub.thy

@@ -1,12 +1,12 @@
-(* System F with SubTypeing  *)
+(* System F with SubsftypePing  *)
 theory SystemFSub
   imports "SystemFSub_Types"
 begin
 
-abbreviation in_context :: "var \<Rightarrow> type \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ <: _ \<in> _" [55,55,55] 60) where
+abbreviation in_context :: "var \<Rightarrow> sftype \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ <: _ \<in> _" [55,55,55] 60) where
   "x <: t \<in> \<Gamma> \<equiv> (x, t) \<in> set \<Gamma>"
-abbreviation well_scoped :: "type \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ closed'_in _" [55, 55] 60) where
-  "well_scoped S \<Gamma> \<equiv> FFVars_Type S \<subseteq> dom \<Gamma>"
+abbreviation well_scoped :: "sftype \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ closed'_in _" [55, 55] 60) where
+  "well_scoped S \<Gamma> \<equiv> FFVars_sftypeP S \<subseteq> dom \<Gamma>"
 
 inductive wf :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> bool"  where
   wf_Nil[intro]: "wf []"
@@ -19,18 +19,18 @@ print_theorems
 
 lemma in_context_eqvt:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
-  shows "x <: T \<in> \<Gamma> \<Longrightarrow> f x <: rrename_Type f T \<in> map_context f \<Gamma>"
+  shows "x <: T \<in> \<Gamma> \<Longrightarrow> f x <: rrename_sftypeP f T \<in> map_context f \<Gamma>"
   using assms unfolding map_context_def by auto
 
 lemma extend_eqvt:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
-  shows "map_context f (\<Gamma>,,x<:T) = map_context f \<Gamma>,,f x <: rrename_Type f T"
+  shows "map_context f (\<Gamma>,,x<:T) = map_context f \<Gamma>,,f x <: rrename_sftypeP f T"
   using assms unfolding map_context_def by simp
 
 lemma closed_in_eqvt:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
-  shows "S closed_in \<Gamma> \<Longrightarrow> rrename_Type f S closed_in map_context f \<Gamma>"
-  using assms by (auto simp: Type.FFVars_rrenames)
+  shows "S closed_in \<Gamma> \<Longrightarrow> rrename_sftypeP f S closed_in map_context f \<Gamma>"
+  using assms by (auto simp: sftypeP.FFVars_rrenames)
 
 lemma wf_eqvt:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
@@ -42,11 +42,11 @@ unfolding map_context_def proof (induction \<Gamma>)
     using closed_in_eqvt map_context_def by fastforce
 qed simp
 
-abbreviation Tsupp :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> type \<Rightarrow> type \<Rightarrow> var set" where
-  "Tsupp \<Gamma> T\<^sub>1 T\<^sub>2 \<equiv> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<union> FFVars_Type T\<^sub>1 \<union> FFVars_Type T\<^sub>2"
+abbreviation Tsupp :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> sftype \<Rightarrow> sftype \<Rightarrow> var set" where
+  "Tsupp \<Gamma> T\<^sub>1 T\<^sub>2 \<equiv> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<union> FFVars_sftypeP T\<^sub>1 \<union> FFVars_sftypeP T\<^sub>2"
 
 lemma small_Tsupp: "small (Tsupp \<Gamma> T\<^sub>1 T\<^sub>2)"
-  by (auto simp: small_def Type.card_of_FFVars_bounds Type.Un_bound var_Type_pre_class.UN_bound set_bd_UNIV Type.set_bd)
+  by (auto simp: small_def sftypeP.card_of_FFVars_bounds sftypeP.Un_bound var_sftypeP_pre_class.UN_bound set_bd_UNIV sftypeP.set_bd)
 
 lemma fresh: "\<exists>xx. xx \<notin> Tsupp \<Gamma> T\<^sub>1 T\<^sub>2"
   by (metis emp_bound equals0D imageI inf.commute inf_absorb2 small_Tsupp small_def small_isPerm subsetI)
@@ -73,17 +73,17 @@ qed
 
 (* *)
 
-inductive ty :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [55,55,55] 60) where
+inductive ty :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> sftype \<Rightarrow> sftype \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [55,55,55] 60) where
   SA_Top: "\<lbrakk>wf \<Gamma>; S closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-| SA_Refl_TVar: "\<lbrakk>wf \<Gamma>; TyVar x closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TyVar x <: TyVar x"
-| SA_Trans_TVar: "\<lbrakk> X<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TyVar X <: T"
+| SA_Refl_TVar: "\<lbrakk>wf \<Gamma>; TVr x closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TVr x <: TVr x"
+| SA_Trans_TVar: "\<lbrakk> X<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TVr X <: T"
 | SA_Arrow: "\<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2"
 | SA_All: "\<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> \<forall>X<:S\<^sub>1. S\<^sub>2 <: \<forall>X<:T\<^sub>1 .T\<^sub>2"
 
 inductive_cases
   SA_TopE[elim!]: "\<Gamma> \<turnstile> Top <: T"
 and
-  SA_TVarE: "\<Gamma> \<turnstile> S <: TyVar Z"
+  SA_TVarE: "\<Gamma> \<turnstile> S <: TVr Z"
 and
   SA_ArrER: "\<Gamma> \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2"
 and
@@ -102,24 +102,24 @@ lemma well_scoped:
 using assms proof (induction \<Gamma> S T rule: ty.induct)
 case (SA_Trans_TVar x U \<Gamma> T) {
   case 1 then show ?case using SA_Trans_TVar
-    by (metis fst_conv imageI singletonD subsetI Type.set(1))
+    by (metis fst_conv imageI singletonD subsetI sftypeP.set(1))
 next
   case 2 then show ?case using SA_Trans_TVar by simp
 } qed auto
 
 declare ty.intros[intro]
 
-lemma ty_fresh_extend: "\<Gamma>,, x <: U \<turnstile> S <: T \<Longrightarrow> x \<notin> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<and> x \<notin> FFVars_Type U"
+lemma ty_fresh_extend: "\<Gamma>,, x <: U \<turnstile> S <: T \<Longrightarrow> x \<notin> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<and> x \<notin> FFVars_sftypeP U"
   by (metis (no_types, lifting) UnE fst_conv snd_conv subsetD wf_ConsE wf_FFVars wf_context)
 
 make_binder_inductive ty
   subgoal for R B \<sigma> \<Gamma> T1 T2
     unfolding split_beta
     by (elim disj_forward exE)
-      (auto simp add: isPerm_def supp_inv_bound map_context_def[symmetric] Type_vvsubst_rrename
-        Type.rrename_comps Type.FFVars_rrenames wf_eqvt extend_eqvt
+      (auto simp add: isPerm_def supp_inv_bound map_context_def[symmetric] sftypeP_vvsubst_rrename
+        sftypeP.rrename_comps sftypeP.FFVars_rrenames wf_eqvt extend_eqvt
         | ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
-        | ((rule exI[of _ "rrename_Type \<sigma> _"])+, (rule conjI)?, rule in_context_eqvt))+
+        | ((rule exI[of _ "rrename_sftypeP \<sigma> _"])+, (rule conjI)?, rule in_context_eqvt))+
   subgoal premises prems for R B \<Gamma> T1 T2
     using prems
     unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
@@ -144,7 +144,7 @@ make_binder_inductive ty
          apply (drule prems(2)[rule_format, of "id(X := Z, Z := X)" "\<Gamma>,, X <: T\<^sub>1" "S\<^sub>2" "T\<^sub>2", rotated 2])
            apply (auto simp: extend_eqvt)
         apply(rule cong[OF cong[OF cong], THEN iffD1, of R , OF refl, rotated -1, 
-          of _ "rrename_Type (id(X := Z, Z := X)) S\<^sub>2"]) 
+          of _ "rrename_sftypeP (id(X := Z, Z := X)) S\<^sub>2"]) 
           apply (drule ty_fresh_extend)
           apply (simp_all add: supp_swap_bound)
           by (metis (no_types, opaque_lifting) image_iff map_context_def map_context_swap_FFVars)