author | wenzelm |
Mon, 11 Sep 2006 21:35:19 +0200 | |
changeset 20503 | 503ac4c5ef91 |
parent 20399 | c4450e8967aa |
child 21087 | 3e56528a39f7 |
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 |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
3 |
(*<*) |
19501 | 4 |
theory Fsub |
5 |
imports "../Nominal" |
|
18269 | 6 |
begin |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
7 |
(*>*) |
18269 | 8 |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
9 |
text{* Authors: Christian Urban, |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
10 |
Benjamin Pierce, |
18650 | 11 |
Dimitrios Vytiniotis |
12 |
Stephanie Weirich and |
|
13 |
Steve Zdancewic |
|
18266
55c201fe4c95
added an authors section (please let me know if somebody is left out or unhappy)
urbanc
parents:
18263
diff
changeset
|
14 |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
15 |
with great help from Stefan Berghofer and Markus Wenzel. *} |
18246 | 16 |
|
18621 | 17 |
section {* Types for Names, Nominal Datatype Declaration for Types and Terms *} |
18424 | 18 |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
19 |
text {* The main point of this solution is to use names everywhere (be they bound, |
18621 | 20 |
binding or free). In System \FSUB{} there are two kinds of names corresponding to |
21 |
type-variables and to term-variables. These two kinds of names are represented in |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
22 |
the nominal datatype package as atom-types @{text "tyvrs"} and @{text "vrs"}: *} |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
23 |
|
18246 | 24 |
atom_decl tyvrs vrs |
25 |
||
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
26 |
text{* There are numerous facts that come with this declaration: for example that |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
27 |
there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *} |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
28 |
|
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
29 |
text{* The constructors for types and terms in System \FSUB{} contain abstractions |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
30 |
over type-variables and term-variables. The nominal datatype-package uses |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
31 |
@{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *} |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
32 |
|
18424 | 33 |
nominal_datatype ty = |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
34 |
Tvar "tyvrs" |
18424 | 35 |
| Top |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
36 |
| Arrow "ty" "ty" ("_ \<rightarrow> _" [100,100] 100) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
37 |
| Forall "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" |
18246 | 38 |
|
18424 | 39 |
nominal_datatype trm = |
40 |
Var "vrs" |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
41 |
| Lam "\<guillemotleft>vrs\<guillemotright>trm" "ty" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
42 |
| Tabs "\<guillemotleft>tyvrs\<guillemotright>trm" "ty" |
18424 | 43 |
| App "trm" "trm" |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
44 |
| Tapp "trm" "ty" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
45 |
|
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
46 |
text {* To be polite to the eye, some more familiar notation is introduced. |
18621 | 47 |
Because of the change in the order of arguments, one needs to use |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
48 |
translation rules, instead of syntax annotations at the term-constructors |
18650 | 49 |
as given above for @{term "Arrow"}. *} |
18246 | 50 |
|
51 |
syntax |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
52 |
Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<forall>[_<:_]._" [100,100,100] 100) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
53 |
Lam_syn :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
54 |
Tabs_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Tabs [_<:_]._" [100,100,100] 100) |
18424 | 55 |
|
18246 | 56 |
translations |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
57 |
"\<forall>[X<:T\<^isub>1].T\<^isub>2" \<rightleftharpoons> "ty.Forall X T\<^isub>2 T\<^isub>1" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
58 |
"Lam [x:T].t" \<rightleftharpoons> "trm.Lam x t T" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
59 |
"Tabs [X<:T].t" \<rightleftharpoons> "trm.Tabs X t T" |
18246 | 60 |
|
18621 | 61 |
text {* Again there are numerous facts that are proved automatically for @{typ "ty"} |
18650 | 62 |
and @{typ "trm"}: for example that the set of free variables, i.e.~the @{text "support"}, |
63 |
is finite. However note that nominal-datatype declarations do \emph{not} define |
|
64 |
``classical" constructor-based datatypes, but rather define $\alpha$-equivalence |
|
18621 | 65 |
classes---we can for example show that $\alpha$-equivalent @{typ "ty"}s |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
66 |
and @{typ "trm"}s are equal: *} |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
67 |
|
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
68 |
lemma alpha_illustration: |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
69 |
shows "\<forall>[X<:T].(Tvar X) = \<forall>[Y<:T].(Tvar Y)" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
70 |
and "Lam [x:T].(Var x) = Lam [y:T].(Var y)" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
71 |
by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
72 |
|
18621 | 73 |
section {* SubTyping Contexts *} |
18246 | 74 |
|
75 |
types ty_context = "(tyvrs\<times>ty) list" |
|
76 |
||
18650 | 77 |
text {* Typing contexts are represented as lists that ``grow" on the left; we |
18621 | 78 |
thereby deviating from the convention in the POPLmark-paper. The lists contain |
18650 | 79 |
pairs of type-variables and types (this is sufficient for Part 1A). *} |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
80 |
|
18628 | 81 |
text {* In order to state validity-conditions for typing-contexts, the notion of |
18621 | 82 |
a @{text "domain"} of a typing-context is handy. *} |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
83 |
|
18246 | 84 |
consts |
85 |
"domain" :: "ty_context \<Rightarrow> tyvrs set" |
|
86 |
primrec |
|
87 |
"domain [] = {}" |
|
88 |
"domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" |
|
89 |
||
90 |
lemma domain_eqvt: |
|
91 |
fixes pi::"tyvrs prm" |
|
92 |
shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" |
|
18655
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
93 |
by (induct \<Gamma>, simp_all add: perm_empty perm_insert perm_fst) |
18246 | 94 |
|
95 |
lemma finite_domain: |
|
96 |
shows "finite (domain \<Gamma>)" |
|
97 |
by (induct \<Gamma>, auto) |
|
98 |
||
18621 | 99 |
lemma domain_supp: |
100 |
shows "(supp (domain \<Gamma>)) = (domain \<Gamma>)" |
|
101 |
by (simp only: at_fin_set_supp at_tyvrs_inst finite_domain) |
|
102 |
||
18424 | 103 |
lemma domain_inclusion: |
104 |
assumes a: "(X,T)\<in>set \<Gamma>" |
|
105 |
shows "X\<in>(domain \<Gamma>)" |
|
106 |
using a by (induct \<Gamma>, auto) |
|
18246 | 107 |
|
18424 | 108 |
lemma domain_existence: |
109 |
assumes a: "X\<in>(domain \<Gamma>)" |
|
110 |
shows "\<exists>T.(X,T)\<in>set \<Gamma>" |
|
111 |
using a by (induct \<Gamma>, auto) |
|
18246 | 112 |
|
113 |
lemma domain_append: |
|
114 |
shows "domain (\<Gamma>@\<Delta>) = ((domain \<Gamma>) \<union> (domain \<Delta>))" |
|
115 |
by (induct \<Gamma>, auto) |
|
116 |
||
18621 | 117 |
lemma fresh_domain_cons: |
118 |
fixes X::"tyvrs" |
|
119 |
shows "X\<sharp>(domain (Y#\<Gamma>)) = (X\<sharp>(fst Y) \<and> X\<sharp>(domain \<Gamma>))" |
|
120 |
by (simp add: fresh_fin_insert pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst finite_domain) |
|
121 |
||
122 |
lemma fresh_domain: |
|
123 |
fixes X::"tyvrs" |
|
124 |
assumes a: "X\<sharp>\<Gamma>" |
|
125 |
shows "X\<sharp>(domain \<Gamma>)" |
|
126 |
using a |
|
127 |
apply(induct \<Gamma>) |
|
128 |
apply(simp add: fresh_set_empty) |
|
129 |
apply(simp only: fresh_domain_cons) |
|
130 |
apply(auto simp add: fresh_prod fresh_list_cons) |
|
131 |
done |
|
132 |
||
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
133 |
text {* Not all lists of type @{typ "ty_context"} are well-formed. One condition |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
134 |
requires that in @{term "(X,S)#\<Gamma>"} all free variables of @{term "S"} must be |
18621 | 135 |
in the @{term "domain"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"} |
18650 | 136 |
in @{term "\<Gamma>"}. The set of free variables of @{term "S"} is the |
18621 | 137 |
@{text "support"} of @{term "S"}. *} |
18246 | 138 |
|
139 |
constdefs |
|
140 |
"closed_in" :: "ty \<Rightarrow> ty_context \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) |
|
141 |
"S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(domain \<Gamma>)" |
|
142 |
||
143 |
lemma closed_in_eqvt: |
|
144 |
fixes pi::"tyvrs prm" |
|
145 |
assumes a: "S closed_in \<Gamma>" |
|
146 |
shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" |
|
147 |
using a |
|
148 |
proof (unfold "closed_in_def") |
|
18424 | 149 |
assume "supp S \<subseteq> (domain \<Gamma>)" |
18246 | 150 |
hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)" |
151 |
by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
152 |
thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))" |
|
153 |
by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
154 |
qed |
|
155 |
||
18621 | 156 |
text {* Now validity of a context is a straightforward inductive definition. *} |
157 |
||
18246 | 158 |
consts |
159 |
valid_rel :: "ty_context set" |
|
160 |
valid_sym :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100) |
|
161 |
translations |
|
162 |
"\<turnstile> \<Gamma> ok" \<rightleftharpoons> "\<Gamma> \<in> valid_rel" |
|
163 |
inductive valid_rel |
|
164 |
intros |
|
18621 | 165 |
valid_nil[simp]: "\<turnstile> [] ok" |
166 |
valid_cons[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(domain \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> ((X,T)#\<Gamma>) ok" |
|
18246 | 167 |
|
168 |
lemma valid_eqvt: |
|
169 |
fixes pi::"tyvrs prm" |
|
170 |
assumes a: "\<turnstile> \<Gamma> ok" |
|
171 |
shows "\<turnstile> (pi\<bullet>\<Gamma>) ok" |
|
172 |
using a |
|
173 |
proof (induct) |
|
18621 | 174 |
case valid_nil |
175 |
show "\<turnstile> (pi\<bullet>[]) ok" by simp |
|
18246 | 176 |
next |
18621 | 177 |
case (valid_cons T X \<Gamma>) |
178 |
have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by fact |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
179 |
moreover |
18621 | 180 |
have "X\<sharp>(domain \<Gamma>)" by fact |
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19501
diff
changeset
|
181 |
hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_bij domain_eqvt[symmetric]) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
182 |
moreover |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
183 |
have "T closed_in \<Gamma>" by fact |
18621 | 184 |
hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_eqvt) |
185 |
ultimately show "\<turnstile> (pi\<bullet>((X,T)#\<Gamma>)) ok" by simp |
|
18246 | 186 |
qed |
187 |
||
188 |
lemma validE: |
|
189 |
assumes a: "\<turnstile> ((X,T)#\<Gamma>) ok" |
|
18621 | 190 |
shows "\<turnstile> \<Gamma> ok \<and> X\<sharp>(domain \<Gamma>) \<and> T closed_in \<Gamma>" |
18246 | 191 |
using a by (cases, auto) |
192 |
||
18424 | 193 |
lemma validE_append: |
194 |
assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok" |
|
195 |
shows "\<turnstile> \<Gamma> ok" |
|
196 |
using a by (induct \<Delta>, auto dest: validE) |
|
18246 | 197 |
|
18424 | 198 |
lemma replace_type: |
199 |
assumes a: "\<turnstile> (\<Delta>@(X,T)#\<Gamma>) ok" |
|
200 |
and b: "S closed_in \<Gamma>" |
|
201 |
shows "\<turnstile> (\<Delta>@(X,S)#\<Gamma>) ok" |
|
18621 | 202 |
using a b |
18246 | 203 |
apply(induct \<Delta>) |
18621 | 204 |
apply(auto dest!: validE intro!: valid_cons simp add: domain_append closed_in_def) |
18246 | 205 |
done |
206 |
||
18650 | 207 |
text {* Well-formed contexts have a unique type-binding for a type-variable. *} |
208 |
||
18246 | 209 |
lemma uniqueness_of_ctxt: |
210 |
fixes \<Gamma>::"ty_context" |
|
18412 | 211 |
assumes a: "\<turnstile> \<Gamma> ok" |
212 |
and b: "(X,T)\<in>set \<Gamma>" |
|
213 |
and c: "(X,S)\<in>set \<Gamma>" |
|
214 |
shows "T=S" |
|
18621 | 215 |
using a b c |
216 |
proof (induct) |
|
217 |
case valid_nil thus "T=S" by simp |
|
218 |
next |
|
219 |
case (valid_cons U Y \<Gamma>) |
|
220 |
moreover |
|
221 |
{ fix \<Gamma>::"ty_context" |
|
222 |
assume a: "X\<sharp>(domain \<Gamma>)" |
|
223 |
have "\<not>(\<exists>T.(X,T)\<in>(set \<Gamma>))" using a |
|
224 |
proof (induct \<Gamma>) |
|
225 |
case (Cons Y \<Gamma>) |
|
226 |
thus "\<not> (\<exists>T.(X,T)\<in>set(Y#\<Gamma>))" |
|
227 |
by (simp only: fresh_domain_cons, auto simp add: fresh_atm) |
|
228 |
qed (simp) |
|
229 |
} |
|
230 |
ultimately show "T=S" by auto |
|
231 |
qed |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
232 |
|
18628 | 233 |
section {* Size and Capture-Avoiding Substitution for Types *} |
18621 | 234 |
|
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
235 |
constdefs |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
236 |
size_ty_Tvar :: "tyvrs \<Rightarrow> nat" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
237 |
"size_ty_Tvar \<equiv> \<lambda>_. 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
238 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
239 |
size_ty_Top :: "nat" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
240 |
"size_ty_Top \<equiv> 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
241 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
242 |
size_ty_Fun :: "ty \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
243 |
"size_ty_Fun \<equiv> \<lambda>_ _ r1 r2. r1 + r2 + 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
244 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
245 |
size_ty_All :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
246 |
"size_ty_All \<equiv> \<lambda>_ _ _ r1 r2. r1 + r2 + 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
247 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
248 |
size_ty :: "ty \<Rightarrow> nat" |
20399 | 249 |
"size_ty \<equiv> ty_rec size_ty_Tvar size_ty_Top size_ty_Fun size_ty_All" |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
250 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
251 |
lemma fin_size_ty: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
252 |
shows "finite ((supp size_ty_Tvar)::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
253 |
and "finite ((supp size_ty_Top)::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
254 |
and "finite ((supp size_ty_Fun)::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
255 |
and "finite ((supp size_ty_All)::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
256 |
by (finite_guess add: size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def size_ty_All_def perm_nat_def)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
257 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
258 |
lemma fcb_size_ty_All: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
259 |
assumes "X\<sharp>size_ty_All" "X\<sharp>T2" "X\<sharp>r2" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
260 |
shows "X\<sharp>(size_ty_All X T1 T2 r1 r2)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
261 |
by (simp add: fresh_def supp_nat) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
262 |
|
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
263 |
lemma size_ty[simp]: |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
264 |
shows "size_ty (Tvar X) = 1" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
265 |
and "size_ty (Top) = 1" |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
266 |
and "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
267 |
and "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
268 |
apply(unfold size_ty_def) |
20399 | 269 |
apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
270 |
apply(simp_all add: fin_size_ty fcb_size_ty_All) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
271 |
apply(simp add: size_ty_Tvar_def) |
20399 | 272 |
apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
273 |
apply(simp_all add: fin_size_ty fcb_size_ty_All) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
274 |
apply(simp add: size_ty_Top_def) |
20399 | 275 |
apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
276 |
apply(simp_all add: fin_size_ty fcb_size_ty_All) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
277 |
apply(simp add: size_ty_Fun_def) |
20399 | 278 |
apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
279 |
apply(simp_all add: fin_size_ty fcb_size_ty_All) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
280 |
apply(fresh_guess add: perm_nat_def size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def size_ty_All_def)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
281 |
apply(simp add: size_ty_All_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
282 |
done |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
283 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
284 |
constdefs |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
285 |
subst_Tvar :: "tyvrs \<Rightarrow>ty \<Rightarrow> tyvrs \<Rightarrow> ty" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
286 |
"subst_Tvar X T \<equiv> \<lambda>Y. (if Y=X then T else (Tvar Y))" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
287 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
288 |
subst_Top :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
289 |
"subst_Top X T \<equiv> Top" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
290 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
291 |
subst_Fun :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
292 |
"subst_Fun X T \<equiv> \<lambda>_ _ r1 r2. r1 \<rightarrow> r2" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
293 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
294 |
subst_All :: "tyvrs \<Rightarrow> ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
295 |
"subst_All X T \<equiv> \<lambda>Y _ _ r1 r2. \<forall>[Y<:r2].r1" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
296 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
297 |
subst_ty :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" |
20399 | 298 |
"subst_ty X T \<equiv> ty_rec (subst_Tvar X T) (subst_Top X T) (subst_Fun X T) (subst_All X T)" |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
299 |
|
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
300 |
lemma supports_subst_Tvar: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
301 |
shows "((supp (X,T))::tyvrs set) supports (subst_Tvar X T)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
302 |
apply(supports_simp add: subst_Tvar_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
303 |
apply(rule impI) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
304 |
apply(drule pt_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
305 |
apply(perm_simp) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
306 |
done |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
307 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
308 |
lemma supports_subst_Top: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
309 |
shows "((supp (X,T))::tyvrs set) supports subst_Top X T" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
310 |
by (supports_simp add: subst_Top_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
311 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
312 |
lemma supports_subst_Fun: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
313 |
shows "((supp (X,T))::tyvrs set) supports subst_Fun X T" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
314 |
by (supports_simp add: subst_Fun_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
315 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
316 |
lemma supports_subst_All: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
317 |
shows "((supp (X,T))::tyvrs set) supports subst_All X T" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
318 |
apply(supports_simp add: subst_All_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
319 |
apply(perm_full_simp) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
320 |
done |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
321 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
322 |
lemma fin_supp_subst: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
323 |
shows "finite ((supp (subst_Tvar X T))::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
324 |
and "finite ((supp (subst_Top X T))::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
325 |
and "finite ((supp (subst_Fun X T))::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
326 |
and "finite ((supp (subst_All X T))::tyvrs set)" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
327 |
apply - |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
328 |
apply(rule supports_finite) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
329 |
apply(rule supports_subst_Tvar) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
330 |
apply(simp add: fs_tyvrs1) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
331 |
apply(finite_guess add: subst_Top_def subst_Fun_def subst_All_def fs_tyvrs1)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
332 |
apply(perm_full_simp) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
333 |
done |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
334 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
335 |
lemma fcb_subst_All: |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
336 |
assumes fr: "X\<sharp>(subst_All Y T)" "X\<sharp>T2" "X\<sharp>r2" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
337 |
shows "X\<sharp>(subst_All Y T) X T1 T2 r1 r2" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
338 |
apply (simp add: subst_All_def abs_fresh fr) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
339 |
done |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
340 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
341 |
syntax |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
342 |
subst_ty_syn :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
343 |
|
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
344 |
translations |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
345 |
"T1[Y:=T2]\<^isub>t\<^isub>y" \<rightleftharpoons> "subst_ty Y T2 T1" |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
346 |
|
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
347 |
lemma subst_ty[simp]: |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
348 |
shows "(Tvar X)[Y:=T]\<^isub>t\<^isub>y= (if X=Y then T else (Tvar X))" |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
349 |
and "(Top)[Y:=T]\<^isub>t\<^isub>y = Top" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
350 |
and "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)" |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
351 |
and "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))" |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
352 |
apply - |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
353 |
apply(unfold subst_ty_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
354 |
apply(rule trans) |
20399 | 355 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
356 |
apply(assumption)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
357 |
apply(simp add: subst_Tvar_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
358 |
apply(rule trans) |
20399 | 359 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
360 |
apply(assumption)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
361 |
apply(simp add: subst_Top_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
362 |
apply(rule trans) |
20399 | 363 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
364 |
apply(assumption)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
365 |
apply(simp add: subst_Fun_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
366 |
apply(rule trans) |
20399 | 367 |
apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All]) |
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
368 |
apply(assumption)+ |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
369 |
apply(rule supports_fresh) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
370 |
apply(rule supports_subst_Tvar) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
371 |
apply(simp add: fs_tyvrs1, simp add: fresh_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
372 |
apply(fresh_guess add: fresh_prod subst_Top_def fs_tyvrs1) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
373 |
apply(fresh_guess add: fresh_prod subst_Fun_def fs_tyvrs1) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
374 |
apply(fresh_guess add: fresh_prod subst_All_def fs_tyvrs1) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
375 |
apply(perm_full_simp) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
376 |
apply(assumption) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
377 |
apply(simp add: subst_All_def) |
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
378 |
done |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
379 |
|
18621 | 380 |
consts subst_tyc :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
381 |
primrec |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
382 |
"([])[Y:=T]\<^isub>t\<^isub>y\<^isub>c= []" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
383 |
"(XT#\<Gamma>)[Y:=T]\<^isub>t\<^isub>y\<^isub>c = (fst XT,(snd XT)[Y:=T]\<^isub>t\<^isub>y)#(\<Gamma>[Y:=T]\<^isub>t\<^isub>y\<^isub>c)" |
18246 | 384 |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
385 |
section {* Subtyping-Relation *} |
18246 | 386 |
|
18650 | 387 |
text {* The definition for the subtyping-relation follows quite closely what is written |
388 |
in the POPLmark-paper, except for the premises dealing with well-formed contexts and |
|
389 |
the freshness constraint @{term "X\<sharp>\<Gamma>"} in the @{text "S_Forall"}-rule. (The freshness |
|
390 |
constraint is specific to the \emph{nominal approach}. Note, however, that the constraint |
|
391 |
does \emph{not} make the subtyping-relation ``partial"\ldots because we work over |
|
392 |
$\alpha$-equivalence classes.) *} |
|
18628 | 393 |
|
18246 | 394 |
consts |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
395 |
subtype_of :: "(ty_context \<times> ty \<times> ty) set" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
396 |
syntax |
18621 | 397 |
subtype_of_syn :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_<:_" [100,100,100] 100) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
398 |
|
18246 | 399 |
translations |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
400 |
"\<Gamma> \<turnstile> S <: T" \<rightleftharpoons> "(\<Gamma>,S,T) \<in> subtype_of" |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
401 |
inductive subtype_of |
18246 | 402 |
intros |
18621 | 403 |
S_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" |
404 |
S_Var[intro]: "\<lbrakk>(X,S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T" |
|
405 |
S_Refl[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X" |
|
406 |
S_Arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^isub>1 \<rightarrow> S\<^isub>2) <: (T\<^isub>1 \<rightarrow> T\<^isub>2)" |
|
407 |
S_Forall[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; X\<sharp>\<Gamma>; ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> |
|
408 |
\<Longrightarrow> \<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" |
|
18246 | 409 |
|
410 |
lemma subtype_implies_closed: |
|
411 |
assumes a: "\<Gamma> \<turnstile> S <: T" |
|
412 |
shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" |
|
413 |
using a |
|
414 |
proof (induct) |
|
415 |
case (S_Top S \<Gamma>) |
|
18424 | 416 |
have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp) |
18246 | 417 |
moreover |
418 |
have "S closed_in \<Gamma>" by fact |
|
419 |
ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp |
|
420 |
next |
|
421 |
case (S_Var S T X \<Gamma>) |
|
422 |
have "(X,S)\<in>set \<Gamma>" by fact |
|
18424 | 423 |
hence "X \<in> domain \<Gamma>" by (rule domain_inclusion) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
424 |
hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm) |
18246 | 425 |
moreover |
426 |
have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact |
|
427 |
hence "T closed_in \<Gamma>" by force |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
428 |
ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp |
18424 | 429 |
qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp) |
18246 | 430 |
|
431 |
lemma subtype_implies_ok: |
|
432 |
fixes X::"tyvrs" |
|
433 |
assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
434 |
shows "\<turnstile> \<Gamma> ok" |
|
435 |
using a1 by (induct, auto) |
|
436 |
||
437 |
lemma subtype_implies_fresh: |
|
438 |
fixes X::"tyvrs" |
|
439 |
assumes a1: "\<Gamma> \<turnstile> S <: T" |
|
440 |
and a2: "X\<sharp>\<Gamma>" |
|
18424 | 441 |
shows "X\<sharp>S \<and> X\<sharp>T" |
18246 | 442 |
proof - |
443 |
from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok) |
|
18621 | 444 |
with a2 have "X\<sharp>domain(\<Gamma>)" by (simp add: fresh_domain) |
18424 | 445 |
moreover |
18246 | 446 |
from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed) |
18424 | 447 |
hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" |
18621 | 448 |
and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: domain_supp closed_in_def) |
18424 | 449 |
ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def) |
18246 | 450 |
qed |
451 |
||
452 |
lemma subtype_eqvt: |
|
453 |
fixes pi::"tyvrs prm" |
|
454 |
shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
455 |
apply(erule subtype_of.induct) |
18246 | 456 |
apply(force intro: valid_eqvt closed_in_eqvt) |
18655
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
457 |
apply(force intro!: S_Var |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
458 |
intro: closed_in_eqvt valid_eqvt |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
459 |
dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst] |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
460 |
simp add: pt_list_set_pi[OF pt_tyvrs_inst, symmetric]) |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
461 |
apply(force intro: valid_eqvt |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
462 |
dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst] |
73cebafb9a89
merged the silly lemmas into the eqvt proof of subtype
urbanc
parents:
18650
diff
changeset
|
463 |
simp add: domain_eqvt) |
18246 | 464 |
apply(force) |
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19501
diff
changeset
|
465 |
apply(force intro!: S_Forall simp add: fresh_prod fresh_bij) |
18246 | 466 |
done |
467 |
||
18628 | 468 |
text {* The most painful part of the subtyping definition is the strengthening of the |
469 |
induction principle. The induction principle that comes for free with the definition of |
|
18650 | 470 |
@{term "subtype_of"} requires to prove the @{text "S_Forall"}-case for \emph{all} binders |
471 |
@{text "X"}. This will often cause some renaming-manoeuvres in the reasoning. To avoid this, |
|
18628 | 472 |
we strengthening the induction-principle so that we only have to establish |
18650 | 473 |
the @{text "S_Forall"}-case for \emph{fresh} binders @{text "X"}. The property that allows |
474 |
us to strengthen the induction-principle is that the equivariance of @{text "subtype_of"}. *} |
|
18628 | 475 |
|
18621 | 476 |
lemma subtype_of_induct[consumes 1, case_names S_Top S_Var S_Refl S_Arrow S_Forall]: |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
477 |
fixes P :: "'a::fs_tyvrs\<Rightarrow>ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow>bool" |
18246 | 478 |
assumes a: "\<Gamma> \<turnstile> S <: T" |
18621 | 479 |
and a1: "\<And>\<Gamma> S x. \<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> S Top" |
480 |
and a2: "\<And>\<Gamma> X S T x. \<lbrakk>(X,S)\<in>set \<Gamma>; \<Gamma> \<turnstile> S <: T; \<And>z. P z \<Gamma> S T\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) T" |
|
481 |
and a3: "\<And>\<Gamma> X x. \<lbrakk>\<turnstile> \<Gamma> ok; X\<in>domain \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Tvar X) (Tvar X)" |
|
18628 | 482 |
and a4: "\<And>\<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. |
483 |
\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z \<Gamma> S\<^isub>2 T\<^isub>2\<rbrakk> |
|
18621 | 484 |
\<Longrightarrow> P x \<Gamma> (S\<^isub>1 \<rightarrow> S\<^isub>2) (T\<^isub>1 \<rightarrow> T\<^isub>2)" |
485 |
and a5: "\<And>\<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 x. |
|
18628 | 486 |
\<lbrakk>X\<sharp>x; X\<sharp>(\<Gamma>,S\<^isub>1,T\<^isub>1); \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<And>z. P z \<Gamma> T\<^isub>1 S\<^isub>1; |
487 |
((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2; \<And>z. P z ((X,T\<^isub>1)#\<Gamma>) S\<^isub>2 T\<^isub>2\<rbrakk> |
|
18621 | 488 |
\<Longrightarrow> P x \<Gamma> (\<forall>[X<:S\<^isub>1].S\<^isub>2) (\<forall>[X<:T\<^isub>1].T\<^isub>2)" |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
489 |
shows "P x \<Gamma> S T" |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
490 |
proof - |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
491 |
from a have "\<And>(pi::tyvrs prm) (x::'a::fs_tyvrs). P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
492 |
proof (induct) |
18424 | 493 |
case (S_Top S \<Gamma>) |
494 |
thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>Top)" by (force intro: valid_eqvt closed_in_eqvt a1) |
|
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
495 |
next |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
496 |
case (S_Var S T X \<Gamma>) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
497 |
have "(X,S) \<in> set \<Gamma>" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
498 |
hence "pi\<bullet>(X,S)\<in>pi\<bullet>(set \<Gamma>)" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
499 |
hence "(pi\<bullet>X,pi\<bullet>S)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
18246 | 500 |
moreover |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
501 |
have "\<Gamma> \<turnstile> S <: T" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
502 |
hence "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" by (rule subtype_eqvt) |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
503 |
moreover |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
504 |
have "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
505 |
hence "\<And>x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>S) (pi\<bullet>T)" by simp |
18246 | 506 |
ultimately |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
507 |
show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>T)" by (simp add: a2) |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
508 |
next |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
509 |
case (S_Refl X \<Gamma>) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
510 |
have "\<turnstile> \<Gamma> ok" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
511 |
hence "\<turnstile> (pi\<bullet>\<Gamma>) ok" by (rule valid_eqvt) |
18246 | 512 |
moreover |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
513 |
have "X \<in> domain \<Gamma>" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
514 |
hence "(pi\<bullet>X)\<in>pi\<bullet>domain \<Gamma>" by (rule pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
18246 | 515 |
hence "(pi\<bullet>X)\<in>domain (pi\<bullet>\<Gamma>)" by (simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst]) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
516 |
ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Tvar X)) (pi\<bullet>(Tvar X))" by (simp add: a3) |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
517 |
next |
18424 | 518 |
case S_Arrow thus ?case by (auto intro: a4 subtype_eqvt) |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
519 |
next |
18621 | 520 |
case (S_Forall S1 S2 T1 T2 X \<Gamma>) |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
521 |
have b1: "\<Gamma> \<turnstile> T1 <: S1" by fact |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
522 |
have b2: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>T1) (pi\<bullet>S1)" by fact |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
523 |
have b4: "((X,T1)#\<Gamma>) \<turnstile> S2 <: T2" by fact |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
524 |
have b5: "\<And>(pi::tyvrs prm) x. P x (pi\<bullet>((X,T1)#\<Gamma>)) (pi\<bullet>S2) (pi\<bullet>T2)" by fact |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
525 |
have b3: "X\<sharp>\<Gamma>" by fact |
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
526 |
have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh) |
18246 | 527 |
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)" |
528 |
by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1) |
|
529 |
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)" |
|
530 |
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" |
|
531 |
by (auto simp add: fresh_prod fresh_atm) |
|
532 |
let ?pi' = "[(C,pi\<bullet>X)]@pi" |
|
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
533 |
from b2 have c1: "\<And>x. P x (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>T1) (?pi'\<bullet>S1)" by simp |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
534 |
from b5 have "\<And>x. P x (?pi'\<bullet>((X,T1)#\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
535 |
hence "\<And>x. P x ((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" by simp |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
536 |
hence c2: "\<And>x. P x ((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>S2) (?pi'\<bullet>T2)" using f1 |
18246 | 537 |
by (simp only: pt_tyvrs2 calc_atm, simp) |
538 |
from b3 have "(pi\<bullet>X)\<sharp>(pi\<bullet>\<Gamma>)" |
|
539 |
by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
540 |
with f6 have f6a: "?pi'\<bullet>\<Gamma>=pi\<bullet>\<Gamma>" |
|
541 |
by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
542 |
hence f6': "C\<sharp>(?pi'\<bullet>\<Gamma>)" using f6 by simp |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
543 |
from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>S1)" |
18246 | 544 |
by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
545 |
with f2 have f2a: "?pi'\<bullet>S1=pi\<bullet>S1" |
|
546 |
by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
547 |
hence f2': "C\<sharp>(?pi'\<bullet>S1)" using f2 by simp |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
548 |
from b3' have "(pi\<bullet>X)\<sharp>(pi\<bullet>T1)" |
18246 | 549 |
by (simp add: fresh_prod pt_fresh_bij[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
550 |
with f3 have f3a: "?pi'\<bullet>T1=pi\<bullet>T1" |
|
551 |
by (simp only: pt_tyvrs2 pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
552 |
hence f3': "C\<sharp>(?pi'\<bullet>T1)" using f3 by simp |
|
553 |
from b1 have e1: "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>T1) <: (?pi'\<bullet>S1)" by (rule subtype_eqvt) |
|
554 |
from b4 have "(?pi'\<bullet>((X,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by (rule subtype_eqvt) |
|
555 |
hence "((?pi'\<bullet>X,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" by simp |
|
556 |
hence e2: "((C,?pi'\<bullet>T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>S2) <: (?pi'\<bullet>T2)" using f1 |
|
557 |
by (simp only: pt_tyvrs2 calc_atm, simp) |
|
558 |
have fnew: "C\<sharp>(?pi'\<bullet>\<Gamma>,?pi'\<bullet>S1,?pi'\<bullet>T1)" using f6' f2' f3' by (simp add: fresh_prod) |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
559 |
have main: "P x (?pi'\<bullet>\<Gamma>) (\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) (\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2))" |
18246 | 560 |
using f7 fnew e1 c1 e2 c2 by (rule a5) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
561 |
have alpha1: "(\<forall>[C<:(?pi'\<bullet>S1)].(?pi'\<bullet>S2)) = (pi\<bullet>(\<forall>[X<:S1].S2))" |
18246 | 562 |
using f1 f4 f2a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
563 |
have alpha2: "(\<forall>[C<:(?pi'\<bullet>T1)].(?pi'\<bullet>T2)) = (pi\<bullet>(\<forall>[X<:T1].T2))" |
18246 | 564 |
using f1 f5 f3a[symmetric] by (simp add: ty.inject alpha pt_tyvrs2[symmetric]) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
565 |
show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(\<forall>[X<:S1].S2)) (pi\<bullet>(\<forall>[X<:T1].T2))" |
18246 | 566 |
using alpha1 alpha2 f6a main by simp |
567 |
qed |
|
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
568 |
hence "P x (([]::tyvrs prm)\<bullet>\<Gamma>) (([]::tyvrs prm)\<bullet>S) (([]::tyvrs prm)\<bullet>T)" by blast |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
569 |
thus ?thesis by simp |
18246 | 570 |
qed |
571 |
||
18621 | 572 |
section {* Reflexivity of Subtyping *} |
18246 | 573 |
|
574 |
lemma subtype_reflexivity: |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
575 |
assumes a: "\<turnstile> \<Gamma> ok" |
18424 | 576 |
and b: "T closed_in \<Gamma>" |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
577 |
shows "\<Gamma> \<turnstile> T <: T" |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
578 |
using a b |
18660
9968dc816cda
cahges to use the new induction-principle (now proved in
urbanc
parents:
18655
diff
changeset
|
579 |
proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
580 |
case (Forall X T\<^isub>1 T\<^isub>2) |
18747 | 581 |
have ih_T\<^isub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact |
582 |
have ih_T\<^isub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact |
|
18424 | 583 |
have fresh_cond: "X\<sharp>\<Gamma>" by fact |
18621 | 584 |
hence fresh_domain: "X\<sharp>(domain \<Gamma>)" by (simp add: fresh_domain) |
18424 | 585 |
have "(\<forall>[X<:T\<^isub>2].T\<^isub>1) closed_in \<Gamma>" by fact |
586 |
hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((X,T\<^isub>2)#\<Gamma>)" |
|
587 |
by (auto simp add: closed_in_def ty.supp abs_supp) |
|
588 |
have ok: "\<turnstile> \<Gamma> ok" by fact |
|
18621 | 589 |
hence ok': "\<turnstile> ((X,T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_domain by simp |
18424 | 590 |
have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
591 |
moreover |
18424 | 592 |
have "((X,T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp |
593 |
ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T\<^isub>2].T\<^isub>1 <: \<forall>[X<:T\<^isub>2].T\<^isub>1" using fresh_cond |
|
18621 | 594 |
by (simp add: subtype_of.S_Forall) |
18246 | 595 |
qed (auto simp add: closed_in_def ty.supp supp_atm) |
596 |
||
18621 | 597 |
lemma subtype_reflexivity_semiautomated: |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
598 |
assumes a: "\<turnstile> \<Gamma> ok" |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
599 |
and b: "T closed_in \<Gamma>" |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
600 |
shows "\<Gamma> \<turnstile> T <: T" |
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
601 |
using a b |
18660
9968dc816cda
cahges to use the new induction-principle (now proved in
urbanc
parents:
18655
diff
changeset
|
602 |
apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct) |
18747 | 603 |
apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
604 |
--{* Too bad that this instantiation cannot be found automatically by |
18621 | 605 |
\isakeyword{auto}; \isakeyword{blast} would find it if we had not used |
18628 | 606 |
an explicit definition for @{text "closed_in_def"}. *} |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
607 |
apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec) |
18747 | 608 |
apply(force dest: fresh_domain simp add: closed_in_def) |
18246 | 609 |
done |
610 |
||
18747 | 611 |
|
18628 | 612 |
section {* Weakening *} |
18246 | 613 |
|
18628 | 614 |
text {* In order to prove weakening we introduce the notion of a type-context extending |
615 |
another. This generalization seems to make the proof for weakening to be |
|
616 |
smoother than if we had strictly adhered to the version in the POPLmark-paper. *} |
|
18246 | 617 |
|
618 |
constdefs |
|
619 |
extends :: "ty_context \<Rightarrow> ty_context \<Rightarrow> bool" ("_ extends _" [100,100] 100) |
|
620 |
"\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (X,Q)\<in>set \<Gamma> \<longrightarrow> (X,Q)\<in>set \<Delta>" |
|
621 |
||
622 |
lemma extends_domain: |
|
623 |
assumes a: "\<Delta> extends \<Gamma>" |
|
624 |
shows "domain \<Gamma> \<subseteq> domain \<Delta>" |
|
625 |
using a |
|
626 |
apply (auto simp add: extends_def) |
|
627 |
apply (drule domain_existence) |
|
628 |
apply (force simp add: domain_inclusion) |
|
629 |
done |
|
630 |
||
631 |
lemma extends_closed: |
|
632 |
assumes a1: "T closed_in \<Gamma>" |
|
633 |
and a2: "\<Delta> extends \<Gamma>" |
|
634 |
shows "T closed_in \<Delta>" |
|
635 |
using a1 a2 |
|
636 |
by (auto dest: extends_domain simp add: closed_in_def) |
|
637 |
||
18424 | 638 |
lemma extends_memb: |
639 |
assumes a: "\<Delta> extends \<Gamma>" |
|
640 |
and b: "(X,T) \<in> set \<Gamma>" |
|
641 |
shows "(X,T) \<in> set \<Delta>" |
|
642 |
using a b by (simp add: extends_def) |
|
643 |
||
18246 | 644 |
lemma weakening: |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
645 |
assumes a: "\<Gamma> \<turnstile> S <: T" |
18424 | 646 |
and b: "\<turnstile> \<Delta> ok" |
647 |
and c: "\<Delta> extends \<Gamma>" |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
648 |
shows "\<Delta> \<turnstile> S <: T" |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
649 |
using a b c |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
650 |
proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct) |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
651 |
case (S_Top \<Gamma> S) |
18246 | 652 |
have lh_drv_prem: "S closed_in \<Gamma>" by fact |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
653 |
have "\<turnstile> \<Delta> ok" by fact |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
654 |
moreover |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
655 |
have "\<Delta> extends \<Gamma>" by fact |
18424 | 656 |
hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed) |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
657 |
ultimately show "\<Delta> \<turnstile> S <: Top" by force |
18246 | 658 |
next |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
659 |
case (S_Var \<Gamma> X S T) |
18246 | 660 |
have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
661 |
have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
662 |
have ok: "\<turnstile> \<Delta> ok" by fact |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
663 |
have extends: "\<Delta> extends \<Gamma>" by fact |
18424 | 664 |
have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb) |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
665 |
moreover |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
666 |
have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
667 |
ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force |
18246 | 668 |
next |
18305
a780f9c1538b
changed everything until the interesting transitivity_narrowing
urbanc
parents:
18269
diff
changeset
|
669 |
case (S_Refl \<Gamma> X) |
18246 | 670 |
have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
671 |
have "\<turnstile> \<Delta> ok" by fact |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
672 |
moreover |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
673 |
have "\<Delta> extends \<Gamma>" by fact |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
674 |
hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
675 |
ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force |
18246 | 676 |
next |
18424 | 677 |
case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) thus "\<Delta> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by blast |
18246 | 678 |
next |
18621 | 679 |
case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
18424 | 680 |
have fresh_cond: "X\<sharp>\<Delta>" by fact |
18621 | 681 |
hence fresh_domain: "X\<sharp>(domain \<Delta>)" by (simp add: fresh_domain) |
18424 | 682 |
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
683 |
have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact |
|
684 |
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
|
685 |
hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
686 |
have ok: "\<turnstile> \<Delta> ok" by fact |
18424 | 687 |
have ext: "\<Delta> extends \<Gamma>" by fact |
688 |
have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed) |
|
18621 | 689 |
hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
690 |
moreover |
18424 | 691 |
have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def) |
692 |
ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
693 |
moreover |
18424 | 694 |
have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp |
18621 | 695 |
ultimately show "\<Delta> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" using ok by (force intro: S_Forall) |
18246 | 696 |
qed |
697 |
||
18650 | 698 |
text {* In fact all ``non-binding" cases can be solved automatically: *} |
18246 | 699 |
|
18628 | 700 |
lemma weakening_more_automated: |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
701 |
assumes a: "\<Gamma> \<turnstile> S <: T" |
18424 | 702 |
and b: "\<turnstile> \<Delta> ok" |
703 |
and c: "\<Delta> extends \<Gamma>" |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
704 |
shows "\<Delta> \<turnstile> S <: T" |
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
705 |
using a b c |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
706 |
proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_induct) |
18621 | 707 |
case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2) |
18424 | 708 |
have fresh_cond: "X\<sharp>\<Delta>" by fact |
18621 | 709 |
hence fresh_domain: "X\<sharp>(domain \<Delta>)" by (simp add: fresh_domain) |
18424 | 710 |
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
711 |
have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact |
|
712 |
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact |
|
713 |
hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
714 |
have ok: "\<turnstile> \<Delta> ok" by fact |
18424 | 715 |
have ext: "\<Delta> extends \<Gamma>" by fact |
716 |
have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed) |
|
18621 | 717 |
hence "\<turnstile> ((X,T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force |
18628 | 718 |
moreover |
18424 | 719 |
have "((X,T\<^isub>1)#\<Delta>) extends ((X,T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def) |
720 |
ultimately have "((X,T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
721 |
moreover |
18424 | 722 |
have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp |
18621 | 723 |
ultimately show "\<Delta> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" using ok by (force intro: S_Forall) |
18424 | 724 |
qed (blast intro: extends_closed extends_memb dest: extends_domain)+ |
18246 | 725 |
|
18628 | 726 |
section {* Transitivity and Narrowing *} |
727 |
||
18650 | 728 |
text {* Some inversion lemmas that are needed in the transitivity and narrowing proof.*} |
729 |
||
730 |
lemma S_TopE: |
|
731 |
assumes a: "\<Gamma> \<turnstile> Top <: T" |
|
732 |
shows "T = Top" |
|
733 |
using a by (cases, auto) |
|
734 |
||
735 |
lemma S_ArrowE_left: |
|
736 |
assumes a: "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" |
|
737 |
shows "T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2)" |
|
738 |
using a by (cases, auto simp add: ty.inject) |
|
739 |
||
740 |
lemma S_ForallE_left: |
|
741 |
shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<rbrakk> |
|
742 |
\<Longrightarrow> T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = \<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)" |
|
743 |
apply(frule subtype_implies_ok) |
|
744 |
apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T") |
|
745 |
apply(auto simp add: ty.inject alpha) |
|
746 |
apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI) |
|
747 |
apply(rule conjI) |
|
748 |
apply(rule sym) |
|
749 |
apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
750 |
apply(rule pt_tyvrs3) |
|
751 |
apply(simp) |
|
752 |
apply(rule at_ds5[OF at_tyvrs_inst]) |
|
753 |
apply(rule conjI) |
|
754 |
apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm) |
|
755 |
apply(drule_tac \<Gamma>="((Xa,T\<^isub>1)#\<Gamma>)" in subtype_implies_closed)+ |
|
756 |
apply(simp add: closed_in_def) |
|
757 |
apply(drule fresh_domain)+ |
|
758 |
apply(simp add: fresh_def) |
|
759 |
apply(subgoal_tac "X \<notin> (insert Xa (domain \<Gamma>))")(*A*) |
|
760 |
apply(force) |
|
761 |
(*A*)apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domain]) |
|
762 |
(* 2nd conjunct *)apply(frule_tac X="X" in subtype_implies_fresh) |
|
763 |
apply(assumption) |
|
764 |
apply(drule_tac X="Xa" in subtype_implies_fresh) |
|
765 |
apply(assumption) |
|
766 |
apply(simp add: fresh_prod) |
|
767 |
apply(drule_tac pi="[(X,Xa)]" in subtype_eqvt) |
|
768 |
apply(simp add: calc_atm) |
|
769 |
apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
770 |
done |
|
771 |
||
772 |
text {* Next we prove the transitivity and narrowing for the subtyping-relation. |
|
18621 | 773 |
The POPLmark-paper says the following: |
774 |
||
18650 | 775 |
\begin{quote} |
18621 | 776 |
\begin{lemma}[Transitivity and Narrowing] \ |
777 |
\begin{enumerate} |
|
778 |
\item If @{term "\<Gamma> \<turnstile> S<:Q"} and @{term "\<Gamma> \<turnstile> Q<:T"}, then @{term "\<Gamma> \<turnstile> S<:T"}. |
|
779 |
\item If @{text "\<Gamma>,X<:Q,\<Delta> \<turnstile> M<:N"} and @{term "\<Gamma> \<turnstile> P<:Q"} then @{text "\<Gamma>,X<:P,\<Delta> \<turnstile> M<:N"}. |
|
780 |
\end{enumerate} |
|
781 |
\end{lemma} |
|
782 |
||
783 |
The two parts are proved simultaneously, by induction on the size |
|
784 |
of @{term "Q"}. The argument for part (2) assumes that part (1) has |
|
785 |
been established already for the @{term "Q"} in question; part (1) uses |
|
786 |
part (2) only for strictly smaller @{term "Q"}. |
|
18650 | 787 |
\end{quote} |
18621 | 788 |
|
789 |
For the induction on the size of @{term "Q"}, we use the induction-rule |
|
790 |
@{text "measure_induct_rule"}: |
|
791 |
||
792 |
\begin{center} |
|
793 |
@{thm measure_induct_rule[of "size_ty",no_vars]} |
|
794 |
\end{center} |
|
18410 | 795 |
|
18628 | 796 |
That means in order to show a property @{term "P a"} for all @{term "a"}, |
18650 | 797 |
the induct-rule requires to prove that for all @{term x} @{term "P x"} holds using the |
18621 | 798 |
assumption that for all @{term y} whose size is strictly smaller than |
799 |
that of @{term x} the property @{term "P y"} holds. *} |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
800 |
|
18621 | 801 |
lemma |
802 |
shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" |
|
803 |
and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N" |
|
20503 | 804 |
proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule) |
18621 | 805 |
case (less Q) |
806 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
807 |
First we mention the induction hypotheses of the outer induction for later |
|
808 |
reference:\end{minipage}*} |
|
809 |
have IH_trans: |
|
810 |
"\<And>Q' \<Gamma> S T. \<lbrakk>size_ty Q' < size_ty Q; \<Gamma>\<turnstile>S<:Q'; \<Gamma>\<turnstile>Q'<:T\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>S<:T" by fact |
|
811 |
have IH_narrow: |
|
812 |
"\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(X,Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk> |
|
813 |
\<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N" by fact |
|
814 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
815 |
We proceed with the transitivity proof as an auxiliary lemma, because it needs |
|
816 |
to be referenced in the narrowing proof.\end{minipage}*} |
|
817 |
have transitivity_aux: |
|
818 |
"\<And>\<Gamma> S T. \<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T" |
|
18246 | 819 |
proof - |
18424 | 820 |
fix \<Gamma>' S' T |
18621 | 821 |
assume "\<Gamma>' \<turnstile> S' <: Q" --{* left-hand derivation *} |
822 |
and "\<Gamma>' \<turnstile> Q <: T" --{* right-hand derivation *} |
|
823 |
thus "\<Gamma>' \<turnstile> S' <: T" |
|
18747 | 824 |
proof (nominal_induct \<Gamma>' S' Q\<equiv>Q rule: subtype_of_induct) |
18424 | 825 |
case (S_Top \<Gamma> S) |
18621 | 826 |
--{* \begin{minipage}[t]{0.9\textwidth} |
827 |
In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S <: Top"}, giving |
|
828 |
us @{term "\<turnstile> \<Gamma> ok"} and @{term "S closed_in \<Gamma>"}. This case is straightforward, |
|
829 |
because the right-hand derivation must be of the form @{term "\<Gamma> \<turnstile> Top <: Top"} |
|
830 |
giving us the equation @{term "T = Top"}.\end{minipage}*} |
|
18424 | 831 |
hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp |
832 |
hence T_inst: "T = Top" by (simp add: S_TopE) |
|
18621 | 833 |
have "\<turnstile> \<Gamma> ok" |
834 |
and "S closed_in \<Gamma>" by fact |
|
835 |
hence "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top) |
|
18424 | 836 |
thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp |
18246 | 837 |
next |
18621 | 838 |
case (S_Var \<Gamma> Y U) |
839 |
-- {* \begin{minipage}[t]{0.9\textwidth} |
|
840 |
In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> Tvar Y <: Q"} |
|
841 |
with @{term "S = Tvar Y"}. We have therefore @{term "(Y,U)"} |
|
18650 | 842 |
is in @{term "\<Gamma>"} and by inner induction hypothesis that @{term "\<Gamma> \<turnstile> U <: T"}. |
18621 | 843 |
By @{text "S_Var"} follows @{term "\<Gamma> \<turnstile> Tvar Y <: T"}.\end{minipage}*} |
18424 | 844 |
hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp |
18621 | 845 |
have "(Y,U) \<in> set \<Gamma>" by fact |
846 |
with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by (simp add: subtype_of.S_Var) |
|
18246 | 847 |
next |
18424 | 848 |
case (S_Refl \<Gamma> X) |
18621 | 849 |
--{* \begin{minipage}[t]{0.9\textwidth} |
850 |
In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(Tvar X) <: (Tvar X)"} with |
|
851 |
@{term "Q=Tvar X"}. The goal then follows immediately from the right-hand |
|
852 |
derivation.\end{minipage}*} |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
853 |
thus "\<Gamma> \<turnstile> Tvar X <: T" by simp |
18246 | 854 |
next |
18621 | 855 |
case (S_Arrow \<Gamma> S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) |
856 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
857 |
In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: Q\<^isub>1 \<rightarrow> Q\<^isub>2"} with |
|
858 |
@{term "S\<^isub>1\<rightarrow>S\<^isub>2=S"} and @{term "Q\<^isub>1\<rightarrow>Q\<^isub>2=Q"}. We know that the @{text "size_ty"} of |
|
859 |
@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q}; |
|
860 |
so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. |
|
861 |
We also have the sub-derivations @{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "\<Gamma>\<turnstile>S\<^isub>2<:Q\<^isub>2"}. |
|
18628 | 862 |
The right-hand derivation is @{term "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T"}. There exist types |
18621 | 863 |
@{text "T\<^isub>1,T\<^isub>2"} such that @{term "T=Top \<or> T=T\<^isub>1\<rightarrow>T\<^isub>2"}. The @{term "Top"}-case is |
864 |
straightforward once we know @{term "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. |
|
865 |
In the other case we have the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "\<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"}. |
|
866 |
Using the outer induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"} |
|
867 |
and @{term "\<Gamma>\<turnstile>S\<^isub>2<:T\<^isub>2"}. By rule @{text "S_Arrow"} follows @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"}, |
|
868 |
which is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>"}.\end{minipage}*} |
|
869 |
hence rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp |
|
870 |
from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q` |
|
871 |
have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto |
|
872 |
have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact |
|
873 |
have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact |
|
874 |
from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)" |
|
875 |
by (simp add: S_ArrowE_left) |
|
876 |
moreover |
|
877 |
have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in \<Gamma>" |
|
878 |
using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed) |
|
879 |
hence "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp) |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
880 |
moreover |
18424 | 881 |
have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok) |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
882 |
moreover |
18621 | 883 |
{ assume "\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2" |
884 |
then obtain T\<^isub>1 T\<^isub>2 |
|
885 |
where T_inst: "T = T\<^isub>1 \<rightarrow> T\<^isub>2" |
|
886 |
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" |
|
887 |
and rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force |
|
888 |
from IH_trans[of "Q\<^isub>1"] |
|
889 |
have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp |
|
18246 | 890 |
moreover |
18621 | 891 |
from IH_trans[of "Q\<^isub>2"] |
892 |
have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp |
|
893 |
ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by (simp add: subtype_of.S_Arrow) |
|
894 |
hence "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
895 |
} |
18621 | 896 |
ultimately show "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" by blast |
18246 | 897 |
next |
18621 | 898 |
case (S_Forall \<Gamma> X S\<^isub>1 S\<^isub>2 Q\<^isub>1 Q\<^isub>2) |
899 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
900 |
In this case the left-hand derivation is @{text "\<Gamma>\<turnstile>\<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:Q\<^isub>1].Q\<^isub>2"} with |
|
901 |
@{text "\<forall>[X<:S\<^isub>1].S\<^isub>2=S"} and @{text "\<forall>[X<:Q\<^isub>1].Q\<^isub>2=Q"}. We therefore have the sub-derivations |
|
902 |
@{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "((X,Q\<^isub>1)#\<Gamma>)\<turnstile>S\<^isub>2<:Q\<^isub>2"}. Since @{term "X"} is a binder, we |
|
903 |
assume that it is sufficiently fresh; in particular we have the freshness conditions |
|
18650 | 904 |
@{term "X\<sharp>\<Gamma>"} and @{term "X\<sharp>Q\<^isub>1"} (these assumptions are provided by the strong |
905 |
induction-rule @{text "subtype_of_induct"}). We know that the @{text "size_ty"} of |
|
18621 | 906 |
@{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q}; |
907 |
so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}. |
|
908 |
The right-hand derivation is @{text "\<Gamma> \<turnstile> \<forall>[X<:Q\<^isub>1].Q\<^isub>2 <: T"}. Since @{term "X\<sharp>\<Gamma>"} |
|
909 |
and @{term "X\<sharp>Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that |
|
910 |
@{text "T=Top \<or> T=\<forall>[X<:T\<^isub>1].T\<^isub>2"}. The @{term "Top"}-case is straightforward once we know |
|
911 |
@{text "(\<forall>[X<:S\<^isub>1].S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. In the other case we have |
|
18628 | 912 |
the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"}. Using the outer |
18621 | 913 |
induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"}. From the outer |
18628 | 914 |
induction for narrowing we get @{term "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using again |
915 |
induction for transitivity we obtain @{term "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. By rule |
|
916 |
@{text "S_Forall"} and the freshness condition @{term "X\<sharp>\<Gamma>"} follows |
|
18650 | 917 |
@{text "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2"}, which is @{text "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T\<^isub>"}. |
18628 | 918 |
\end{minipage}*} |
18621 | 919 |
hence rh_drv: "\<Gamma> \<turnstile> \<forall>[X<:Q\<^isub>1].Q\<^isub>2 <: T" by simp |
920 |
have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact |
|
921 |
have lh_drv_prm\<^isub>2: "((X,Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact |
|
922 |
have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" by fact |
|
923 |
from `\<forall>[X<:Q\<^isub>1].Q\<^isub>2 = Q` |
|
20395
9a60e3151244
added definition for size and substitution using the recursion
urbanc
parents:
19972
diff
changeset
|
924 |
have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " using fresh_cond by auto |
18621 | 925 |
from rh_drv |
926 |
have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=\<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2)" |
|
927 |
using fresh_cond by (simp add: S_ForallE_left) |
|
928 |
moreover |
|
929 |
have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in ((X,Q\<^isub>1)#\<Gamma>)" |
|
930 |
using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed) |
|
931 |
hence "(\<forall>[X<:S\<^isub>1].S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp) |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
932 |
moreover |
18424 | 933 |
have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok) |
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
934 |
moreover |
18621 | 935 |
{ assume "\<exists>T\<^isub>1 T\<^isub>2. T=\<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2" |
936 |
then obtain T\<^isub>1 T\<^isub>2 |
|
937 |
where T_inst: "T = \<forall>[X<:T\<^isub>1].T\<^isub>2" |
|
938 |
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" |
|
939 |
and rh_drv_prm\<^isub>2:"((X,T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force |
|
940 |
from IH_trans[of "Q\<^isub>1"] |
|
941 |
have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast |
|
942 |
moreover |
|
943 |
from IH_narrow[of "Q\<^isub>1" "[]"] |
|
944 |
have "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>1\<^isub>2_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp |
|
945 |
with IH_trans[of "Q\<^isub>2"] |
|
946 |
have "((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 by simp |
|
947 |
ultimately have "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: \<forall>[X<:T\<^isub>1].T\<^isub>2" |
|
948 |
using fresh_cond by (simp add: subtype_of.S_Forall) |
|
949 |
hence "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T" using T_inst by simp |
|
18353
4dd468ccfdf7
transitivity should be now in a reasonable state. But
urbanc
parents:
18306
diff
changeset
|
950 |
} |
18621 | 951 |
ultimately show "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T" by blast |
18246 | 952 |
qed |
953 |
qed |
|
954 |
||
18621 | 955 |
{ --{* The transitivity proof is now by the auxiliary lemma. *} |
956 |
case 1 |
|
957 |
have "\<Gamma> \<turnstile> S <: Q" |
|
958 |
and "\<Gamma> \<turnstile> Q <: T" by fact |
|
959 |
thus "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux) |
|
960 |
next |
|
961 |
--{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"}. *} |
|
962 |
case 2 |
|
963 |
have "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N" --{* left-hand derivation *} |
|
964 |
and "\<Gamma> \<turnstile> P<:Q" by fact --{* right-hand derivation *} |
|
965 |
thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N" |
|
966 |
proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of_induct) |
|
18424 | 967 |
case (S_Top _ S \<Delta> \<Gamma> X) |
18621 | 968 |
--{* \begin{minipage}[t]{0.9\textwidth} |
969 |
In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> S <: Top"}. We show |
|
970 |
that the context @{term "\<Delta>@[(X,P)]@\<Gamma>"} is ok and that @{term S} is closed in |
|
971 |
@{term "\<Delta>@[(X,P)]@\<Gamma>"}. Then we can apply the @{text "S_Top"}-rule.\end{minipage}*} |
|
972 |
hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
|
973 |
and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
|
18424 | 974 |
have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
975 |
hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
18621 | 976 |
with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
18412 | 977 |
moreover |
18621 | 978 |
from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(X,P)]@\<Gamma>)" |
979 |
by (simp add: closed_in_def domain_append) |
|
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
980 |
ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.S_Top) |
18246 | 981 |
next |
18424 | 982 |
case (S_Var _ Y S N \<Delta> \<Gamma> X) |
18621 | 983 |
--{* \begin{minipage}[t]{0.9\textwidth} |
18628 | 984 |
In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} and |
985 |
by inner induction hypothesis we have @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N"}. We therefore |
|
18621 | 986 |
know that the contexts @{term "\<Delta>@[(X,Q)]@\<Gamma>"} and @{term "\<Delta>@[(X,P)]@\<Gamma>"} are ok, and that |
18628 | 987 |
@{term "(Y,S)"} is in @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We need to show that |
988 |
@{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N"} holds. In case @{term "X\<noteq>Y"} we know that |
|
989 |
@{term "(Y,S)"} is in @{term "\<Delta>@[(X,P)]@\<Gamma>"} and can use the inner induction hypothesis |
|
990 |
and rule @{text "S_Var"} to conclude. In case @{term "X=Y"} we can infer that |
|
991 |
@{term "S=Q"}; moreover we have that @{term "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>"} and therefore |
|
992 |
by @{text "weakening"} that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we |
|
993 |
obtain then @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule |
|
994 |
@{text "S_Var"}.\end{minipage}*} |
|
18621 | 995 |
hence IH_inner: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S <: N" |
996 |
and lh_drv_prm: "(Y,S) \<in> set (\<Delta>@[(X,Q)]@\<Gamma>)" |
|
997 |
and rh_drv: "\<Gamma> \<turnstile> P<:Q" |
|
998 |
and ok\<^isub>Q: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok) |
|
999 |
hence ok\<^isub>P: "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) |
|
1000 |
show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" |
|
1001 |
proof (cases "X=Y") |
|
1002 |
case False |
|
1003 |
have "X\<noteq>Y" by fact |
|
1004 |
hence "(Y,S)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm by simp |
|
1005 |
with IH_inner show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.S_Var) |
|
1006 |
next |
|
1007 |
case True |
|
1008 |
have memb\<^isub>X\<^isub>Q: "(X,Q)\<in>set (\<Delta>@[(X,Q)]@\<Gamma>)" by simp |
|
1009 |
have memb\<^isub>X\<^isub>P: "(X,P)\<in>set (\<Delta>@[(X,P)]@\<Gamma>)" by simp |
|
1010 |
have eq: "X=Y" by fact |
|
1011 |
hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt) |
|
18424 | 1012 |
hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp |
1013 |
moreover |
|
1014 |
have "(\<Delta>@[(X,P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def) |
|
18621 | 1015 |
hence "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening) |
1016 |
ultimately have "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_aux) |
|
1017 |
thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by (simp only: subtype_of.S_Var) |
|
1018 |
qed |
|
18246 | 1019 |
next |
18424 | 1020 |
case (S_Refl _ Y \<Delta> \<Gamma> X) |
18621 | 1021 |
--{* \begin{minipage}[t]{0.9\textwidth} |
1022 |
In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y"} and we |
|
18628 | 1023 |
therefore know that @{term "\<Delta>@[(X,Q)]@\<Gamma>"} is ok and that @{term "Y"} is in |
18621 | 1024 |
the domain of @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. We therefore know that @{term "\<Delta>@[(X,P)]@\<Gamma>"} is ok |
1025 |
and that @{term Y} is in the domain of @{term "\<Delta>@[(X,P)]@\<Gamma>"}. We can conclude by applying |
|
1026 |
rule @{text "S_Refl"}.\end{minipage}*} |
|
1027 |
hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(X,Q)]@\<Gamma>) ok" |
|
1028 |
and lh_drv_prm\<^isub>2: "Y \<in> domain (\<Delta>@[(X,Q)]@\<Gamma>)" by simp_all |
|
18424 | 1029 |
have "\<Gamma> \<turnstile> P <: Q" by fact |
1030 |
hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
|
18621 | 1031 |
with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(X,P)]@\<Gamma>) ok" by (simp add: replace_type) |
18424 | 1032 |
moreover |
18621 | 1033 |
from lh_drv_prm\<^isub>2 have "Y \<in> domain (\<Delta>@[(X,P)]@\<Gamma>)" by (simp add: domain_append) |
18577
a636846a02c7
added more documentation; will now try out a modification
urbanc
parents:
18424
diff
changeset
|
1034 |
ultimately show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.S_Refl) |
18246 | 1035 |
next |
18621 | 1036 |
case (S_Arrow _ Q\<^isub>1 Q\<^isub>2 S\<^isub>1 S\<^isub>2 \<Delta> \<Gamma> X) |
1037 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
1038 |
In this case the left-hand derivation is @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2"} |
|
1039 |
and the proof is trivial.\end{minipage}*} |
|
1040 |
thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast |
|
18424 | 1041 |
next |
18621 | 1042 |
case (S_Forall _ Y S\<^isub>1 S\<^isub>2 T\<^isub>1 T\<^isub>2 \<Delta> \<Gamma> X) |
1043 |
--{* \begin{minipage}[t]{0.9\textwidth} |
|
18628 | 1044 |
In this case the left-hand derivation is @{text "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> \<forall>[Y<:S\<^isub>1].S\<^isub>2 <: \<forall>[Y<:T\<^isub>1].T\<^isub>2"} |
18621 | 1045 |
and therfore we know that the binder @{term Y} is fresh for @{term "\<Delta>@[(X,Q)]@\<Gamma>"}. By |
1046 |
the inner induction hypothesis we have that @{term "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"} and |
|
1047 |
@{term "((Y,T\<^isub>1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. Since @{term P} is a subtype of @{term Q} |
|
1048 |
we can infer that @{term Y} is fresh for @{term P} and thus also fresh for |
|
1049 |
@{term "\<Delta>@[(X,P)]@\<Gamma>"}. We can then conclude by applying rule @{text "S_Forall"}. |
|
1050 |
\end{minipage}*} |
|
1051 |
hence IH_inner\<^isub>1: "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" |
|
1052 |
and IH_inner\<^isub>2: "((Y,T\<^isub>1)#\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" |
|
1053 |
and lh_drv_prm: "Y\<sharp>(\<Delta>@[(X,Q)]@\<Gamma>)" by force+ |
|
18424 | 1054 |
have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact |
18621 | 1055 |
hence "Y\<sharp>P" using lh_drv_prm by (simp only: fresh_list_append subtype_implies_fresh) |
1056 |
hence "Y\<sharp>(\<Delta>@[(X,P)]@\<Gamma>)" using lh_drv_prm |
|
18424 | 1057 |
by (simp add: fresh_list_append fresh_list_cons fresh_prod) |
18621 | 1058 |
with IH_inner\<^isub>1 IH_inner\<^isub>2 |
1059 |
show "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> \<forall>[Y<:S\<^isub>1].S\<^isub>2 <: \<forall>[Y<:T\<^isub>1].T\<^isub>2" by (simp add: subtype_of.S_Forall) |
|
18246 | 1060 |
qed |
18621 | 1061 |
} |
18246 | 1062 |
qed |
1063 |
||
18416 | 1064 |
end |