Theory Lam_Funs

theory Lam_Funs
  imports "../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\<sharp>ϑ ==> ϑ<(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\<sharp>(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 ("\<box>" 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
  "\<box>[|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" ("_ o _" [100,100] 100)
where
  "\<box> o E' = E'"
| "(CAppL E t') o E' = CAppL (E o E') t'"
| "(CAppR t' E) o E' = CAppR t' (E o E')"
| "(CLam [x].E) o E' = CLam [x].(E o E')"
by (rule TrueI)+
  
lemma clam_compose:
  shows "(E1 o E2)[|t|] = E1[|E2[|t|]|]"
by (induct E1 rule: clam.induct) (auto)

end