# HG changeset patch
# User urbanc
# Date 1133372232 -3600
# Node ID a780f9c1538b6e7a74c7ecf77de63ac80282af2e
# Parent  684832c9fa620fef6aad4618f8ddea4974ff51ca
changed everything until the interesting transitivity_narrowing
proof.

diff -r 684832c9fa62 -r a780f9c1538b src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 30 18:13:31 2005 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 30 18:37:12 2005 +0100
@@ -90,7 +90,6 @@
 "subst_ctxt [] Y T = []"
 "subst_ctxt (XT#Xs) Y T = (fst XT, subst_ty (snd XT) Y T)#(subst_ctxt Xs Y T)"
 
-
 text {* valid contexts *}
 
 constdefs
@@ -200,7 +199,6 @@
 apply(simp add: domain_append)
 done
 
-
 lemma fresh_implies_not_member[rule_format]:
   fixes \<Gamma>::"ty_context"
   shows "X\<sharp>\<Gamma> \<longrightarrow> \<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))"
@@ -214,7 +212,6 @@
   apply (induct \<Gamma>)
   apply (auto dest!: validE fresh_implies_not_member)
   done
-
  
 section {* Subtyping *}
 
@@ -312,55 +309,41 @@
   shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)"
 apply(erule subtype_of_rel.induct)
 apply(force intro: valid_eqvt closed_in_eqvt)
-(*
-apply(simp)
-apply(rule S_Var)
-apply(rule valid_eqvt)
-apply(assumption)
-*)
-(* FIXME: here *)
-(* apply(auto intro: closed_in_eqvt valid_eqvt dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) *)
 apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1)
 apply(force intro: valid_eqvt silly_eqvt2)
 apply(force)
 apply(force intro!: S_All simp add: fresh_prod pt_fresh_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst])
 done
 
-lemma subtype_of_rel_induct_aux[rule_format]:
-  fixes  P :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>'a::fs_tyvrs\<Rightarrow>bool"
+lemma subtype_of_rel_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_All]:
+  fixes  P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool"
   assumes a: "\<Gamma> \<turnstile> S <: T"
-  and a1:    "\<And>x \<Gamma> S. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P \<Gamma> S Top x"
-  and a2:    "\<And>x \<Gamma> X S T. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<forall>z. P \<Gamma> S T z)
-              \<Longrightarrow> P \<Gamma> (TyVar X) T x"
-  and a3:    "\<And>x \<Gamma> X. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>(domain \<Gamma>) \<Longrightarrow> P \<Gamma> (TyVar X) (TyVar X) x"
-  and a4:    "\<And>x \<Gamma> S1 S2 T1 T2. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> 
-              (\<forall>z. P \<Gamma> S2 T2 z) \<Longrightarrow> P \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2) x"
-  and a5:    "\<And>x \<Gamma> X S1 S2 T1 T2. 
-              X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S1,T1) \<Longrightarrow> \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2 
-              \<Longrightarrow> (\<forall>z. P ((X,T1)#\<Gamma>) S2 T2 z) \<Longrightarrow> P \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2) x"
-  shows "\<forall>(pi::tyvrs prm) (x::'a::fs_tyvrs). P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x"
-using a
-proof (induct)
-  case (S_Top S \<Gamma>)
-  have b1: "\<turnstile> \<Gamma> ok" by fact 
-  have b2: "S closed_in \<Gamma>" by fact
-  show ?case
-  proof (intro strip, simp)
-    fix pi::"tyvrs prm" and x::"'a::fs_tyvrs"
+  and a1:    "\<And>\<Gamma> S x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P x \<Gamma> S Top"
+  and a2:    "\<And>\<Gamma> X S T x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<And>z. P z \<Gamma> S T)
+              \<Longrightarrow> P x \<Gamma> (TyVar X) T"
+  and a3:    "\<And>\<Gamma> X x. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (TyVar X) (TyVar X)"  
+  and a4:    "\<And>\<Gamma> S1 S2 T1 T2 x. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<And>z. P z \<Gamma> T1 S1) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> 
+              (\<And>z. P z \<Gamma> S2 T2) \<Longrightarrow> P x \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2)"
+  and a5:    "\<And>\<Gamma> X S1 S2 T1 T2 x. 
+              X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S1,T1) \<Longrightarrow> \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<And>z. P z \<Gamma> T1 S1) \<Longrightarrow> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2 
+              \<Longrightarrow> (\<And>z. P z ((X,T1)#\<Gamma>) S2 T2) \<Longrightarrow> P x \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2)"
+  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 S \<Gamma>)
+    have b1: "\<turnstile> \<Gamma> ok" by fact 
+    have b2: "S closed_in \<Gamma>" by fact
     from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
     moreover
     from b2 have "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (rule closed_in_eqvt)
-    ultimately show "P (pi \<bullet> \<Gamma>) (pi \<bullet> S) Top x" by (rule a1)
-  qed
-next
-  case (S_Var S T X \<Gamma>)
-  have b1: "\<turnstile> \<Gamma> ok" by fact 
-  have b2: "(X,S) \<in> set \<Gamma>" by fact
-  have b3: "\<Gamma> \<turnstile> S <: T" by fact
-  have b4: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x" by fact
-  show ?case
-  proof (intro strip, simp)
-    fix pi::"tyvrs prm" and x::"'a::fs_tyvrs"
+    ultimately show "P x (pi \<bullet> \<Gamma>) (pi \<bullet> S) (pi\<bullet>Top)" by (simp add: a1)
+  next
+    case (S_Var S T X \<Gamma>)
+    have b1: "\<turnstile> \<Gamma> ok" by fact 
+    have b2: "(X,S) \<in> set \<Gamma>" by fact
+    have b3: "\<Gamma> \<turnstile> S <: T" by fact
+    have b4: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact
     from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
     moreover
     from b2 have "pi\<bullet>(X,S)\<in>pi\<bullet>(set \<Gamma>)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
@@ -368,47 +351,39 @@
     moreover 
     from b3 have "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt)
     moreover 
-    from b4 have "\<forall>x. P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x" by simp
+    from b4 have "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp
     ultimately 
-    show "P (pi\<bullet>\<Gamma>) (TyVar (pi\<bullet>X)) (pi\<bullet>T) x" by (rule a2)
-  qed
-next
-  case (S_Refl X \<Gamma>)
-  have b1: "\<turnstile> \<Gamma> ok" by fact
-  have b2: "X \<in> domain \<Gamma>" by fact
-  show ?case
-  proof (intro strip, simp)
-    fix pi::"tyvrs prm" and x::"'a::fs_tyvrs"
+    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>T)" by (simp add: a2)
+  next
+    case (S_Refl X \<Gamma>)
+    have b1: "\<turnstile> \<Gamma> ok" by fact
+    have b2: "X \<in> domain \<Gamma>" by fact
     from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt)
     moreover
     from b2 have "(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 pt_list_set_pi[OF pt_tyvrs_inst])
-    ultimately show "P (pi\<bullet>\<Gamma>) (TyVar (pi\<bullet>X)) (TyVar (pi\<bullet>X)) x" by (rule a3)
-  qed
-next
-  case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt)
-next
-  case (S_All S1 S2 T1 T2 X \<Gamma>)
-  have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact 
-  have b2: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1) x" by fact
-  have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact
-  have b5: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2) x" by fact
-  have b3': "X\<sharp>\<Gamma>" by fact
-  have b3'': "X\<sharp>(T1,S1)" using b1 b3' by (rule subtype_implies_fresh)
-  have b3: "X\<sharp>(\<Gamma>,S1,T1)" using b3' b3'' by (simp add: fresh_prod)
-  show ?case
-  proof (intro strip)
-    fix pi::"tyvrs prm" and x::"'a::fs_tyvrs"
+    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>(TyVar X))" by (simp add: a3)
+  next
+    case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt)
+  next
+    case (S_All S1 S2 T1 T2 X \<Gamma>)
+    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,S1)" using b1 b3' by (rule subtype_implies_fresh)
+    have b3: "X\<sharp>(\<Gamma>,S1,T1)" using b3' b3'' by (simp add: fresh_prod)
     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 at_exists_fresh[OF at_tyvrs_inst], 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: "\<forall>x. P (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>T1) (?pi'\<bullet>S1) x" by simp
-    from b5 have "\<forall>x. P (?pi'\<bullet>((X,T1)#\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" by simp
-    hence "\<forall>x. P ((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" by simp
-    hence c2: "\<forall>x. P ((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" using f1
+    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])
@@ -431,39 +406,25 @@
     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 (?pi'\<bullet>\<Gamma>) (\<forall> [C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall> [C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) x"
+    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 (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall> [X<:S1].S2)) (pi\<bullet>(\<forall> [X<:T1].T2)) x"
+    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
 
-lemma subtype_of_rel_induct[case_names S_Top S_Var S_Refl S_Arrow S_All]:
-  fixes  P :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>'a::fs_tyvrs\<Rightarrow>bool"
-  assumes a: "\<Gamma> \<turnstile> S <: T"
-  and a1:    "\<And>x \<Gamma> S. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P \<Gamma> S Top x"
-  and a2:    "\<And>x \<Gamma> X S T. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<forall>z. P \<Gamma> S T z)
-              \<Longrightarrow> P \<Gamma> (TyVar X) T x"
-  and a3:    "\<And>x \<Gamma> X. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P \<Gamma> (TyVar X) (TyVar X) x"  
-  and a4:    "\<And>x \<Gamma> S1 S2 T1 T2. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> 
-              (\<forall>z. P \<Gamma> S2 T2 z) \<Longrightarrow> P \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2) x"
-  and a5:    "\<And>x \<Gamma> X S1 S2 T1 T2. 
-              X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S1,T1) \<Longrightarrow> \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2 
-              \<Longrightarrow> (\<forall>z. P ((X,T1)#\<Gamma>) S2 T2 z) \<Longrightarrow> P \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2) x"
-  shows "P \<Gamma> S T x"
-using a a1 a2 a3 a4 a5 subtype_of_rel_induct_aux[of  "\<Gamma>" "S" "T" "P" "[]" "x", simplified] by force
-
-
 section {* Two proofs for reflexivity of subtyping *}
 
 lemma subtype_reflexivity:
   shows "\<turnstile> \<Gamma> ok \<longrightarrow> T closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T <: T"
-proof(nominal_induct T rule: ty.induct_unsafe)
-  case (TAll \<Gamma> X T1 T2)
+proof(nominal_induct T fresh: \<Gamma> rule: ty.induct_unsafe)
+  case (TAll X T1 T2)
   have i1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T1 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T1 <: T1" by fact 
   have i2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T2 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T2 <: T2" by fact
   have f: "X\<sharp>\<Gamma>" by fact
@@ -481,13 +442,15 @@
   qed
 qed (auto simp add: closed_in_def ty.supp supp_atm)
 
-lemma subtype_refl:
-  shows "\<turnstile> \<Gamma> ok \<longrightarrow> T closed_in \<Gamma> \<longrightarrow>  \<Gamma> \<turnstile> T <: T"
-apply(nominal_induct T rule: ty.induct_unsafe)
+lemma subtype_reflexivity:
+  assumes a: "\<turnstile> \<Gamma> ok"
+  and     b: "T closed_in \<Gamma>"
+  shows "\<Gamma> \<turnstile> T <: T"
+using a b
+apply(nominal_induct T fresh: \<Gamma> rule: ty.induct_unsafe)
 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
-(* FIXME: the new induction method from Markus will fix this uglyness *)
-apply(atomize)
-apply(drule_tac x="(tyvrs, ty2)#z" in spec)
+(* too bad that this cannot be found automatically *)
+apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec)
 apply(force simp add: closed_in_def)
 done
 
@@ -545,7 +508,7 @@
   fixes P :: "ty"
   and   X :: "tyvrs"
   shows "X\<sharp>(T,P) \<longrightarrow> X\<sharp>(subst_ty T Y P)"
-  apply (nominal_induct T rule: ty.induct_unsafe)
+  apply (nominal_induct T fresh: T Y P rule: ty.induct_unsafe)
   apply (auto simp add: fresh_prod abs_fresh)
   done
 
@@ -633,8 +596,8 @@
   assumes a1: "\<Gamma> \<turnstile> S <: T"
   shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T"
   using a1 
-proof (nominal_induct \<Gamma> S T rule: subtype_of_rel_induct)
-  case (S_Top \<Delta> \<Gamma> S) 
+proof (nominal_induct \<Gamma> S T fresh: \<Delta> rule: subtype_of_rel_induct)
+  case (S_Top \<Gamma> S) 
   have lh_drv_prem: "S closed_in \<Gamma>" by fact
   show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: Top"
   proof (intro strip)
@@ -645,9 +608,9 @@
     ultimately show "\<Delta> \<turnstile> S <: Top" by force
   qed
 next 
-  case (S_Var \<Delta> \<Gamma> X S T)
+  case (S_Var \<Gamma> X S T)
   have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact
-  have ih: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" by fact
+  have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" by fact
   show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> TyVar X <: T"
   proof (intro strip)
     assume ok: "\<turnstile> \<Delta> ok"
@@ -658,7 +621,7 @@
     ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force
   qed
 next
-  case (S_Refl \<Delta> \<Gamma> X)
+  case (S_Refl \<Gamma> X)
   have lh_drv_prem: "X \<in> domain \<Gamma>" by fact
   show ?case
   proof (intro strip)
@@ -671,10 +634,10 @@
 next 
   case S_Arrow thus ?case by force
 next
-  case (S_All \<Delta> \<Gamma> X S1 S2 T1 T2)
+  case (S_All \<Gamma> X S1 S2 T1 T2)
   have fresh: "X\<sharp>\<Delta>" by fact
-  have ih1: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
-  have ih2: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
+  have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
+  have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact
   hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2"
@@ -698,19 +661,19 @@
   assumes a1: "\<Gamma> \<turnstile> S <: T"
   shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T"
   using a1 
-proof (nominal_induct \<Gamma> S T rule: subtype_of_rel_induct)
-  case (S_Top \<Delta> \<Gamma> S) thus ?case by (force intro: extends_closed)
+proof (nominal_induct \<Gamma> S T fresh: \<Delta> rule: subtype_of_rel_induct)
+  case (S_Top \<Gamma> S) thus ?case by (force intro: extends_closed)
 next 
-  case (S_Var \<Delta> \<Gamma> X S T) thus ?case by (force simp add: extends_def)
+  case (S_Var \<Gamma> X S T) thus ?case by (force simp add: extends_def)
 next
-  case (S_Refl \<Delta> \<Gamma> X) thus ?case by (force dest: extends_domain)
+  case (S_Refl \<Gamma> X) thus ?case by (force dest: extends_domain)
 next 
   case S_Arrow thus ?case by force
 next
-  case (S_All \<Delta> \<Gamma> X S1 S2 T1 T2)
+  case (S_All \<Gamma> X S1 S2 T1 T2)
   have fresh: "X\<sharp>\<Delta>" by fact
-  have ih1: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
-  have ih2: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
+  have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact
+  have ih2: "\<And> \<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact
   hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2"