theory Ex2
imports "../NewParser"
begin

text {* example 2 *}

atom_decl name

nominal_datatype trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"          bind_set x in t
| Let p::"pat" "trm" t::"trm"     bind "f p" in t
and pat =
  PN
| PS "name"
| PD "name" "name"
binder
  f::"pat \<Rightarrow> atom list"
where
  "f PN = []"
| "f (PS x) = [atom x]"
| "f (PD x y) = [atom x, atom y]"

thm trm_pat.bn
thm trm_pat.perm
thm trm_pat.induct
thm trm_pat.distinct
thm trm_pat.fv[simplified trm_pat.supp(1-2)]

lemma lets_overlap1:
  "atom a \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y"
  by (simp add: trm_pat.eq_iff alphas)

lemma lets_overlap2:
  "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> Let (PD a a) x y = Let (PD b b) x y"
  apply (simp add: trm_pat.eq_iff alphas trm_pat.supp)
  apply (rule_tac x="(a\<leftrightarrow>b)" in exI)
  apply (simp add: eqvts)
  apply (rule conjI)
  prefer 2
  apply (rule Nominal2_Supp.supp_perm_eq)
  apply (unfold fresh_star_def)
  apply (unfold fresh_def)
  apply (unfold flip_def)
  apply (simp_all add: supp_swap)
  apply auto
  done

end