theory Lambda
imports "../Nominal2" 
begin

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  bind x in l

thm lam.distinct
thm lam.induct
thm lam.exhaust lam.strong_exhaust
thm lam.fv_defs
thm lam.bn_defs
thm lam.perm_simps
thm lam.eq_iff
thm lam.fv_bn_eqvt
thm lam.size_eqvt

nominal_primrec
  depth :: "lam \<Rightarrow> nat"
where
  "depth (Var x) = 1"
| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
| "depth (Lam x t) = (depth t) + 1"
apply(rule_tac y="x" in lam.exhaust)
apply(simp_all)[3]
apply(simp_all only: lam.distinct)
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
apply(subst (asm) Abs_eq_iff)
apply(erule exE)
apply(simp add: alphas)
apply(clarify)
apply(rule trans)
apply(rule_tac p="p" in supp_perm_eq[symmetric])
apply(simp add: pure_supp)
apply(simp add: fresh_star_def)
apply(simp add: eqvt_at_def)
done

termination
  apply(relation "measure size")
  apply(simp_all add: lam.size)
  done
  
lemma removeAll_eqvt[eqvt]:
  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
by (induct xs) (auto)

lemma supp_removeAll:
  fixes x::"atom"
  shows "supp (removeAll x xs) = (supp xs - {x})"
apply(induct xs)
apply(simp_all add: supp_Nil supp_Cons)
apply(rule conjI)
apply(rule impI)
apply(simp add: supp_atom)
apply(rule impI)
apply(simp add: supp_atom)
apply(blast)
done

nominal_primrec 
  frees_lst :: "lam \<Rightarrow> atom list"
where
  "frees_lst (Var x) = [atom x]"
| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
apply(rule_tac y="x" in lam.exhaust)
apply(simp_all)[3]
apply(simp_all only: lam.distinct)
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
apply(simp add: Abs_eq_iff)
apply(erule exE)
apply(simp add: alphas)
apply(simp add: atom_eqvt)
apply(clarify)
apply(rule trans)
apply(rule_tac p="p" in supp_perm_eq[symmetric])
apply(simp (no_asm) add: supp_removeAll)
apply(drule supp_eqvt_at)
apply(simp add: finite_supp)
apply(auto simp add: fresh_star_def)[1]
unfolding eqvt_at_def
apply(simp only: removeAll_eqvt atom_eqvt)
done

termination
  apply(relation "measure size")
  apply(simp_all add: lam.size)
  done

(* a small lemma *)
lemma
  "supp t = set (frees_lst t)"
apply(induct t rule: lam.induct)
apply(simp_all add: lam.supp supp_at_base)
done

nominal_primrec
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
where
  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
apply(case_tac x)
apply(simp)
apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
apply(simp add: lam.eq_iff lam.distinct)
apply(auto)[1]
apply(simp add: lam.eq_iff lam.distinct)
apply(auto)[1]
apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
apply(simp_all add: lam.distinct)[5]
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
apply(erule conjE)+
oops


end