1 (* $Id$ *) |
1 (* $Id$ *) |
2 |
2 |
|
3 (*<*) |
3 theory fsub |
4 theory fsub |
4 imports "../nominal" |
5 imports "../nominal" |
5 begin |
6 begin |
6 |
7 (*>*) |
7 text {* Authors: Christian Urban, |
8 |
8 Benjamin Pierce, |
9 text{* Authors: Christian Urban, |
9 Steve Zdancewic. |
10 Benjamin Pierce, |
10 Stephanie Weihrich and |
11 Steve Zdancewic, |
11 Dimitrios Vytiniotis; |
12 Stephanie Weihrich and |
12 |
13 Dimitrios Vytiniotis, |
13 with help from Stefan Berghofer and Markus Wenzel. |
14 |
14 *} |
15 with great help from Stefan Berghofer and Markus Wenzel. *} |
15 |
|
16 |
16 |
17 section {* Atom Types, Types and Terms *} |
17 section {* Atom Types, Types and Terms *} |
18 |
18 |
|
19 text {* The main point of this solution is to use names everywhere (be they bound, |
|
20 binding or free). There are two kinds of names corresponding to type-variables and |
|
21 to term-variables in System \FSUB. These two kinds of names are represented in |
|
22 the nominal datatype package as atom-types @{text "tyvrs"} and @{text "vrs"}: *} |
|
23 |
19 atom_decl tyvrs vrs |
24 atom_decl tyvrs vrs |
20 |
25 |
|
26 text{* There are numerous facts that come with this declaration: for example that |
|
27 there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *} |
|
28 |
|
29 text{* The constructors for types and terms in System \FSUB{} contain abstractions |
|
30 over type-variables and term-variables. The nominal datatype-package uses |
|
31 @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *} |
|
32 |
21 nominal_datatype ty = |
33 nominal_datatype ty = |
22 TVar "tyvrs" |
34 Tvar "tyvrs" |
23 | Top |
35 | Top |
24 | Arrow "ty" "ty" ("_ \<rightarrow> _" [900,900] 900) |
36 | Arrow "ty" "ty" ("_ \<rightarrow> _" [100,100] 100) |
25 | TAll "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" |
37 | Forall "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" |
26 |
38 |
27 nominal_datatype trm = |
39 nominal_datatype trm = |
28 Var "vrs" |
40 Var "vrs" |
29 | Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty" |
41 | Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty" |
30 | TAbs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty" |
42 | Tabs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty" |
31 | App "trm" "trm" |
43 | App "trm" "trm" |
32 | TApp "trm" "ty" |
44 | Tapp "trm" "ty" |
|
45 |
|
46 text {* To be polite to the eye, some more familiar notation is introduced. |
|
47 Because of the change in the order of the argument, one needs to use |
|
48 translation rules, instead of syntax annotations at the term-constructors |
|
49 like for @{term "Arrow"}. *} |
33 |
50 |
34 syntax |
51 syntax |
35 TAll_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall> [_<:_]._" [900,900,900] 900) |
52 Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall>[_<:_]._" [100,100,100] 100) |
36 Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100) |
53 Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100) |
37 TAbs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100) |
54 Tabs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Tabs [_<:_]._" [100,100,100] 100) |
38 |
55 |
39 translations |
56 translations |
40 "\<forall>[a<:ty1].ty2" \<rightleftharpoons> "TAll a ty2 ty1" |
57 "\<forall>[X<:T\<^isub>1].T\<^isub>2" \<rightleftharpoons> "ty.Forall X T\<^isub>2 T\<^isub>1" |
41 "Lam [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys" |
58 "Lam [x:T].t" \<rightleftharpoons> "trm.Lam x t T" |
42 "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys" |
59 "Tabs [X<:T].t" \<rightleftharpoons> "trm.Tabs X t T" |
43 |
60 |
44 subsection {* Typing contexts and Their Domains *} |
61 text {* Note that the nominal-datatype declarations for @{typ "ty"} and @{typ "trm"} |
|
62 do \emph{not} define "classical" constructor-based datatypes, but rather define |
|
63 $\alpha$-equivalence classes. Indeed we can show that $\alpha$-equivalent @{typ "ty"}s |
|
64 and @{typ "trm"}s are equal: *} |
|
65 |
|
66 lemma alpha_illustration: |
|
67 shows "\<forall>[X<:T].(Tvar X) = \<forall>[Y<:T].(Tvar Y)" |
|
68 and "Lam [x:T].(Var x) = Lam [y:T].(Var y)" |
|
69 by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm) |
|
70 |
|
71 section {* Typing Contexts *} |
45 |
72 |
46 types ty_context = "(tyvrs\<times>ty) list" |
73 types ty_context = "(tyvrs\<times>ty) list" |
|
74 |
|
75 text {* Typing contexts are represented as lists "growing" on the left, |
|
76 in contrast to the POPLmark-paper. *} |
|
77 |
|
78 text {* In order to state valitity-conditions for typing-context, the notion of |
|
79 a domain of a typing-context is handy. *} |
47 |
80 |
48 consts |
81 consts |
49 "domain" :: "ty_context \<Rightarrow> tyvrs set" |
82 "domain" :: "ty_context \<Rightarrow> tyvrs set" |
50 primrec |
83 primrec |
51 "domain [] = {}" |
84 "domain [] = {}" |
73 |
105 |
74 lemma domain_append: |
106 lemma domain_append: |
75 shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))" |
107 shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))" |
76 by (induct \<Gamma>, auto) |
108 by (induct \<Gamma>, auto) |
77 |
109 |
78 section {* Size Functions and Capture Avoiding Substitutiuon for Types *} |
110 text {* Not all lists of type @{typ "ty_context"} are well-formed. One condition |
79 |
111 requires that in @{term "(X,S)#\<Gamma>"} all free variables of @{term "S"} must be |
80 text {* they cannot yet be defined conveniently unless we have a recursion combinator *} |
112 in @{term "domain \<Gamma>"}, that is @{term "S"} must be closed in @{term "\<Gamma>"}. *} |
81 |
|
82 consts size_ty :: "ty \<Rightarrow> nat" |
|
83 |
|
84 lemma size_ty[simp]: |
|
85 shows "size_ty (TVar X) = 1" |
|
86 and "size_ty (Top) = 1" |
|
87 and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (t1 \<rightarrow> t2) = m + n + 1" |
|
88 and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall> [a<:t1].t2) = m + n + 1" |
|
89 sorry |
|
90 |
|
91 consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" |
|
92 |
|
93 lemma subst_ty[simp]: |
|
94 shows "subst_ty (TVar X) Y T = (if X=Y then T else (TVar X))" |
|
95 and "subst_ty Top Y T = Top" |
|
96 and "subst_ty (T1 \<rightarrow> T2) Y T = (subst_ty T1 Y T) \<rightarrow> (subst_ty T2 Y T)" |
|
97 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))" |
|
98 and "\<lbrakk>X\<sharp>Y; X\<sharp>T\<rbrakk> \<Longrightarrow> subst_ty (\<forall>[X<:T1].T2) Y T = (\<forall>[X<:(subst_ty T1 Y T)].(subst_ty T2 Y T))" |
|
99 sorry |
|
100 |
|
101 |
|
102 consts subst_ctxt :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" |
|
103 primrec |
|
104 "subst_ctxt [] Y T = []" |
|
105 "subst_ctxt (XT#Xs) Y T = (fst XT, subst_ty (snd XT) Y T)#(subst_ctxt Xs Y T)" |
|
106 |
|
107 subsection {* valid contexts *} |
|
108 |
113 |
109 constdefs |
114 constdefs |
110 "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) |
115 "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) |
111 "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)" |
116 "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)" |
112 |
117 |
113 lemma closed_in_def2: |
118 lemma closed_in_def2: |
114 shows "(S closed_in \<Gamma>) = ((supp S)\<subseteq>((supp (domain \<Gamma>)):: tyvrs set))" |
119 shows "(S closed_in \<Gamma>) = ((supp S)\<subseteq>((supp (domain \<Gamma>))::tyvrs set))" |
115 apply(simp add: closed_in_def) |
120 apply(simp add: closed_in_def at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain]) |
116 apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain]) |
|
117 done |
121 done |
118 |
122 |
119 lemma closed_in_eqvt: |
123 lemma closed_in_eqvt: |
120 fixes pi::"tyvrs prm" |
124 fixes pi::"tyvrs prm" |
121 assumes a: "S closed_in \<Gamma>" |
125 assumes a: "S closed_in \<Gamma>" |
134 valid_sym :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100) |
138 valid_sym :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100) |
135 translations |
139 translations |
136 "\<turnstile> \<Gamma> ok" \<rightleftharpoons> "\<Gamma> \<in> valid_rel" |
140 "\<turnstile> \<Gamma> ok" \<rightleftharpoons> "\<Gamma> \<in> valid_rel" |
137 inductive valid_rel |
141 inductive valid_rel |
138 intros |
142 intros |
139 v1[intro]: "\<turnstile> [] ok" |
143 v_nil[intro]: "\<turnstile> [] ok" |
140 v2[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>\<Gamma>; T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> ((X,T)#\<Gamma>) ok" |
144 v_cons[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>\<Gamma>; T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> ((X,T)#\<Gamma>) ok" |
|
145 |
141 |
146 |
142 lemma valid_eqvt: |
147 lemma valid_eqvt: |
143 fixes pi::"tyvrs prm" |
148 fixes pi::"tyvrs prm" |
144 assumes a: "\<turnstile> \<Gamma> ok" |
149 assumes a: "\<turnstile> \<Gamma> ok" |
145 shows "\<turnstile> (pi\<bullet>\<Gamma>) ok" |
150 shows "\<turnstile> (pi\<bullet>\<Gamma>) ok" |
146 using a |
151 using a |
147 proof (induct) |
152 proof (induct) |
148 case v1 |
153 case v_nil |
149 show ?case by force |
154 show "\<turnstile> (pi\<bullet>[]) ok" by (simp add: valid_rel.v_nil) |
150 next |
155 next |
151 case (v2 T X \<Gamma>) |
156 case (v_cons T X \<Gamma>) |
152 have a1: "\<turnstile> (pi \<bullet> \<Gamma>) ok" by fact |
157 have "\<turnstile> (pi \<bullet> \<Gamma>) ok" by fact |
153 have a2: "X\<sharp>\<Gamma>" by fact |
158 moreover |
154 have a3: "T closed_in \<Gamma>" by fact |
159 have "X\<sharp>\<Gamma>" by fact |
155 show ?case |
160 hence "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt) |
156 proof (simp, rule valid_rel.v2) |
161 moreover |
157 show "\<turnstile> (pi \<bullet> \<Gamma>) ok" using a1 by simp |
162 have "T closed_in \<Gamma>" by fact |
158 next |
163 hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (rule closed_in_eqvt) |
159 show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: fresh_eqvt) |
164 ultimately show "\<turnstile> (pi\<bullet>((X,T)#\<Gamma>)) ok" by (simp add: valid_rel.v_cons) |
160 next |
|
161 show "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" using a3 by (rule closed_in_eqvt) |
|
162 qed |
|
163 qed |
165 qed |
164 |
166 |
165 lemma validE: |
167 lemma validE: |
166 assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok" |
168 assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok" |
167 shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>\<Gamma> \<and> T closed_in \<Gamma>" |
169 shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>\<Gamma> \<and> T closed_in \<Gamma>" |
214 |
216 |
215 lemma fresh_implies_not_member: |
217 lemma fresh_implies_not_member: |
216 fixes \<Gamma>::"ty_context" |
218 fixes \<Gamma>::"ty_context" |
217 assumes a: "X\<sharp>\<Gamma>" |
219 assumes a: "X\<sharp>\<Gamma>" |
218 shows "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))" |
220 shows "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))" |
219 using a |
221 using a by (induct \<Gamma>, auto dest: validE simp add: fresh_list_cons fresh_prod fresh_atm) |
220 apply (induct \<Gamma>) |
|
221 apply (auto dest: validE simp add: fresh_list_cons fresh_prod fresh_atm) |
|
222 done |
|
223 |
222 |
224 lemma uniqueness_of_ctxt: |
223 lemma uniqueness_of_ctxt: |
225 fixes \<Gamma>::"ty_context" |
224 fixes \<Gamma>::"ty_context" |
226 assumes a: "\<turnstile> \<Gamma> ok" |
225 assumes a: "\<turnstile> \<Gamma> ok" |
227 and b: "(X,T)\<in>set \<Gamma>" |
226 and b: "(X,T)\<in>set \<Gamma>" |
228 and c: "(X,S)\<in>set \<Gamma>" |
227 and c: "(X,S)\<in>set \<Gamma>" |
229 shows "T=S" |
228 shows "T=S" |
230 using a b c |
229 using a b c by (induct \<Gamma>, auto dest: validE fresh_implies_not_member) |
231 apply (induct \<Gamma>) |
230 |
232 apply (auto dest!: validE fresh_implies_not_member) |
231 subsection {* Size Functions and Capture-Avoiding Substitutiuon for Types *} |
233 done |
232 |
|
233 text {* In the current version of the nominal datatype |
|
234 package even simple functions (such as size of types and capture-avoiding |
|
235 substitution) can only be defined manually via some sophisticated proof |
|
236 constructions. Therefore we sill just assume them here. *} |
|
237 |
|
238 consts size_ty :: "ty \<Rightarrow> nat" |
|
239 |
|
240 lemma size_ty[simp]: |
|
241 shows "size_ty (Tvar X) = 1" |
|
242 and "size_ty (Top) = 1" |
|
243 and "\<lbrakk>size_ty t\<^isub>1 = m ; size_ty t\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (t\<^isub>1 \<rightarrow> t\<^isub>2) = m + n + 1" |
|
244 and "\<lbrakk>size_ty t\<^isub>1 = m ; size_ty t\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall>[a<:t\<^isub>1].t\<^isub>2) = m + n + 1" |
|
245 sorry |
|
246 |
|
247 consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100) |
|
248 |
|
249 lemma subst_ty[simp]: |
|
250 shows "(Tvar X)[Y:=T]\<^isub>t\<^isub>y = (if X=Y then T else (Tvar X))" |
|
251 and "(Top)[Y:=T]\<^isub>t\<^isub>y = Top" |
|
252 and "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)" |
|
253 and "X\<sharp>(Y,T) \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))" |
|
254 and "\<lbrakk>X\<sharp>Y; X\<sharp>T\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))" |
|
255 sorry |
|
256 |
|
257 consts subst_ctxt :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100) |
|
258 primrec |
|
259 "([])[Y:=T]\<^isub>t\<^isub>y\<^isub>c= []" |
|
260 "(XT#\<Gamma>)[Y:=T]\<^isub>t\<^isub>y\<^isub>c = (fst XT,(snd XT)[Y:=T]\<^isub>t\<^isub>y)#(\<Gamma>[Y:=T]\<^isub>t\<^isub>y\<^isub>c)" |
234 |
261 |
235 section {* Subtyping *} |
262 section {* Subtyping-Relation *} |
236 |
263 |
237 consts |
264 consts |
238 subtype_of_rel :: "(ty_context \<times> ty \<times> ty) set" |
265 subtype_of :: "(ty_context \<times> ty \<times> ty) set" |
239 subtype_of_sym :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [100,100,100] 100) |
266 syntax |
|
267 subtype_of_syn :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [100,100,100] 100) |
|
268 |
240 translations |
269 translations |
241 "\<Gamma> \<turnstile> S <: T" \<rightleftharpoons> "(\<Gamma>,S,T) \<in> subtype_of_rel" |
270 "\<Gamma> \<turnstile> S <: T" \<rightleftharpoons> "(\<Gamma>,S,T) \<in> subtype_of" |
242 inductive subtype_of_rel |
271 inductive subtype_of |
243 intros |
272 intros |
244 S_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" |
273 S_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" |
245 S_Var[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (TVar X) <: T" |
274 S_Var[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T" |
246 S_Refl[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> TVar X <: TVar X" |
275 S_Refl[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X" |
247 S_Arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; \<Gamma> \<turnstile> S2 <: T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S1 \<rightarrow> S2) <: (T1 \<rightarrow> T2)" |
276 S_Arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^isub>1 \<rightarrow> S\<^isub>2) <: (T\<^isub>1 \<rightarrow> T\<^isub>2)" |
248 S_All[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; X\<sharp>\<Gamma>; ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2\<rbrakk> |
277 S_All[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; X\<sharp>\<Gamma>; ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> |
249 \<Longrightarrow> \<Gamma> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
278 \<Longrightarrow> \<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" |
250 |
279 |
251 lemma subtype_implies_closed: |
280 lemma subtype_implies_closed: |
252 assumes a: "\<Gamma> \<turnstile> S <: T" |
281 assumes a: "\<Gamma> \<turnstile> S <: T" |
253 shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" |
282 shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" |
254 using a |
283 using a |
309 done |
337 done |
310 |
338 |
311 lemma subtype_eqvt: |
339 lemma subtype_eqvt: |
312 fixes pi::"tyvrs prm" |
340 fixes pi::"tyvrs prm" |
313 shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
341 shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
314 apply(erule subtype_of_rel.induct) |
342 apply(erule subtype_of.induct) |
315 apply(force intro: valid_eqvt closed_in_eqvt) |
343 apply(force intro: valid_eqvt closed_in_eqvt) |
316 apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1) |
344 apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1) |
317 apply(force intro: valid_eqvt silly_eqvt2) |
345 apply(force intro: valid_eqvt silly_eqvt2) |
318 apply(force) |
346 apply(force) |
319 apply(force intro!: S_All simp add: fresh_prod pt_fresh_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
347 apply(force intro!: S_All simp add: fresh_prod fresh_eqvt) |
320 done |
348 done |
321 |
349 |
322 lemma subtype_of_rel_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_All]: |
350 lemma subtype_of_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_All]: |
323 fixes P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool" |
351 fixes P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool" |
324 assumes a: "\<Gamma> \<turnstile> S <: T" |
352 assumes a: "\<Gamma> \<turnstile> S <: T" |
325 and a1: "\<And>\<Gamma> S x. \<turnstile> \<Gamma> ok \<Longrightarrow> S closed_in \<Gamma> \<Longrightarrow> P x \<Gamma> S Top" |
353 and a1: "\<And>\<Gamma> S x. \<turnstile> \<Gamma> ok \<Longrightarrow> S closed_in \<Gamma> \<Longrightarrow> P x \<Gamma> S Top" |
326 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) |
354 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) |
327 \<Longrightarrow> P x \<Gamma> (TVar X) T" |
355 \<Longrightarrow> P x \<Gamma> (Tvar X) T" |
328 and a3: "\<And>\<Gamma> X x. \<turnstile> \<Gamma> ok \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (TVar X) (TVar X)" |
356 and a3: "\<And>\<Gamma> X x. \<turnstile> \<Gamma> ok \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P x \<Gamma> (Tvar X) (Tvar X)" |
329 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> |
357 and a4: "\<And>\<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> (\<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1) \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> |
330 (\<And>z. P z \<Gamma> S2 T2) \<Longrightarrow> P x \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2)" |
358 (\<And>z. P z \<Gamma> S\<^isub>2 T\<^isub>2) \<Longrightarrow> P x \<Gamma> (S\<^isub>1 \<rightarrow> S\<^isub>2) (T\<^isub>1 \<rightarrow> T\<^isub>2)" |
331 and a5: "\<And>\<Gamma> X S1 S2 T1 T2 x. |
359 and a5: "\<And>\<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S\<^isub>1,T\<^isub>1) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> (\<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1) |
332 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 |
360 \<Longrightarrow> ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> (\<And>z. P z ((X,T\<^isub>1)#\<Gamma>) S\<^isub>2 T\<^isub>2) \<Longrightarrow> P x \<Gamma> (\<forall>[X<:S\<^isub>1].S\<^isub>2) (\<forall>[X<:T\<^isub>1].T\<^isub>2)" |
333 \<Longrightarrow> (\<And>z. P z ((X,T1)#\<Gamma>) S2 T2) \<Longrightarrow> P x \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2)" |
|
334 shows "P x \<Gamma> S T" |
361 shows "P x \<Gamma> S T" |
335 proof - |
362 proof - |
336 from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" |
363 from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" |
337 proof (induct) |
364 proof (induct) |
338 case (S_Top S \<Gamma>) |
365 case (S_Top S \<Gamma>) |
339 thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1) |
366 thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1) |
340 next |
367 next |
341 case (S_Var S T X \<Gamma>) |
368 case (S_Var S T X \<Gamma>) |
342 have b1: "\<turnstile> \<Gamma> ok" by fact |
369 have "\<turnstile> \<Gamma> ok" by fact |
343 have b2: "(X,S) \<in> set \<Gamma>" by fact |
370 hence "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
344 have b3: "\<Gamma> \<turnstile> S <: T" by fact |
|
345 have b4: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact |
|
346 from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
|
347 moreover |
371 moreover |
348 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]) |
372 have "(X,S) \<in> set \<Gamma>" by fact |
|
373 hence "pi\<bullet>(X,S)\<in>pi\<bullet>(set \<Gamma>)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
349 hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
374 hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
350 moreover |
375 moreover |
351 from b3 have "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt) |
376 have "\<Gamma> \<turnstile> S <: T" by fact |
352 moreover |
377 hence "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt) |
353 from b4 have "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp |
378 moreover |
|
379 have "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact |
|
380 hence "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp |
354 ultimately |
381 ultimately |
355 show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TVar X)) (pi\<bullet>T)" by (simp add: a2) |
382 show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>T)" by (simp add: a2) |
356 next |
383 next |
357 case (S_Refl X \<Gamma>) |
384 case (S_Refl X \<Gamma>) |
358 have b1: "\<turnstile> \<Gamma> ok" by fact |
385 have "\<turnstile> \<Gamma> ok" by fact |
359 have b2: "X \<in> domain \<Gamma>" by fact |
386 hence "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
360 from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
|
361 moreover |
387 moreover |
362 from b2 have "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
388 have "X \<in> domain \<Gamma>" by fact |
|
389 hence "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
363 hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst]) |
390 hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst]) |
364 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(TVar X)) (pi\<bullet>(TVar X))" by (simp add: a3) |
391 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>(Tvar X))" by (simp add: a3) |
365 next |
392 next |
366 case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt) |
393 case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt) |
367 next |
394 next |
368 case (S_All S1 S2 T1 T2 X \<Gamma>) |
395 case (S_All S1 S2 T1 T2 X \<Gamma>) |
369 have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact |
396 have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact |
370 have b2: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1)" by fact |
397 have b2: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1)" by fact |
371 have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact |
398 have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact |
372 have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact |
399 have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact |
373 have b3': "X\<sharp>\<Gamma>" by fact |
400 have b3: "X\<sharp>\<Gamma>" by fact |
374 have b3'': "X\<sharp>T1" "X\<sharp>S1" using b1 b3' by (simp_all add: subtype_implies_fresh) |
401 have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh) |
375 have b3: "X\<sharp>(\<Gamma>,S1,T1)" using b3' b3'' by (simp add: fresh_prod) |
|
376 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)" |
402 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)" |
377 by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1) |
403 by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1) |
378 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)" |
404 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)" |
379 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" |
405 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" |
380 by (auto simp add: fresh_prod fresh_atm) |
406 by (auto simp add: fresh_prod fresh_atm) |
387 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" |
413 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" |
388 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
414 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
389 with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" |
415 with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" |
390 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
416 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
391 hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp |
417 hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp |
392 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" |
418 from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" |
393 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
419 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
394 with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" |
420 with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" |
395 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
421 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
396 hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp |
422 hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp |
397 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" |
423 from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" |
398 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
424 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
399 with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" |
425 with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" |
400 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
426 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
401 hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp |
427 hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp |
402 from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt) |
428 from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt) |
403 from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt) |
429 from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt) |
404 hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp |
430 hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp |
405 hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1 |
431 hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1 |
406 by (simp only: pt_tyvrs2 calc_atm, simp) |
432 by (simp only: pt_tyvrs2 calc_atm, simp) |
407 have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod) |
433 have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod) |
408 have main: "P x (?pi'\<bullet>\<Gamma>) (\<forall> [C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall> [C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2))" |
434 have main: "P x (?pi'\<bullet>\<Gamma>) (\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2))" |
409 using f7 fnew e1 c1 e2 c2 by (rule a5) |
435 using f7 fnew e1 c1 e2 c2 by (rule a5) |
410 have alpha1: "(\<forall> [C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall> [X<:S1].S2))" |
436 have alpha1: "(\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall>[X<:S1].S2))" |
411 using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
437 using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
412 have alpha2: "(\<forall> [C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall> [X<:T1].T2))" |
438 have alpha2: "(\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall>[X<:T1].T2))" |
413 using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
439 using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
414 show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall> [X<:S1].S2)) (pi\<bullet>(\<forall> [X<:T1].T2))" |
440 show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall>[X<:S1].S2)) (pi\<bullet>(\<forall>[X<:T1].T2))" |
415 using alpha1 alpha2 f6a main by simp |
441 using alpha1 alpha2 f6a main by simp |
416 qed |
442 qed |
417 hence "P x (([]::tyvrs prm)\<bullet>\<Gamma>) (([]::tyvrs prm)\<bullet>S) (([]::tyvrs prm)\<bullet>T)" by blast |
443 hence "P x (([]::tyvrs prm)\<bullet>\<Gamma>) (([]::tyvrs prm)\<bullet>S) (([]::tyvrs prm)\<bullet>T)" by blast |
418 thus ?thesis by simp |
444 thus ?thesis by simp |
419 qed |
445 qed |
437 hence ok': "\<turnstile> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_cond by force |
463 hence ok': "\<turnstile> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_cond by force |
438 have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp |
464 have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp |
439 moreover |
465 moreover |
440 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 |
466 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 |
441 ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T\<^isub>2].T\<^isub>1 <: \<forall>[X<:T\<^isub>2].T\<^isub>1" using fresh_cond |
467 ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T\<^isub>2].T\<^isub>1 <: \<forall>[X<:T\<^isub>2].T\<^isub>1" using fresh_cond |
442 by (simp add: subtype_of_rel.S_All) |
468 by (simp add: subtype_of.S_All) |
443 qed (auto simp add: closed_in_def ty.supp supp_atm) |
469 qed (auto simp add: closed_in_def ty.supp supp_atm) |
444 |
470 |
445 lemma subtype_reflexivity: |
471 lemma subtype_reflexivity: |
446 assumes a: "\<turnstile> \<Gamma> ok" |
472 assumes a: "\<turnstile> \<Gamma> ok" |
447 and b: "T closed_in \<Gamma>" |
473 and b: "T closed_in \<Gamma>" |
448 shows "\<Gamma> \<turnstile> T <: T" |
474 shows "\<Gamma> \<turnstile> T <: T" |
449 using a b |
475 using a b |
450 apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe) |
476 apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe) |
451 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) |
477 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) |
452 --{* Too bad that this instantiation cannot be found automatically. *} |
478 --{* Too bad that this instantiation cannot be found automatically by |
|
479 auto; blast cannot be used since the simplification rule |
|
480 @{text "closed_in_def"} needs to be applied. *} |
453 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec) |
481 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec) |
454 apply(force simp add: closed_in_def) |
482 apply(force simp add: closed_in_def) |
455 done |
483 done |
456 |
484 |
457 text {* Inversion lemmas *} |
485 text {* Inversion lemmas *} |
469 shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>\<Gamma>; X\<sharp>S1\<rbrakk> |
497 shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>\<Gamma>; X\<sharp>S1\<rbrakk> |
470 \<Longrightarrow> T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2)" |
498 \<Longrightarrow> T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2)" |
471 apply(frule subtype_implies_ok) |
499 apply(frule subtype_implies_ok) |
472 apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T") |
500 apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T") |
473 apply(auto simp add: ty.inject alpha) |
501 apply(auto simp add: ty.inject alpha) |
474 apply(rule_tac x="[(X,Xa)]\<bullet>T2" in exI) |
502 apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI) |
475 (* term *) |
503 (* term *) |
476 apply(rule conjI) |
504 apply(rule conjI) |
477 apply(rule sym) |
505 apply(rule sym) |
478 apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
506 apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
479 apply(rule pt_tyvrs3) |
507 apply(rule pt_tyvrs3) |
480 apply(simp) |
508 apply(simp) |
481 apply(rule at_ds5[OF at_tyvrs_inst]) |
509 apply(rule at_ds5[OF at_tyvrs_inst]) |
482 (* 1st conjunct *) |
510 (* 1st conjunct *) |
483 apply(rule conjI) |
511 apply(rule conjI) |
484 apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm) |
512 apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm) |
485 apply(drule_tac \<Gamma>="((Xa,T1)#\<Gamma>)" in subtype_implies_closed)+ |
513 apply(drule_tac \<Gamma>="((Xa,T\<^isub>1)#\<Gamma>)" in subtype_implies_closed)+ |
486 apply(simp add: closed_in_def) |
514 apply(simp add: closed_in_def) |
487 apply(simp add: domain_fresh[of "\<Gamma>" "X", symmetric]) |
515 apply(simp add: domain_fresh[of "\<Gamma>" "X", symmetric]) |
488 apply(simp add: fresh_def) |
516 apply(simp add: fresh_def) |
489 apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*) |
517 apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*) |
490 apply(force) |
518 apply(force) |
621 have ok: "\<turnstile> \<Delta> ok" by fact |
649 have ok: "\<turnstile> \<Delta> ok" by fact |
622 have extends: "\<Delta> extends \<Gamma>" by fact |
650 have extends: "\<Delta> extends \<Gamma>" by fact |
623 have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb) |
651 have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb) |
624 moreover |
652 moreover |
625 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
653 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
626 ultimately show "\<Delta> \<turnstile> TVar X <: T" using ok by force |
654 ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force |
627 next |
655 next |
628 case (S_Refl \<Gamma> X) |
656 case (S_Refl \<Gamma> X) |
629 have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
657 have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
630 have "\<turnstile> \<Delta> ok" by fact |
658 have "\<turnstile> \<Delta> ok" by fact |
631 moreover |
659 moreover |
632 have "\<Delta> extends \<Gamma>" by fact |
660 have "\<Delta> extends \<Gamma>" by fact |
633 hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
661 hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
634 ultimately show "\<Delta> \<turnstile> TVar X <: TVar X" by force |
662 ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force |
635 next |
663 next |
636 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 |
664 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 |
637 next |
665 next |
638 case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
666 case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
639 have fresh_cond: "X\<sharp>\<Delta>" by fact |
667 have fresh_cond: "X\<sharp>\<Delta>" by fact |
648 moreover |
676 moreover |
649 have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def) |
677 have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def) |
650 ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp |
678 ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp |
651 moreover |
679 moreover |
652 have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp |
680 have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp |
653 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) |
681 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) |
654 qed |
682 qed |
655 |
683 |
656 text {* In fact all "non-binding" cases can be solved automatically: *} |
684 text {* In fact all "non-binding" cases can be solved automatically: *} |
657 |
685 |
658 lemma weakening: |
686 lemma weakening: |
659 assumes a: "\<Gamma> \<turnstile> S <: T" |
687 assumes a: "\<Gamma> \<turnstile> S <: T" |
660 and b: "\<turnstile> \<Delta> ok" |
688 and b: "\<turnstile> \<Delta> ok" |
661 and c: "\<Delta> extends \<Gamma>" |
689 and c: "\<Delta> extends \<Gamma>" |
662 shows "\<Delta> \<turnstile> S <: T" |
690 shows "\<Delta> \<turnstile> S <: T" |
663 using a b c |
691 using a b c |
664 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_rel_induct) |
692 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct) |
665 case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
693 case (S_All \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
666 have fresh_cond: "X\<sharp>\<Delta>" by fact |
694 have fresh_cond: "X\<sharp>\<Delta>" by fact |
667 have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
695 have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
668 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 |
696 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 |
669 have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
697 have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
720 --{* Now proceed by the inner induction on the left-hand derivation *} |
748 --{* Now proceed by the inner induction on the left-hand derivation *} |
721 fix \<Gamma>' S' T |
749 fix \<Gamma>' S' T |
722 assume a: "\<Gamma>' \<turnstile> S' <: Q" --{* lh derivation *} |
750 assume a: "\<Gamma>' \<turnstile> S' <: Q" --{* lh derivation *} |
723 assume b: "\<Gamma>' \<turnstile> Q <: T" --{* rh derivation *} |
751 assume b: "\<Gamma>' \<turnstile> Q <: T" --{* rh derivation *} |
724 from a b show "\<Gamma>' \<turnstile> S' <: T" |
752 from a b show "\<Gamma>' \<turnstile> S' <: T" |
725 proof(nominal_induct \<Gamma>' S' Q\<equiv>Q avoiding: \<Gamma>' S' T rule: subtype_of_rel_induct) |
753 proof(nominal_induct \<Gamma>' S' Q\<equiv>Q avoiding: \<Gamma>' S' T rule: subtype_of_induct) |
726 case (S_Top \<Gamma> S) |
754 case (S_Top \<Gamma> S) |
727 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S <: Top"} *} |
755 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S <: Top"} *} |
728 hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp |
756 hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp |
729 hence T_inst: "T = Top" by (simp add: S_TopE) |
757 hence T_inst: "T = Top" by (simp add: S_TopE) |
730 have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact |
758 have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact |
731 have lh_drv_prm2: "S closed_in \<Gamma>" by fact |
759 have lh_drv_prm2: "S closed_in \<Gamma>" by fact |
732 from lh_drv_prm1 lh_drv_prm2 have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top) |
760 from lh_drv_prm1 lh_drv_prm2 have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top) |
733 thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp |
761 thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp |
734 next |
762 next |
735 case (S_Var \<Gamma> Y U Q) |
763 case (S_Var \<Gamma> Y U Q) |
736 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar(Y) <: Q"} *} |
764 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> Tvar(Y) <: Q"} *} |
737 hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp |
765 hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp |
738 have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact |
766 have lh_drv_prm1: "\<turnstile> \<Gamma> ok" by fact |
739 have lh_drv_prm2: "(Y,U)\<in>set \<Gamma>" by fact |
767 have lh_drv_prm2: "(Y,U)\<in>set \<Gamma>" by fact |
740 from IH_inner show "\<Gamma> \<turnstile> TVar Y <: T" using lh_drv_prm1 lh_drv_prm2 |
768 from IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" using lh_drv_prm1 lh_drv_prm2 |
741 by (simp add: subtype_of_rel.S_Var) |
769 by (simp add: subtype_of.S_Var) |
742 next |
770 next |
743 case (S_Refl \<Gamma> X) |
771 case (S_Refl \<Gamma> X) |
744 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> TVar X <: TVar X"} *} |
772 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> Tvar X <: Tvar X"} *} |
745 thus "\<Gamma> \<turnstile> TVar X <: T" by simp |
773 thus "\<Gamma> \<turnstile> Tvar X <: T" by simp |
746 next |
774 next |
747 case (S_Arrow \<Gamma> S1 S2 Q1 Q2) |
775 case (S_Arrow \<Gamma> S1 S2 Q1 Q2) |
748 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: Q1 \<rightarrow> Q2"} *} |
776 --{* in this case lh drv is @{term "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: Q1 \<rightarrow> Q2"} *} |
749 hence rh_drv: "\<Gamma> \<turnstile> Q1 \<rightarrow> Q2 <: T" by simp |
777 hence rh_drv: "\<Gamma> \<turnstile> Q1 \<rightarrow> Q2 <: T" by simp |
750 have Q_inst: "Q1 \<rightarrow> Q2 = Q" by fact |
778 have Q_inst: "Q1 \<rightarrow> Q2 = Q" by fact |
819 proof - |
847 proof - |
820 fix \<Delta>' \<Gamma>' X M N P |
848 fix \<Delta>' \<Gamma>' X M N P |
821 assume a: "(\<Delta>'@[(X,Q)]@\<Gamma>') \<turnstile> M <: N" |
849 assume a: "(\<Delta>'@[(X,Q)]@\<Gamma>') \<turnstile> M <: N" |
822 assume b: "\<Gamma>' \<turnstile> P<:Q" |
850 assume b: "\<Gamma>' \<turnstile> P<:Q" |
823 from a b show "(\<Delta>'@[(X,P)]@\<Gamma>') \<turnstile> M <: N" |
851 from a b show "(\<Delta>'@[(X,P)]@\<Gamma>') \<turnstile> M <: N" |
824 proof (nominal_induct \<Gamma>\<equiv>"\<Delta>'@[(X,Q)]@\<Gamma>'" M N avoiding: \<Delta>' \<Gamma>' X rule: subtype_of_rel_induct) |
852 proof (nominal_induct \<Gamma>\<equiv>"\<Delta>'@[(X,Q)]@\<Gamma>'" M N avoiding: \<Delta>' \<Gamma>' X rule: subtype_of_induct) |
825 case (S_Top _ S \<Delta> \<Gamma> X) |
853 case (S_Top _ S \<Delta> \<Gamma> X) |
826 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"} *} |
854 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"} *} |
827 hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
855 hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
828 and lh_drv_prm2: "S closed_in (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
856 and lh_drv_prm2: "S closed_in (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
829 have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
857 have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
830 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
858 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
831 with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
859 with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
832 moreover |
860 moreover |
833 from lh_drv_prm2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: closed_in_def domain_append) |
861 from lh_drv_prm2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: closed_in_def domain_append) |
834 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of_rel.S_Top) |
862 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.S_Top) |
835 next |
863 next |
836 case (S_Var _ Y S N \<Delta> \<Gamma> X) |
864 case (S_Var _ Y S N \<Delta> \<Gamma> X) |
837 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: N"} *} |
865 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} *} |
838 hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N" |
866 hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N" |
839 and lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
867 and lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
840 and lh_drv_prm2: "(Y,S)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
868 and lh_drv_prm2: "(Y,S)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
841 have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
869 have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
842 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
870 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
843 hence cntxt_ok: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" using lh_drv_prm1 by (simp add: replace_type) |
871 hence cntxt_ok: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" using lh_drv_prm1 by (simp add: replace_type) |
844 -- {* we distinguishing the cases @{term "X\<noteq>Y"} and @{term "X=Y"} (the latter |
872 -- {* we distinguishing the cases @{term "X\<noteq>Y"} and @{term "X=Y"} (the latter |
845 being the interesting one) *} |
873 being the interesting one) *} |
846 { assume "X\<noteq>Y" |
874 { assume "X\<noteq>Y" |
847 hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2 by simp |
875 hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm2 by simp |
848 with IH_inner have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N" |
876 with IH_inner have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" |
849 using cntxt_ok by (simp add: subtype_of_rel.S_Var) |
877 using cntxt_ok by (simp add: subtype_of.S_Var) |
850 } |
878 } |
851 moreover |
879 moreover |
852 { have memb_XQ: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp |
880 { have memb_XQ: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp |
853 have memb_XP: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp |
881 have memb_XP: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp |
854 assume "X=Y" |
882 assume "X=Y" |
856 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp |
884 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp |
857 moreover |
885 moreover |
858 have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def) |
886 have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def) |
859 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv cntxt_ok by (simp only: weakening) |
887 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv cntxt_ok by (simp only: weakening) |
860 ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" using transitivity by simp |
888 ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" using transitivity by simp |
861 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar X <: N" using memb_XP cntxt_ok |
889 hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar X <: N" using memb_XP cntxt_ok |
862 by (simp only: subtype_of_rel.S_Var) |
890 by (simp only: subtype_of.S_Var) |
863 } |
891 } |
864 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: N" by blast |
892 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by blast |
865 next |
893 next |
866 case (S_Refl _ Y \<Delta> \<Gamma> X) |
894 case (S_Refl _ Y \<Delta> \<Gamma> X) |
867 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> TVar Y <: TVar Y"} *} |
895 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y"} *} |
868 hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
896 hence lh_drv_prm1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
869 and lh_drv_prm2: "Y \<in> domain (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
897 and lh_drv_prm2: "Y \<in> domain (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
870 have "\<Gamma> \<turnstile> P <: Q" by fact |
898 have "\<Gamma> \<turnstile> P <: Q" by fact |
871 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
899 hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
872 with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
900 with lh_drv_prm1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
873 moreover |
901 moreover |
874 from lh_drv_prm2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append) |
902 from lh_drv_prm2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append) |
875 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> TVar Y <: TVar Y" by (simp add: subtype_of_rel.S_Refl) |
903 ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.S_Refl) |
876 next |
904 next |
877 case (S_Arrow _ Q1 Q2 S1 S2 \<Delta> \<Gamma> X) |
905 case (S_Arrow _ Q1 Q2 S1 S2 \<Delta> \<Gamma> X) |
878 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2"} *} |
906 --{* in this case lh drv is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2"} *} |
879 thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2" by blast |
907 thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q1 \<rightarrow> Q2 <: S1 \<rightarrow> S2" by blast |
880 next |
908 next |