1 theory Ex1rec

     2 imports "../Parser" 

     3 begin

     4 

     5 atom_decl name

     6 

     7 ML {* val _ = recursive := true *}

     8 ML {* val _ = alpha_type := AlphaGen *}

     9 nominal_datatype lam' =

    10   VAR' "name"

    11 | APP' "lam'" "lam'"

    12 | LAM' x::"name" t::"lam'"  bind x in t

    13 | LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t

    14 and bp' =

    15   BP' "name" "lam'"

    16 binder

    17   bi'::"bp' \<Rightarrow> atom set"

    18 where

    19   "bi' (BP' x t) = {atom x}"

    20 

    21 thm lam'_bp'.fv

    22 thm lam'_bp'.eq_iff[no_vars]

    23 thm lam'_bp'.bn

    24 thm lam'_bp'.perm

    25 thm lam'_bp'.induct

    26 thm lam'_bp'.inducts

    27 thm lam'_bp'.distinct

    28 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}

    29 thm lam'_bp'.fv[simplified lam'_bp'.supp]

    30 

    31 end

    32 

    33 

    34