1 theory Ex3

     2 imports "Parser"

     3 begin

     4 

     5 atom_decl name

     6 

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

     8 nominal_datatype trm0 =

     9   Var0 "name"

    10 | App0 "trm0" "trm0"

    11 | Lam0 x::"name" t::"trm0"          bind x in t

    12 | Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t

    13 and pat0 =

    14   PN0

    15 | PS0 "name"

    16 | PD0 "pat0" "pat0"

    17 binder

    18   f0::"pat0 \<Rightarrow> atom set"

    19 where

    20   "f0 PN0 = {}"

    21 | "f0 (PS0 x) = {atom x}"

    22 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"

    23 

    24 thm trm0_pat0.fv

    25 thm trm0_pat0.eq_iff

    26 thm trm0_pat0.bn

    27 thm trm0_pat0.perm

    28 thm trm0_pat0.induct

    29 thm trm0_pat0.distinct

    30 thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]

    31 

    32 end

    33 

    34 

    35