1 theory ExPS7

     2 imports "Parser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype exp7 =

    11   EVar name

    12 | EUnit

    13 | EPair exp7 exp7

    14 | ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e

    15 and lrb =

    16   Assign name exp7

    17 and lrbs =

    18   Single lrb

    19 | More lrb lrbs

    20 binder

    21   b7 :: "lrb \<Rightarrow> atom set" and

    22   b7s :: "lrbs \<Rightarrow> atom set"

    23 where

    24   "b7 (Assign x e) = {atom x}"

    25 | "b7s (Single a) = b7 a"

    26 | "b7s (More a as) = (b7 a) \<union> (b7s as)"

    27 thm exp7_lrb_lrbs.eq_iff

    28 thm exp7_lrb_lrbs.supp

    29 

    30 end

    31 

    32 

    33