1 theory Ex1

     2 imports "Parser"

     3 begin

     4 

     5 text {* example 1, equivalent to example 2 from Terms *}

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype lam =

    11   VAR "name"

    12 | APP "lam" "lam"

    13 | LAM x::"name" t::"lam" bind x in t

    14 | LET bp::"bp" t::"lam"   bind "bi bp" in 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 lam_bp.fv

    23 thm lam_bp.supp

    24 thm lam_bp.eq_iff

    25 thm lam_bp.bn

    26 thm lam_bp.perm

    27 thm lam_bp.induct

    28 thm lam_bp.inducts

    29 thm lam_bp.distinct

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

    31 thm lam_bp.fv[simplified lam_bp.supp]

    32 

    33 end

    34 

    35 

    36