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