|
theory Lam_Funs
imports "HOL-Nominal.Nominal"
begin
text \<open>
Provides useful definitions for reasoning
with lambda-terms.
\<close>
atom_decl name
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\name\lam" ("Lam [_]._" [100,100] 100)
text \<open>The depth of a lambda-term.\<close>
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 \<open>
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.
\<close>
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 \<open>
We can avoid the definition of frees by
using the build in notion of support.
\<close>
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 \<open>Parallel and single capture-avoiding substitution.\<close>
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 \<theta>::"(name\<times>lam) list"
and X::"name"
shows "pi\(lookup \ X) = lookup (pi\\) (pi\X)"
by (induct \<theta>) (auto simp add: eqvts)
nominal_primrec
psubst :: "(name\lam) list \ lam \ lam" ("_<_>" [95,95] 105)
where
"\<(Var x)> = (lookup \ x)"
| "\<(App e\<^sub>1 e\<^sub>2)> = App (\1>) (\2>)"
| "x\\ \ \<(Lam [x].e)> = Lam [x].(\)"
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\(\) = (pi\\)<(pi\t)>"
by (nominal_induct t avoiding: \<theta> 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')])"
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 \<open>
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.
\<close>
nominal_datatype clam =
Hole ("\" 1000)
| CAppL "clam" "lam"
| CAppR "lam" "clam"
| CLam "name" "clam" ("CLam [_]._" [100,100] 100)
text \<open>Filling a lambda-term into a context.\<close>
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 \<open>Composition od two contexts\<close>
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
¤ Dauer der Verarbeitung: 0.19 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.
|
