theory Lambda
imports "../Nominal/Nominal2" 
begin

section {* Definitions for Lambda Terms *}


text {* type of variables *}

atom_decl name


subsection {* Alpha-Equated Lambda Terms *}

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)


text {* some automatically derived theorems *}

thm lam.distinct
thm lam.eq_iff
thm lam.fresh
thm lam.size
thm lam.exhaust 
thm lam.strong_exhaust
thm lam.induct
thm lam.strong_induct


subsection {* Height Function *}

nominal_function
  height :: "lam \<Rightarrow> int"
where
  "height (Var x) = 1"
| "height (App t1 t2) = max (height t1) (height t2) + 1"
| "height (Lam [x].t) = height t + 1"
apply(simp add: eqvt_def height_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
using [[simproc del: alpha_lst]]
apply(auto)
apply(erule_tac c="()" in Abs_lst1_fcb2)
apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
done

nominal_termination (eqvt)
  by lexicographic_order
  

subsection {* Capture-Avoiding Substitution *}

nominal_function
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90,90,90] 90)
where
  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
  unfolding eqvt_def subst_graph_aux_def
  apply(simp)
  apply(rule TrueI)
  using [[simproc del: alpha_lst]]
  apply(auto)
  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
  apply(blast)+
  apply(simp_all add: fresh_star_def fresh_Pair_elim)
  apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
  apply(simp_all add: Abs_fresh_iff)
  apply(simp add: fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def)
  apply(simp add: perm_supp_eq fresh_star_Pair)
  apply(simp add: eqvt_at_def)
  apply(simp add: perm_supp_eq fresh_star_Pair)
done

nominal_termination (eqvt)
  by lexicographic_order

lemma fresh_fact:
  assumes a: "atom z \<sharp> s"
  and b: "z = y \<or> atom z \<sharp> t"
  shows "atom z \<sharp> t[y ::= s]"
using a b
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
   (auto simp add: fresh_at_base)


end