--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Multi_Recs.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -0,0 +1,49 @@
+theory Multi_Recs
+imports "../Nominal2"
+begin
+
+(* 
+  multiple recursive binders
+
+  example 7 from Peter Sewell's bestiary 
+
+*)
+
+atom_decl name
+
+nominal_datatype multi_recs: exp =
+  Var name
+| Unit
+| Pair exp exp
+| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
+and lrb =
+  Assign name exp
+and lrbs =
+  Single lrb
+| More lrb lrbs
+binder
+  b :: "lrb \<Rightarrow> atom set" and
+  bs :: "lrbs \<Rightarrow> atom set"
+where
+  "b (Assign x e) = {atom x}"
+| "bs (Single a) = b a"
+| "bs (More a as) = (b a) \<union> (bs as)"
+
+thm multi_recs.distinct
+thm multi_recs.induct
+thm multi_recs.inducts
+thm multi_recs.exhaust
+thm multi_recs.fv_defs
+thm multi_recs.bn_defs
+thm multi_recs.perm_simps
+thm multi_recs.eq_iff
+thm multi_recs.fv_bn_eqvt
+thm multi_recs.size_eqvt
+thm multi_recs.supports
+thm multi_recs.fsupp
+thm multi_recs.supp
+
+end
+
+
+