# HG changeset patch
# User paulson
# Date 1146499818 -7200
# Node ID 90fb9e092e66697dfa250cc9945f541b462c3889
# Parent  0cd0bf32ac58c5a7d327ba01d55c82352f8bbaa1
a few more examples

diff -r 0cd0bf32ac58 -r 90fb9e092e66 src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Mon May 01 17:05:13 2006 +0200
+++ b/src/HOL/ex/BT.thy	Mon May 01 18:10:18 2006 +0200
@@ -98,11 +98,31 @@
    apply simp_all
   done
 
+lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
+  apply (induct t)
+   apply simp_all
+  done
+
 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
   apply (induct t)
    apply simp_all
   done
 
+lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
+  apply (induct t)
+   apply simp_all
+  done
+
+lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
+  apply (induct t)
+   apply simp_all
+  done
+
+lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
+  apply (induct t)
+   apply (simp_all add: left_distrib)
+  done
+
 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   apply (induct t)
    apply simp_all
@@ -133,14 +153,6 @@
    apply simp_all
   done
 
-lemma max_add_distrib_left:
-  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
-  shows  "(max x y) + z = max (x+z) (y+z)"
-apply (rule max_of_mono [THEN sym])
-apply clarify
-apply (rule add_le_cancel_right)
-done
-
 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
   apply (induct t1)
    apply (simp_all add: max_add_distrib_left)
@@ -152,4 +164,10 @@
    apply (simp_all add: left_distrib)
   done
 
+lemma bt_map_append:
+     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
+  apply (induct t1)
+   apply simp_all
+  done
+
 end