theory ExPS7
imports "Parser"
begin

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

atom_decl name

ML {* val _ = recursive := true  *}
nominal_datatype exp7 =
  EVar name
| EUnit
| EPair exp7 exp7
| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
and lrb =
  Assign name exp7
and lrbs =
  Single lrb
| More lrb lrbs
binder
  b7 :: "lrb \<Rightarrow> atom set" and
  b7s :: "lrbs \<Rightarrow> atom set"
where
  "b7 (Assign x e) = {atom x}"
| "b7s (Single a) = b7 a"
| "b7s (More a as) = (b7 a) \<union> (b7s as)"
thm exp7_lrb_lrbs.eq_iff
thm exp7_lrb_lrbs.supp

end