|
1 theory fsub |
|
2 imports nominal |
|
3 begin |
|
4 |
|
5 atom_decl tyvrs vrs |
|
6 |
|
7 section {* Types *} |
|
8 |
|
9 nominal_datatype ty = TyVar "tyvrs" |
|
10 | Top |
|
11 | Arrow "ty" "ty" ("_ \<rightarrow> _" [900,900] 900) |
|
12 | TAll "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" |
|
13 |
|
14 syntax |
|
15 TAll_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall> [_<:_]._" [900,900,900] 900) |
|
16 translations |
|
17 "(\<forall>[a<:ty1].ty2)" \<rightleftharpoons> "TAll a ty2 ty1" |
|
18 |
|
19 section {* typing contexts and their domains *} |
|
20 |
|
21 types ty_context = "(tyvrs\<times>ty) list" |
|
22 |
|
23 text {* domain of a context --- (the name "dom" is already used elsewhere) *} |
|
24 consts |
|
25 "domain" :: "ty_context \<Rightarrow> tyvrs set" |
|
26 primrec |
|
27 "domain [] = {}" |
|
28 "domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" |
|
29 |
|
30 lemma domain_eqvt: |
|
31 fixes pi::"tyvrs prm" |
|
32 shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" |
|
33 by (induct \<Gamma>, auto simp add: perm_set_def) |
|
34 |
|
35 lemma finite_domain: |
|
36 fixes \<Gamma>::"ty_context" |
|
37 shows "finite (domain \<Gamma>)" |
|
38 by (induct \<Gamma>, auto) |
|
39 |
|
40 lemma domain_inclusion[rule_format]: |
|
41 shows "(X,T)\<in>set \<Gamma> \<longrightarrow> X\<in>(domain \<Gamma>)" |
|
42 by (induct \<Gamma>, auto) |
|
43 |
|
44 lemma domain_existence[rule_format]: |
|
45 shows "X\<in>(domain \<Gamma>) \<longrightarrow> (\<exists>T.(X,T)\<in>set \<Gamma>)" |
|
46 by (induct \<Gamma>, auto) |
|
47 |
|
48 lemma domain_append: |
|
49 shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))" |
|
50 by (induct \<Gamma>, auto) |
|
51 |
|
52 section {* Two functions over types *} |
|
53 |
|
54 text {* they cannot yet be defined conveniently unless we have a recursion combinator *} |
|
55 |
|
56 consts size_ty :: "ty \<Rightarrow> nat" |
|
57 |
|
58 lemma size_ty[simp]: |
|
59 shows "size_ty (TyVar X) = 1" |
|
60 and "size_ty (Top) = 1" |
|
61 and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (t1 \<rightarrow> t2) = m + n + 1" |
|
62 and "\<lbrakk>size_ty t1 = m ; size_ty t2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall> [a<:t1].t2) = m + n + 1" |
|
63 sorry |
|
64 |
|
65 consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" |
|
66 |
|
67 lemma subst_ty[simp]: |
|
68 shows "subst_ty (TyVar X) Y T = (if X=Y then T else (TyVar X))" |
|
69 and "subst_ty Top Y T = Top" |
|
70 and "subst_ty (T1 \<rightarrow> T2) Y T = (subst_ty T1 Y T) \<rightarrow> (subst_ty T2 Y T)" |
|
71 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))" |
|
72 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))" |
|
73 sorry |
|
74 |
|
75 |
|
76 consts subst_ctxt :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" |
|
77 primrec |
|
78 "subst_ctxt [] Y T = []" |
|
79 "subst_ctxt (XT#Xs) Y T = (fst XT, subst_ty (snd XT) Y T)#(subst_ctxt Xs Y T)" |
|
80 |
|
81 |
|
82 text {* valid contexts *} |
|
83 |
|
84 constdefs |
|
85 "closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) |
|
86 "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)" |
|
87 |
|
88 lemma closed_in_def2: |
|
89 shows "(S closed_in \<Gamma>) = ((supp S)\<subseteq>((supp (domain \<Gamma>)):: tyvrs set))" |
|
90 apply(simp add: closed_in_def) |
|
91 apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain]) |
|
92 done |
|
93 |
|
94 lemma closed_in_eqvt: |
|
95 fixes pi::"tyvrs prm" |
|
96 assumes a: "S closed_in \<Gamma>" |
|
97 shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" |
|
98 using a |
|
99 proof (unfold "closed_in_def") |
|
100 assume "supp S \<subseteq> (domain \<Gamma>)" |
|
101 hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)" |
|
102 by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
103 thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))" |
|
104 by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
105 qed |
|
106 |
|
107 consts |
|
108 valid_rel :: "ty_context set" |
|
109 valid_sym :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100) |
|
110 translations |
|
111 "\<turnstile> \<Gamma> ok" \<rightleftharpoons> "\<Gamma> \<in> valid_rel" |
|
112 inductive valid_rel |
|
113 intros |
|
114 v1[intro]: "\<turnstile> [] ok" |
|
115 v2[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>\<Gamma>; T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> ((X,T)#\<Gamma>) ok" |
|
116 |
|
117 lemma valid_eqvt: |
|
118 fixes pi::"tyvrs prm" |
|
119 assumes a: "\<turnstile> \<Gamma> ok" |
|
120 shows "\<turnstile> (pi\<bullet>\<Gamma>) ok" |
|
121 using a |
|
122 proof (induct) |
|
123 case v1 |
|
124 show ?case by force |
|
125 next |
|
126 case (v2 T X \<Gamma>) |
|
127 have a1: "\<turnstile> (pi \<bullet> \<Gamma>) ok" by fact |
|
128 have a2: "X\<sharp>\<Gamma>" by fact |
|
129 have a3: "T closed_in \<Gamma>" by fact |
|
130 show ?case |
|
131 proof (simp, rule valid_rel.v2) |
|
132 show "\<turnstile> (pi \<bullet> \<Gamma>) ok" using a1 by simp |
|
133 next |
|
134 show "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" using a2 by (simp add: pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
135 next |
|
136 show "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" using a3 by (rule closed_in_eqvt) |
|
137 qed |
|
138 qed |
|
139 |
|
140 lemma validE: |
|
141 assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok" |
|
142 shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>\<Gamma> \<and> T closed_in \<Gamma>" |
|
143 using a by (cases, auto) |
|
144 |
|
145 lemma validE_append[rule_format]: |
|
146 shows "\<turnstile> (\<Delta>@\<Gamma>) ok \<longrightarrow> \<turnstile> \<Gamma> ok" |
|
147 by (induct \<Delta>, auto dest: validE) |
|
148 |
|
149 lemma domain_fresh[rule_format]: |
|
150 fixes X::"tyvrs" |
|
151 shows "\<turnstile> \<Gamma> ok \<longrightarrow> (X\<sharp>(domain \<Gamma>) = X\<sharp>\<Gamma>)" |
|
152 apply(induct \<Gamma>) |
|
153 apply(simp add: fresh_list_nil fresh_set_empty) |
|
154 apply(simp add: fresh_list_cons fresh_prod |
|
155 fresh_fin_insert[OF pt_tyvrs_inst, OF at_tyvrs_inst, OF fs_tyvrs_inst, OF finite_domain]) |
|
156 apply(rule impI) |
|
157 apply(clarify) |
|
158 apply(simp add: fresh_prod) |
|
159 apply(drule validE) |
|
160 apply(simp) |
|
161 apply(simp add: closed_in_def2 fresh_def) |
|
162 apply(force) |
|
163 done |
|
164 |
|
165 lemma closed_in_fresh: |
|
166 fixes X::"tyvrs" |
|
167 assumes a1: "S closed_in \<Gamma>" |
|
168 and a2: "X\<sharp>\<Gamma>" |
|
169 and a3: "\<turnstile> \<Gamma> ok" |
|
170 shows "X\<sharp>S" |
|
171 using a1 a2 a3 |
|
172 apply(simp add: closed_in_def2) |
|
173 apply(simp add: domain_fresh[symmetric]) |
|
174 apply(simp add: fresh_def) |
|
175 apply(force) |
|
176 done |
|
177 |
|
178 lemma replace_type[rule_format]: |
|
179 shows "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok \<longrightarrow> S closed_in \<Gamma> \<longrightarrow> \<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok" |
|
180 apply(induct \<Delta>) |
|
181 apply(auto dest!: validE intro!: v2 simp add: fresh_list_append fresh_list_cons fresh_prod) |
|
182 apply(drule validE_append) |
|
183 apply(drule validE) |
|
184 apply(drule_tac S="S" in closed_in_fresh) |
|
185 apply(simp) |
|
186 apply(force)+ |
|
187 apply(simp add: closed_in_def2) |
|
188 apply(simp add: domain_append) |
|
189 done |
|
190 |
|
191 |
|
192 lemma fresh_implies_not_member[rule_format]: |
|
193 fixes \<Gamma>::"ty_context" |
|
194 shows "X\<sharp>\<Gamma> \<longrightarrow> \<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))" |
|
195 apply (induct \<Gamma>) |
|
196 apply (auto dest: validE simp add: fresh_list_cons fresh_prod fresh_atm) |
|
197 done |
|
198 |
|
199 lemma uniqueness_of_ctxt: |
|
200 fixes \<Gamma>::"ty_context" |
|
201 shows "\<turnstile> \<Gamma> ok \<longrightarrow> (X,T)\<in>(set \<Gamma>) \<longrightarrow> (X,S)\<in>(set \<Gamma>) \<longrightarrow> (T = S)" |
|
202 apply (induct \<Gamma>) |
|
203 apply (auto dest!: validE fresh_implies_not_member) |
|
204 done |
|
205 |
|
206 |
|
207 section {* Subtyping *} |
|
208 |
|
209 consts |
|
210 subtype_of_rel :: "(ty_context \<times> ty \<times> ty) set" |
|
211 subtype_of_sym :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [100,100,100] 100) |
|
212 translations |
|
213 "\<Gamma> \<turnstile> S <: T" \<rightleftharpoons> "(\<Gamma>,S,T) \<in> subtype_of_rel" |
|
214 inductive subtype_of_rel |
|
215 intros |
|
216 S_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" |
|
217 S_Var[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; (X,S) \<in> (set \<Gamma>); \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (TyVar X) <: T" |
|
218 S_Refl[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> (domain \<Gamma>)\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> TyVar X <: TyVar X" |
|
219 S_Arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; \<Gamma> \<turnstile> S2 <: T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S1 \<rightarrow> S2) <: (T1 \<rightarrow> T2)" |
|
220 S_All[intro]: "\<lbrakk>\<Gamma> \<turnstile> T1 <: S1; X\<sharp>\<Gamma>; ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2\<rbrakk> |
|
221 \<Longrightarrow> \<Gamma> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
|
222 |
|
223 lemma subtype_implies_closed: |
|
224 assumes a: "\<Gamma> \<turnstile> S <: T" |
|
225 shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" |
|
226 using a |
|
227 proof (induct) |
|
228 case (S_Top S \<Gamma>) |
|
229 have "Top closed_in \<Gamma>" |
|
230 by (simp add: closed_in_def ty.supp) |
|
231 moreover |
|
232 have "S closed_in \<Gamma>" by fact |
|
233 ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp |
|
234 next |
|
235 case (S_Var S T X \<Gamma>) |
|
236 have "(X,S)\<in>set \<Gamma>" by fact |
|
237 hence "X\<in>(domain \<Gamma>)" by (rule domain_inclusion) |
|
238 hence "(TyVar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm) |
|
239 moreover |
|
240 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact |
|
241 hence "T closed_in \<Gamma>" by force |
|
242 ultimately show "(TyVar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp |
|
243 next |
|
244 case S_Refl thus ?case |
|
245 by (simp add: closed_in_def ty.supp supp_atm) |
|
246 next |
|
247 case S_Arrow thus ?case by (force simp add: closed_in_def ty.supp) |
|
248 next |
|
249 case S_All thus ?case by (auto simp add: closed_in_def ty.supp abs_supp) |
|
250 qed |
|
251 |
|
252 text {* completely automated proof *} |
|
253 lemma subtype_implies_closed: |
|
254 assumes a: "\<Gamma> \<turnstile> S <: T" |
|
255 shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" |
|
256 using a |
|
257 apply (induct) |
|
258 apply (auto simp add: closed_in_def ty.supp abs_supp domain_inclusion supp_atm) |
|
259 done |
|
260 |
|
261 lemma subtype_implies_ok: |
|
262 fixes X::"tyvrs" |
|
263 assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
264 shows "\<turnstile> \<Gamma> ok" |
|
265 using a1 by (induct, auto) |
|
266 |
|
267 lemma subtype_implies_fresh: |
|
268 fixes X::"tyvrs" |
|
269 assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
270 and a2: "X\<sharp>\<Gamma>" |
|
271 shows "X\<sharp>(S,T)" |
|
272 proof - |
|
273 from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok) |
|
274 with a2 have b0: "X\<sharp>domain(\<Gamma>)" by (simp add: domain_fresh) |
|
275 from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed) |
|
276 hence b1: "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" |
|
277 and b2: "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: closed_in_def2) |
|
278 thus "X\<sharp>(S,T)" using b0 b1 b2 by (force simp add: supp_prod fresh_def) |
|
279 qed |
|
280 |
|
281 lemma silly_eqvt1: |
|
282 fixes X::"'a::pt_tyvrs" |
|
283 and S::"'b::pt_tyvrs" |
|
284 and pi::"tyvrs prm" |
|
285 shows "(X,S) \<in> set \<Gamma> \<Longrightarrow> (pi\<bullet>X,pi\<bullet>S) \<in> set (pi\<bullet>\<Gamma>)" |
|
286 apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
287 apply(simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
|
288 done |
|
289 |
|
290 lemma silly_eqvt2: |
|
291 fixes X::"tyvrs" |
|
292 and pi::"tyvrs prm" |
|
293 shows "X \<in> (domain \<Gamma>) \<Longrightarrow> (pi\<bullet>X) \<in> (domain (pi\<bullet>\<Gamma>))" |
|
294 apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
295 apply(simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst] ) |
|
296 done |
|
297 |
|
298 lemma subtype_eqvt: |
|
299 fixes pi::"tyvrs prm" |
|
300 shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
|
301 apply(erule subtype_of_rel.induct) |
|
302 apply(force intro: valid_eqvt closed_in_eqvt) |
|
303 (* |
|
304 apply(simp) |
|
305 apply(rule S_Var) |
|
306 apply(rule valid_eqvt) |
|
307 apply(assumption) |
|
308 *) |
|
309 (* FIXME: here *) |
|
310 (* apply(auto intro: closed_in_eqvt valid_eqvt dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) *) |
|
311 apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1) |
|
312 apply(force intro: valid_eqvt silly_eqvt2) |
|
313 apply(force) |
|
314 apply(force intro!: S_All simp add: fresh_prod pt_fresh_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
315 done |
|
316 |
|
317 lemma subtype_of_rel_induct_aux[rule_format]: |
|
318 fixes P :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>'a::fs_tyvrs\<Rightarrow>bool" |
|
319 assumes a: "\<Gamma> \<turnstile> S <: T" |
|
320 and a1: "\<And>x \<Gamma> S. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P \<Gamma> S Top x" |
|
321 and a2: "\<And>x \<Gamma> X S T. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<forall>z. P \<Gamma> S T z) |
|
322 \<Longrightarrow> P \<Gamma> (TyVar X) T x" |
|
323 and a3: "\<And>x \<Gamma> X. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>(domain \<Gamma>) \<Longrightarrow> P \<Gamma> (TyVar X) (TyVar X) x" |
|
324 and a4: "\<And>x \<Gamma> S1 S2 T1 T2. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> |
|
325 (\<forall>z. P \<Gamma> S2 T2 z) \<Longrightarrow> P \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2) x" |
|
326 and a5: "\<And>x \<Gamma> X S1 S2 T1 T2. |
|
327 X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S1,T1) \<Longrightarrow> \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2 |
|
328 \<Longrightarrow> (\<forall>z. P ((X,T1)#\<Gamma>) S2 T2 z) \<Longrightarrow> P \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2) x" |
|
329 shows "\<forall>(pi::tyvrs prm) (x::'a::fs_tyvrs). P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x" |
|
330 using a |
|
331 proof (induct) |
|
332 case (S_Top S \<Gamma>) |
|
333 have b1: "\<turnstile> \<Gamma> ok" by fact |
|
334 have b2: "S closed_in \<Gamma>" by fact |
|
335 show ?case |
|
336 proof (intro strip, simp) |
|
337 fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" |
|
338 from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
|
339 moreover |
|
340 from b2 have "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (rule closed_in_eqvt) |
|
341 ultimately show "P (pi \<bullet> \<Gamma>) (pi \<bullet> S) Top x" by (rule a1) |
|
342 qed |
|
343 next |
|
344 case (S_Var S T X \<Gamma>) |
|
345 have b1: "\<turnstile> \<Gamma> ok" by fact |
|
346 have b2: "(X,S) \<in> set \<Gamma>" by fact |
|
347 have b3: "\<Gamma> \<turnstile> S <: T" by fact |
|
348 have b4: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x" by fact |
|
349 show ?case |
|
350 proof (intro strip, simp) |
|
351 fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" |
|
352 from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
|
353 moreover |
|
354 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]) |
|
355 hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
|
356 moreover |
|
357 from b3 have "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt) |
|
358 moreover |
|
359 from b4 have "\<forall>x. P (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T) x" by simp |
|
360 ultimately |
|
361 show "P (pi\<bullet>\<Gamma>) (TyVar (pi\<bullet>X)) (pi\<bullet>T) x" by (rule a2) |
|
362 qed |
|
363 next |
|
364 case (S_Refl X \<Gamma>) |
|
365 have b1: "\<turnstile> \<Gamma> ok" by fact |
|
366 have b2: "X \<in> domain \<Gamma>" by fact |
|
367 show ?case |
|
368 proof (intro strip, simp) |
|
369 fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" |
|
370 from b1 have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
|
371 moreover |
|
372 from b2 have "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
373 hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst]) |
|
374 ultimately show "P (pi\<bullet>\<Gamma>) (TyVar (pi\<bullet>X)) (TyVar (pi\<bullet>X)) x" by (rule a3) |
|
375 qed |
|
376 next |
|
377 case S_Arrow thus ?case by (simp, auto intro!: a4 subtype_eqvt) |
|
378 next |
|
379 case (S_All S1 S2 T1 T2 X \<Gamma>) |
|
380 have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact |
|
381 have b2: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1) x" by fact |
|
382 have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact |
|
383 have b5: "\<forall>(pi::tyvrs prm) x. P (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2) x" by fact |
|
384 have b3': "X\<sharp>\<Gamma>" by fact |
|
385 have b3'': "X\<sharp>(T1,S1)" using b1 b3' by (rule subtype_implies_fresh) |
|
386 have b3: "X\<sharp>(\<Gamma>,S1,T1)" using b3' b3'' by (simp add: fresh_prod) |
|
387 show ?case |
|
388 proof (intro strip) |
|
389 fix pi::"tyvrs prm" and x::"'a::fs_tyvrs" |
|
390 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)" |
|
391 by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1) |
|
392 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)" |
|
393 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" |
|
394 by (auto simp add: fresh_prod fresh_atm) |
|
395 let ?pi' = "[(C,pi\<bullet>X)]@pi" |
|
396 from b2 have c1: "\<forall>x. P (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>T1) (?pi'\<bullet>S1) x" by simp |
|
397 from b5 have "\<forall>x. P (?pi'\<bullet>((X,T1)#\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" by simp |
|
398 hence "\<forall>x. P ((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" by simp |
|
399 hence c2: "\<forall>x. P ((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2) x" using f1 |
|
400 by (simp only: pt_tyvrs2 calc_atm, simp) |
|
401 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" |
|
402 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
403 with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" |
|
404 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
405 hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp |
|
406 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" |
|
407 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
408 with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" |
|
409 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
410 hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp |
|
411 from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" |
|
412 by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
413 with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" |
|
414 by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
415 hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp |
|
416 from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt) |
|
417 from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt) |
|
418 hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp |
|
419 hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1 |
|
420 by (simp only: pt_tyvrs2 calc_atm, simp) |
|
421 have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod) |
|
422 have main: "P (?pi'\<bullet>\<Gamma>) (\<forall> [C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall> [C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) x" |
|
423 using f7 fnew e1 c1 e2 c2 by (rule a5) |
|
424 have alpha1: "(\<forall> [C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall> [X<:S1].S2))" |
|
425 using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
|
426 have alpha2: "(\<forall> [C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall> [X<:T1].T2))" |
|
427 using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
|
428 show "P (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall> [X<:S1].S2)) (pi\<bullet>(\<forall> [X<:T1].T2)) x" |
|
429 using alpha1 alpha2 f6a main by simp |
|
430 qed |
|
431 qed |
|
432 |
|
433 lemma subtype_of_rel_induct[case_names S_Top S_Var S_Refl S_Arrow S_All]: |
|
434 fixes P :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>'a::fs_tyvrs\<Rightarrow>bool" |
|
435 assumes a: "\<Gamma> \<turnstile> S <: T" |
|
436 and a1: "\<And>x \<Gamma> S. (\<turnstile> \<Gamma> ok) \<Longrightarrow> (S closed_in \<Gamma>) \<Longrightarrow> P \<Gamma> S Top x" |
|
437 and a2: "\<And>x \<Gamma> X S T. (\<turnstile> \<Gamma> ok) \<Longrightarrow> ((X,S)\<in>set \<Gamma>) \<Longrightarrow> (\<Gamma> \<turnstile> S <: T) \<Longrightarrow> (\<forall>z. P \<Gamma> S T z) |
|
438 \<Longrightarrow> P \<Gamma> (TyVar X) T x" |
|
439 and a3: "\<And>x \<Gamma> X. (\<turnstile> \<Gamma> ok) \<Longrightarrow> X\<in>domain \<Gamma> \<Longrightarrow> P \<Gamma> (TyVar X) (TyVar X) x" |
|
440 and a4: "\<And>x \<Gamma> S1 S2 T1 T2. \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> \<Gamma> \<turnstile> S2 <: T2 \<Longrightarrow> |
|
441 (\<forall>z. P \<Gamma> S2 T2 z) \<Longrightarrow> P \<Gamma> (S1 \<rightarrow> S2) (T1 \<rightarrow> T2) x" |
|
442 and a5: "\<And>x \<Gamma> X S1 S2 T1 T2. |
|
443 X\<sharp>x \<Longrightarrow> X\<sharp>(\<Gamma>,S1,T1) \<Longrightarrow> \<Gamma> \<turnstile> T1 <: S1 \<Longrightarrow> (\<forall>z. P \<Gamma> T1 S1 z) \<Longrightarrow> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2 |
|
444 \<Longrightarrow> (\<forall>z. P ((X,T1)#\<Gamma>) S2 T2 z) \<Longrightarrow> P \<Gamma> (\<forall> [X<:S1].S2) (\<forall> [X<:T1].T2) x" |
|
445 shows "P \<Gamma> S T x" |
|
446 using a a1 a2 a3 a4 a5 subtype_of_rel_induct_aux[of "\<Gamma>" "S" "T" "P" "[]" "x", simplified] by force |
|
447 |
|
448 |
|
449 section {* Two proofs for reflexivity of subtyping *} |
|
450 |
|
451 lemma subtype_reflexivity: |
|
452 shows "\<turnstile> \<Gamma> ok \<longrightarrow> T closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T <: T" |
|
453 proof(nominal_induct T rule: ty.induct_unsafe) |
|
454 case (TAll \<Gamma> X T1 T2) |
|
455 have i1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T1 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T1 <: T1" by fact |
|
456 have i2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T2 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T2 <: T2" by fact |
|
457 have f: "X\<sharp>\<Gamma>" by fact |
|
458 show "\<turnstile> \<Gamma> ok \<longrightarrow> (\<forall>[X<:T2].T1) closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" |
|
459 proof (intro strip) |
|
460 assume "(\<forall>[X<:T2].T1) closed_in \<Gamma>" |
|
461 hence b1: "T2 closed_in \<Gamma>" and b2: "T1 closed_in ((X,T2)#\<Gamma>)" |
|
462 by (auto simp add: closed_in_def ty.supp abs_supp) |
|
463 assume c1: "\<turnstile> \<Gamma> ok" |
|
464 hence c2: "\<turnstile> ((X,T2)#\<Gamma>) ok" using b1 f by force |
|
465 have "\<Gamma> \<turnstile> T2 <: T2" using i2 b1 c1 by simp |
|
466 moreover |
|
467 have "((X,T2)#\<Gamma>) \<turnstile> T1 <: T1" using i1 b2 c2 by simp |
|
468 ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" using f by force |
|
469 qed |
|
470 qed (auto simp add: closed_in_def ty.supp supp_atm) |
|
471 |
|
472 lemma subtype_refl: |
|
473 shows "\<turnstile> \<Gamma> ok \<longrightarrow> T closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T <: T" |
|
474 apply(nominal_induct T rule: ty.induct_unsafe) |
|
475 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) |
|
476 (* FIXME: the new induction method from Markus will fix this uglyness *) |
|
477 apply(atomize) |
|
478 apply(drule_tac x="(tyvrs, ty2)#z" in spec) |
|
479 apply(force simp add: closed_in_def) |
|
480 done |
|
481 |
|
482 text {* Inversion lemmas\<dots> *} |
|
483 lemma S_TopE: |
|
484 shows "\<Gamma> \<turnstile> Top <: T \<Longrightarrow> T = Top" |
|
485 apply(ind_cases "\<Gamma> \<turnstile> Top <: T", auto) |
|
486 done |
|
487 |
|
488 lemma S_ArrowE_left: |
|
489 assumes a: "\<Gamma> \<turnstile> S1 \<rightarrow> S2 <: T" |
|
490 shows "T = Top \<or> (\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> \<Gamma> \<turnstile> S2 <: T2)" |
|
491 using a by (cases, auto simp add: ty.inject) |
|
492 |
|
493 lemma S_AllE_left: |
|
494 shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T; X\<sharp>(\<Gamma>,S1)\<rbrakk> |
|
495 \<Longrightarrow> T = Top \<or> (\<exists>T1 T2. T = \<forall>[X<:T1].T2 \<and> \<Gamma> \<turnstile> T1 <: S1 \<and> ((X,T1)#\<Gamma>) \<turnstile> S2 <: T2)" |
|
496 apply(frule subtype_implies_ok) |
|
497 apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S1].S2 <: T") |
|
498 apply(auto simp add: ty.inject alpha) |
|
499 apply(rule_tac x="[(X,Xa)]\<bullet>T2" in exI) |
|
500 (* term *) |
|
501 apply(rule conjI) |
|
502 apply(rule sym) |
|
503 apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
504 apply(rule pt_tyvrs3) |
|
505 apply(simp) |
|
506 apply(rule at_ds5[OF at_tyvrs_inst]) |
|
507 (* 1st conjunct *) |
|
508 apply(rule conjI) |
|
509 apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm) |
|
510 apply(simp add: fresh_prod) |
|
511 apply(drule_tac \<Gamma>="((Xa,T1)#\<Gamma>)" in subtype_implies_closed)+ |
|
512 apply(simp add: closed_in_def) |
|
513 apply(auto simp add: domain_fresh[of "\<Gamma>" "X", symmetric]) |
|
514 apply(simp add: fresh_def) |
|
515 apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*) |
|
516 apply(force) |
|
517 (*A*) |
|
518 apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain]) |
|
519 (* 2nd conjunct *) |
|
520 apply(frule_tac X="X" in subtype_implies_fresh) |
|
521 apply(simp add: fresh_prod) |
|
522 apply(drule_tac X="Xa" in subtype_implies_fresh) |
|
523 apply(assumption) |
|
524 apply(simp add: fresh_prod) |
|
525 apply(drule_tac pi="[(X,Xa)]" in subtype_eqvt) |
|
526 apply(simp add: calc_atm) |
|
527 apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
528 done |
|
529 |
|
530 section {* Type substitution *} |
|
531 |
|
532 lemma subst_ty_fresh[rule_format]: |
|
533 fixes P :: "ty" |
|
534 and X :: "tyvrs" |
|
535 shows "X\<sharp>(T,P) \<longrightarrow> X\<sharp>(subst_ty T Y P)" |
|
536 apply (nominal_induct T rule: ty.induct_unsafe) |
|
537 apply (auto simp add: fresh_prod abs_fresh) |
|
538 done |
|
539 |
|
540 lemma subst_ctxt_fresh[rule_format]: |
|
541 fixes X::"tyvrs" |
|
542 shows "X\<sharp>(\<Gamma>,P) \<longrightarrow> X\<sharp>(subst_ctxt \<Gamma> Y P)" |
|
543 apply (induct \<Gamma>) |
|
544 apply (auto intro: subst_ty_fresh simp add: fresh_prod fresh_list_cons) |
|
545 done |
|
546 |
|
547 (* |
|
548 lemma subst_ctxt_closed: |
|
549 shows "subst_ty b X P closed_in (subst_ctxt \<Delta> X P @ \<Gamma>)" |
|
550 |
|
551 |
|
552 lemma substitution_ok: |
|
553 shows "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>) ok \<longrightarrow> \<Gamma> \<turnstile> P <: Q \<longrightarrow> \<turnstile> ((subst_ctxt \<Delta> X P)@\<Gamma>) ok" |
|
554 apply (induct \<Delta>) |
|
555 apply (auto dest: validE) |
|
556 apply (rule v2) |
|
557 apply assumption |
|
558 apply (drule validE) |
|
559 apply (auto simp add: fresh_list_append) |
|
560 apply (rule subst_ctxt_fresh) |
|
561 apply (simp add: fresh_prod) |
|
562 apply (drule_tac X = "a" in subtype_implies_fresh) |
|
563 apply (simp add: fresh_list_cons) |
|
564 apply (simp add: fresh_prod) |
|
565 apply (simp add: fresh_list_cons) |
|
566 apply (drule validE) |
|
567 |
|
568 done |
|
569 *) |
|
570 |
|
571 (* note: What should nominal induct do if the context is compound? *) |
|
572 (* |
|
573 lemma type_substitution: |
|
574 assumes a0: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> S <: T" |
|
575 shows "\<turnstile> (\<Delta>@(X,Q)#\<Gamma>) ok \<longrightarrow> \<Gamma> \<turnstile> P <: Q |
|
576 \<longrightarrow> ((subst_ctxt \<Delta> X P)@\<Gamma>) \<turnstile> (subst_ty S X P) <: (subst_ty T X P)" |
|
577 using a0 |
|
578 thm subtype_of_rel_induct |
|
579 apply(rule subtype_of_rel_induct[of "\<Delta>@(X,Q)#\<Gamma>" "S" "T" _ "P"]) |
|
580 apply(auto) |
|
581 apply(rule S_Top) |
|
582 defer |
|
583 defer |
|
584 defer |
|
585 apply(rule S_Var) |
|
586 defer |
|
587 defer |
|
588 defer |
|
589 defer |
|
590 apply(rule S_Refl) |
|
591 defer |
|
592 defer |
|
593 |
|
594 |
|
595 apply (nominal_induct \<Delta> X Q \<Gamma> S T rule: subtype_of_rel_induct) |
|
596 *) |
|
597 |
|
598 section {* Weakening *} |
|
599 |
|
600 constdefs |
|
601 extends :: "ty_context \<Rightarrow> ty_context \<Rightarrow> bool" ("_ extends _" [100,100] 100) |
|
602 "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (X,Q)\<in>set \<Gamma> \<longrightarrow> (X,Q)\<in>set \<Delta>" |
|
603 |
|
604 lemma extends_domain: |
|
605 assumes a: "\<Delta> extends \<Gamma>" |
|
606 shows "domain \<Gamma> \<subseteq> domain \<Delta>" |
|
607 using a |
|
608 apply (auto simp add: extends_def) |
|
609 apply (drule domain_existence) |
|
610 apply (force simp add: domain_inclusion) |
|
611 done |
|
612 |
|
613 lemma extends_closed: |
|
614 assumes a1: "T closed_in \<Gamma>" |
|
615 and a2: "\<Delta> extends \<Gamma>" |
|
616 shows "T closed_in \<Delta>" |
|
617 using a1 a2 |
|
618 by (auto dest: extends_domain simp add: closed_in_def) |
|
619 |
|
620 lemma weakening: |
|
621 assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
622 shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" |
|
623 using a1 |
|
624 proof (nominal_induct \<Gamma> S T rule: subtype_of_rel_induct) |
|
625 case (S_Top \<Delta> \<Gamma> S) |
|
626 have lh_drv_prem: "S closed_in \<Gamma>" by fact |
|
627 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: Top" |
|
628 proof (intro strip) |
|
629 assume "\<turnstile> \<Delta> ok" |
|
630 moreover |
|
631 assume "\<Delta> extends \<Gamma>" |
|
632 hence "S closed_in \<Delta>" using lh_drv_prem by (rule_tac extends_closed) |
|
633 ultimately show "\<Delta> \<turnstile> S <: Top" by force |
|
634 qed |
|
635 next |
|
636 case (S_Var \<Delta> \<Gamma> X S T) |
|
637 have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact |
|
638 have ih: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" by fact |
|
639 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> TyVar X <: T" |
|
640 proof (intro strip) |
|
641 assume ok: "\<turnstile> \<Delta> ok" |
|
642 and extends: "\<Delta> extends \<Gamma>" |
|
643 have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp add: extends_def) |
|
644 moreover |
|
645 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
|
646 ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force |
|
647 qed |
|
648 next |
|
649 case (S_Refl \<Delta> \<Gamma> X) |
|
650 have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
|
651 show ?case |
|
652 proof (intro strip) |
|
653 assume "\<turnstile> \<Delta> ok" |
|
654 moreover |
|
655 assume "\<Delta> extends \<Gamma>" |
|
656 hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
|
657 ultimately show "\<Delta> \<turnstile> TyVar X <: TyVar X" by force |
|
658 qed |
|
659 next |
|
660 case S_Arrow thus ?case by force |
|
661 next |
|
662 case (S_All \<Delta> \<Gamma> X S1 S2 T1 T2) |
|
663 have fresh: "X\<sharp>\<Delta>" by fact |
|
664 have ih1: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
|
665 have ih2: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
|
666 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
|
667 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
668 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
|
669 proof (intro strip) |
|
670 assume ok: "\<turnstile> \<Delta> ok" |
|
671 and extends: "\<Delta> extends \<Gamma>" |
|
672 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
|
673 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
|
674 moreover |
|
675 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
|
676 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
|
677 moreover |
|
678 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
|
679 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
|
680 qed |
|
681 qed |
|
682 |
|
683 text {* more automated proof *} |
|
684 |
|
685 lemma weakening: |
|
686 assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
687 shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" |
|
688 using a1 |
|
689 proof (nominal_induct \<Gamma> S T rule: subtype_of_rel_induct) |
|
690 case (S_Top \<Delta> \<Gamma> S) thus ?case by (force intro: extends_closed) |
|
691 next |
|
692 case (S_Var \<Delta> \<Gamma> X S T) thus ?case by (force simp add: extends_def) |
|
693 next |
|
694 case (S_Refl \<Delta> \<Gamma> X) thus ?case by (force dest: extends_domain) |
|
695 next |
|
696 case S_Arrow thus ?case by force |
|
697 next |
|
698 case (S_All \<Delta> \<Gamma> X S1 S2 T1 T2) |
|
699 have fresh: "X\<sharp>\<Delta>" by fact |
|
700 have ih1: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
|
701 have ih2: "\<forall>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
|
702 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
|
703 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
704 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
|
705 proof (intro strip) |
|
706 assume ok: "\<turnstile> \<Delta> ok" |
|
707 and extends: "\<Delta> extends \<Gamma>" |
|
708 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
|
709 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
|
710 moreover |
|
711 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
|
712 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
|
713 moreover |
|
714 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
|
715 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
|
716 qed |
|
717 qed |
|
718 |
|
719 (* helper lemma to calculate the measure of the induction *) |
|
720 lemma measure_eq [simp]: "(x, y) \<in> measure f = (f x < f y)" |
|
721 by (simp add: measure_def inv_image_def) |
|
722 |
|
723 (* HERE *) |
|
724 |
|
725 |
|
726 lemma transitivity_and_narrowing: |
|
727 "(\<forall>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<longrightarrow> \<Gamma> \<turnstile> Q <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T) \<and> |
|
728 (\<forall>\<Delta> \<Gamma> X P M N. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<longrightarrow> \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
|
729 proof (rule wf_induct [of "measure size_ty" _ Q, rule_format]) |
|
730 show "wf (measure size_ty)" by simp |
|
731 next |
|
732 case (goal2 Q) |
|
733 note IH1_outer = goal2[THEN conjunct1] |
|
734 and IH2_outer = goal2[THEN conjunct2, THEN spec, of _ "[]", simplified] |
|
735 (* CHECK: Not clear whether the condition size_ty Q = size_ty Q' is needed, or whether |
|
736 just doing it for Q'=Q is enough *) |
|
737 have transitivity: |
|
738 "\<And>\<Gamma> S Q' T. \<Gamma> \<turnstile> S <: Q' \<Longrightarrow> size_ty Q = size_ty Q' \<longrightarrow> \<Gamma> \<turnstile> Q' <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T" |
|
739 proof - |
|
740 |
|
741 (* We first handle the case where T = Top once and for all; this saves some |
|
742 repeated argument below (just like on paper :-). We establish a little lemma |
|
743 that is invoked where needed in each case of the induction. *) |
|
744 have top_case: |
|
745 "\<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'" |
|
746 proof - |
|
747 fix \<Gamma> S T' P |
|
748 assume S_Top_prem1: "S closed_in \<Gamma>" |
|
749 and S_Top_prem2: "\<turnstile> \<Gamma> ok" |
|
750 and alternative: "P \<longrightarrow> \<Gamma> \<turnstile> S <: T'" |
|
751 and "T'=Top \<or> P" |
|
752 moreover |
|
753 { assume "T'=Top" |
|
754 hence "\<Gamma> \<turnstile> S <: T'" using S_Top_prem1 S_Top_prem2 by (simp add: S_Top) |
|
755 } |
|
756 moreover |
|
757 { assume P |
|
758 with alternative have "\<Gamma> \<turnstile> S <: T'" by simp |
|
759 } |
|
760 ultimately show "\<Gamma> \<turnstile> S <: T'" by blast |
|
761 qed |
|
762 |
|
763 (* Now proceed by induction on the left-hand derivation *) |
|
764 fix \<Gamma> S Q' T |
|
765 assume a: "\<Gamma> \<turnstile> S <: Q'" |
|
766 from a show "size_ty Q = size_ty Q' \<longrightarrow> \<Gamma> \<turnstile> Q' <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T" |
|
767 (* FIXME : nominal induct does not work here because Gamma S and Q are fixed variables *) |
|
768 (* FIX: It would be better to use S',\<Gamma>',etc., instead of S1,\<Gamma>1, for consistency, in the cases |
|
769 where these do not refer to sub-phrases of S, etc. *) |
|
770 proof(rule subtype_of_rel_induct[of "\<Gamma>" "S" "Q'" _ "T"]) |
|
771 case (goal1 T' \<Gamma>1 S1) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> S1 <: Top" |
|
772 --"automatic proof: thus ?case proof (auto intro!: S_Top dest: S_TopE)" |
|
773 assume lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" |
|
774 and lh_drv_prem2: "S1 closed_in \<Gamma>1" |
|
775 show "size_ty Q = size_ty Top \<longrightarrow> \<Gamma>1 \<turnstile> Top <: T' \<longrightarrow> \<Gamma>1 \<turnstile> S1 <: T'" |
|
776 proof (intro strip) |
|
777 assume "\<Gamma>1 \<turnstile> Top <: T'" --"rh drv." |
|
778 hence "T' = Top" by (rule S_TopE) |
|
779 thus "\<Gamma>1 \<turnstile> S1 <: T'" using top_case[of "\<Gamma>1" "S1" "False" "T'"] lh_drv_prem1 lh_drv_prem2 |
|
780 by simp |
|
781 qed |
|
782 next |
|
783 case (goal2 T' \<Gamma>1 X1 S1 T1) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1" |
|
784 --"automatic proof: thus ?case proof (auto intro!: S_Var)" |
|
785 have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact |
|
786 have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact |
|
787 have IH_inner: "\<forall>T. size_ty Q = size_ty T1 \<longrightarrow> \<Gamma>1 \<turnstile> T1 <: T \<longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact |
|
788 show "size_ty Q = size_ty T1 \<longrightarrow> \<Gamma>1 \<turnstile> T1 <: T' \<longrightarrow> \<Gamma>1 \<turnstile> TyVar X1 <: T'" |
|
789 proof (intro strip) |
|
790 assume "\<Gamma>1 \<turnstile> T1 <: T'" --"right-hand drv." |
|
791 and "size_ty Q = size_ty T1" |
|
792 with IH_inner have "\<Gamma>1 \<turnstile> S1 <: T'" by simp |
|
793 thus "\<Gamma>1 \<turnstile> TyVar X1 <: T'" using lh_drv_prem1 lh_drv_prem2 by (simp add: S_Var) |
|
794 qed |
|
795 next |
|
796 case goal3 --"S_Refl case" show ?case by simp |
|
797 next |
|
798 case (goal4 T' \<Gamma>1 S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q' == \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2" |
|
799 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
|
800 have lh_drv_prem2: "\<Gamma>1 \<turnstile> S2 <: T2" by fact |
|
801 show "size_ty Q = size_ty (T1 \<rightarrow> T2) \<longrightarrow> \<Gamma>1 \<turnstile> T1 \<rightarrow> T2 <: T' \<longrightarrow> \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T'" |
|
802 proof (intro strip) |
|
803 assume measure: "size_ty Q = size_ty (T1 \<rightarrow> T2)" |
|
804 and rh_deriv: "\<Gamma>1 \<turnstile> T1 \<rightarrow> T2 <: T'" |
|
805 have "S1 closed_in \<Gamma>1" and "S2 closed_in \<Gamma>1" |
|
806 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
|
807 hence "(S1 \<rightarrow> S2) closed_in \<Gamma>1" by (simp add: closed_in_def ty.supp) |
|
808 moreover |
|
809 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
|
810 moreover |
|
811 have "T' = Top \<or> (\<exists>T3 T4. T'= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4)" |
|
812 using rh_deriv by (rule S_ArrowE_left) |
|
813 moreover |
|
814 { assume "\<exists>T3 T4. T'= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4" |
|
815 then obtain T3 T4 |
|
816 where T'_inst: "T'= T3 \<rightarrow> T4" |
|
817 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
|
818 and rh_drv_prem2: "\<Gamma>1 \<turnstile> T2 <: T4" by force |
|
819 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
|
820 using measure rh_drv_prem1 lh_drv_prem1 by (force simp add: ty.inject) |
|
821 moreover |
|
822 from IH1_outer[of "T2"] have "\<Gamma>1 \<turnstile> S2 <: T4" |
|
823 using measure rh_drv_prem2 lh_drv_prem2 by (force simp add: ty.inject) |
|
824 ultimately have "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T'" using T'_inst by force |
|
825 } |
|
826 ultimately show "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T'" using top_case[of "\<Gamma>1" "S1\<rightarrow>S2" _ "T'"] by blast |
|
827 qed |
|
828 next |
|
829 case (goal5 T' \<Gamma>1 X S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> \<forall>[X:S1].S2 <: \<forall>[X:T1].T2" |
|
830 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
|
831 have lh_drv_prem2: "((X,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact |
|
832 have fresh_cond: "X\<sharp>(\<Gamma>1,S1,T1)" by fact |
|
833 show "size_ty Q = size_ty (\<forall>[X<:T1].T2) \<longrightarrow> \<Gamma>1 \<turnstile> \<forall>[X<:T1].T2 <: T' \<longrightarrow> \<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" |
|
834 proof (intro strip) |
|
835 assume measure: "size_ty Q = size_ty (\<forall>[X<:T1].T2)" |
|
836 and rh_deriv: "\<Gamma>1 \<turnstile> \<forall>[X<:T1].T2 <: T'" |
|
837 have "S1 closed_in \<Gamma>1" and "S2 closed_in ((X,T1)#\<Gamma>1)" |
|
838 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
|
839 hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>1" by (force simp add: closed_in_def ty.supp abs_supp) |
|
840 moreover |
|
841 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
|
842 moreover |
|
843 (* FIX: Maybe T3,T4 could be T1',T2' *) |
|
844 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)" |
|
845 using rh_deriv fresh_cond by (auto dest: S_AllE_left simp add: fresh_prod) |
|
846 moreover |
|
847 { assume "\<exists>T3 T4. T'=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" |
|
848 then obtain T3 T4 |
|
849 where T'_inst: "T'= \<forall>[X<:T3].T4" |
|
850 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
|
851 and rh_drv_prem2:"((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" by force |
|
852 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
|
853 using lh_drv_prem1 rh_drv_prem1 measure by (force simp add: ty.inject) |
|
854 moreover |
|
855 from IH2_outer[of "T1"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T2" |
|
856 using measure lh_drv_prem2 rh_drv_prem1 by force |
|
857 with IH1_outer[of "T2"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T4" |
|
858 using measure rh_drv_prem2 by force |
|
859 moreover |
|
860 ultimately have "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" |
|
861 using fresh_cond T'_inst by (simp add: fresh_prod S_All) |
|
862 } |
|
863 ultimately show "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" using top_case[of "\<Gamma>1" "\<forall>[X<:S1].S2" _ "T'"] by blast |
|
864 qed |
|
865 qed |
|
866 qed |
|
867 |
|
868 (* test |
|
869 have narrowing: |
|
870 "\<And>\<Delta> \<Gamma> X M N. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P<:Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
|
871 proof - |
|
872 fix \<Delta> \<Gamma> X M N |
|
873 assume a: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N" |
|
874 thus "\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N" |
|
875 thm subtype_of_rel_induct |
|
876 thm subtype_of_rel.induct |
|
877 using a proof (induct) |
|
878 using a proof (induct rule: subtype_of_rel_induct[of "\<Delta>@(X,Q)#\<Gamma>" "M" "N" _ "()"]) |
|
879 *) |
|
880 |
|
881 have narrowing: |
|
882 "\<And>\<Delta> \<Gamma> \<Gamma>' X M N. \<Gamma>' \<turnstile> M <: N \<Longrightarrow> \<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P<:Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
|
883 proof - |
|
884 fix \<Delta> \<Gamma> \<Gamma>' X M N |
|
885 assume "\<Gamma>' \<turnstile> M <: N" |
|
886 thus "\<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
|
887 (* FIXME : nominal induct does not work here because Gamma' M and N are fixed variables *) |
|
888 (* FIX: Same comment about S1,\<Gamma>1 *) |
|
889 proof (rule subtype_of_rel_induct[of "\<Gamma>'" "M" "N" "\<lambda>\<Gamma>' M N (\<Delta>,\<Gamma>,X). |
|
890 \<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" "(\<Delta>,\<Gamma>,X)", simplified], |
|
891 simp_all only: split_paired_all split_conv) |
|
892 case (goal1 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 S1) |
|
893 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |
|
894 have lh_drv_prem2: "S1 closed_in \<Gamma>2" by fact |
|
895 show "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1 \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: Top)" |
|
896 proof (intro strip) |
|
897 fix P |
|
898 assume a1: "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1" |
|
899 assume a2: "\<Gamma>1 \<turnstile> P <: Q" |
|
900 from a2 have "P closed_in \<Gamma>1" by (simp add: subtype_implies_closed) |
|
901 hence a3: "\<turnstile> (\<Delta>1@(X1,P)#\<Gamma>1) ok" using lh_drv_prem1 a1 by (rule_tac replace_type, simp_all) |
|
902 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: Top" |
|
903 using a1 a3 lh_drv_prem2 by (force simp add: closed_in_def domain_append) |
|
904 qed |
|
905 next |
|
906 case (goal2 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 X2 S1 T1) |
|
907 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |
|
908 have lh_drv_prem2: "(X2,S1)\<in>set \<Gamma>2" by fact |
|
909 have lh_drv_prem3: "\<Gamma>2 \<turnstile> S1 <: T1" by fact |
|
910 have IH_inner: |
|
911 "\<forall>\<Delta>1 \<Gamma>1 X1. \<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1 \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: T1)" by fact |
|
912 show "\<Gamma>2 = (\<Delta>1@(X1,Q)#\<Gamma>1) \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: T1)" |
|
913 proof (intro strip) |
|
914 fix P |
|
915 assume a1: "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1" |
|
916 and a2: "\<Gamma>1 \<turnstile> P <: Q" |
|
917 from a2 have "P closed_in \<Gamma>1" by (simp add: subtype_implies_closed) |
|
918 hence a3: "\<turnstile> (\<Delta>1@(X1,P)#\<Gamma>1) ok" |
|
919 using lh_drv_prem1 a1 by (rule_tac replace_type, simp_all) |
|
920 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: T1" |
|
921 proof (cases "X1=X2") |
|
922 case False |
|
923 have b0: "X1\<noteq>X2" by fact |
|
924 from lh_drv_prem3 a1 a2 IH_inner |
|
925 have b1: "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: T1" by simp |
|
926 from lh_drv_prem2 a1 b0 have b2: "(X2,S1)\<in>set (\<Delta>1@(X1,P)#\<Gamma>1)" by simp |
|
927 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: T1" using a3 b2 b1 by (rule S_Var) |
|
928 next |
|
929 case True |
|
930 have b0: "X1=X2" by fact |
|
931 have a4: "S1=Q" |
|
932 proof - |
|
933 have c0: "(X2,Q)\<in>set \<Gamma>2" using b0 a1 by simp |
|
934 with lh_drv_prem1 lh_drv_prem2 show "S1=Q" by (simp add: uniqueness_of_ctxt) |
|
935 qed |
|
936 have a5: "(\<Delta>1@(X1,P)#\<Gamma>1) extends \<Gamma>1" by (force simp add: extends_def) |
|
937 have a6: "(\<Delta>1@(X2,P)#\<Gamma>1) \<turnstile> P <: Q" using b0 a5 a2 a3 by (simp add: weakening) |
|
938 have a7: "(\<Delta>1@(X2,P)#\<Gamma>1) \<turnstile> Q <: T1" using b0 IH_inner a1 lh_drv_prem3 a2 a4 by simp |
|
939 have a8: "(\<Delta>1@(X2,P)#\<Gamma>1) \<turnstile> P <: T1" using a6 a7 transitivity by blast |
|
940 have a9: "(X2,P)\<in>set (\<Delta>1@(X1,P)#\<Gamma>1)" using b0 by simp |
|
941 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: T1" using a3 b0 a8 a9 by (force simp add: S_Var) |
|
942 qed |
|
943 qed |
|
944 next |
|
945 case (goal3 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 X2) |
|
946 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |
|
947 have lh_drv_prem2: "X2 \<in> domain \<Gamma>2" by fact |
|
948 show "\<Gamma>2 = (\<Delta>1@(X1,Q)#\<Gamma>1) \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: TyVar X2)" |
|
949 proof (intro strip) |
|
950 fix P |
|
951 assume a1: "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1" |
|
952 and a2: "\<Gamma>1 \<turnstile> P <: Q" |
|
953 from a2 have "P closed_in \<Gamma>1" by (simp add: subtype_implies_closed) |
|
954 hence a3: "\<turnstile> (\<Delta>1@(X1,P)#\<Gamma>1) ok" |
|
955 using lh_drv_prem1 a1 by (rule_tac replace_type, simp_all) |
|
956 have b0: "X2 \<in> domain (\<Delta>1@(X1,P)#\<Gamma>1)" using lh_drv_prem2 a1 by (simp add: domain_append) |
|
957 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> TyVar X2 <: TyVar X2" using a3 b0 by (rule S_Refl) |
|
958 qed |
|
959 next |
|
960 case goal4 thus ?case by blast |
|
961 next |
|
962 case (goal5 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 X2 S1 S2 T1 T2) |
|
963 have IH_inner1: |
|
964 "\<forall>\<Delta>1 \<Gamma>1 X1. \<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1 \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> T1 <: S1)" by fact |
|
965 have IH_inner2: |
|
966 "\<forall>\<Delta>1 \<Gamma>1 X1. (X2,T1)#\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1 \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S2 <: T2)" |
|
967 by fact |
|
968 have lh_drv_prem1: "\<Gamma>2 \<turnstile> T1 <: S1" by fact |
|
969 have lh_drv_prem2: "X2 \<sharp> (\<Gamma>2,S1, T1)" by fact |
|
970 have lh_drv_prem3: "((X2,T1) # \<Gamma>2) \<turnstile> S2 <: T2" by fact |
|
971 have freshness: "X2\<sharp>(\<Delta>1, \<Gamma>1, X1)" by fact |
|
972 show "\<Gamma>2 = (\<Delta>1@(X1,Q)#\<Gamma>1) \<longrightarrow> |
|
973 (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> \<forall> [X2<:S1].S2 <: \<forall> [X2<:T1].T2)" |
|
974 proof (intro strip) |
|
975 fix P |
|
976 assume a1: "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1" |
|
977 and a2: "\<Gamma>1 \<turnstile> P <: Q" |
|
978 have b0: "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> T1 <: S1" using a1 a2 lh_drv_prem1 IH_inner1 by simp |
|
979 have b1: "(((X2,T1)#\<Delta>1)@(X1,P)#\<Gamma>1) \<turnstile> S2 <: T2" using a1 a2 lh_drv_prem3 IH_inner2 |
|
980 apply auto |
|
981 apply (drule_tac x="(X2,T1)#\<Delta>1" in spec) |
|
982 apply(simp) |
|
983 done |
|
984 have b3: "X2\<sharp>(\<Delta>1@(X1,P)#\<Gamma>1)" using lh_drv_prem2 freshness a2 |
|
985 by (auto simp add: fresh_prod fresh_list_append fresh_list_cons dest: subtype_implies_fresh) |
|
986 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> \<forall> [X2<:S1].S2 <: \<forall> [X2<:T1].T2" using b0 b3 b1 by force |
|
987 qed |
|
988 qed |
|
989 qed |
|
990 from transitivity narrowing show ?case by blast |
|
991 qed |
|
992 |
|
993 |
|
994 |
|
995 section {* Terms *} |
|
996 |
|
997 nominal_datatype trm = Var "vrs" |
|
998 | Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty" |
|
999 | TAbs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty" |
|
1000 | App "trm" "trm" |
|
1001 | TApp "trm" "ty" |
|
1002 |
|
1003 consts |
|
1004 Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100) |
|
1005 TAbs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("TAbs [_<:_]._" [100,100,100] 100) |
|
1006 translations |
|
1007 "Lam [a:tys].t" \<rightleftharpoons> "trm.Lam a t tys" |
|
1008 "TAbs [a<:tys].t" \<rightleftharpoons> "trm.TAbs a t tys" |
|
1009 |