1 theory Multi_Recs2

     2 imports "../Nominal2"

     3 begin

     4 

     5 (* 

     6   multiple recursive binders - multiple letrecs with multiple 

     7   clauses for each functions

     8 

     9   example 8 from Peter Sewell's bestiary (originally due

    10   to James Cheney) 

    11 

    12 *)

    13 

    14 atom_decl name

    15 

    16 nominal_datatype fun_recs: exp =

    17   Var name

    18 | Unit 

    19 | Pair exp exp

    20 | LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e

    21 and fnclause =

    22   K x::name p::pat f::exp bind (set) "b_pat p" in f

    23 and fnclauses =

    24   S fnclause

    25 | ORs fnclause fnclauses

    26 and lrb =

    27   Clause fnclauses

    28 and lrbs =

    29   Single lrb

    30 | More lrb lrbs

    31 and pat =

    32   PVar name

    33 | PUnit

    34 | PPair pat pat

    35 binder

    36   b_lrbs :: "lrbs \<Rightarrow> atom set" and

    37   b_pat :: "pat \<Rightarrow> atom set" and

    38   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and

    39   b_fnclause :: "fnclause \<Rightarrow> atom set" and

    40   b_lrb :: "lrb \<Rightarrow> atom set"

    41 where

    42   "b_lrbs (Single l) = b_lrb l"

    43 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"

    44 | "b_pat (PVar x) = {atom x}"

    45 | "b_pat (PUnit) = {}"

    46 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"

    47 | "b_fnclauses (S fc) = (b_fnclause fc)"

    48 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"

    49 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"

    50 | "b_fnclause (K x pat exp) = {atom x}"

    51 

    52 thm fun_recs.distinct

    53 thm fun_recs.induct

    54 thm fun_recs.inducts

    55 thm fun_recs.exhaust

    56 thm fun_recs.fv_defs

    57 thm fun_recs.bn_defs

    58 thm fun_recs.perm_simps

    59 thm fun_recs.eq_iff

    60 thm fun_recs.fv_bn_eqvt

    61 thm fun_recs.size_eqvt

    62 thm fun_recs.supports

    63 thm fun_recs.fsupp

    64 thm fun_recs.supp

    65 

    66 

    67 end

    68 

    69 

    70