1 theory Multi_Recs

     2 imports "../Nominal2"

     3 begin

     4 

     5 (* 

     6   multiple recursive binders

     7 

     8   example 7 from Peter Sewell's bestiary 

     9 

    10 *)

    11 

    12 atom_decl name

    13 

    14 nominal_datatype multi_recs: exp =

    15   Var name

    16 | Unit

    17 | Pair exp exp

    18 | LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e

    19 and lrb =

    20   Assign name exp

    21 and lrbs =

    22   Single lrb

    23 | More lrb lrbs

    24 binder

    25   b :: "lrb \<Rightarrow> atom set" and

    26   bs :: "lrbs \<Rightarrow> atom set"

    27 where

    28   "b (Assign x e) = {atom x}"

    29 | "bs (Single a) = b a"

    30 | "bs (More a as) = (b a) \<union> (bs as)"

    31 

    32 thm multi_recs.distinct

    33 thm multi_recs.induct

    34 thm multi_recs.inducts

    35 thm multi_recs.exhaust

    36 thm multi_recs.fv_defs

    37 thm multi_recs.bn_defs

    38 thm multi_recs.perm_simps

    39 thm multi_recs.eq_iff

    40 thm multi_recs.fv_bn_eqvt

    41 thm multi_recs.size_eqvt

    42 thm multi_recs.supports

    43 thm multi_recs.fsupp

    44 thm multi_recs.supp

    45 

    46 end

    47 

    48 

    49