--- 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"
--- 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"
--- 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"
--- 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"