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(simp add: fresh_nat) 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: fresh_def) apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]]) apply(simp add: supp_atm) 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) (simp_all add: lam.supp supp_atm abs_supp) 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(simp add: abs_fresh)+ 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) (simp_all add: eqvts fresh_bij) 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'])" by (simp_all add: fresh_list_cons fresh_list_nil) 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