Add rose_reduce, etc.

src/coalgebras/ltreeScript.sml

@@ -987,6 +987,16 @@ Proof
   \\ fs [EVERY_MEM,MEM_MAP,PULL_EXISTS]
 QED
 
+local
+  val thm = Q.prove (‘!t. ltree_finite t ==> ?r. from_rose r = t’,
+                     METIS_TAC [ltree_finite_from_rose]);
+in
+  (* |- !t. ltree_finite t ==> from_rose (to_rose t) = t *)
+  val to_rose_def = new_specification
+    ("to_rose_def", ["to_rose"],
+     SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] thm);
+end;
+
 Definition rose_node_def[simp] :
     rose_node (Rose a ts) = a
 End
@@ -995,6 +1005,13 @@ Definition rose_children_def[simp] :
     rose_children (Rose a ts) = ts
 End
 
+(* This is a general recursive reduction function for rose trees *)
+Definition rose_reduce_def :
+    rose_reduce f ((Rose a ts) :'a rose_tree) = f a (MAP (rose_reduce f) ts)
+Termination
+    WF_REL_TAC ‘measure (rose_tree_size (\x. 0) o SND)’
+End
+
 (* tidy up theory exports *)
 
 val _ = List.app Theory.delete_binding