1 theory ExPS7

     2 imports "../Nominal2"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

     9 declare [[STEPS = 31]]

    10 

    11 nominal_datatype exp =

    12   Var name

    13 | Unit

    14 | Pair exp exp

    15 | LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e

    16 and lrb =

    17   Assign name exp

    18 and lrbs =

    19   Single lrb

    20 | More lrb lrbs

    21 binder

    22   b :: "lrb \<Rightarrow> atom set" and

    23   bs :: "lrbs \<Rightarrow> atom set"

    24 where

    25   "b (Assign x e) = {atom x}"

    26 | "bs (Single a) = b a"

    27 | "bs (More a as) = (b a) \<union> (bs as)"

    28 

    29 

    30 

    31 end

    32 

    33 

    34