# HG changeset patch
# User blanchet
# Date 1392391329 -3600
# Node ID 9deb5066508fa88cd39a9aa376859b1719b20335
# Parent  f223445a4d0c3a3f70499f37749ddd56366b16e0
added examples/tests

diff -r f223445a4d0c -r 9deb5066508f src/HOL/BNF_Examples/Misc_Codatatype.thy
--- a/src/HOL/BNF_Examples/Misc_Codatatype.thy	Fri Feb 14 16:21:41 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy	Fri Feb 14 16:22:09 2014 +0100
@@ -54,6 +54,8 @@
 codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
 and 'a branch = Branch 'a "'a tree'"
 
+codatatype 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
+
 codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
diff -r f223445a4d0c -r 9deb5066508f src/HOL/BNF_Examples/Misc_Datatype.thy
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Fri Feb 14 16:21:41 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Fri Feb 14 16:22:09 2014 +0100
@@ -52,6 +52,8 @@
 datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
 and 'a branch = Branch 'a "'a tree'"
 
+datatype_new 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
+
 datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
diff -r f223445a4d0c -r 9deb5066508f src/HOL/BNF_Examples/Misc_Primcorec.thy
--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy	Fri Feb 14 16:21:41 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy	Fri Feb 14 16:22:09 2014 +0100
@@ -84,6 +84,19 @@
   "branch_of_stream s = (case s of Stream h t \<Rightarrow> Branch h (tree'_of_stream t))"
 
 primcorec
+  id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
+  id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
+  id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
+where
+  "id_tree t = (case t of BRTree a ts ts' => BRTree a (id_trees1 ts) (id_trees2 ts'))" |
+  "id_trees1 ts = (case ts of
+       MyNil => MyNil
+     | MyCons t ts => MyCons (id_tree t) (id_trees1 ts))" |
+  "id_trees2 ts = (case ts of
+       MyNil => MyNil
+     | MyCons t ts => MyCons (id_tree t) (id_trees2 ts))"
+
+primcorec
   freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
   freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
   freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
diff -r f223445a4d0c -r 9deb5066508f src/HOL/BNF_Examples/Misc_Primrec.thy
--- a/src/HOL/BNF_Examples/Misc_Primrec.thy	Fri Feb 14 16:21:41 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primrec.thy	Fri Feb 14 16:22:09 2014 +0100
@@ -91,6 +91,17 @@
   "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
 
 primrec_new
+  id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
+  id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
+  id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
+where
+  "id_tree (BRTree a ts ts') = BRTree a (id_trees1 ts) (id_trees2 ts')" |
+  "id_trees1 MyNil = MyNil" |
+  "id_trees1 (MyCons t ts) = MyCons (id_tree t) (id_trees1 ts)" |
+  "id_trees2 MyNil = MyNil" |
+  "id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)"
+
+primrec_new
   is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
   is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
   is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"