1 theory Ex2

     2 imports "Parser"

     3 begin

     4 

     5 text {* example 2 *}

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype trm' =

    11   Var "name"

    12 | App "trm'" "trm'"

    13 | Lam x::"name" t::"trm'"          bind x in t

    14 | Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t

    15 and pat' =

    16   PN

    17 | PS "name"

    18 | PD "name" "name"

    19 binder

    20   f::"pat' \<Rightarrow> atom set"

    21 where

    22   "f PN = {}"

    23 | "f (PD x y) = {atom x, atom y}"

    24 | "f (PS x) = {atom x}"

    25 

    26 thm trm'_pat'.fv

    27 thm trm'_pat'.eq_iff

    28 thm trm'_pat'.bn

    29 thm trm'_pat'.perm

    30 thm trm'_pat'.induct

    31 thm trm'_pat'.distinct

    32 thm trm'_pat'.fv[simplified trm'_pat'.supp]

    33 

    34 end

    35 

    36 

    37