theory ExPS6

imports "Parser"

begin

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

atom_decl name

(* The binding structure is too complicated, so we cannot show equivalence *)

ML {* val _ = cheat_equivp := 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