1 theory Ex2

     2 imports "../NewParser"

     3 begin

     4 

     5 text {* example 2 *}

     6 declare [[STEPS = 9]]

     7 

     8 atom_decl name

     9 

    10 nominal_datatype trm =

    11   Var "name"

    12 | App "trm" "trm"

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

    14 | Let p::"pat" "trm" t::"trm"   bind_set "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 fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]

    27 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]

    28 

    29 

    30 

    31 

    32 thm trm_pat.bn

    33 thm trm_pat.perm

    34 thm trm_pat.induct

    35 thm trm_pat.distinct

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

    37 

    38 

    39 end

    40 

    41 

    42