# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285376019 -7200
# Node ID 6bab47906dbea2ccd5a5dddd70d57796b95b8a4d
# Parent  594f3401605f2587eea40c2fbf726811178d323e
added example about datatypes

diff -r 594f3401605f -r 6bab47906dbe Nominal/Ex/Datatypes.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sat Sep 25 02:53:39 2010 +0200
@@ -0,0 +1,68 @@
+theory Datatypes
+imports "../Nominal2" 
+begin
+
+(* 
+  plain nominal_datatype definition without an 
+  atom_decl - example by John Matthews
+*)
+
+nominal_datatype 'a Maybe = 
+  Nothing 
+| Just 'a
+
+
+thm Maybe.distinct
+thm Maybe.induct
+thm Maybe.exhaust
+thm Maybe.fv_defs
+thm Maybe.bn_defs
+thm Maybe.perm_simps
+thm Maybe.eq_iff
+thm Maybe.fv_bn_eqvt
+thm Maybe.size_eqvt
+thm Maybe.supp
+
+(*
+  using a datatype inside a nominal_datatype
+*)
+
+atom_decl name
+
+datatype foo = Foo | Bar
+
+
+instantiation foo :: pure
+begin
+
+definition
+  "p \<bullet> (f::foo) = f"
+
+instance
+apply(default)
+apply(simp_all add:  permute_foo_def)
+done
+
+end
+
+
+nominal_datatype baz =
+  Baz x::name t::foo bind x in t
+
+
+thm baz.distinct
+thm baz.induct
+thm baz.exhaust
+thm baz.fv_defs
+thm baz.bn_defs
+thm baz.perm_simps
+thm baz.eq_iff
+thm baz.fv_bn_eqvt
+thm baz.size_eqvt
+thm baz.supp
+  
+
+end
+
+
+
diff -r 594f3401605f -r 6bab47906dbe Slides/ROOT1.ML
--- a/Slides/ROOT1.ML	Thu Sep 23 05:28:40 2010 +0200
+++ b/Slides/ROOT1.ML	Sat Sep 25 02:53:39 2010 +0200
@@ -1,4 +1,4 @@
-show_question_marks := false;
+(* show_question_marks := false; *)
 quick_and_dirty := true;
 
 no_document use_thy "LaTeXsugar";
diff -r 594f3401605f -r 6bab47906dbe Slides/ROOT2.ML
--- a/Slides/ROOT2.ML	Thu Sep 23 05:28:40 2010 +0200
+++ b/Slides/ROOT2.ML	Sat Sep 25 02:53:39 2010 +0200
@@ -1,6 +1,8 @@
-show_question_marks := false;
+(* show_question_marks := false; *)
+
 quick_and_dirty := true;
 
+
 no_document use_thy "LaTeXsugar";
 
 use_thy "Slides2"
\ No newline at end of file