|
1 (* $Id$ *) |
|
2 |
|
3 theory CK_Machine |
|
4 imports "../Nominal" |
|
5 begin |
|
6 |
|
7 text {* |
|
8 |
|
9 This theory establishes soundness and completeness for a CK-machine |
|
10 with respect to a cbv-big-step semantics. The language includes |
|
11 functions, recursion, booleans and numbers. In the soundness proof |
|
12 the small-step cbv-reduction relation is used to get the induction |
|
13 through. Type preservation is proved for the machine and also for |
|
14 the small- and big-step semantics. |
|
15 |
|
16 The theory is inspired by notes of Roshan James from Indiana University |
|
17 and the lecture notes by Andy Pitts for his semantics course. See |
|
18 |
|
19 http://www.cs.indiana.edu/~rpjames/lm.pdf |
|
20 http://www.cl.cam.ac.uk/teaching/2001/Semantics/ |
|
21 |
|
22 *} |
|
23 |
|
24 atom_decl name |
|
25 |
|
26 nominal_datatype lam = |
|
27 VAR "name" |
|
28 | APP "lam" "lam" |
|
29 | LAM "\<guillemotleft>name\<guillemotright>lam" ("LAM [_]._") |
|
30 | NUM "nat" |
|
31 | DIFF "lam" "lam" ("_ -- _") |
|
32 | PLUS "lam" "lam" ("_ ++ _") |
|
33 | TRUE |
|
34 | FALSE |
|
35 | IF "lam" "lam" "lam" |
|
36 | FIX "\<guillemotleft>name\<guillemotright>lam" ("FIX [_]._") |
|
37 | ZET "lam" (* zero test *) |
|
38 | EQI "lam" "lam" (* equality test on numbers *) |
|
39 |
|
40 section {* Capture-Avoiding Substitution *} |
|
41 |
|
42 consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
|
43 |
|
44 nominal_primrec |
|
45 "(VAR x)[y::=s] = (if x=y then s else (VAR x))" |
|
46 "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" |
|
47 "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])" |
|
48 "(NUM n)[y::=s] = NUM n" |
|
49 "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])" |
|
50 "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])" |
|
51 "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])" |
|
52 "TRUE[y::=s] = TRUE" |
|
53 "FALSE[y::=s] = FALSE" |
|
54 "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])" |
|
55 "(ZET t)[y::=s] = ZET (t[y::=s])" |
|
56 "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])" |
|
57 apply(finite_guess)+ |
|
58 apply(rule TrueI)+ |
|
59 apply(simp add: abs_fresh)+ |
|
60 apply(fresh_guess)+ |
|
61 done |
|
62 |
|
63 lemma subst_eqvt[eqvt]: |
|
64 fixes pi::"name prm" |
|
65 shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]" |
|
66 by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct) |
|
67 (auto simp add: perm_bij fresh_atm fresh_bij) |
|
68 |
|
69 lemma fresh_fact: |
|
70 fixes z::"name" |
|
71 shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]" |
|
72 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
|
73 (auto simp add: abs_fresh fresh_prod fresh_atm fresh_nat) |
|
74 |
|
75 lemma subst_rename: |
|
76 assumes a: "y\<sharp>t" |
|
77 shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]" |
|
78 using a |
|
79 by (nominal_induct t avoiding: x y s rule: lam.strong_induct) |
|
80 (auto simp add: calc_atm fresh_atm abs_fresh perm_nat_def) |
|
81 |
|
82 section {* Evaluation Contexts *} |
|
83 |
|
84 datatype ctx = |
|
85 Hole ("\<box>") |
|
86 | CAPPL "ctx" "lam" |
|
87 | CAPPR "lam" "ctx" |
|
88 | CDIFFL "ctx" "lam" |
|
89 | CDIFFR "lam" "ctx" |
|
90 | CPLUSL "ctx" "lam" |
|
91 | CPLUSR "lam" "ctx" |
|
92 | CIF "ctx" "lam" "lam" |
|
93 | CZET "ctx" |
|
94 | CEQIL "ctx" "lam" |
|
95 | CEQIR "lam" "ctx" |
|
96 |
|
97 fun |
|
98 filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>") |
|
99 where |
|
100 "\<box>\<lbrakk>t\<rbrakk> = t" |
|
101 | "(CAPPL E t')\<lbrakk>t\<rbrakk> = APP (E\<lbrakk>t\<rbrakk>) t'" |
|
102 | "(CAPPR t' E)\<lbrakk>t\<rbrakk> = APP t' (E\<lbrakk>t\<rbrakk>)" |
|
103 | "(CDIFFL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) -- t'" |
|
104 | "(CDIFFR t' E)\<lbrakk>t\<rbrakk> = t' -- (E\<lbrakk>t\<rbrakk>)" |
|
105 | "(CPLUSL E t')\<lbrakk>t\<rbrakk> = (E\<lbrakk>t\<rbrakk>) ++ t'" |
|
106 | "(CPLUSR t' E)\<lbrakk>t\<rbrakk> = t' ++ (E\<lbrakk>t\<rbrakk>)" |
|
107 | "(CIF E t1 t2)\<lbrakk>t\<rbrakk> = IF (E\<lbrakk>t\<rbrakk>) t1 t2" |
|
108 | "(CZET E)\<lbrakk>t\<rbrakk> = ZET (E\<lbrakk>t\<rbrakk>)" |
|
109 | "(CEQIL E t')\<lbrakk>t\<rbrakk> = EQI (E\<lbrakk>t\<rbrakk>) t'" |
|
110 | "(CEQIR t' E)\<lbrakk>t\<rbrakk> = EQI t' (E\<lbrakk>t\<rbrakk>)" |
|
111 |
|
112 fun |
|
113 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _") |
|
114 where |
|
115 "\<box> \<circ> E' = E'" |
|
116 | "(CAPPL E t') \<circ> E' = CAPPL (E \<circ> E') t'" |
|
117 | "(CAPPR t' E) \<circ> E' = CAPPR t' (E \<circ> E')" |
|
118 | "(CDIFFL E t') \<circ> E' = CDIFFL (E \<circ> E') t'" |
|
119 | "(CDIFFR t' E) \<circ> E' = CDIFFR t' (E \<circ> E')" |
|
120 | "(CPLUSL E t') \<circ> E' = CPLUSL (E \<circ> E') t'" |
|
121 | "(CPLUSR t' E) \<circ> E' = CPLUSR t' (E \<circ> E')" |
|
122 | "(CIF E t1 t2) \<circ> E' = CIF (E \<circ> E') t1 t2" |
|
123 | "(CZET E) \<circ> E' = CZET (E \<circ> E')" |
|
124 | "(CEQIL E t') \<circ> E' = CEQIL (E \<circ> E') t'" |
|
125 | "(CEQIR t' E) \<circ> E' = CEQIR t' (E \<circ> E')" |
|
126 |
|
127 lemma ctx_compose: |
|
128 shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" |
|
129 by (induct E1 rule: ctx.induct) (auto) |
|
130 |
|
131 fun |
|
132 ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>") |
|
133 where |
|
134 "[]\<down> = \<box>" |
|
135 | "(E#Es)\<down> = (Es\<down>) \<circ> E" |
|
136 |
|
137 section {* CK Machine *} |
|
138 |
|
139 inductive |
|
140 val :: "lam\<Rightarrow>bool" |
|
141 where |
|
142 v_LAM[intro]: "val (LAM [x].e)" |
|
143 | v_NUM[intro]: "val (NUM n)" |
|
144 | v_FALSE[intro]: "val FALSE" |
|
145 | v_TRUE[intro]: "val TRUE" |
|
146 |
|
147 equivariance val |
|
148 |
|
149 inductive |
|
150 machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>") |
|
151 where |
|
152 m1[intro]: "<APP e1 e2,Es> \<mapsto> <e1,(CAPPL \<box> e2)#Es>" |
|
153 | m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<mapsto> <e2,(CAPPR v \<box>)#Es>" |
|
154 | m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<mapsto> <e[y::=v],Es>" |
|
155 | m4[intro]: "<e1 -- e2, Es> \<mapsto> <e1,(CDIFFL \<box> e2)#Es>" |
|
156 | m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<mapsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>" |
|
157 | m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1 - n2),Es>" |
|
158 | m4'[intro]:"<e1 ++ e2, Es> \<mapsto> <e1,(CPLUSL \<box> e2)#Es>" |
|
159 | m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<mapsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>" |
|
160 | m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1+n2),Es>" |
|
161 | m7[intro]: "<IF e1 e2 e3,Es> \<mapsto> <e1,(CIF \<box> e2 e3)#Es>" |
|
162 | m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<mapsto> <e1,Es>" |
|
163 | m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<mapsto> <e2,Es>" |
|
164 | mA[intro]: "<FIX [x].t,Es> \<mapsto> <t[x::=FIX [x].t],Es>" |
|
165 | mB[intro]: "<ZET e,Es> \<mapsto> <e,(CZET \<box>)#Es>" |
|
166 | mC[intro]: "<NUM 0,(CZET \<box>)#Es> \<mapsto> <TRUE,Es>" |
|
167 | mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZET \<box>)#Es> \<mapsto> <FALSE,Es>" |
|
168 | mE[intro]: "<EQI e1 e2,Es> \<mapsto> <e1,(CEQIL \<box> e2)#Es>" |
|
169 | mF[intro]: "<NUM n1,(CEQIL \<box> e2)#Es> \<mapsto> <e2,(CEQIR (NUM n1) \<box>)#Es>" |
|
170 | mG[intro]: "<NUM n,(CEQIR (NUM n) \<box>)#Es> \<mapsto> <TRUE,Es>" |
|
171 | mH[intro]: "n1\<noteq>n2 \<Longrightarrow> <NUM n1,(CEQIR (NUM n2) \<box>)#Es> \<mapsto> <FALSE,Es>" |
|
172 |
|
173 inductive |
|
174 "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto>* <_,_>") |
|
175 where |
|
176 ms1[intro]: "<e,Es> \<mapsto>* <e,Es>" |
|
177 | ms2[intro]: "\<lbrakk><e1,Es1> \<mapsto> <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>" |
|
178 |
|
179 lemma ms3[intro,trans]: |
|
180 assumes a: "<e1,Es1> \<mapsto>* <e2,Es2>" "<e2,Es2> \<mapsto>* <e3,Es3>" |
|
181 shows "<e1,Es1> \<mapsto>* <e3,Es3>" |
|
182 using a by (induct) (auto) |
|
183 |
|
184 lemma ms4[intro]: |
|
185 assumes a: "<e1,Es1> \<mapsto> <e2,Es2>" |
|
186 shows "<e1,Es1> \<mapsto>* <e2,Es2>" |
|
187 using a by (rule ms2) (rule ms1) |
|
188 |
|
189 section {* Evaluation Relation *} |
|
190 |
|
191 inductive |
|
192 eval :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<Down> _") |
|
193 where |
|
194 eval_NUM[intro]: "NUM n \<Down> NUM n" |
|
195 | eval_DIFF[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 -- t2 \<Down> NUM (n1 - n2)" |
|
196 | eval_PLUS[intro]: "\<lbrakk>t1 \<Down> (NUM n1); t2 \<Down> (NUM n2)\<rbrakk> \<Longrightarrow> t1 ++ t2 \<Down> NUM (n1 + n2)" |
|
197 | eval_LAM[intro]: "LAM [x].t \<Down> LAM [x].t" |
|
198 | eval_APP[intro]: "\<lbrakk>t1\<Down> LAM [x].t; t2\<Down> t2'; t[x::=t2']\<Down> t'\<rbrakk> \<Longrightarrow> APP t1 t2 \<Down> t'" |
|
199 | eval_FIX[intro]: "t[x::= FIX [x].t] \<Down> t' \<Longrightarrow> FIX [x].t \<Down> t'" |
|
200 | eval_IF1[intro]: "\<lbrakk>t1 \<Down> TRUE; t2 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'" |
|
201 | eval_IF2[intro]: "\<lbrakk>t1 \<Down> FALSE; t3 \<Down> t'\<rbrakk> \<Longrightarrow> IF t1 t2 t3 \<Down> t'" |
|
202 | eval_TRUE[intro]: "TRUE \<Down> TRUE" |
|
203 | eval_FALSE[intro]:"FALSE \<Down> FALSE" |
|
204 | eval_ZET1[intro]: "t \<Down> NUM 0 \<Longrightarrow> ZET t \<Down> TRUE" |
|
205 | eval_ZET2[intro]: "\<lbrakk>t \<Down> NUM n; 0 < n\<rbrakk> \<Longrightarrow> ZET t \<Down> FALSE" |
|
206 | eval_EQ1[intro]: "\<lbrakk>t1 \<Down> NUM n; t2 \<Down> NUM n\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> TRUE" |
|
207 | eval_EQ2[intro]: "\<lbrakk>t1 \<Down> NUM n1; t2 \<Down> NUM n2; n1\<noteq>n2\<rbrakk> \<Longrightarrow> EQI t1 t2 \<Down> FALSE" |
|
208 |
|
209 declare lam.inject[simp] |
|
210 inductive_cases eval_elim: |
|
211 "APP t1 t2 \<Down> t'" |
|
212 "IF t1 t2 t3 \<Down> t'" |
|
213 "ZET t \<Down> t'" |
|
214 "EQI t1 t2 \<Down> t'" |
|
215 "t1 ++ t2 \<Down> t'" |
|
216 "t1 -- t2 \<Down> t'" |
|
217 "(NUM n) \<Down> t" |
|
218 "TRUE \<Down> t" |
|
219 "FALSE \<Down> t" |
|
220 declare lam.inject[simp del] |
|
221 |
|
222 lemma eval_to: |
|
223 assumes a: "t \<Down> t'" |
|
224 shows "val t'" |
|
225 using a by (induct) (auto) |
|
226 |
|
227 lemma eval_val: |
|
228 assumes a: "val t" |
|
229 shows "t \<Down> t" |
|
230 using a by (induct) (auto) |
|
231 |
|
232 theorem eval_implies_machine_star_ctx: |
|
233 assumes a: "t \<Down> t'" |
|
234 shows "<t,Es> \<mapsto>* <t',Es>" |
|
235 using a |
|
236 by (induct arbitrary: Es) |
|
237 (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+ |
|
238 |
|
239 text {* Completeness Property *} |
|
240 |
|
241 corollary eval_implies_machine_star: |
|
242 assumes a: "t \<Down> t'" |
|
243 shows "<t,[]> \<mapsto>* <t',[]>" |
|
244 using a by (auto dest: eval_implies_machine_star_ctx) |
|
245 |
|
246 section {* CBV Reduction Relation *} |
|
247 |
|
248 lemma less_eqvt[eqvt]: |
|
249 fixes pi::"name prm" |
|
250 and n1 n2::"nat" |
|
251 shows "(pi\<bullet>(n1 < n2)) = ((pi\<bullet>n1) < (pi\<bullet>n2))" |
|
252 by (simp add: perm_nat_def perm_bool) |
|
253 |
|
254 inductive |
|
255 cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _") |
|
256 where |
|
257 cbv1': "\<lbrakk>val v; x\<sharp>v\<rbrakk> \<Longrightarrow> APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" |
|
258 | cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t t2 \<longrightarrow>cbv APP t' t2" |
|
259 | cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> APP t2 t \<longrightarrow>cbv APP t2 t'" |
|
260 | cbv4[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t -- t2 \<longrightarrow>cbv t' -- t2" |
|
261 | cbv5[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 -- t \<longrightarrow>cbv t2 -- t'" |
|
262 | cbv6[intro]: "(NUM n1) -- (NUM n2) \<longrightarrow>cbv NUM (n1 - n2)" |
|
263 | cbv4'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t ++ t2 \<longrightarrow>cbv t' ++ t2" |
|
264 | cbv5'[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> t2 ++ t \<longrightarrow>cbv t2 ++ t'" |
|
265 | cbv6'[intro]:"(NUM n1) ++ (NUM n2) \<longrightarrow>cbv NUM (n1 + n2)" |
|
266 | cbv7[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> IF t t1 t2 \<longrightarrow>cbv IF t' t1 t2" |
|
267 | cbv8[intro]: "IF TRUE t1 t2 \<longrightarrow>cbv t1" |
|
268 | cbv9[intro]: "IF FALSE t1 t2 \<longrightarrow>cbv t2" |
|
269 | cbvA[intro]: "FIX [x].t \<longrightarrow>cbv t[x::=FIX [x].t]" |
|
270 | cbvB[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> ZET t \<longrightarrow>cbv ZET t'" |
|
271 | cbvC[intro]: "ZET (NUM 0) \<longrightarrow>cbv TRUE" |
|
272 | cbvD[intro]: "0 < n \<Longrightarrow> ZET (NUM n) \<longrightarrow>cbv FALSE" |
|
273 | cbvE[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t t2 \<longrightarrow>cbv EQI t' t2" |
|
274 | cbvF[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> EQI t2 t \<longrightarrow>cbv EQI t2 t'" |
|
275 | cbvG[intro]: "EQI (NUM n) (NUM n) \<longrightarrow>cbv TRUE" |
|
276 | cbvH[intro]: "n1\<noteq>n2 \<Longrightarrow> EQI (NUM n1) (NUM n2) \<longrightarrow>cbv FALSE" |
|
277 |
|
278 equivariance cbv |
|
279 nominal_inductive cbv |
|
280 by (simp_all add: abs_fresh fresh_fact) |
|
281 |
|
282 lemma cbv1[intro]: |
|
283 assumes a: "val v" |
|
284 shows "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" |
|
285 proof - |
|
286 obtain y::"name" where fs: "y\<sharp>(x,t,v)" by (rule exists_fresh, rule fin_supp, blast) |
|
287 have "APP (LAM [x].t) v = APP (LAM [y].([(y,x)]\<bullet>t)) v" using fs |
|
288 by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) |
|
289 also have "\<dots> \<longrightarrow>cbv ([(y,x)]\<bullet>t)[y::=v]" using fs a by (auto simp add: cbv.eqvt cbv1') |
|
290 also have "\<dots> = t[x::=v]" using fs by (simp add: subst_rename[symmetric]) |
|
291 finally show "APP (LAM [x].t) v \<longrightarrow>cbv t[x::=v]" by simp |
|
292 qed |
|
293 |
|
294 inductive |
|
295 "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _") |
|
296 where |
|
297 cbvs1[intro]: "e \<longrightarrow>cbv* e" |
|
298 | cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3" |
|
299 |
|
300 lemma cbvs3[intro,trans]: |
|
301 assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3" |
|
302 shows "e1 \<longrightarrow>cbv* e3" |
|
303 using a by (induct) (auto) |
|
304 |
|
305 lemma cbv_in_ctx: |
|
306 assumes a: "t \<longrightarrow>cbv t'" |
|
307 shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" |
|
308 using a by (induct E) (auto) |
|
309 |
|
310 lemma machine_implies_cbv_star_ctx: |
|
311 assumes a: "<e,Es> \<mapsto> <e',Es'>" |
|
312 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
|
313 using a by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx) |
|
314 |
|
315 lemma machine_star_implies_cbv_star_ctx: |
|
316 assumes a: "<e,Es> \<mapsto>* <e',Es'>" |
|
317 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
|
318 using a |
|
319 by (induct) (auto dest: machine_implies_cbv_star_ctx) |
|
320 |
|
321 lemma machine_star_implies_cbv_star: |
|
322 assumes a: "<e,[]> \<mapsto>* <e',[]>" |
|
323 shows "e \<longrightarrow>cbv* e'" |
|
324 using a by (auto dest: machine_star_implies_cbv_star_ctx) |
|
325 |
|
326 lemma cbv_eval: |
|
327 assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3" |
|
328 shows "t1 \<Down> t3" |
|
329 using a |
|
330 by (induct arbitrary: t3) |
|
331 (auto elim!: eval_elim intro: eval_val) |
|
332 |
|
333 lemma cbv_star_eval: |
|
334 assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3" |
|
335 shows "t1 \<Down> t3" |
|
336 using a by (induct) (auto simp add: cbv_eval) |
|
337 |
|
338 lemma cbv_star_implies_eval: |
|
339 assumes a: "t \<longrightarrow>cbv* v" "val v" |
|
340 shows "t \<Down> v" |
|
341 using a |
|
342 by (induct) |
|
343 (auto simp add: eval_val cbv_star_eval dest: cbvs2) |
|
344 |
|
345 text {* Soundness Property *} |
|
346 |
|
347 theorem machine_star_implies_eval: |
|
348 assumes a: "<t1,[]> \<mapsto>* <t2,[]>" |
|
349 and b: "val t2" |
|
350 shows "t1 \<Down> t2" |
|
351 proof - |
|
352 from a have "t1 \<longrightarrow>cbv* t2" by (simp add: machine_star_implies_cbv_star) |
|
353 then show "t1 \<Down> t2" using b by (simp add: cbv_star_implies_eval) |
|
354 qed |
|
355 |
|
356 section {* Typing *} |
|
357 |
|
358 nominal_datatype ty = |
|
359 tVAR "string" |
|
360 | tBOOL |
|
361 | tINT |
|
362 | tARR "ty" "ty" ("_ \<rightarrow> _") |
|
363 |
|
364 declare ty.inject[simp] |
|
365 |
|
366 lemma ty_fresh: |
|
367 fixes x::"name" |
|
368 and T::"ty" |
|
369 shows "x\<sharp>T" |
|
370 by (induct T rule: ty.induct) |
|
371 (auto simp add: fresh_string) |
|
372 |
|
373 types tctx = "(name\<times>ty) list" |
|
374 |
|
375 abbreviation |
|
376 "sub_tctx" :: "tctx \<Rightarrow> tctx \<Rightarrow> bool" ("_ \<subseteq> _") |
|
377 where |
|
378 "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2" |
|
379 |
|
380 inductive |
|
381 valid :: "tctx \<Rightarrow> bool" |
|
382 where |
|
383 v1[intro]: "valid []" |
|
384 | v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)" |
|
385 |
|
386 equivariance valid |
|
387 |
|
388 lemma valid_elim[dest]: |
|
389 assumes a: "valid ((x,T)#\<Gamma>)" |
|
390 shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>" |
|
391 using a by (cases) (auto) |
|
392 |
|
393 lemma valid_insert: |
|
394 assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)" |
|
395 shows "valid (\<Delta> @ \<Gamma>)" |
|
396 using a |
|
397 by (induct \<Delta>) |
|
398 (auto simp add: fresh_list_append fresh_list_cons dest!: valid_elim) |
|
399 |
|
400 lemma fresh_set: |
|
401 shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)" |
|
402 by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) |
|
403 |
|
404 lemma context_unique: |
|
405 assumes a1: "valid \<Gamma>" |
|
406 and a2: "(x,T) \<in> set \<Gamma>" |
|
407 and a3: "(x,U) \<in> set \<Gamma>" |
|
408 shows "T = U" |
|
409 using a1 a2 a3 |
|
410 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm) |
|
411 |
|
412 section {* Typing Relation *} |
|
413 |
|
414 inductive |
|
415 typing :: "tctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") |
|
416 where |
|
417 t_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> VAR x : T" |
|
418 | t_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> APP t\<^isub>1 t\<^isub>2 : T\<^isub>2" |
|
419 | t_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> LAM [x].t : T\<^isub>1 \<rightarrow> T\<^isub>2" |
|
420 | t_NUM[intro]: "\<Gamma> \<turnstile> (NUM n) : tINT" |
|
421 | t_DIFF[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : tINT; \<Gamma> \<turnstile> t\<^isub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 -- t\<^isub>2 : tINT" |
|
422 | t_PLUS[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : tINT; \<Gamma> \<turnstile> t\<^isub>2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 ++ t\<^isub>2 : tINT" |
|
423 | t_TRUE[intro]: "\<Gamma> \<turnstile> TRUE : tBOOL" |
|
424 | t_FALSE[intro]: "\<Gamma> \<turnstile> FALSE : tBOOL" |
|
425 | t_IF[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : tBOOL; \<Gamma> \<turnstile> t2 : T; \<Gamma> \<turnstile> t3 : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> IF t1 t2 t3 : T" |
|
426 | t_ZET[intro]: "\<Gamma> \<turnstile> t : tINT \<Longrightarrow> \<Gamma> \<turnstile> ZET t : tBOOL" |
|
427 | t_EQI[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : tINT; \<Gamma> \<turnstile> t2 : tINT\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> EQI t1 t2 : tBOOL" |
|
428 | t_FIX[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T)#\<Gamma> \<turnstile> t : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> FIX [x].t : T" |
|
429 |
|
430 declare lam.inject[simp] |
|
431 inductive_cases typing_inversion[elim]: |
|
432 "\<Gamma> \<turnstile> t\<^isub>1 -- t\<^isub>2 : T" |
|
433 "\<Gamma> \<turnstile> t\<^isub>1 ++ t\<^isub>2 : T" |
|
434 "\<Gamma> \<turnstile> IF t1 t2 t3 : T" |
|
435 "\<Gamma> \<turnstile> ZET t : T" |
|
436 "\<Gamma> \<turnstile> EQI t1 t2 : T" |
|
437 "\<Gamma> \<turnstile> APP t1 t2 : T" |
|
438 declare lam.inject[simp del] |
|
439 |
|
440 equivariance typing |
|
441 nominal_inductive typing |
|
442 by (simp_all add: abs_fresh ty_fresh) |
|
443 |
|
444 lemma t_LAM_inversion[dest]: |
|
445 assumes ty: "\<Gamma> \<turnstile> LAM [x].t : T" |
|
446 and fc: "x\<sharp>\<Gamma>" |
|
447 shows "\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" |
|
448 using ty fc |
|
449 by (cases rule: typing.strong_cases) |
|
450 (auto simp add: alpha lam.inject abs_fresh ty_fresh) |
|
451 |
|
452 lemma t_FIX_inversion[dest]: |
|
453 assumes ty: "\<Gamma> \<turnstile> FIX [x].t : T" |
|
454 and fc: "x\<sharp>\<Gamma>" |
|
455 shows "(x,T)#\<Gamma> \<turnstile> t : T" |
|
456 using ty fc |
|
457 by (cases rule: typing.strong_cases) |
|
458 (auto simp add: alpha lam.inject abs_fresh ty_fresh) |
|
459 |
|
460 section {* Type Preservation for the CBV Reduction Relation *} |
|
461 |
|
462 lemma weakening: |
|
463 fixes \<Gamma>1 \<Gamma>2::"tctx" |
|
464 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
465 and b: "valid \<Gamma>2" |
|
466 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
|
467 shows "\<Gamma>2 \<turnstile> t : T" |
|
468 using a b c |
|
469 by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
|
470 (auto | atomize)+ |
|
471 |
|
472 lemma type_substitution_aux: |
|
473 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" |
|
474 and b: "\<Gamma> \<turnstile> e' : T'" |
|
475 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" |
|
476 using a b |
|
477 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
|
478 case (t_VAR \<Gamma>' y T x e' \<Delta>) |
|
479 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" |
|
480 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" |
|
481 and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all |
|
482 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) |
|
483 { assume eq: "x=y" |
|
484 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) |
|
485 with a3 have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using eq a4 by (auto intro: weakening) |
|
486 } |
|
487 moreover |
|
488 { assume ineq: "x\<noteq>y" |
|
489 from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp |
|
490 then have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using ineq a4 by auto |
|
491 } |
|
492 ultimately show "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" by blast |
|
493 qed (auto | force simp add: fresh_list_append fresh_list_cons)+ |
|
494 |
|
495 corollary type_substitution: |
|
496 assumes a: "(x,T')#\<Gamma> \<turnstile> e : T" |
|
497 and b: "\<Gamma> \<turnstile> e' : T'" |
|
498 shows "\<Gamma> \<turnstile> e[x::=e'] : T" |
|
499 using a b |
|
500 by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified]) |
|
501 |
|
502 theorem cbv_type_preservation: |
|
503 assumes a: "t \<longrightarrow>cbv t'" |
|
504 and b: "\<Gamma> \<turnstile> t : T" |
|
505 shows "\<Gamma> \<turnstile> t' : T" |
|
506 using a b |
|
507 apply(nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) |
|
508 apply(auto elim!: typing_inversion dest: t_LAM_inversion simp add: type_substitution) |
|
509 apply(frule t_FIX_inversion) |
|
510 apply(auto simp add: type_substitution) |
|
511 done |
|
512 |
|
513 corollary cbv_star_type_preservation: |
|
514 assumes a: "t \<longrightarrow>cbv* t'" |
|
515 and b: "\<Gamma> \<turnstile> t : T" |
|
516 shows "\<Gamma> \<turnstile> t' : T" |
|
517 using a b |
|
518 by (induct) (auto intro: cbv_type_preservation) |
|
519 |
|
520 section {* Type Preservation for the Machine and Evaluation Relation *} |
|
521 |
|
522 theorem machine_type_preservation: |
|
523 assumes a: "<t,[]> \<mapsto>* <t',[]>" |
|
524 and b: "\<Gamma> \<turnstile> t : T" |
|
525 shows "\<Gamma> \<turnstile> t' : T" |
|
526 proof - |
|
527 from a have "t \<longrightarrow>cbv* t'" by (simp add: machine_star_implies_cbv_star) |
|
528 then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbv_star_type_preservation) |
|
529 qed |
|
530 |
|
531 theorem eval_type_preservation: |
|
532 assumes a: "t \<Down> t'" |
|
533 and b: "\<Gamma> \<turnstile> t : T" |
|
534 shows "\<Gamma> \<turnstile> t' : T" |
|
535 proof - |
|
536 from a have "<t,[]> \<mapsto>* <t',[]>" by (simp add: eval_implies_machine_star) |
|
537 then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation) |
|
538 qed |
|
539 |
|
540 end |
|
541 |
|
542 |
|
543 |
|
544 |
|
545 |
|
546 |
|
547 |
|
548 |
|
549 |
|
550 |