1 theory Foo1

     2 imports "../Nominal2" 

     3 begin

     4 

     5 (* 

     6   Contrived example that has more than one

     7   binding function for a datatype

     8 *)

     9 

    10 atom_decl name

    11 

    12 nominal_datatype foo: trm =

    13   Var "name"

    14 | App "trm" "trm"

    15 | Lam x::"name" t::"trm"  bind x in t

    16 | Let1 a::"assg" t::"trm"  bind "bn1 a" in t

    17 | Let2 a::"assg" t::"trm"  bind "bn2 a" in t

    18 | Let3 a::"assg" t::"trm"  bind "bn3 a" in t

    19 and assg =

    20   As "name" "name" "trm"

    21 binder

    22   bn1::"assg \<Rightarrow> atom list" and

    23   bn2::"assg \<Rightarrow> atom list" and

    24   bn3::"assg \<Rightarrow> atom list"

    25 where

    26   "bn1 (As x y t) = [atom x]"

    27 | "bn2 (As x y t) = [atom y]"

    28 | "bn3 (As x y t) = [atom x, atom y]"

    29 

    30 thm foo.distinct

    31 thm foo.induct

    32 thm foo.inducts

    33 thm foo.exhaust

    34 thm foo.fv_defs

    35 thm foo.bn_defs

    36 thm foo.perm_simps

    37 thm foo.eq_iff

    38 thm foo.fv_bn_eqvt

    39 thm foo.size_eqvt

    40 thm foo.supports

    41 thm foo.fsupp

    42 thm foo.supp

    43 thm foo.fresh

    44 

    45 

    46 end

    47 

    48 

    49