theory ExPS8
imports "Parser"
begin

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

atom_decl name

(* One function is recursive and the other one is not,
   and as the parser cannot handle this we cannot set
   the reference.  *)
ML {* val _ = recursive := false  *}

nominal_datatype exp8 =
  EVar name
| EUnit
| EPair exp8 exp8
| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
and fnclause =
  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
and fnclauses =
  S fnclause
| ORs fnclause fnclauses
and lrb8 =
  Clause fnclauses
and lrbs8 =
  Single lrb8
| More lrb8 lrbs8
and pat8 =
  PVar name
| PUnit
| PPair pat8 pat8
binder
  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
  b_pat :: "pat8 \<Rightarrow> atom set" and
  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
  b_fnclause :: "fnclause \<Rightarrow> atom set" and
  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
where
  "b_lrbs8 (Single l) = b_lrb8 l"
| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 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_lrb8 (Clause fcs) = (b_fnclauses fcs)"
| "b_fnclause (K x pat exp8) = {atom x}"

thm exp7_lrb_lrbs.eq_iff
thm exp7_lrb_lrbs.supp

end