1 theory Ex3

     2 imports "../NewParser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

     9 nominal_datatype trm =

    10   Var "name"

    11 | App "trm" "trm"

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

    13 | Let p::"pat" "trm" t::"trm"   bind_set "f p" in t

    14 and pat =

    15   PN

    16 | PS "name"

    17 | PD "pat" "pat"

    18 binder

    19   f::"pat \<Rightarrow> atom set"

    20 where

    21   "f PN = {}"

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

    23 | "f (PD p1 p2) = (f p1) \<union> (f p2)"

    24 

    25 thm trm_pat.fv

    26 thm trm_pat.eq_iff

    27 thm trm_pat.bn

    28 thm trm_pat.perm

    29 thm trm_pat.induct

    30 thm trm_pat.distinct

    31 thm trm_pat.fv[simplified trm_pat.supp(1-2)]

    32 

    33 

    34 

    35 end

    36 

    37 

    38