theory ExPS8
imports "../NewParser"
begin

(* example 8 from Peter Sewell's bestiary *)

atom_decl name

ML {* val _ = cheat_fv_rsp := true *}
ML {* val _ = cheat_equivp := true *}
ML {* val _ = cheat_alpha_bn_rsp := true *}

nominal_datatype exp =
  EVar name
| EUnit
| EPair exp exp
| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e
and fnclause =
  K x::name p::pat f::exp bind_set "b_pat p" in f
and fnclauses =
  S fnclause
| ORs fnclause fnclauses
and lrb =
  Clause fnclauses
and lrbs =
  Single lrb
| More lrb lrbs
and pat =
  PVar name
| PUnit
| PPair pat pat
binder
  b_lrbs :: "lrbs \<Rightarrow> atom set" and
  b_pat :: "pat \<Rightarrow> atom set" and
  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
  b_fnclause :: "fnclause \<Rightarrow> atom set" and
  b_lrb :: "lrb \<Rightarrow> atom set"
where
  "b_lrbs (Single l) = b_lrb l"
| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
| "b_pat (PVar x) = {atom x}"
| "b_pat (PUnit) = {}"
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
| "b_fnclauses (S fc) = (b_fnclause fc)"
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
| "b_fnclause (K x pat exp) = {atom x}"

thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff

equivariance alpha_exp_raw
end