--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExPS7.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,33 @@
+theory ExPS7
+imports "../Parser"
+begin
+
+(* example 7 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := true  *}
+nominal_datatype exp7 =
+  EVar name
+| EUnit
+| EPair exp7 exp7
+| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+and lrb =
+  Assign name exp7
+and lrbs =
+  Single lrb
+| More lrb lrbs
+binder
+  b7 :: "lrb \<Rightarrow> atom set" and
+  b7s :: "lrbs \<Rightarrow> atom set"
+where
+  "b7 (Assign x e) = {atom x}"
+| "b7s (Single a) = b7 a"
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
+thm exp7_lrb_lrbs.eq_iff
+thm exp7_lrb_lrbs.supp
+
+end
+
+
+