1 theory LetRec

     2 imports "../NewParser"

     3 begin

     4 

     5 declare [[STEPS = 14]]

     6 

     7 atom_decl name

     8 

     9 nominal_datatype let_rec:

    10  lam =

    11   Var "name"

    12 | App "lam" "lam"

    13 | Lam x::"name" t::"lam"     bind (set) x in t

    14 | Let_Rec bp::"bp" t::"lam"  bind (set) "bi bp" in bp t

    15 and bp =

    16   Bp "name" "lam"

    17 binder

    18   bi::"bp \<Rightarrow> atom set"

    19 where

    20   "bi (Bp x t) = {atom x}"

    21 

    22 thm let_rec.distinct

    23 thm let_rec.induct

    24 thm let_rec.exhaust

    25 thm let_rec.fv_defs

    26 thm let_rec.bn_defs

    27 thm let_rec.perm_simps

    28 thm let_rec.eq_iff

    29 thm let_rec.fv_bn_eqvt

    30 thm let_rec.size_eqvt

    31 

    32 

    33 end

    34 

    35 

    36