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