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