theory Multi_Recs2

imports "../Nominal2"

begin

(* 

  multiple recursive binders - multiple letrecs with multiple 

  clauses for each functions

  example 8 from Peter Sewell's bestiary (originally due

  to James Cheney) 

*)

atom_decl name

nominal_datatype fun_recs: exp =

  Var name

| Unit 

| Pair exp exp

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

and fnclause =

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

and fnclauses =

  S fnclause

| ORs fnclause fnclauses

and lrb =

  Clause fnclauses

and lrbs =

  Single lrb

| More lrb lrbs

and pat =

  PVar name

| PUnit

| PPair pat pat

binder

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

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

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

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

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

where

  "b_lrbs (Single l) = b_lrb l"

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

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

| "b_pat (PUnit) = {}"

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

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

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

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

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

thm fun_recs.distinct

thm fun_recs.induct

thm fun_recs.inducts

thm fun_recs.exhaust

thm fun_recs.fv_defs

thm fun_recs.bn_defs

thm fun_recs.perm_simps

thm fun_recs.eq_iff

thm fun_recs.fv_bn_eqvt

thm fun_recs.size_eqvt

thm fun_recs.supports

thm fun_recs.fsupp

thm fun_recs.supp

end