--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -0,0 +1,70 @@
+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
+
+
+