author | urbanc |
Tue, 08 Jan 2008 23:11:08 +0100 | |
changeset 25867 | c24395ea4e71 |
parent 25858 | 6704045112a8 |
child 26763 | fba4995cb0f9 |
permissions | -rw-r--r-- |
25722 | 1 |
(* $Id$ *) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
2 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
3 |
theory Contexts |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
4 |
imports "../Nominal" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
5 |
begin |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
6 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
7 |
text {* |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
8 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
9 |
We show here that the Plotkin-style of defining |
25751 | 10 |
reduction relations (based on congruence rules) is |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
11 |
equivalent to the Felleisen-Hieb-style representation |
25858 | 12 |
(based on contexts), and show cbv-evaluation via a |
25867 | 13 |
CK-machine described by Roshan James. |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
14 |
|
25751 | 15 |
The interesting point is that contexts do not contain |
16 |
any binders. On the other hand the operation of filling |
|
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
17 |
a term into a context produces an alpha-equivalent term. |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
18 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
19 |
*} |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
20 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
21 |
atom_decl name |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
22 |
|
25867 | 23 |
text {* |
24 |
Lambda-Terms - the Lam-term constructor binds a name |
|
25 |
*} |
|
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
26 |
nominal_datatype lam = |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
27 |
Var "name" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
28 |
| App "lam" "lam" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
29 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
30 |
|
25751 | 31 |
text {* |
25867 | 32 |
Contexts - the lambda case in contexts does not bind a name, |
33 |
even if we introduce the notation [_]._ for CLam. |
|
25751 | 34 |
*} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
35 |
nominal_datatype ctx = |
25858 | 36 |
Hole ("\<box>" 1000) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
37 |
| CAppL "ctx" "lam" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
38 |
| CAppR "lam" "ctx" |
25722 | 39 |
| CLam "name" "ctx" ("CLam [_]._" [100,100] 100) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
40 |
|
25867 | 41 |
text {* Capture-avoiding substitution *} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
42 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
43 |
consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
44 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
45 |
nominal_primrec |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
46 |
"(Var x)[y::=s] = (if x=y then s else (Var x))" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
47 |
"(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
48 |
"x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
49 |
apply(finite_guess)+ |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
50 |
apply(rule TrueI)+ |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
51 |
apply(simp add: abs_fresh) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
52 |
apply(fresh_guess)+ |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
53 |
done |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
54 |
|
25867 | 55 |
text {* |
56 |
Filling is the operation that fills a term into a hole. |
|
57 |
This operation is possibly capturing. |
|
58 |
*} |
|
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
59 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
60 |
consts |
25751 | 61 |
filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
62 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
63 |
nominal_primrec |
25858 | 64 |
"\<box><t> = t" |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
65 |
"(CAppL E t')<t> = App (E<t>) t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
66 |
"(CAppR t' E)<t> = App t' (E<t>)" |
25722 | 67 |
"(CLam [x].E)<t> = Lam [x].(E<t>)" |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
68 |
by (rule TrueI)+ |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
69 |
|
25858 | 70 |
text {* |
71 |
While contexts themselves are not alpha-equivalence classes, the |
|
72 |
filling operation produces an alpha-equivalent lambda-term. |
|
73 |
*} |
|
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
74 |
lemma alpha_test: |
25858 | 75 |
shows "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)" |
76 |
and "(CLam [x].\<box>)<Var x> = (CLam [y].\<box>)<Var y>" |
|
77 |
by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm) |
|
25722 | 78 |
|
25867 | 79 |
text {* The composition of two contexts. *} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
80 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
81 |
consts |
25867 | 82 |
ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
83 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
84 |
nominal_primrec |
25858 | 85 |
"\<box> \<circ> E' = E'" |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
86 |
"(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
87 |
"(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
88 |
"(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
89 |
by (rule TrueI)+ |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
90 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
91 |
lemma ctx_compose: |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
92 |
shows "E1<E2<t>> = (E1 \<circ> E2)<t>" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
93 |
by (induct E1 rule: ctx.weak_induct) (auto) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
94 |
|
25751 | 95 |
text {* Beta-reduction via contexts in the Felleisen-Hieb style. *} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
96 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
97 |
inductive |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
98 |
ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
99 |
where |
25858 | 100 |
xbeta[intro]: "E<App (Lam [x].t) t'> \<longrightarrow>x E<t[x::=t']>" |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
101 |
|
25751 | 102 |
text {* Beta-reduction via congruence rules in the Plotkin style. *} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
103 |
|
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
104 |
inductive |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
105 |
cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
106 |
where |
25858 | 107 |
obeta[intro]: "App (Lam [x].t) t' \<longrightarrow>o t[x::=t']" |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
108 |
| oapp1[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t t2 \<longrightarrow>o App t' t2" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
109 |
| oapp2[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t2 t \<longrightarrow>o App t2 t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
110 |
| olam[intro]: "t \<longrightarrow>o t' \<Longrightarrow> Lam [x].t \<longrightarrow>o Lam [x].t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
111 |
|
25751 | 112 |
text {* The proof that shows both relations are equal. *} |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
113 |
|
25858 | 114 |
lemma cong_red_in_ctx: |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
115 |
assumes a: "t \<longrightarrow>o t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
116 |
shows "E<t> \<longrightarrow>o E<t'>" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
117 |
using a |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
118 |
by (induct E rule: ctx.weak_induct) (auto) |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
119 |
|
25858 | 120 |
lemma ctx_red_in_ctx: |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
121 |
assumes a: "t \<longrightarrow>x t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
122 |
shows "E<t> \<longrightarrow>x E<t'>" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
123 |
using a |
25858 | 124 |
by (induct) (auto simp add: ctx_compose) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
125 |
|
25858 | 126 |
theorem ctx_red_implies_cong_red: |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
127 |
assumes a: "t \<longrightarrow>x t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
128 |
shows "t \<longrightarrow>o t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
129 |
using a |
25858 | 130 |
by (induct) (auto intro!: cong_red_in_ctx) |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
131 |
|
25858 | 132 |
theorem cong_red_implies_ctx_red: |
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
133 |
assumes a: "t \<longrightarrow>o t'" |
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
134 |
shows "t \<longrightarrow>x t'" |
25858 | 135 |
using a |
136 |
proof (induct) |
|
137 |
case (obeta x t' t) |
|
138 |
have "\<box><App (Lam [x].t) t'> \<longrightarrow>x \<box><t[x::=t']>" by (rule xbeta) |
|
139 |
then show "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp |
|
140 |
qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *) |
|
141 |
||
25867 | 142 |
section {* We now use context in a CBV list machine *} |
25858 | 143 |
|
144 |
text {* First the function that composes a list of contexts *} |
|
145 |
||
146 |
primrec |
|
25867 | 147 |
ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>" [80] 80) |
148 |
where |
|
149 |
"[]\<down> = \<box>" |
|
150 |
| "(E#Es)\<down> = (Es\<down>) \<circ> E" |
|
25858 | 151 |
|
152 |
text {* Values *} |
|
153 |
inductive |
|
154 |
val :: "lam\<Rightarrow>bool" |
|
155 |
where |
|
156 |
v_Lam[intro]: "val (Lam [x].e)" |
|
157 |
| v_Var[intro]: "val (Var x)" |
|
158 |
||
25867 | 159 |
text {* CBV-reduction using contexts *} |
25858 | 160 |
inductive |
161 |
cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _" [80,80] 80) |
|
162 |
where |
|
163 |
cbv_beta[intro]: "val v \<Longrightarrow> E<App (Lam [x].e) v> \<longrightarrow>cbv E<e[x::=v]>" |
|
164 |
||
165 |
text {* reflexive, transitive closure of CBV reduction *} |
|
166 |
inductive |
|
167 |
"cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _" [80,80] 80) |
|
168 |
where |
|
169 |
cbvs1[intro]: "e \<longrightarrow>cbv* e" |
|
170 |
| cbvs2[intro]: "e \<longrightarrow>cbv e' \<Longrightarrow> e \<longrightarrow>cbv* e'" |
|
171 |
| cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3" |
|
172 |
||
25867 | 173 |
text {* A little CK-machine, which builds up a list of evaluation contexts. *} |
25858 | 174 |
inductive |
175 |
machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>" [60,60,60,60] 60) |
|
176 |
where |
|
177 |
m1[intro]: "<App e1 e2, Es> \<mapsto> <e1,(CAppL \<box> e2)#Es>" |
|
178 |
| m2[intro]: "val v \<Longrightarrow> <v,(CAppL \<box> e2)#Es> \<mapsto> <e2,(CAppR v \<box>)#Es>" |
|
179 |
| m3[intro]: "val v \<Longrightarrow> <v,(CAppR (Lam [x].e) \<box>)#Es> \<mapsto> <e[x::=v],Es>" |
|
180 |
||
181 |
lemma machine_red_implies_cbv_reds_aux: |
|
182 |
assumes a: "<e,Es> \<mapsto> <e',Es'>" |
|
183 |
shows "(Es\<down>)<e> \<longrightarrow>cbv* (Es'\<down>)<e'>" |
|
184 |
using a |
|
185 |
by (induct) (auto simp add: ctx_compose[symmetric]) |
|
186 |
||
187 |
lemma machine_execution_implies_cbv_reds: |
|
188 |
assumes a: "<e,[]> \<mapsto> <e',[]>" |
|
189 |
shows "e \<longrightarrow>cbv* e'" |
|
190 |
using a |
|
191 |
by (auto dest: machine_red_implies_cbv_reds_aux) |
|
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
192 |
|
25867 | 193 |
text {* |
194 |
One would now like to show something about the opposite |
|
195 |
direction, by according to Amr Sabry this amounts to |
|
196 |
showing a standardisation lemma, which is hard. |
|
197 |
*} |
|
198 |
||
25499
7e0ad4838ce9
an example file for how to treat Felleisen-Hieb-style contexts
urbanc
parents:
diff
changeset
|
199 |
end |