1 theory Ex1rec

     2 imports "Parser" "../Attic/Prove"

     3 begin

     4 

     5 atom_decl name

     6 

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

     8 nominal_datatype lam' =

     9   VAR' "name"

    10 | APP' "lam'" "lam'"

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

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

    13 and bp' =

    14   BP' "name" "lam'"

    15 binder

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

    17 where

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

    19 

    20 thm lam'_bp'.fv

    21 thm lam'_bp'.eq_iff[no_vars]

    22 thm lam'_bp'.bn

    23 thm lam'_bp'.perm

    24 thm lam'_bp'.induct

    25 thm lam'_bp'.inducts

    26 thm lam'_bp'.distinct

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

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

    29 

    30 end

    31 

    32 

    33