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