theory Ex3
imports "../NewParser"
begin

(* Example 3, identical to example 1 from Terms.thy *)

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_set "f p" in t
and pat =
  PN
| PS "name"
| PD "pat" "pat"
binder
  f::"pat \<Rightarrow> atom set"
where
  "f PN = {}"
| "f (PS x) = {atom x}"
| "f (PD p1 p2) = (f p1) \<union> (f p2)"

thm trm_pat.fv
thm trm_pat.eq_iff
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)]


declare permute_trm_raw_permute_pat_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]

equivariance alpha_trm_raw


end