1 (*<*)

     2 theory Test

     3 imports "../Parser"

     4 begin

     5 

     6 (* This file contains only the examples that are not supposed to work yet. *)

     7 

     8 

     9 atom_decl name

    10 

    11 (* example 4 from Terms.thy *)

    12 (* fv_eqvt does not work, we need to repaire defined permute functions

    13    defined fv and defined alpha... *)

    14 (* lists-datastructure does not work yet

    15 nominal_datatype trm4 =

    16   Vr4 "name"

    17 | Ap4 "trm4" "trm4 list"

    18 | Lm4 x::"name" t::"trm4"  bind x in t

    19 

    20 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

    21 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

    22 *)

    23 

    24 (* example 8 from Terms.thy *)

    25 

    26 (* Binding in a term under a bn, needs to fail *)

    27 (*

    28 nominal_datatype foo8 =

    29   Foo0 "name"

    30 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"

    31 and bar8 =

    32   Bar0 "name"

    33 | Bar1 "name" s::"name" b::"bar8" bind s in b

    34 binder

    35   bv8

    36 where

    37   "bv8 (Bar0 x) = {}"

    38 | "bv8 (Bar1 v x b) = {atom v}"

    39 *)

    40 

    41 (* example 9 from Peter Sewell's bestiary *)

    42 (* run out of steam at the moment *)

    43 

    44 end

    45 (*>*)

    46 

    47