1 theory ExNotRsp

     2 imports "../Parser"

     3 begin

     4 

     5 atom_decl name

     6 

     7 (* example 6 from Terms.thy *)

     8 

     9 nominal_datatype trm6 =

    10   Vr6 "name"

    11 | Lm6 x::"name" t::"trm6"         bind x in t

    12 | Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right

    13 binder

    14   bv6

    15 where

    16   "bv6 (Vr6 n) = {}"

    17 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"

    18 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"

    19 

    20 (* example 7 from Terms.thy *)

    21 nominal_datatype trm7 =

    22   Vr7 "name"

    23 | Lm7 l::"name" r::"trm7"   bind l in r

    24 | Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r

    25 binder

    26   bv7

    27 where

    28   "bv7 (Vr7 n) = {atom n}"

    29 | "bv7 (Lm7 n t) = bv7 t - {atom n}"

    30 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"

    31 *)

    32 

    33 (* example 9 from Terms.thy *)

    34 nominal_datatype lam9 =

    35   Var9 "name"

    36 | Lam9 n::"name" l::"lam9" bind n in l

    37 and bla9 =

    38   Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s

    39 binder

    40   bv9

    41 where

    42   "bv9 (Var9 x) = {}"

    43 | "bv9 (Lam9 x b) = {atom x}"

    44 

    45 end

    46 

    47 

    48