theory Contexts
imports "HOL-Nominal.Nominal"
begin
text \<open>
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.
\<close>
atom_decl name
text \<open>
Lambda-Terms - the Lam-term constructor binds a name
\<close>
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\name\lam" ("Lam [_]._" [100,100] 100)
text \<open>
Contexts - the lambda case in contexts does not bind
a name, even if we introduce the notation [_]._ for CLam.
\<close>
nominal_datatype ctx =
Hole ("\" 1000)
| CAppL "ctx" "lam"
| CAppR "lam" "ctx"
| CLam "name" "ctx" ("CLam [_]._" [100,100] 100)
text \<open>Capture-Avoiding Substitution\<close>
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 \<open>
Filling is the operation that fills a term into a hole.
This operation is possibly capturing.
\<close>
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 \<open>
While contexts themselves are not alpha-equivalence classes, the
filling operation produces an alpha-equivalent lambda-term.
\<close>
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 \<open>The composition of two contexts.\<close>
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 \<open>Beta-reduction via contexts in the Felleisen-Hieb style.\<close>
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 \<open>Beta-reduction via congruence rules in the Plotkin style.\<close>
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 \<open>The proof that shows both relations are equal.\<close>
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
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
