1 theory SingleLet

     2 imports "../Parser"

     3 begin

     4 

     5 atom_decl name

     6 

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

     8 

     9 nominal_datatype trm =

    10   Var "name"

    11 | App "trm" "trm"

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

    13 | Let a::"assg" t::"trm"  bind "bn a" in t

    14 and assg =

    15   As "name" "trm"

    16 binder

    17   bn::"assg \<Rightarrow> atom set"

    18 where

    19   "bn (As x t) = {atom x}"

    20 

    21 print_theorems

    22 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]

    23 

    24 thm trm_assg.fv

    25 thm trm_assg.supp

    26 thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]

    27 thm trm_assg.bn

    28 thm trm_assg.perm

    29 thm trm_assg.induct

    30 thm trm_assg.inducts

    31 thm trm_assg.distinct

    32 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}

    33 thm trm_assg.fv[simplified trm_assg.supp]

    34 

    35 end

    36 

    37 

    38