1 theory ExPS6

     2 imports "Parser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

     9 (* The binding structure is too complicated, so equivalence the

    10    way we define it is not true *)

    11 

    12 ML {* val _ = recursive := false  *}

    13 nominal_datatype exp6 =

    14   EVar name

    15 | EPair exp6 exp6

    16 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1

    17 and pat6 =

    18   PVar' name

    19 | PUnit'

    20 | PPair' pat6 pat6

    21 binder

    22   bp6 :: "pat6 \<Rightarrow> atom set"

    23 where

    24   "bp6 (PVar' x) = {atom x}"

    25 | "bp6 (PUnit') = {}"

    26 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"

    27 

    28 thm exp6_pat6.fv

    29 thm exp6_pat6.eq_iff

    30 thm exp6_pat6.bn

    31 thm exp6_pat6.perm

    32 thm exp6_pat6.induct

    33 thm exp6_pat6.distinct

    34 thm exp6_pat6.supp

    35 

    36 end

    37 

    38 

    39