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₁ t₂)[y::=s] = App (t₁[y::=s]) (t₂[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