# Theory Lam_Funs

theory Lam_Funs
imports Nominal
```theory Lam_Funs
imports "HOL-Nominal.Nominal"
begin

text ‹
Provides useful definitions for reasoning
with lambda-terms.
›

atom_decl name

nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "«name»lam" ("Lam [_]._" [100,100] 100)

text ‹The depth of a lambda-term.›

nominal_primrec
depth :: "lam ⇒ nat"
where
"depth (Var x) = 1"
| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
| "depth (Lam [a].t) = (depth t) + 1"
apply(finite_guess)+
apply(rule TrueI)+
apply(fresh_guess)+
done

text ‹
The free variables of a lambda-term. A complication in this
function arises from the fact that it returns a name set, which
is not a finitely supported type. Therefore we have to prove
the invariant that frees always returns a finite set of names.
›

nominal_primrec (invariant: "λs::name set. finite s")
frees :: "lam ⇒ name set"
where
"frees (Var a) = {a}"
| "frees (App t1 t2) = (frees t1) ∪ (frees t2)"
| "frees (Lam [a].t) = (frees t) - {a}"
apply(finite_guess)+
apply(simp)+
apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]])
apply(blast)
apply(fresh_guess)+
done

text ‹
We can avoid the definition of frees by
using the build in notion of support.
›

lemma frees_equals_support:
shows "frees t = supp t"
by (nominal_induct t rule: lam.strong_induct)

text ‹Parallel and single capture-avoiding substitution.›

fun
lookup :: "(name×lam) list ⇒ name ⇒ lam"
where
"lookup [] x        = Var x"
| "lookup ((y,e)#θ) x = (if x=y then e else lookup θ x)"

lemma lookup_eqvt[eqvt]:
fixes pi::"name prm"
and   θ::"(name×lam) list"
and   X::"name"
shows "pi∙(lookup θ X) = lookup (pi∙θ) (pi∙X)"
by (induct θ) (auto simp add: eqvts)

nominal_primrec
psubst :: "(name×lam) list ⇒ lam ⇒ lam"  ("_<_>" [95,95] 105)
where
"θ<(Var x)> = (lookup θ x)"
| "θ<(App e⇩1 e⇩2)> = App (θ<e⇩1>) (θ<e⇩2>)"
| "x♯θ ⟹ θ<(Lam [x].e)> = Lam [x].(θ<e>)"
apply(finite_guess)+
apply(rule TrueI)+
apply(fresh_guess)+
done

lemma psubst_eqvt[eqvt]:
fixes pi::"name prm"
and   t::"lam"
shows "pi∙(θ<t>) = (pi∙θ)<(pi∙t)>"
by (nominal_induct t avoiding: θ rule: lam.strong_induct)

abbreviation
subst :: "lam ⇒ name ⇒ lam ⇒ lam" ("_[_::=_]" [100,100,100] 100)
where
"t[x::=t']  ≡ ([(x,t')])<t>"

lemma subst[simp]:
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
and   "x♯(y,t') ⟹ (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"

lemma subst_supp:
shows "supp(t1[a::=t2]) ⊆ (((supp(t1)-{a})∪supp(t2))::name set)"
apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
apply(blast)+
done

text ‹
Contexts - lambda-terms with a single hole.
Note that the lambda case in contexts does not bind a
name, even if we introduce the notation [_]._ for CLam.
›
nominal_datatype clam =
Hole ("□" 1000)
| CAppL "clam" "lam"
| CAppR "lam" "clam"
| CLam "name" "clam"  ("CLam [_]._" [100,100] 100)

text ‹Filling a lambda-term into a context.›

nominal_primrec
filling :: "clam ⇒ 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 ‹Composition od two contexts›

nominal_primrec
clam_compose :: "clam ⇒ clam ⇒ clam" ("_ ∘ _" [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 clam_compose:
shows "(E1 ∘ E2)⟦t⟧ = E1⟦E2⟦t⟧⟧"
by (induct E1 rule: clam.induct) (auto)

end
```