# HG changeset patch
# User urbanc
# Date 1175038183 -7200
# Node ID c55f5631a4ecedbe9dfbc7c338bdbe4b0a6158f0
# Parent  35debf264656fa0e6f08512895668bc71b3a8a5d
adapted to nominal_inductive infrastructure

diff -r 35debf264656 -r c55f5631a4ec src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 01:09:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 01:29:43 2007 +0200
@@ -87,9 +87,11 @@
   "domain [] = {}"
   "domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" 
 
-lemma domain_eqvt:
+lemma domain_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
-  shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" 
+  and   pi'::"vrs prm"
+  shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)"
+  and   "pi'\<bullet>(domain \<Gamma>) = domain (pi'\<bullet>\<Gamma>)"
   by (induct \<Gamma>) (simp_all add: eqvt)
 
 lemma finite_domain:
@@ -140,7 +142,7 @@
   "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
   "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)"
 
-lemma closed_in_eqvt:
+lemma closed_in_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
@@ -153,32 +155,35 @@
     by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst])
 qed
 
+lemma ty_vrs_prm_simp:
+  fixes pi::"vrs prm"
+  and   S::"ty"
+  shows "pi\<bullet>S = S"
+by (induct S rule: ty.induct_weak) (auto simp add: calc_atm)
+
+lemma ty_context_vrs_prm_simp:
+  fixes pi::"vrs prm"
+  and   \<Gamma>::"ty_context"
+  shows "pi\<bullet>\<Gamma> = \<Gamma>"
+by (induct \<Gamma>) 
+   (auto simp add: calc_atm ty_vrs_prm_simp)
+
+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: ty_vrs_prm_simp ty_context_vrs_prm_simp)
+
 text {* Now validity of a context is a straightforward inductive definition. *}
   
-inductive2 valid_rel :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
+inductive2 
+  valid_rel :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
 where
   valid_nil[simp]:  "\<turnstile> [] ok"
 | valid_cons[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(domain \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> ((X,T)#\<Gamma>) ok"
 
-lemma valid_eqvt:
-  fixes pi::"tyvrs prm"
-  assumes a: "\<turnstile> \<Gamma> ok" 
-  shows "\<turnstile> (pi\<bullet>\<Gamma>) ok"
-  using a
-proof (induct)
-  case valid_nil
-  show "\<turnstile> (pi\<bullet>[]) ok" by simp
-next
-  case (valid_cons \<Gamma> X T)
-  have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by fact
-  moreover
-  have "X\<sharp>(domain \<Gamma>)" by fact
-  hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_bij domain_eqvt[symmetric])
-  moreover
-  have "T closed_in \<Gamma>" by fact
-  hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_eqvt)
-  ultimately show "\<turnstile> (pi\<bullet>((X,T)#\<Gamma>)) ok" by simp
-qed
+equivariance valid_rel
 
 lemma validE:
   assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok"
@@ -259,7 +264,8 @@
   apply (fresh_guess)+
   done
 
-consts subst_tyc :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100)
+consts 
+  subst_tyc :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100)
 primrec
 "([])[Y:=T]\<^isub>t\<^isub>y\<^isub>c= []"
 "(XT#\<Gamma>)[Y:=T]\<^isub>t\<^isub>y\<^isub>c = (fst XT,(snd XT)[Y:=T]\<^isub>t\<^isub>y)#(\<Gamma>[Y:=T]\<^isub>t\<^isub>y\<^isub>c)"
@@ -273,14 +279,20 @@
   does \emph{not} make the subtyping-relation ``partial"\ldots because we work over
   $\alpha$-equivalence classes.) *}
 
-inductive2 subtype_of :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
+inductive2 
+  subtype_of :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
 where
   S_Top[intro]:    "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
 | S_Var[intro]:    "\<lbrakk>(X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T"
 | S_Refl[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
 | S_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)" 
-| S_Forall[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; X\<sharp>\<Gamma>; ((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"  
+| S_Forall[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; X\<sharp>\<Gamma>; ((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:
+  fixes X::"tyvrs"
+  assumes a: "\<Gamma> \<turnstile> S <: T"
+  shows "\<turnstile> \<Gamma> ok"  
+using a by (induct) (auto)
 
 lemma subtype_implies_closed:
   assumes a: "\<Gamma> \<turnstile> S <: T"
@@ -303,12 +315,6 @@
   ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
 qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp)
 
-lemma subtype_implies_ok:
-  fixes X::"tyvrs"
-  assumes a1: "\<Gamma> \<turnstile> S <: T"
-  shows "\<turnstile> \<Gamma> ok"  
-using a1 by (induct, auto)
-
 lemma subtype_implies_fresh:
   fixes X::"tyvrs"
   assumes a1: "\<Gamma> \<turnstile> S <: T"
@@ -324,125 +330,10 @@
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
 qed
 
-lemma subtype_eqvt:
-  fixes pi::"tyvrs prm"
-  shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)"
-apply(erule subtype_of.induct)
-apply(force intro: valid_eqvt closed_in_eqvt eqvt)
-apply(force intro!: S_Var
-            intro: closed_in_eqvt valid_eqvt 
-            dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
-            simp add: set_eqvt)
-apply(force intro: valid_eqvt
-            dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
-            simp add: domain_eqvt)
-apply(force)
-apply(force intro!: S_Forall simp add: fresh_prod fresh_bij)
-done
-
-text {* The most painful part of the subtyping definition is the strengthening of the
-  induction principle. The induction principle that comes for free with the definition of 
-  @{term "subtype_of"} requires to prove the @{text "S_Forall"}-case for \emph{all} binders
-  @{text "X"}. This will often cause some renaming-manoeuvres in the reasoning. To avoid this,
-  we strengthening the induction-principle so that we only have to establish
-  the @{text "S_Forall"}-case for \emph{fresh} binders @{text "X"}. The property that allows
-  us to strengthen the induction-principle is that the equivariance of @{text "subtype_of"}. *}
+nominal_inductive subtype_of  
+  by (simp_all add: abs_fresh subtype_implies_fresh)
 
-lemma subtype_of_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_Forall]:
-  fixes  P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool"
-  assumes a: "\<Gamma> \<turnstile> S <: T"
-  and a1: "\<And>\<Gamma> S x. \<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> S Top"
-  and a2: "\<And>\<Gamma> X S T x. \<lbrakk>(X,S)\<in>set \<Gamma>; \<Gamma> \<turnstile> S <: T; \<And>z. P z \<Gamma> S T\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) T"
-  and a3: "\<And>\<Gamma> X x. \<lbrakk>\<turnstile> \<Gamma> ok; X\<in>domain \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) (Tvar X)"  
-  and a4: "\<And>\<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. 
-  \<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z \<Gamma> S\<^isub>2 T\<^isub>2\<rbrakk> 
-  \<Longrightarrow> P x \<Gamma> (S\<^isub>1 \<rightarrow> S\<^isub>2) (T\<^isub>1 \<rightarrow> T\<^isub>2)"
-  and a5: "\<And>\<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. 
-  \<lbrakk>X\<sharp>x; X\<sharp>(\<Gamma>,S\<^isub>1,T\<^isub>1); \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; 
-  ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z ((X,T\<^isub>1)#\<Gamma>) S\<^isub>2 T\<^isub>2\<rbrakk>
-  \<Longrightarrow> P x \<Gamma> (\<forall>[X<:S\<^isub>1].S\<^isub>2) (\<forall>[X<:T\<^isub>1].T\<^isub>2)"
-  shows "P x \<Gamma> S T"
-proof -
-  from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)"
-  proof (induct)
-    case (S_Top \<Gamma> S) 
-    thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1)
-  next
-    case (S_Var X S \<Gamma> T)
-    have "(X,S) \<in> set \<Gamma>" by fact
-    hence "pi\<bullet>(X,S)\<in>pi\<bullet>(set \<Gamma>)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt)
-    moreover
-    have "\<Gamma> \<turnstile> S <: T" by fact
-    hence "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt)
-    moreover
-    have  "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact
-    hence "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp
-    ultimately 
-    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>T)" by (simp add: a2)
-  next
-    case (S_Refl \<Gamma> X)
-    have "\<turnstile> \<Gamma> ok" by fact
-    hence "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
-    moreover
-    have "X \<in> domain \<Gamma>" by fact
-    hence "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt set_eqvt)
-    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>(Tvar X))" by (simp add: a3)
-  next
-    case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt)
-  next
-    case (S_Forall \<Gamma> T1 S1 X S2 T2)
-    have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact 
-    have b2: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1)" by fact
-    have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact
-    have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact
-    have b3: "X\<sharp>\<Gamma>" by fact
-    have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh)
-    have "\<exists>C::tyvrs. C\<sharp>(pi\<bullet>X,pi\<bullet>S2,pi\<bullet>T2,pi\<bullet>S1,pi\<bullet>T1,pi\<bullet>\<Gamma>,x)"
-      by (rule exists_fresh', simp add: fs_tyvrs1)
-    then obtain C::"tyvrs" where  f1: "C\<noteq>(pi\<bullet>X)" and f2: "C\<sharp>(pi\<bullet>S1)" and f3: "C\<sharp>(pi\<bullet>T1)"
-      and f4: "C\<sharp>(pi\<bullet>S2)" and f5: "C\<sharp>(pi\<bullet>T2)" and f6: "C\<sharp>(pi\<bullet>\<Gamma>)" and f7: "C\<sharp>x"
-      by (auto simp add: fresh_prod fresh_atm)
-    let ?pi' = "[(C,pi\<bullet>X)]@pi"
-    from b2 have c1: "\<And>x. P x (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>T1) (?pi'\<bullet>S1)" by simp
-    from b5 have "\<And>x. P x (?pi'\<bullet>((X,T1)#\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp
-    hence "\<And>x. P x ((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp
-    hence c2: "\<And>x. P x ((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" using f1
-      by (simp only: pt_tyvrs2 calc_atm, simp)
-    from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" 
-      by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" 
-      by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp
-    from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" 
-      by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" 
-      by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp
-    from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" 
-      by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" 
-      by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-    hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp
-    from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt)
-    from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt)
-    hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp
-    hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1
-      by (simp only: pt_tyvrs2 calc_atm, simp)
-    have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod)
-    have main: "P x (?pi'\<bullet>\<Gamma>) (\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2))"
-      using f7 fnew e1 c1 e2 c2 by (rule a5)
-    have alpha1: "(\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall>[X<:S1].S2))"
-      using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric])
-    have alpha2: "(\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall>[X<:T1].T2))"
-      using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric])
-    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall>[X<:S1].S2)) (pi\<bullet>(\<forall>[X<:T1].T2))"
-      using alpha1 alpha2 f6a main by simp  
-  qed
-  hence "P x (([]::tyvrs prm)\<bullet>\<Gamma>) (([]::tyvrs prm)\<bullet>S) (([]::tyvrs prm)\<bullet>T)" by blast
-  thus ?thesis by simp
-qed
+thm subtype_of.strong_induct
 
 section {* Reflexivity of Subtyping *}
 
@@ -522,7 +413,7 @@
   and c: "\<Delta> extends \<Gamma>"
   shows "\<Delta> \<turnstile> S <: T"
   using a b c 
-proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct)
+proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
   case (S_Top \<Gamma> S) 
   have lh_drv_prem: "S closed_in \<Gamma>" by fact
   have "\<turnstile> \<Delta> ok" by fact
@@ -531,7 +422,7 @@
   hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed)
   ultimately show "\<Delta> \<turnstile> S <: Top" by force
 next 
-  case (S_Var \<Gamma> X S T)
+  case (S_Var X S \<Gamma> T)
   have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact
   have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact
   have ok: "\<turnstile> \<Delta> ok" by fact
@@ -549,9 +440,9 @@
   hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain)
   ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force
 next 
-  case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) thus "\<Delta> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by blast
+  case (S_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 (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
+  case (S_Forall \<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>(domain \<Delta>)" by (simp add: fresh_domain)
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
@@ -578,8 +469,8 @@
   and c: "\<Delta> extends \<Gamma>"
   shows "\<Delta> \<turnstile> S <: T"
   using a b c 
-proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct)
-  case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
+proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
+  case (S_Forall \<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>(domain \<Delta>)" by (simp add: fresh_domain)
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
@@ -639,7 +530,7 @@
   apply(drule_tac X="Xa" in subtype_implies_fresh)
   apply(assumption)
   apply(simp add: fresh_prod)
-  apply(drule_tac pi="[(X,Xa)]" in subtype_eqvt)
+  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
@@ -696,7 +587,7 @@
     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_induct) 
+    proof (nominal_induct \<Gamma>' S' Q\<equiv>Q rule: subtype_of.strong_induct) 
       case (S_Top \<Gamma> S) 
 	--{* \begin{minipage}[t]{0.9\textwidth}
 	In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S <: Top"}, giving
@@ -710,7 +601,7 @@
       hence "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
       thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
     next
-      case (S_Var \<Gamma> Y U) 
+      case (S_Var 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)"} 
@@ -727,7 +618,7 @@
 	derivation.\end{minipage}*}
       thus "\<Gamma> \<turnstile> Tvar X <: T" by simp
     next
-      case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) 
+      case (S_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 
@@ -770,7 +661,7 @@
       }
       ultimately show "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" by blast
     next
-      case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) 
+      case (S_Forall \<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 @{text "\<Gamma>\<turnstile>\<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:Q\<^isub>1].Q\<^isub>2"} with 
 	@{text "\<forall>[X<:S\<^isub>1].S\<^isub>2=S"} and @{text "\<forall>[X<:Q\<^isub>1].Q\<^isub>2=Q"}. We therefore have the sub-derivations  
@@ -794,7 +685,8 @@
       hence 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: "((X,Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
-      have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" by fact
+      have "X\<sharp>\<Gamma>" by fact
+      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
       from rh_drv 
@@ -838,7 +730,7 @@
     have  "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N" --{* left-hand derivation *}
       and "\<Gamma> \<turnstile> P<:Q" by fact --{* right-hand derivation *}
     thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N" 
-    proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of_induct) 
+    proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of.strong_induct) 
       case (S_Top _ S \<Delta> \<Gamma> X)
 	--{* \begin{minipage}[t]{0.9\textwidth}
 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"}. We show
@@ -854,7 +746,7 @@
 	by (simp add: closed_in_def domain_append)
       ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
     next
-      case (S_Var _ Y S N \<Delta> \<Gamma> X) 
+      case (S_Var Y S _ N \<Delta> \<Gamma> X) 
 	--{* \begin{minipage}[t]{0.9\textwidth}
 	In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} and
 	by inner induction hypothesis we have @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"}. We therefore 
@@ -908,13 +800,13 @@
       from lh_drv_prm\<^isub>2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append)
       ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.S_Refl)
     next
-      case (S_Arrow _ Q\<^isub>1 Q\<^isub>2 S\<^isub>1 S\<^isub>2 \<Delta> \<Gamma> X) 
+      case (S_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>@[(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>@[(X,P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
     next
-      case (S_Forall _ Y S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 \<Delta> \<Gamma> X)
+      case (S_Forall _ 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 @{text "(\<Delta>@[(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>@[(X,Q)]@\<Gamma>"}. By