theory Contexts
imports "HOL-Nominal.Nominal"
begin
text ‹
We
show here that the Plotkin-style of defining
beta-reduction (based on congruence rules)
is
equivalent
to the Felleisen-Hieb-style representation
(based on contexts).
The interesting point
in this
theory is that contexts
do not contain any binders. On the other hand the operation
of filling a
term into a
context produces an alpha-equivalent
term.
›
atom_decl name
text ‹
Lambda-Terms - the Lam-term constructor binds a name
›
nominal_datatype lam =
Var
"name"
| App
"lam" "lam"
| Lam
"\name\lam" (
‹Lam [_]._
› [100,100] 100)
text ‹
Contexts - the lambda
case in contexts does not bind
a name, even
if we introduce the
notation [_]._
for CLam.
›
nominal_datatype ctx =
Hole (
‹◻› 1000)
| CAppL
"ctx" "lam"
| CAppR
"lam" "ctx"
| CLam
"name" "ctx" (
‹CLam [_]._
› [100,100] 100)
text ‹Capture-Avoiding Substitution
›
nominal_primrec
subst ::
"lam \ name \ lam \ lam" (
‹_[_::=_]
› [100,100,100] 100)
where
"(Var x)[y::=s] = (if x=y then s else (Var x))"
|
"(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])"
|
"x\(y,s) \ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done
text ‹
Filling
is the operation that fills a
term into a hole.
This operation
is possibly capturing.
›
nominal_primrec
filling ::
"ctx \ lam \ lam" (
‹_
[_
]› [100,100] 100)
where
"\\t\ = t"
|
"(CAppL E t')\t\ = App (E\t\) t'"
|
"(CAppR t' E)\t\ = App t' (E\t\)"
|
"(CLam [x].E)\t\ = Lam [x].(E\t\)"
by (rule TrueI)+
text ‹
While contexts themselves are not alpha-equivalence
classes, the
filling operation produces an alpha-equivalent lambda-term.
›
lemma alpha_test:
shows "x\y \ (CLam [x].\) \ (CLam [y].\)"
and "(CLam [x].\)\Var x\ = (CLam [y].\)\Var y\"
by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm)
text ‹The composition of two contexts.
›
nominal_primrec
ctx_compose ::
"ctx \ ctx \ ctx" (
‹_
∘ _
› [100,100] 100)
where
"\ \ E' = E'"
|
"(CAppL E t') \ E' = CAppL (E \ E') t'"
|
"(CAppR t' E) \ E' = CAppR t' (E \ E')"
|
"(CLam [x].E) \ E' = CLam [x].(E \ E')"
by (rule TrueI)+
lemma ctx_compose:
shows "(E1 \ E2)\t\ = E1\E2\t\\"
by (induct E1 rule: ctx.induct) (auto)
text ‹Beta-reduction via contexts
in the Felleisen-Hieb style.
›
inductive
ctx_red ::
"lam\lam\bool" (
‹_
⟶x _
› [80,80] 80)
where
xbeta[intro]:
"E\App (Lam [x].t) t'\ \x E\t[x::=t']\"
text ‹Beta-reduction via congruence rules
in the Plotkin style.
›
inductive
cong_red ::
"lam\lam\bool" (
‹_
⟶o _
› [80,80] 80)
where
obeta[intro]:
"App (Lam [x].t) t' \o t[x::=t']"
| oapp1[intro]:
"t \o t' \ App t t2 \o App t' t2"
| oapp2[intro]:
"t \o t' \ App t2 t \o App t2 t'"
| olam[intro]:
"t \o t' \ Lam [x].t \o Lam [x].t'"
text ‹The
proof that
shows both relations are equal.
›
lemma cong_red_in_ctx:
assumes a:
"t \o t'"
shows "E\t\ \o E\t'\"
using a
by (induct E rule: ctx.induct) (auto)
lemma ctx_red_in_ctx:
assumes a:
"t \x t'"
shows "E\t\ \x E\t'\"
using a
by (induct) (auto simp add: ctx_compose[symmetric])
theorem ctx_red_implies_cong_red:
assumes a:
"t \x t'"
shows "t \o t'"
using a
by (induct) (auto intro: cong_red_in_ctx)
theorem cong_red_implies_ctx_red:
assumes a:
"t \o t'"
shows "t \x t'"
using a
proof (induct)
case (obeta x t
' t)
have "\\App (Lam [x].t) t'\ \x \\t[x::=t']\" by (rule xbeta)
then show "App (Lam [x].t) t' \x t[x::=t']" by simp
qed (metis ctx_red_in_ctx filling.simps)+
(* found by SledgeHammer *)
lemma ctx_existence:
assumes a:
"t \o t'"
shows "\C s s'. t = C\s\ \ t' = C\s'\ \ s \o s'"
using a
by (induct) (metis cong_red.
intros filling.simps)+
end
