1 theory Ex1

     2 imports "../Nominal2"

     3 begin

     4 

     5 (* free names in bar are bound in foo *)

     6 

     7 atom_decl name

     8 

     9 nominal_datatype foo =

    10   Foo0 "name"

    11 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f

    12 and bar =

    13   Bar0 "name"

    14 | Bar1 "name" s::"name" b::"bar" bind (set) s in b

    15 binder

    16   bv

    17 where

    18   "bv (Bar0 x) = {}"

    19 | "bv (Bar1 v x b) = {atom v}"

    20 

    21 

    22 thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]

    23 

    24 lemma

    25   "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"

    26 apply(simp only: foo_bar.fv_defs)

    27 apply(simp only: foo_bar.bn_defs)

    28 apply(simp only: supp_at_base)

    29 apply(simp)

    30 done

    31 

    32 end

    33 

    34