# Theory Contexts

theory Contexts
imports Nominal
```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⇩1 t⇩2)[y::=s] = App (t⇩1[y::=s]) (t⇩2[y::=s])"
| "x♯(y,s) ⟹ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
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
```