--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Ex1.thy	Sun Aug 29 13:36:03 2010 +0800
@@ -0,0 +1,34 @@
+theory Ex1
+imports "../Nominal2"
+begin
+
+(* free names in bar are bound in foo *)
+
+atom_decl name
+
+nominal_datatype foo =
+  Foo0 "name"
+| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
+and bar =
+  Bar0 "name"
+| Bar1 "name" s::"name" b::"bar" bind (set) s in b
+binder
+  bv
+where
+  "bv (Bar0 x) = {}"
+| "bv (Bar1 v x b) = {atom v}"
+
+
+thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]
+
+lemma
+  "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
+apply(simp only: foo_bar.fv_defs)
+apply(simp only: foo_bar.bn_defs)
+apply(simp only: supp_at_base)
+apply(simp)
+done
+
+end
+
+