1 theory ExPS6

     2 imports "Parser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype exp6 =

    11   EVar name

    12 | EPair exp6 exp6

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

    14 and pat6 =

    15   PVar' name

    16 | PUnit'

    17 | PPair' pat6 pat6

    18 binder

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

    20 where

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

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

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

    24 

    25 thm exp6_pat6.fv

    26 thm exp6_pat6.eq_iff

    27 thm exp6_pat6.bn

    28 thm exp6_pat6.perm

    29 thm exp6_pat6.induct

    30 thm exp6_pat6.distinct

    31 

    32 end

    33 

    34 

    35