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" bind 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_primrec

  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(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 

unfolding eqvt_def

apply(rule allI)

apply(simp add: permute_fun_def)

apply(rule ext)

apply(rule ext)

apply(simp add: permute_bool_def)

apply(rule iffI)

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="- p \<bullet> x" in meta_spec)

apply(drule_tac x="- p \<bullet> xa" in meta_spec)

apply(simp)

apply(drule_tac x="-p" in meta_spec)

apply(drule_tac x="x" in meta_spec)

apply(drule_tac x="xa" in meta_spec)

apply(simp)

apply(erule height_graph.induct)

apply(perm_simp)

apply(rule height_graph.intros)

apply(perm_simp)

apply(rule height_graph.intros)

apply(assumption)

apply(assumption)

apply(perm_simp)

apply(rule height_graph.intros)

apply(assumption)

apply(rule_tac y="x" in lam.exhaust)

apply(auto simp add: lam.distinct lam.eq_iff)

apply(simp add: Abs_eq_iff alphas)

apply(clarify)

apply(subst (4) supp_perm_eq[where p="p", symmetric])

apply(simp add: pure_supp  fresh_star_def)

apply(simp add: eqvt_at_def)

done

termination

  by (relation "measure size") (simp_all add: lam.size)

subsection {* Capture-Avoiding Substitution *}

nominal_primrec

  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])"

apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 

unfolding eqvt_def

apply(rule allI)

apply(simp add: permute_fun_def)

apply(rule ext)

apply(rule ext)

apply(simp add: permute_bool_def)

apply(rule iffI)

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="- p \<bullet> x" in meta_spec)

apply(drule_tac x="- p \<bullet> xa" in meta_spec)

apply(simp)

apply(drule_tac x="-p" in meta_spec)

apply(drule_tac x="x" in meta_spec)

apply(drule_tac x="xa" in meta_spec)

apply(simp)

apply(erule subst_graph.induct)

apply(perm_simp)

apply(rule subst_graph.intros)

apply(perm_simp)

apply(rule subst_graph.intros)

apply(assumption)

apply(assumption)

apply(perm_simp)

apply(rule subst_graph.intros)

apply(simp add: fresh_Pair)

apply(assumption)

apply(auto simp add: lam.distinct lam.eq_iff)

apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

apply(blast)+

apply(simp add: fresh_star_def)

apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")

apply(subst (asm) Abs_eq_iff2)

apply(simp add: alphas atom_eqvt)

apply(clarify)

apply(rule trans)

apply(rule_tac p="p" in supp_perm_eq[symmetric])

apply(rule fresh_star_supp_conv)

apply(drule fresh_star_perm_set_conv)

apply(simp add: finite_supp)

apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")

apply(auto simp add: fresh_star_def)[1]

apply(simp (no_asm) add: fresh_star_def)

apply(rule conjI)

apply(simp (no_asm) add: Abs_fresh_iff)

apply(clarify)

apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)

apply(simp add: finite_supp)

apply(simp (no_asm_use) add: fresh_Pair)

apply(simp add: Abs_fresh_iff)

apply(simp)

apply(simp add: Abs_fresh_iff)

apply(subgoal_tac "p \<bullet> ya = ya")

apply(subgoal_tac "p \<bullet> sa = sa")

apply(simp add: atom_eqvt eqvt_at_def)

apply(rule perm_supp_eq)

apply(auto simp add: fresh_star_def fresh_Pair)[1]

apply(rule perm_supp_eq)

apply(auto simp add: fresh_star_def fresh_Pair)[1]

apply(rule conjI)

apply(simp add: Abs_fresh_iff)

apply(drule sym)

apply(simp add: Abs_fresh_iff)

done

termination

  by (relation "measure (\<lambda>(t, _, _). size t)")

     (simp_all add: lam.size)

lemma subst_eqvt[eqvt]:

  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"

by (induct t x s rule: subst.induct) (simp_all)

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: lam.fresh fresh_at_base)

end