--- a/Nominal/Abs.thy	Tue Mar 02 15:07:27 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 16:03:19 2010 +0100
@@ -500,5 +500,14 @@
 oops
 
 *)
+
+fun
+  distinct_perms 
+where
+  "distinct_perms [] = True"
+| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
+
+
+
 end
 

--- a/Nominal/Test.thy	Tue Mar 02 15:07:27 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 16:03:19 2010 +0100
@@ -332,7 +332,102 @@
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
 *)
 
-thm bv_raw.simps
+(*thm bv_raw.simps*)
+
+(* example 3 from Peter Sewell's bestiary *)
+nominal_datatype exp =
+  Var name
+| App exp exp
+| Lam x::name e::exp bind x in e
+| Let x::name p::pat e1::exp e2::exp bind x in e2, bind "bp p" in e1
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
+binder
+  bp :: "pat \<Rightarrow> atom set"
+where
+  "bp (PVar x) = {atom x}"
+| "bp (PUnit) = {}"
+| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
+
+(* example 6 from Peter Sewell's bestiary *)
+nominal_datatype exp6 =
+  EVar name
+| EPair exp6 exp6
+| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
+and pat6 =
+  PVar name
+| PUnit
+| PPair pat6 pat6
+binder
+  bp6 :: "pat6 \<Rightarrow> atom set"
+where
+  "bp6 (PVar x) = {atom x}"
+| "bp6 (PUnit) = {}"
+| "bp6 (PPair p1 p2) = bp6 p1 \<union> bp6 p2"
+
+(* example 7 from Peter Sewell's bestiary *)
+nominal_datatype exp7 =
+  EVar name
+| EUnit
+| EPair exp7 exp7
+| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
+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)"
+
+(* example 8 from Peter Sewell's bestiary *)
+nominal_datatype exp8 =
+  EVar name
+| EUnit
+| EPair exp8 exp8
+| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
+and fnclause =
+  K x::name p::pat8 e::exp8 bind "b_pat p" in e
+and fnclauses =
+  S fnclause
+| ORs fnclause fnclauses
+and lrb8 =
+  Clause fnclauses
+and lrbs8 =
+  Single lrb8
+| More lrb8 lrbs8
+and pat8 =
+  PVar name
+| PUnit
+| PPair pat8 pat8
+binder
+  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
+  b_pat :: "pat8 \<Rightarrow> atom set" and
+  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+  b_fnclause :: "fnclause \<Rightarrow> atom set" and
+  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
+where
+  "b_lrbs8 (Single l) = b_lrb8 l"
+| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 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_lrb8 (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp8) = {atom x}"
+
+
+
+
+(* example 9 from Peter Sewell's bestiary *)
+(* run out of steam at the moment *)
 
 end
 

Binary file sewell.pdf has changed