1 theory NoneExamples

     2 imports "../NewParser"

     3 begin

     4 

     5 atom_decl name

     6 

     7 (* this example binds bound names and

     8    so is not respectful *)

     9 (*

    10 nominal_datatype trm =

    11   Vr "name"

    12 | Lm x::"name" t::"trm"         bind x in t

    13 | Lt left::"trm" right::"trm"   bind "bv left" in right

    14 binder

    15   bv

    16 where

    17   "bv (Vr n) = {}"

    18 | "bv (Lm n t) = {atom n} \<union> bv t"

    19 | "bv (Lt l r) = bv l \<union> bv r"

    20 *)

    21 

    22 (* this example uses "-" in the binding function; 

    23    at the moment this is unsupported *)

    24 (*

    25 nominal_datatype trm' =

    26   Vr' "name"

    27 | Lm' l::"name" r::"trm'"   bind l in r

    28 | Lt' l::"trm'" r::"trm'"   bind "bv' l" in r

    29 binder

    30   bv'

    31 where

    32   "bv' (Vr' n) = {atom n}"

    33 | "bv' (Lm' n t) = bv' t - {atom n}"

    34 | "bv' (Lt' l r) = bv' l \<union> bv' r"

    35 *)

    36 

    37 (* this example again binds bound names  *)

    38 (*

    39 nominal_datatype trm'' =

    40   Va'' "name"

    41 | Lm'' n::"name" l::"trm''" bind n in l

    42 and bla'' =

    43   Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s

    44 binder

    45   bv''

    46 where

    47   "bv'' (Vm'' x) = {}"

    48 | "bv'' (Lm'' x b) = {atom x}"

    49 *)

    50 

    51 end

    52 

    53 

    54