1 theory Ex1rec

     2 imports "../NewParser"

     3 begin

     4 

     5 declare [[STEPS = 9]]

     6 

     7 atom_decl name

     8 

     9 nominal_datatype lam =

    10   Var "name"

    11 | App "lam" "lam"

    12 | Lam x::"name" t::"lam"  bind_set x in t

    13 | Let bp::"bp" t::"lam"   bind_set "bi bp" in bp 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 

    22 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros

    23 

    24 thm lam_bp.fv

    25 thm lam_bp.eq_iff[no_vars]

    26 thm lam_bp.bn

    27 thm lam_bp.perm

    28 thm lam_bp.induct

    29 thm lam_bp.inducts

    30 thm lam_bp.distinct

    31 thm lam_bp.supp

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

    33 thm lam_bp.fv[simplified lam_bp.supp(1-2)]

    34 

    35 

    36 

    37 end

    38 

    39 

    40