theory ExPS6
imports "../Parser"
begin

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

atom_decl name

(* The binding structure is too complicated, so equivalence the
   way we define it is not true *)

ML {* val _ = recursive := false  *}
nominal_datatype exp6 =
  EVar name
| EPair exp6 exp6
| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
and pat6 =
  PVar' name
| PUnit'
| PPair' pat6 pat6
binder
  bp6 :: "pat6 \<Rightarrow> atom set"
where
  "bp6 (PVar' x) = {atom x}"
| "bp6 (PUnit') = {}"
| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"

thm exp6_pat6.fv
thm exp6_pat6.eq_iff
thm exp6_pat6.bn
thm exp6_pat6.perm
thm exp6_pat6.induct
thm exp6_pat6.distinct
thm exp6_pat6.supp

end