theory ExPS6imports "../Parser"begin(* example 6 from Peter Sewell's bestiary *)atom_decl name(* The binding structure is too complicated, so equivalence the way we define it is not 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 e1and pat6 = PVar' name| PUnit'| PPair' pat6 pat6binder 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.fvthm exp6_pat6.eq_iffthm exp6_pat6.bnthm exp6_pat6.permthm exp6_pat6.inductthm exp6_pat6.distinctthm exp6_pat6.suppend