theory ExPS6
imports "../NewParser"
begin

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

atom_decl name

(* Is this binding structure supported - I think not 
   because e1 occurs twice as body *)

nominal_datatype exp =
  Var name
| Pair exp exp
| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
and pat =
  PVar name
| PUnit
| PPair pat pat
binder
  bp :: "pat \<Rightarrow> atom list"
where
  "bp (PVar x) = [atom x]"
| "bp (PUnit) = []"
| "bp (PPair p1 p2) = bp p1 @ bp p2"

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

declare permute_exp_raw_permute_pat_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]

equivariance alpha_exp_raw


end