1 theory Ex3

     2 imports "../Parser"

     3 begin

     4 

     5 (* Example 3, identical to example 1 from Terms.thy *)

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype trm0 =

    11   Var0 "name"

    12 | App0 "trm0" "trm0"

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

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

    15 and pat0 =

    16   PN0

    17 | PS0 "name"

    18 | PD0 "pat0" "pat0"

    19 binder

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

    21 where

    22   "f0 PN0 = {}"

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

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

    25 

    26 thm trm0_pat0.fv

    27 thm trm0_pat0.eq_iff

    28 thm trm0_pat0.bn

    29 thm trm0_pat0.perm

    30 thm trm0_pat0.induct

    31 thm trm0_pat0.distinct

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

    33 

    34 end

    35 

    36 

    37