# HG changeset patch
# User urbanc
# Date 1136903011 -3600
# Node ID da46244359659d61337ac3594b0300577664680b
# Parent  f0acb66858b4703820e8336f3044953b8cd33188
tuned

diff -r f0acb66858b4 -r da4624435965 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Tue Jan 10 02:32:10 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Tue Jan 10 15:23:31 2006 +0100
@@ -76,9 +76,9 @@
 
 text {* Typing contexts are represented as lists "growing" on the left; we
   thereby deviating from the convention in the POPLmark-paper. The lists contain
-  pairs of type-variables and types. *}
+  pairs of type-variables and types (this is sufficient for the Part 1A). *}
 
-text {* In order to state valitity-conditions for typing-contexts, the notion of
+text {* In order to state validity-conditions for typing-contexts, the notion of
   a @{text "domain"} of a typing-context is handy. *}
 
 consts
@@ -195,14 +195,6 @@
   shows "\<turnstile> \<Gamma> ok"
   using a by (induct \<Delta>, auto dest: validE)
 
-lemma closed_in_fresh:
-  fixes X::"tyvrs"
-  assumes a: "S closed_in \<Gamma>"
-  and     b: "X\<sharp>(domain \<Gamma>)" 
-  and     c: "\<turnstile> \<Gamma> ok"
-  shows "X\<sharp>S"
-using a b c by (force simp add: fresh_def domain_supp closed_in_def)
-
 lemma replace_type:
   assumes a: "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok"
   and     b: "S closed_in \<Gamma>"
@@ -236,11 +228,11 @@
   ultimately show "T=S" by auto
 qed 
 
-section {* Size and Capture-Avoiding Substitutiuon for Types *}
+section {* Size and Capture-Avoiding Substitution for Types *}
 
 text {* In the current version of the nominal datatype-package even simple 
   functions (such as size of types and capture-avoiding substitution) can 
-  only be defined manually via some labourious proof constructions. Therefore 
+  only be defined manually via some laborious proof constructions. Therefore 
   we sill just assume them here. *}
 
 consts size_ty :: "ty \<Rightarrow> nat"
@@ -269,6 +261,10 @@
  
 section {* Subtyping-Relation *}
 
+text {* The subtype relation follows what is written in the POPLmark-paper, except 
+  for the premises dealing with well-formed contexts and the freshness constraint
+  @{term "X\<sharp>\<Gamma>"} in the rule @{text "S_Forall"}. *}
+
 consts
   subtype_of :: "(ty_context \<times> ty \<times> ty) set"   
 syntax 
@@ -327,6 +323,10 @@
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
 qed
 
+text {* Two silly lemmas that are necessary to show that @{text "subtype_of"} is
+  equivariant. They are necessary at the moment until we have a tactic that shows
+  equivariance automatically. *}
+
 lemma silly_eqvt1:
   fixes X::"'a::pt_tyvrs"
   and   S::"'b::pt_tyvrs"
@@ -355,16 +355,27 @@
 apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt)
 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 all binders
+  @{text "X"}. This will require 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 fresh binders @{text "X"}. The property that allows
+  us to strengthen the induction-principle is that the relation @{text "subtype_of"} is
+  equivariant. *}
+
 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> 
+  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>
+  \<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 -
@@ -483,27 +494,28 @@
 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
   --{* Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
-  the definition @{text "closed_in_def"}. *}
+  an explicit definition for @{text "closed_in_def"}. *}
 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec)
 apply(force simp add: closed_in_def fresh_domain)
 done
 
-text {* Inversion lemmas *}
+text {* Some inversion lemmas: *}
+
 lemma S_TopE:
   assumes a: "\<Gamma> \<turnstile> Top <: T"
   shows "T = Top"
 using a by (cases, auto) 
 
 lemma S_ArrowE_left:
-  assumes a: "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" 
-  shows "T = Top \<or> (\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> \<Gamma> \<turnstile> S2 <: T2)"
+  assumes a: "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" 
+  shows "T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2)"
 using a by (cases, auto simp add: ty.inject)
 
 lemma S_ForallE_left:
-  shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>\<Gamma>; X\<sharp>S1\<rbrakk>
-         \<Longrightarrow> T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2)"
+  shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<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> ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)"
   apply(frule subtype_implies_ok)
-  apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T")
+  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)
   (* term *)
@@ -535,78 +547,11 @@
   apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   done
 
-section {* Type Substitution *}
-
-lemma subst_ty_fresh:
-  fixes X :: "tyvrs"
-  assumes a: "X\<sharp>(T,P)"
-  shows "X\<sharp>T[Y:=P]\<^isub>t\<^isub>y"
-  using a
-  apply (nominal_induct T avoiding : T Y P rule: ty.induct_unsafe)
-  apply (auto simp add: fresh_prod abs_fresh)
-  done
-
-lemma subst_ctxt_fresh:
-  fixes X::"tyvrs"
-  assumes a: "X\<sharp>(\<Gamma>,P)"
-  shows "X\<sharp>\<Gamma>[Y:=P]\<^isub>t\<^isub>y\<^isub>c"
-  using a
-  apply (induct \<Gamma>)
-  apply (auto intro: subst_ty_fresh simp add: fresh_prod fresh_list_cons)
-  done
-
-(*
-lemma subst_ctxt_closed:
-  shows  "subst_ty b X P closed_in (subst_ctxt \<Delta> X P @ \<Gamma>)"
-
+section {* Weakening *}
 
-lemma substitution_ok:
-  shows "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>) ok \<longrightarrow> \<Gamma> \<turnstile> P <: Q \<longrightarrow> \<turnstile> ((subst_ctxt \<Delta> X P)@\<Gamma>)  ok"
-  apply (induct \<Delta>)
-  apply (auto dest: validE)
-  apply (rule v2)
-  apply assumption
-  apply (drule validE)
-  apply (auto simp add: fresh_list_append)
-  apply (rule subst_ctxt_fresh)
-  apply (simp add: fresh_prod)
-  apply (drule_tac X = "a" in subtype_implies_fresh)
-  apply (simp add: fresh_list_cons)
-  apply (simp add: fresh_prod)
-  apply (simp add: fresh_list_cons)
-  apply (drule validE)
-
-done
-*)
-
-(* note: What should nominal induct do if the context is compound? *)
-(*
-lemma type_substitution:
-  assumes a0: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> S <: T"
-  shows "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>) ok \<longrightarrow> \<Gamma> \<turnstile> P <: Q 
-         \<longrightarrow> ((subst_ctxt \<Delta> X P)@\<Gamma>) \<turnstile> (subst_ty S X P) <: (subst_ty T X P)"
-  using a0 
-  thm subtype_of_induct
-  apply(rule subtype_of_induct[of "\<Delta>@(X,Q)#\<Gamma>" "S" "T" _ "P"])
-  apply(auto)
-  apply(rule S_Top)
-  defer
-  defer
-  defer
-  apply(rule S_Var)
-  defer
-  defer
-  defer
-  defer
-  apply(rule S_Refl)
-  defer
-  defer
-
-
-apply (nominal_induct \<Delta> X Q \<Gamma> S T rule: subtype_of_induct)
-*)
-
-section {* Weakening *}
+text {* In order to prove weakening we introduce the notion of a type-context extending 
+  another. This generalization seems to make the proof for weakening to be
+  smoother than if we had strictly adhered to the version in the POPLmark-paper. *}
 
 constdefs 
   extends :: "ty_context \<Rightarrow> ty_context \<Rightarrow> bool" ("_ extends _" [100,100] 100)
@@ -690,7 +635,7 @@
 
 text {* In fact all "non-binding" cases can be solved automatically: *}
 
-lemma weakening_semiautomated:
+lemma weakening_more_automated:
   assumes a: "\<Gamma> \<turnstile> S <: T"
   and b: "\<turnstile> \<Delta> ok"
   and c: "\<Delta> extends \<Gamma>"
@@ -708,7 +653,7 @@
   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> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force   
-  moreover 
+  moreover
   have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
   ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
   moreover
@@ -716,6 +661,9 @@
   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: S_Forall)
 qed (blast intro: extends_closed extends_memb dest: extends_domain)+
 
+
+section {* Transitivity and Narrowing *}
+
 text {* Next we prove the transitivity and narrowing for the subtyping relation. 
 The POPLmark-paper says the following:
 
@@ -738,7 +686,7 @@
 @{thm measure_induct_rule[of "size_ty",no_vars]}
 \end{center}
 
-It says in English: in order to show a property @{term "P a"} for all @{term "a"}, 
+That means in order to show a property @{term "P a"} for all @{term "a"}, 
 it requires to prove that for all @{term x} @{term "P x"} holds using the 
 assumption that for all @{term y} whose size is strictly smaller than 
 that of @{term x} the property @{term "P y"} holds. *}
@@ -804,7 +752,7 @@
 	@{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 exists types 
+	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"}. 
@@ -854,12 +802,13 @@
 	and @{term "X\<sharp>Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that 
 	@{text "T=Top \<or> T=\<forall>[X<:T\<^isub>1].T\<^isub>2"}. The @{term "Top"}-case is straightforward once we know 
 	@{text "(\<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"}. @{term "((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"}. Using the outer 
+	the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "((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 "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using induction 
-	again @{term "((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 @{text "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"}.which is 
-	@{text "\<Gamma> \<turnstile>  \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T\<^isub>"}.\end{minipage}*}
+	induction for narrowing we get @{term "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using again 
+	induction for transitivity we obtain @{term "((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 
+	@{text "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"}.which is @{text "\<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
       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
@@ -925,17 +874,17 @@
     next
       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"}. We therefore 
+	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 
 	know that the contexts @{term "\<Delta>@[(X,Q)]@\<Gamma>"} and @{term "\<Delta>@[(X,P)]@\<Gamma>"} are ok, and that 
-	@{term "(Y,S)"} is in @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. By inner induction hypothesis we have 
-	@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"}. We need to show that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N"} 
-	holds. In case @{term "X\<noteq>Y"} we know that @{term "(Y,S)"} is in @{term "\<Delta>@[(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>@[(X,P)]@\<Gamma>) extends \<Gamma>"} and therefore by @{text "weakening"} that 
-	@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we obtain then 
-	@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule @{text "S_Var"}.
-	\end{minipage}*}
+	@{term "(Y,S)"} is in @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We need to show that 
+	@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N"}  holds. In case @{term "X\<noteq>Y"} we know that 
+	@{term "(Y,S)"} is in @{term "\<Delta>@[(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>@[(X,P)]@\<Gamma>) extends \<Gamma>"} and therefore 
+	by @{text "weakening"} that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we 
+	obtain then @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule 
+	@{text "S_Var"}.\end{minipage}*}
       hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"
 	and lh_drv_prm: "(Y,S) \<in> set (\<Delta>@[(X,Q)]@\<Gamma>)"
 	and rh_drv: "\<Gamma> \<turnstile> P<:Q"
@@ -964,7 +913,7 @@
       case (S_Refl _ Y \<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 <: Tvar Y"} and we
-	therefore know that @{term "\<Delta>@[(X,Q)]@\<Gamma>"} is ok and thad @{term "Y"} is in 
+	therefore know that @{term "\<Delta>@[(X,Q)]@\<Gamma>"} is ok and that @{term "Y"} is in 
 	the domain of @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We therefore know that @{term "\<Delta>@[(X,P)]@\<Gamma>"} is ok
 	and that @{term Y} is in the domain of @{term "\<Delta>@[(X,P)]@\<Gamma>"}. We can conclude by applying 
 	rule @{text "S_Refl"}.\end{minipage}*}
@@ -985,7 +934,7 @@
     next
       case (S_Forall _ Y S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 \<Delta> \<Gamma> X)
 	--{* \begin{minipage}[t]{0.9\textwidth}
-	In this case teh 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"}
+	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
 	the inner induction hypothesis we have that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"} and 
 	@{term "((Y,T\<^isub>1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. Since @{term P} is a subtype of @{term Q}
@@ -1005,5 +954,4 @@
   } 
 qed
 
-
 end
\ No newline at end of file