--- a/src/HOL/Nominal/Examples/Fsub.thy Fri Dec 16 16:59:32 2005 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy Fri Dec 16 18:20:03 2005 +0100
@@ -4,35 +4,47 @@
imports "../nominal"
begin
-text {* Authors: Christian Urban
- Benjamin Pierce
- Steve Zdancewic
- Stephanie Weihrich
- Dimitrios Vytiniotis
+text {* Authors: Christian Urban,
+ Benjamin Pierce,
+ Steve Zdancewic.
+ Stephanie Weihrich and
+ Dimitrios Vytiniotis;
- with help from Stefan Berghofer, Markus Wenzel
+ with help from Stefan Berghofer and Markus Wenzel.
*}
+section {* Atom Types, Types and Terms *}
+
atom_decl tyvrs vrs
-section {* Types *}
+nominal_datatype ty =
+ TVar "tyvrs"
+ | Top
+ | Arrow "ty" "ty" ("_ \<rightarrow> _" [900,900] 900)
+ | TAll "\<guillemotleft>tyvrs\<guillemotright>ty" "ty"
-nominal_datatype ty = TyVar "tyvrs"
- | Top
- | Arrow "ty" "ty" ("_ \<rightarrow> _" [900,900] 900)
- | TAll "\<guillemotleft>tyvrs\<guillemotright>ty" "ty"
+nominal_datatype trm =
+ Var "vrs"
+ | Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty"
+ | TAbs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
+ | App "trm" "trm"
+ | TApp "trm" "ty"
syntax
TAll_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall> [_<:_]._" [900,900,900] 900)
+ Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100)
+ TAbs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100)
+
translations
- "(\<forall>[a<:ty1].ty2)" \<rightleftharpoons> "TAll a ty2 ty1"
+ "\<forall>[a<:ty1].ty2" \<rightleftharpoons> "TAll a ty2 ty1"
+ "Lam [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys"
+ "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys"
-section {* typing contexts and their domains *}
+subsection {* Typing contexts and Their Domains *}
types ty_context = "(tyvrs\<times>ty) list"
-text {* domain of a context --- (the name "dom" is already used elsewhere) *}
consts
"domain" :: "ty_context \<Rightarrow> tyvrs set"
primrec
@@ -49,26 +61,28 @@
shows "finite (domain \<Gamma>)"
by (induct \<Gamma>, auto)
-lemma domain_inclusion[rule_format]:
- shows "(X,T)\<in>set \<Gamma> \<longrightarrow> X\<in>(domain \<Gamma>)"
- by (induct \<Gamma>, auto)
+lemma domain_inclusion:
+ assumes a: "(X,T)\<in>set \<Gamma>"
+ shows "X\<in>(domain \<Gamma>)"
+ using a by (induct \<Gamma>, auto)
-lemma domain_existence[rule_format]:
- shows "X\<in>(domain \<Gamma>) \<longrightarrow> (\<exists>T.(X,T)\<in>set \<Gamma>)"
- by (induct \<Gamma>, auto)
+lemma domain_existence:
+ assumes a: "X\<in>(domain \<Gamma>)"
+ shows "\<exists>T.(X,T)\<in>set \<Gamma>"
+ using a by (induct \<Gamma>, auto)
lemma domain_append:
shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))"
by (induct \<Gamma>, auto)
-section {* Two functions over types *}
+section {* Size Functions and Capture Avoiding Substitutiuon for Types *}
text {* they cannot yet be defined conveniently unless we have a recursion combinator *}
consts size_ty :: "ty \<Rightarrow> nat"
lemma size_ty[simp]:
- shows "size_ty (TyVar X) = 1"
+ shows "size_ty (TVar X) = 1"
and "size_ty (Top) = 1"
and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (t1 \<rightarrow> t2) = m + n + 1"
and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall> [a<:t1].t2) = m + n + 1"
@@ -77,7 +91,7 @@
consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty"
lemma subst_ty[simp]:
- shows "subst_ty (TyVar X) Y T = (if X=Y then T else (TyVar X))"
+ shows "subst_ty (TVar X) Y T = (if X=Y then T else (TVar X))"
and "subst_ty Top Y T = Top"
and "subst_ty (T1 \<rightarrow> T2) Y T = (subst_ty T1 Y T) \<rightarrow> (subst_ty T2 Y T)"
and "X\<sharp>(Y,T) \<Longrightarrow> subst_ty (\<forall>[X<:T1].T2) Y T = (\<forall>[X<:(subst_ty T1 Y T)].(subst_ty T2 Y T))"
@@ -90,7 +104,7 @@
"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 *}
+subsection {* valid contexts *}
constdefs
"closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
@@ -108,7 +122,7 @@
shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
using a
proof (unfold "closed_in_def")
- assume "supp S \<subseteq> (domain \<Gamma>)"
+ assume "supp S \<subseteq> (domain \<Gamma>)"
hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)"
by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst])
thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))"
@@ -142,7 +156,7 @@
proof (simp, rule valid_rel.v2)
show "\<turnstile> (pi \<bullet> \<Gamma>) ok" using a1 by simp
next
- show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst])
+ show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: fresh_eqvt)
next
show "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" using a3 by (rule closed_in_eqvt)
qed
@@ -153,24 +167,20 @@
shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>\<Gamma> \<and> T closed_in \<Gamma>"
using a by (cases, auto)
-lemma validE_append[rule_format]:
- shows "\<turnstile> (\<Delta>@\<Gamma>) ok \<longrightarrow> \<turnstile> \<Gamma> ok"
- by (induct \<Delta>, auto dest: validE)
+lemma validE_append:
+ assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok"
+ shows "\<turnstile> \<Gamma> ok"
+ using a by (induct \<Delta>, auto dest: validE)
-lemma domain_fresh[rule_format]:
+lemma domain_fresh:
fixes X::"tyvrs"
- shows "\<turnstile> \<Gamma> ok \<longrightarrow> (X\<sharp>(domain \<Gamma>) = X\<sharp>\<Gamma>)"
+ assumes a: "\<turnstile> \<Gamma> ok"
+ shows "X\<sharp>(domain \<Gamma>) = X\<sharp>\<Gamma>"
+using a
apply(induct \<Gamma>)
-apply(simp add: fresh_list_nil fresh_set_empty)
-apply(simp add: fresh_list_cons fresh_prod
- fresh_fin_insert[OF pt_tyvrs_inst, OF at_tyvrs_inst, OF fs_tyvrs_inst, OF finite_domain])
-apply(rule impI)
-apply(clarify)
-apply(simp add: fresh_prod)
-apply(drule validE)
-apply(simp)
-apply(simp add: closed_in_def2 fresh_def)
-apply(force)
+apply(auto simp add: fresh_list_nil fresh_list_cons fresh_set_empty fresh_prod fresh_atm
+ fresh_fin_insert[OF pt_tyvrs_inst, OF at_tyvrs_inst, OF fs_tyvrs_inst, OF finite_domain])
+apply(force simp add: closed_in_def2 fresh_def)
done
lemma closed_in_fresh:
@@ -186,8 +196,11 @@
apply(force)
done
-lemma replace_type[rule_format]:
- shows "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok \<longrightarrow> S closed_in \<Gamma> \<longrightarrow> \<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok"
+lemma replace_type:
+ assumes a: "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok"
+ and b: "S closed_in \<Gamma>"
+ shows "\<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok"
+using a b
apply(induct \<Delta>)
apply(auto dest!: validE intro!: v2 simp add: fresh_list_append fresh_list_cons fresh_prod)
apply(drule validE_append)
@@ -199,9 +212,11 @@
apply(simp add: domain_append)
done
-lemma fresh_implies_not_member[rule_format]:
+lemma fresh_implies_not_member:
fixes \<Gamma>::"ty_context"
- shows "X\<sharp>\<Gamma> \<longrightarrow> \<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))"
+ assumes a: "X\<sharp>\<Gamma>"
+ shows "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))"
+ using a
apply (induct \<Gamma>)
apply (auto dest: validE simp add: fresh_list_cons fresh_prod fresh_atm)
done
@@ -227,8 +242,8 @@
inductive subtype_of_rel
intros
S_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-S_Var[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> (set \<Gamma>); \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (TyVar X) <: T"
-S_Refl[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> (domain \<Gamma>)\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> TyVar X <: TyVar X"
+S_Var[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; (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> T1 <: S1; \<Gamma> \<turnstile> S2 <: T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S1 \<rightarrow> S2) <: (T1 \<rightarrow> T2)"
S_All[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; X\<sharp>\<Gamma>; ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2\<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2"
@@ -239,37 +254,21 @@
using a
proof (induct)
case (S_Top S \<Gamma>)
- have "Top closed_in \<Gamma>"
- by (simp add: closed_in_def ty.supp)
+ have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
moreover
have "S closed_in \<Gamma>" by fact
ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp
next
case (S_Var S T X \<Gamma>)
have "(X,S)\<in>set \<Gamma>" by fact
- hence "X\<in>(domain \<Gamma>)" by (rule domain_inclusion)
- hence "(TyVar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
+ hence "X \<in> domain \<Gamma>" by (rule domain_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 "(TyVar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
-next
- case S_Refl thus ?case
- by (simp add: closed_in_def ty.supp supp_atm)
-next
- case S_Arrow thus ?case by (force simp add: closed_in_def ty.supp)
-next
- case S_All thus ?case by (auto simp add: closed_in_def ty.supp abs_supp)
-qed
+ 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)
-text {* a completely automated proof *}
-lemma subtype_implies_closed:
- assumes a: "\<Gamma> \<turnstile> S <: T"
- shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>"
-using a
-apply (induct)
-apply (auto simp add: closed_in_def ty.supp abs_supp domain_inclusion supp_atm)
-done
lemma subtype_implies_ok:
fixes X::"tyvrs"
@@ -281,14 +280,15 @@
fixes X::"tyvrs"
assumes a1: "\<Gamma> \<turnstile> S <: T"
and a2: "X\<sharp>\<Gamma>"
- shows "X\<sharp>(S,T)"
+ shows "X\<sharp>S \<and> X\<sharp>T"
proof -
from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
- with a2 have b0: "X\<sharp>domain(\<Gamma>)" by (simp add: domain_fresh)
+ with a2 have "X\<sharp>domain(\<Gamma>)" by (simp add: domain_fresh)
+ moreover
from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
- hence b1: "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)"
- and b2: "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: closed_in_def2)
- thus "X\<sharp>(S,T)" using b0 b1 b2 by (force simp add: supp_prod fresh_def)
+ hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)"
+ and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: closed_in_def2)
+ ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
qed
lemma silly_eqvt1:
@@ -322,10 +322,10 @@
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>\<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 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> (TVar X) T"
+ and a3: "\<And>\<Gamma> X x. \<turnstile> \<Gamma> ok \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (TVar X) (TVar 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.
@@ -335,13 +335,8 @@
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 x (pi \<bullet> \<Gamma>) (pi \<bullet> S) (pi\<bullet>Top)" by (simp add: a1)
+ case (S_Top S \<Gamma>)
+ 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 S T X \<Gamma>)
have b1: "\<turnstile> \<Gamma> ok" by fact
@@ -357,7 +352,7 @@
moreover
from b4 have "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp
ultimately
- show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>T)" by (simp add: a2)
+ show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TVar X)) (pi\<bullet>T)" by (simp add: a2)
next
case (S_Refl X \<Gamma>)
have b1: "\<turnstile> \<Gamma> ok" by fact
@@ -366,9 +361,9 @@
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 x (pi\<bullet>\<Gamma>) (pi\<bullet>(TyVar X)) (pi\<bullet>(TyVar X))" by (simp add: a3)
+ 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 (simp, auto intro!: a4 subtype_eqvt)
+ case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt)
next
case (S_All S1 S2 T1 T2 X \<Gamma>)
have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact
@@ -376,7 +371,7 @@
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>T1" "X\<sharp>S1" using b1 b3' by (simp_all add: 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)
@@ -423,27 +418,28 @@
thus ?thesis by simp
qed
-section {* Two proofs for reflexivity of subtyping *}
+subsection {* Reflexivity of Subtyping *}
lemma subtype_reflexivity:
assumes a: "\<turnstile> \<Gamma> ok"
- and b: "T closed_in \<Gamma>"
+ and b: "T closed_in \<Gamma>"
shows "\<Gamma> \<turnstile> T <: T"
using a b
proof(nominal_induct T avoiding: \<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
- have "(\<forall>[X<:T2].T1) closed_in \<Gamma>" by fact
- hence b1: "T2 closed_in \<Gamma>" and b2: "T1 closed_in ((X,T2)#\<Gamma>)"
- by (auto simp add: closed_in_def ty.supp abs_supp)
- have c1: "\<turnstile> \<Gamma> ok" by fact
- hence c2: "\<turnstile> ((X,T2)#\<Gamma>) ok" using b1 f by force
- have "\<Gamma> \<turnstile> T2 <: T2" using i2 b1 c1 by simp
+ case (TAll X T\<^isub>1 T\<^isub>2)
+ have ih_T\<^isub>1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact
+ have ih_T\<^isub>2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
+ have fresh_cond: "X\<sharp>\<Gamma>" by fact
+ 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 ((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> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_cond by force
+ have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
moreover
- have "((X,T2)#\<Gamma>) \<turnstile> T1 <: T1" using i1 b2 c2 by simp
- ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" using f by force
+ have "((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_rel.S_All)
qed (auto simp add: closed_in_def ty.supp supp_atm)
lemma subtype_reflexivity:
@@ -453,24 +449,24 @@
using a b
apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
-(* too bad that this cannot be found automatically *)
+--{* Too bad that this instantiation cannot be found automatically. *}
apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec)
apply(force simp add: closed_in_def)
done
-text {* Inversion lemmas. . . *}
+text {* Inversion lemmas *}
lemma S_TopE:
- shows "\<Gamma> \<turnstile> Top <: T \<Longrightarrow> T = Top"
-apply(ind_cases "\<Gamma> \<turnstile> Top <: T", auto)
-done
+ 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)"
-using a by (cases, auto simp add: ty.inject)
+using a by (cases, auto simp add: ty.inject)
lemma S_AllE_left:
- shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>(\<Gamma>,S1)\<rbrakk>
+ 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)"
apply(frule subtype_implies_ok)
apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T")
@@ -486,10 +482,9 @@
(* 1st conjunct *)
apply(rule conjI)
apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm)
- apply(simp add: fresh_prod)
apply(drule_tac \<Gamma>="((Xa,T1)#\<Gamma>)" in subtype_implies_closed)+
apply(simp add: closed_in_def)
- apply(auto simp add: domain_fresh[of "\<Gamma>" "X", symmetric])
+ apply(simp add: domain_fresh[of "\<Gamma>" "X", symmetric])
apply(simp add: fresh_def)
apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*)
apply(force)
@@ -497,7 +492,7 @@
apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain])
(* 2nd conjunct *)
apply(frule_tac X="X" in subtype_implies_fresh)
- apply(simp add: fresh_prod)
+ apply(assumption)
apply(drule_tac X="Xa" in subtype_implies_fresh)
apply(assumption)
apply(simp add: fresh_prod)
@@ -506,19 +501,22 @@
apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
done
-section {* Type substitution *}
+section {* Type Substitution *}
-lemma subst_ty_fresh[rule_format]:
- fixes P :: "ty"
- and X :: "tyvrs"
- shows "X\<sharp>(T,P) \<longrightarrow> X\<sharp>(subst_ty T Y P)"
+lemma subst_ty_fresh:
+ fixes X :: "tyvrs"
+ assumes a: "X\<sharp>(T,P)"
+ shows "X\<sharp>(subst_ty T Y P)"
+ 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[rule_format]:
+lemma subst_ctxt_fresh:
fixes X::"tyvrs"
- shows "X\<sharp>(\<Gamma>,P) \<longrightarrow> X\<sharp>(subst_ctxt \<Gamma> Y P)"
+ assumes a: "X\<sharp>(\<Gamma>,P)"
+ shows "X\<sharp>(subst_ctxt \<Gamma> Y P)"
+ using a
apply (induct \<Gamma>)
apply (auto intro: subst_ty_fresh simp add: fresh_prod fresh_list_cons)
done
@@ -596,10 +594,16 @@
using a1 a2
by (auto dest: extends_domain simp add: closed_in_def)
+lemma extends_memb:
+ assumes a: "\<Delta> extends \<Gamma>"
+ and b: "(X,T) \<in> set \<Gamma>"
+ shows "(X,T) \<in> set \<Delta>"
+ using a b by (simp add: extends_def)
+
lemma weakening:
assumes a: "\<Gamma> \<turnstile> S <: T"
- and b: "\<turnstile> \<Delta> ok"
- and c: "\<Delta> extends \<Gamma>"
+ and b: "\<turnstile> \<Delta> ok"
+ 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_rel_induct)
@@ -608,7 +612,7 @@
have "\<turnstile> \<Delta> ok" by fact
moreover
have "\<Delta> extends \<Gamma>" by fact
- hence "S closed_in \<Delta>" using lh_drv_prem by (rule_tac extends_closed)
+ 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)
@@ -616,10 +620,10 @@
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
have extends: "\<Delta> extends \<Gamma>" by fact
- have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp add: extends_def)
+ have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb)
moreover
have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp
- ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force
+ ultimately show "\<Delta> \<turnstile> TVar X <: T" using ok by force
next
case (S_Refl \<Gamma> X)
have lh_drv_prem: "X \<in> domain \<Gamma>" by fact
@@ -627,90 +631,84 @@
moreover
have "\<Delta> extends \<Gamma>" by fact
hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain)
- ultimately show "\<Delta> \<turnstile> TyVar X <: TyVar X" by force
+ ultimately show "\<Delta> \<turnstile> TVar X <: TVar X" by force
next
- case S_Arrow thus ?case by force
+ 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
next
- case (S_All \<Gamma> X S1 S2 T1 T2)
- have fresh: "X\<sharp>\<Delta>" 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)
+ case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
+ have fresh_cond: "X\<sharp>\<Delta>" by fact
+ 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 ((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 extends: "\<Delta> extends \<Gamma>" by fact
- have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed)
- hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force
+ 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_cond ok by force
moreover
- have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def)
- ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp
+ 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
- have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp
- ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All)
+ 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: S_All)
qed
-text {* more automated proof *}
+text {* In fact all "non-binding" cases can be solved automatically: *}
lemma weakening:
assumes a: "\<Gamma> \<turnstile> S <: T"
- and b: "\<turnstile> \<Delta> ok"
- and c: "\<Delta> extends \<Gamma>"
+ and b: "\<turnstile> \<Delta> ok"
+ 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_rel_induct)
- case (S_Top \<Gamma> S) thus ?case by (force intro: extends_closed)
-next
- case (S_Var \<Gamma> X S T) thus ?case by (force simp add: extends_def)
-next
- case (S_Refl \<Gamma> X) thus ?case by (force dest: extends_domain)
-next
- case S_Arrow thus ?case by force
-next
- case (S_All \<Gamma> X S1 S2 T1 T2)
- have fresh: "X\<sharp>\<Delta>" 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)
+ case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2)
+ have fresh_cond: "X\<sharp>\<Delta>" by fact
+ 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 ((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 extends: "\<Delta> extends \<Gamma>" by fact
- have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed)
- hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force
+ 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_cond ok by force
moreover
- have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def)
- ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp
+ 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
- have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp
- ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All)
-qed
+ 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: S_All)
+qed (blast intro: extends_closed extends_memb dest: extends_domain)+
+text {* our contexts grow from right to left *}
lemma transitivity_and_narrowing:
shows "\<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
- and "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
+ and "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N"
proof (induct Q fixing: \<Gamma> S T and \<Delta> \<Gamma> X P M N taking: "size_ty" rule: measure_induct_rule)
- case (less Q)
- note IH1_outer = less[THEN conjunct1, rule_format]
- and IH2_outer = less[THEN conjunct2, THEN spec, of _ "[]", simplified, rule_format]
+ case (less Q)
+ note IH_trans = prems[THEN conjunct1, rule_format]
+ note IH_narrow = prems[THEN conjunct2, THEN spec, of _ "[]", simplified, rule_format]
+ --{* The inner induction for transitivity over @{term "\<Gamma> \<turnstile> S <: Q"} *}
have transitivity:
"\<And>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
proof -
- -- {* We first handle the case where T = Top once and for all; this saves some
- repeated argument below (just like on paper :-). We establish a little lemma
- that is invoked where needed in each case of the induction. *}
+ -- {* We first handle the case where T = Top once and for all; this saves some
+ repeated argument below (just like on paper :-). To do so we establish a little
+ lemma that is invoked where needed in the induction for transitivity. *}
have top_case:
"\<And>\<Gamma> S T' P. \<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>; P \<Longrightarrow> \<Gamma> \<turnstile> S <: T'; T'=Top \<or> P\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T'"
proof -
fix \<Gamma> S T' P
- assume S_Top_prem1: "S closed_in \<Gamma>"
- and S_Top_prem2: "\<turnstile> \<Gamma> ok"
+ assume S_Top_prm1: "S closed_in \<Gamma>"
+ and S_Top_prm2: "\<turnstile> \<Gamma> ok"
and alternative: "P \<Longrightarrow> \<Gamma> \<turnstile> S <: T'"
and "T'=Top \<or> P"
moreover
{ assume "T'=Top"
- hence "\<Gamma> \<turnstile> S <: T'" using S_Top_prem1 S_Top_prem2 by (simp add: S_Top)
+ hence "\<Gamma> \<turnstile> S <: T'" using S_Top_prm1 S_Top_prm2 by (simp add: S_Top)
}
moreover
{ assume P
@@ -719,199 +717,184 @@
ultimately show "\<Gamma> \<turnstile> S <: T'" by blast
qed
- (* Now proceed by induction on the left-hand derivation *)
- fix \<Gamma> S T
- assume a: "\<Gamma> \<turnstile> S <: Q"
- assume b: "\<Gamma> \<turnstile> Q <: T"
- from a b show "\<Gamma> \<turnstile> S <: T"
- proof(nominal_induct \<Gamma> S Q\<equiv>Q avoiding: \<Gamma> S T rule: subtype_of_rel_induct)
- case (S_Top \<Gamma>1 S1) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 <: Top"} *}
- have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
- have lh_drv_prem2: "S1 closed_in \<Gamma>1" by fact
- have Q_inst: "Top=Q" by fact
- have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" --"rh drv." by fact
- hence "T = Top" using Q_inst by (simp add: S_TopE)
- thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 by blast
+ --{* Now proceed by the inner induction on the left-hand derivation *}
+ fix \<Gamma>' S' T
+ assume a: "\<Gamma>' \<turnstile> S' <: Q" --{* lh derivation *}
+ assume b: "\<Gamma>' \<turnstile> Q <: T" --{* rh derivation *}
+ from a b show "\<Gamma>' \<turnstile> S' <: T"
+ proof(nominal_induct \<Gamma>' S' Q\<equiv>Q avoiding: \<Gamma>' S' T rule: subtype_of_rel_induct)
+ case (S_Top \<Gamma> S)
+ --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S <: Top"} *}
+ hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
+ hence T_inst: "T = Top" by (simp add: S_TopE)
+ have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact
+ have lh_drv_prm2: "S closed_in \<Gamma>" by fact
+ from lh_drv_prm1 lh_drv_prm2 have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top)
+ thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
next
- case (S_Var \<Gamma>1 X1 S1 T1) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1"} *}
- have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
- have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact
- have IH_inner: "\<And>T. \<Gamma>1 \<turnstile> Q <: T \<Longrightarrow> T1=Q \<Longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact
- have Q_inst: "T1=Q" by fact
- have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" by fact
- with IH_inner have "\<Gamma>1 \<turnstile> S1 <: T" using Q_inst by simp
- thus "\<Gamma>1 \<turnstile> TyVar X1 <: T" using lh_drv_prem1 lh_drv_prem2 by (simp add: subtype_of_rel.S_Var)
+ case (S_Var \<Gamma> Y U Q)
+ --{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar(Y) <: Q"} *}
+ hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
+ have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact
+ have lh_drv_prm2: "(Y,U)\<in>set \<Gamma>" by fact
+ from IH_inner show "\<Gamma> \<turnstile> TVar Y <: T" using lh_drv_prm1 lh_drv_prm2
+ by (simp add: subtype_of_rel.S_Var)
next
- case S_Refl --{* @{text S_Refl} case *}
- thus ?case by simp
+ case (S_Refl \<Gamma> X)
+ --{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar X <: TVar X"} *}
+ thus "\<Gamma> \<turnstile> TVar X <: T" by simp
next
- case (S_Arrow \<Gamma>1 S1 S2 T1 T2) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2"} *}
- have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
- have lh_drv_prem2: "\<Gamma>1 \<turnstile> S2 <: T2" by fact
- have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact
- have Q_inst: "T1 \<rightarrow> T2 = Q" by fact
- have measure: "size_ty T1 < size_ty Q" "size_ty T2 < size_ty Q " using Q_inst by force+
- have "S1 closed_in \<Gamma>1" and "S2 closed_in \<Gamma>1"
- using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed)
- hence "(S1 \<rightarrow> S2) closed_in \<Gamma>1" by (simp add: closed_in_def ty.supp)
+ case (S_Arrow \<Gamma> S1 S2 Q1 Q2)
+ --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: Q1 \<rightarrow> Q2"} *}
+ hence rh_drv: "\<Gamma> \<turnstile> Q1 \<rightarrow> Q2 <: T" by simp
+ have Q_inst: "Q1 \<rightarrow> Q2 = Q" by fact
+ hence Q1_less: "size_ty Q1 < size_ty Q"
+ and Q2_less: "size_ty Q2 < size_ty Q" by auto
+ have lh_drv_prm1: "\<Gamma> \<turnstile> Q1 <: S1" by fact
+ have lh_drv_prm2: "\<Gamma> \<turnstile> S2 <: Q2" by fact
+ have "S1 closed_in \<Gamma>" and "S2 closed_in \<Gamma>"
+ using lh_drv_prm1 lh_drv_prm2 by (simp_all add: subtype_implies_closed)
+ hence "(S1 \<rightarrow> S2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
moreover
- have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok)
+ have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
moreover
- have "T = Top \<or> (\<exists>T3 T4. T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4)"
- using rh_deriv Q_inst by (simp add:S_ArrowE_left)
+ from rh_drv have "T = Top \<or> (\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> \<Gamma> \<turnstile> Q2 <: T2)"
+ by (simp add: S_ArrowE_left)
moreover
- { assume "\<exists>T3 T4. T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4"
- then obtain T3 T4
- where T_inst: "T= T3 \<rightarrow> T4"
- and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1"
- and rh_drv_prem2: "\<Gamma>1 \<turnstile> T2 <: T4" by force
- from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" using measure rh_drv_prem1 lh_drv_prem1 by blast
+ { assume "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> \<Gamma> \<turnstile> Q2 <: T2"
+ then obtain T1 T2
+ where T_inst: "T = T1 \<rightarrow> T2"
+ and rh_drv_prm1: "\<Gamma> \<turnstile> T1 <: Q1"
+ and rh_drv_prm2: "\<Gamma> \<turnstile> Q2 <: T2" by force
+ from IH_trans[of "Q1"] have "\<Gamma> \<turnstile> T1 <: S1" using Q1_less rh_drv_prm1 lh_drv_prm1 by simp
moreover
- from IH1_outer[of "T2"] have "\<Gamma>1 \<turnstile> S2 <: T4" using measure rh_drv_prem2 lh_drv_prem2 by blast
- ultimately have "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using T_inst by force
+ from IH_trans[of "Q2"] have "\<Gamma> \<turnstile> S2 <: T2" using Q2_less rh_drv_prm2 lh_drv_prm2 by simp
+ ultimately have "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2" by (simp add: subtype_of_rel.S_Arrow)
+ hence "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" using T_inst by simp
}
- ultimately show "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using top_case[of "\<Gamma>1" "S1\<rightarrow>S2" _ "T'"] by blast
+ ultimately show "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" using top_case by blast
next
- case (S_All \<Gamma>1 X S1 S2 T1 T2) --{* lh drv.: @{term "\<Gamma>\<turnstile>S<:Q \<equiv> \<Gamma>1\<turnstile>\<forall>[X<:S1].S2 <: \<forall>[X<:T1].T2"} *}
- have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
- have lh_drv_prem2: "((X,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact
- have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact
- have fresh_cond: "X\<sharp>\<Gamma>1" "X\<sharp>S1" "X\<sharp>T1" by fact
- have Q_inst: "\<forall>[X<:T1].T2 = Q" by fact
- have measure: "size_ty T1 < size_ty Q" "size_ty T2 < size_ty Q " using Q_inst by force+
- have "S1 closed_in \<Gamma>1" and "S2 closed_in ((X,T1)#\<Gamma>1)"
- using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed)
- hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>1" by (force simp add: closed_in_def ty.supp abs_supp)
+ case (S_All \<Gamma> X S1 S2 Q1 Q2)
+ --{* in this case lh drv is @{term "\<Gamma>\<turnstile>\<forall>[X<:S1].S2 <: \<forall>[X<:Q1].Q2"} *}
+ hence rh_drv: "\<Gamma> \<turnstile> \<forall>[X<:Q1].Q2 <: T" by simp
+ have lh_drv_prm1: "\<Gamma> \<turnstile> Q1 <: S1" by fact
+ have lh_drv_prm2: "((X,Q1)#\<Gamma>) \<turnstile> S2 <: Q2" by fact
+ have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q1" by fact
+ have Q_inst: "\<forall>[X<:Q1].Q2 = Q" by fact
+ hence Q1_less: "size_ty Q1 < size_ty Q"
+ and Q2_less: "size_ty Q2 < size_ty Q " by auto
+ have "S1 closed_in \<Gamma>" and "S2 closed_in ((X,Q1)#\<Gamma>)"
+ using lh_drv_prm1 lh_drv_prm2 by (simp_all add: subtype_implies_closed)
+ hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
moreover
- have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok)
+ have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
moreover
- (* FIX: Maybe T3,T4 could be T1',T2' *)
- have "T = Top \<or> (\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4)"
- using rh_deriv fresh_cond Q_inst by (auto dest: S_AllE_left simp add: fresh_prod)
+ from rh_drv have "T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> ((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2)"
+ using fresh_cond by (simp add: S_AllE_left)
moreover
- { assume "\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4"
- then obtain T3 T4
- where T_inst: "T= \<forall>[X<:T3].T4"
- and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1"
- and rh_drv_prem2:"((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" by force
- from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1"
- using lh_drv_prem1 rh_drv_prem1 measure by blast
+ { assume "\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: Q1 \<and> ((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2"
+ then obtain T1 T2
+ where T_inst: "T = \<forall>[X<:T1].T2"
+ and rh_drv_prm1: "\<Gamma> \<turnstile> T1 <: Q1"
+ and rh_drv_prm2:"((X,T1)#\<Gamma>) \<turnstile> Q2 <: T2" by force
+ from IH_trans[of "Q1"] have "\<Gamma> \<turnstile> T1 <: S1"
+ using lh_drv_prm1 rh_drv_prm1 Q1_less by blast
moreover
- from IH2_outer[of "T1"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T2"
- using measure lh_drv_prem2 rh_drv_prem1 by force
- with IH1_outer[of "T2"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T4"
- using measure rh_drv_prem2 by force
+ from IH_narrow[of "Q1"] have "((X,T1)#\<Gamma>) \<turnstile> S2 <: Q2"
+ using Q1_less lh_drv_prm2 rh_drv_prm1 by blast
+ with IH_trans[of "Q2"] have "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2"
+ using Q2_less rh_drv_prm2 by blast
moreover
- ultimately have "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T"
- using fresh_cond T_inst by (simp add: fresh_prod subtype_of_rel.S_All)
+ ultimately have "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: \<forall>[X<:T1].T2"
+ using fresh_cond by (simp add: subtype_of_rel.S_All)
+ hence "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T" using T_inst by simp
}
- ultimately show "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T" using Q_inst top_case[of "\<Gamma>1" "\<forall>[X<:S1].S2" _ "T'"]
- by auto
+ ultimately show "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T" using top_case by blast
qed
qed
+ --{* The inner induction for narrowing over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"} *}
have narrowing:
- "\<And>\<Delta> \<Gamma> X M N P. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P<:Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
+ "\<And>\<Delta> \<Gamma> X M N P. (\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N"
proof -
- fix \<Delta> \<Gamma> X M N P
- assume a: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N"
- assume b: "\<Gamma> \<turnstile> P<:Q"
- show "(\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N"
- using a b
- proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@(X,Q)#\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of_rel_induct)
- case (S_Top \<Gamma>1 S1 \<Delta> \<Gamma>2 X)
- then have lh_drv_prem1: "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>2) ok"
- and lh_drv_prem2: "S1 closed_in (\<Delta>@(X,Q)#\<Gamma>2)" by (simp_all only:)
- have rh_drv: "\<Gamma>2 \<turnstile> P <: Q" by fact
- hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
- with lh_drv_prem1 have "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" by (simp only: replace_type)
+ fix \<Delta>' \<Gamma>' X M N P
+ assume a: "(\<Delta>'@[(X,Q)]@\<Gamma>') \<turnstile> M <: N"
+ assume b: "\<Gamma>' \<turnstile> P<:Q"
+ from a b show "(\<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_rel_induct)
+ case (S_Top _ S \<Delta> \<Gamma> X)
+ --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"} *}
+ hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok"
+ and lh_drv_prm2: "S closed_in (\<Delta>@[(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_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
moreover
- from lh_drv_prem2 have "S1 closed_in (\<Delta>@(X,P)#\<Gamma>2)" by (simp add: closed_in_def domain_append)
- ultimately show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: Top" by (rule subtype_of_rel.S_Top)
+ from lh_drv_prm2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: closed_in_def domain_append)
+ ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top)
next
- case (S_Var \<Gamma>1 X1 S1 T1 \<Delta> \<Gamma>2 X)
- then have lh_drv_prem1: "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>2) ok"
- and lh_drv_prem2: "(X1,S1)\<in>set (\<Delta>@(X,Q)#\<Gamma>2)"
- and lh_drv_prem3: "(\<Delta>@(X,Q)#\<Gamma>2) \<turnstile> S1 <: T1"
- and IH_inner: "\<Gamma>2 \<turnstile> P <: Q \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: T1" by (simp_all only:)
- have rh_drv: "\<Gamma>2 \<turnstile> P <: Q" by fact
- hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
- hence a3: "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" using lh_drv_prem1 by (simp only: replace_type)
- show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1"
- proof (cases "X=X1")
- case False
- have b0: "X\<noteq>X1" by fact
- from lh_drv_prem3 rh_drv IH_inner
- have b1: "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: T1" by simp
- from lh_drv_prem2 b0 have b2: "(X1,S1)\<in>set (\<Delta>@(X,P)#\<Gamma>2)" by simp
- show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1" using a3 b2 b1 by (rule subtype_of_rel.S_Var)
- next
- case True
- have b0: "X=X1" by fact
- have a4: "S1=Q"
- proof -
- have "(X1,Q)\<in>set (\<Delta>@(X,Q)#\<Gamma>2)" using b0 by simp
- with lh_drv_prem1 lh_drv_prem2 show "S1=Q" by (blast intro: uniqueness_of_ctxt)
- qed
- have a5: "(\<Delta>@(X,P)#\<Gamma>2) extends \<Gamma>2" by (force simp add: extends_def)
- have a6: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> P <: Q" using b0 a5 rh_drv a3 by (simp add: weakening)
- have a7: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> Q <: T1" using b0 IH_inner lh_drv_prem3 rh_drv a4 by simp
- have a8: "(\<Delta>@(X1,P)#\<Gamma>2) \<turnstile> P <: T1" using a6 a7 transitivity by blast
- have a9: "(X1,P)\<in>set (\<Delta>@(X,P)#\<Gamma>2)" using b0 by simp
- show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: T1" using a3 b0 a8 a9 by force
- qed
+ case (S_Var _ Y S N \<Delta> \<Gamma> X)
+ --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: N"} *}
+ hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"
+ and lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok"
+ and lh_drv_prm2: "(Y,S)\<in>set (\<Delta>@[(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)
+ hence cntxt_ok: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" using lh_drv_prm1 by (simp add: replace_type)
+ -- {* we distinguishing the cases @{term "X\<noteq>Y"} and @{term "X=Y"} (the latter
+ being the interesting one) *}
+ { assume "X\<noteq>Y"
+ hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2 by simp
+ with IH_inner have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N"
+ using cntxt_ok by (simp add: subtype_of_rel.S_Var)
+ }
+ moreover
+ { have memb_XQ: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp
+ have memb_XP: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp
+ assume "X=Y"
+ hence "S=Q" using lh_drv_prm1 lh_drv_prm2 memb_XQ by (simp only: uniqueness_of_ctxt)
+ hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
+ moreover
+ have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
+ hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv cntxt_ok by (simp only: weakening)
+ ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" using transitivity by simp
+ hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar X <: N" using memb_XP cntxt_ok
+ by (simp only: subtype_of_rel.S_Var)
+ }
+ ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N" by blast
next
- case (S_Refl \<Gamma>1 X1 \<Delta> \<Gamma>2 X)
- have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
- have lh_drv_prem2: "X1 \<in> domain \<Gamma>1" by fact
- have \<Gamma>1_inst: "\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma>2" by fact
- have "\<Gamma>2 \<turnstile> P <: Q" by fact
- hence "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed)
- hence a3: "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" using lh_drv_prem1 \<Gamma>1_inst by (simp add: replace_type)
- have b0: "X1 \<in> domain (\<Delta>@(X,P)#\<Gamma>2)" using lh_drv_prem2 \<Gamma>1_inst by (simp add: domain_append)
- show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> TyVar X1 <: TyVar X1" using a3 b0 by (rule subtype_of_rel.S_Refl)
- next
- case S_Arrow thus ?case by blast
+ case (S_Refl _ Y \<Delta> \<Gamma> X)
+ --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: TVar Y"} *}
+ hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok"
+ and lh_drv_prm2: "Y \<in> domain (\<Delta>@[(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_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type)
+ moreover
+ from lh_drv_prm2 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_rel.S_Refl)
next
- case (S_All \<Gamma>1 X1 S1 S2 T1 T2 \<Delta> \<Gamma>2 X)
- have IH_inner1: "\<And>\<Delta> \<Gamma> X. \<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Gamma>1 = \<Delta>@(X,Q)#\<Gamma> \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> T1 <: S1" by fact
- have IH_inner2: "\<And>\<Delta> \<Gamma> X. \<Gamma> \<turnstile> P <: Q \<Longrightarrow> (X1,T1)#\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma> \<Longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> S2 <: T2"
- by fact
- have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact
- have lh_drv_prem2: "X1\<sharp>\<Gamma>1" "X1\<sharp>S1" "X1\<sharp>T1" by fact (* check this whether this is the lh_drv_p2 *)
- have lh_drv_prem3: "((X1,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact
- have \<Gamma>1_inst: "\<Gamma>1 = \<Delta>@(X,Q)#\<Gamma>2" by fact
- have a2: "\<Gamma>2 \<turnstile> P <: Q" by fact
- have b0: "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> T1 <: S1" using \<Gamma>1_inst a2 lh_drv_prem1 IH_inner1 by simp
- have b1: "(((X1,T1)#\<Delta>)@(X,P)#\<Gamma>2) \<turnstile> S2 <: T2" using \<Gamma>1_inst a2 lh_drv_prem3 IH_inner2
- apply(auto)
- apply(drule_tac x="\<Gamma>2" in meta_spec)
- apply(drule_tac x="(X1,T1)#\<Delta>" in meta_spec)
- apply(auto)
- done
- have b3: "X1\<sharp>(\<Delta>@(X,P)#\<Gamma>2)" using lh_drv_prem2 \<Gamma>1_inst a2
- by (auto simp add: fresh_prod fresh_list_append fresh_list_cons dest: subtype_implies_fresh)
- show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> \<forall> [X1<:S1].S2 <: \<forall> [X1<:T1].T2" using b0 b3 b1 by force
+ case (S_Arrow _ Q1 Q2 S1 S2 \<Delta> \<Gamma> X)
+ --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2"} *}
+ thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2" by blast
+ next
+ case (S_All _ Y S1 S2 T1 T2 \<Delta> \<Gamma> X)
+ --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> \<forall>[Y<:S1].S2 <: \<forall>[Y<:T1].T2"} *}
+ hence IH_inner1: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T1 <: S1"
+ and IH_inner2: "((Y,T1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S2 <: T2"
+ and lh_drv_prm2: "Y\<sharp>(\<Delta>@[(X,Q)]@\<Gamma>)" by force+
+ have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
+ hence "Y\<sharp>P" using lh_drv_prm2 by (simp only: fresh_list_append subtype_implies_fresh)
+ hence "Y\<sharp>(\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2
+ by (simp add: fresh_list_append fresh_list_cons fresh_prod)
+ with IH_inner1 IH_inner2
+ show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> \<forall>[Y<:S1].S2 <: \<forall>[Y<:T1].T2" by (simp add: subtype_of_rel.S_All)
qed
qed
from transitivity narrowing show ?case by blast
qed
-
-section {* Terms *}
-nominal_datatype trm = Var "vrs"
- | Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty"
- | TAbs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
- | App "trm" "trm"
- | TApp "trm" "ty"
-
-consts
- Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100)
- TAbs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100)
-translations
- "Lam [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys"
- "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys"
end
\ No newline at end of file