1 theory LetPat

     2 imports "../NewParser"

     3 begin

     4 

     5 declare [[STEPS = 100]]

     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 "name" "name"

    18 binder

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

    20 where

    21   "f PN = {}"

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

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

    24 

    25 thm trm_pat.distinct

    26 thm trm_pat.induct

    27 thm trm_pat.exhaust

    28 thm trm_pat.fv_defs

    29 thm trm_pat.bn_defs

    30 thm trm_pat.perm_simps

    31 thm trm_pat.eq_iff

    32 thm trm_pat.fv_bn_eqvt

    33 thm trm_pat.size_eqvt

    34 

    35 

    36 end

    37 

    38 

    39