theory ExPS7
imports "../NewParser"
begin

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

atom_decl name

nominal_datatype exp =
  Var name
| Unit
| Pair exp exp
| LetRec l::"lrbs" e::"exp"  bind_set "bs l" in l e
and lrb =
  Assign name exp
and lrbs =
  Single lrb
| More lrb lrbs
binder
  b :: "lrb \<Rightarrow> atom set" and
  bs :: "lrbs \<Rightarrow> atom set"
where
  "b (Assign x e) = {atom x}"
| "bs (Single a) = b a"
| "bs (More a as) = (b a) \<union> (bs as)"

thm exp_lrb_lrbs.eq_iff
thm exp_lrb_lrbs.supp


end