--- a/src/HOL/ex/BT.thy Thu Feb 01 20:48:58 2001 +0100
+++ b/src/HOL/ex/BT.thy Thu Feb 01 20:51:13 2001 +0100
@@ -3,26 +3,29 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
-Binary trees (based on the ZF version)
+Binary trees (based on the ZF version).
*)
-BT = Main +
+header {* Binary trees *}
+
+theory BT = Main:
-datatype 'a bt = Lf
- | Br 'a ('a bt) ('a bt)
-
+datatype 'a bt =
+ Lf
+ | Br 'a "'a bt" "'a bt"
+
consts
- n_nodes :: 'a bt => nat
- n_leaves :: 'a bt => nat
- reflect :: 'a bt => 'a bt
- bt_map :: ('a=>'b) => ('a bt => 'b bt)
- preorder :: 'a bt => 'a list
- inorder :: 'a bt => 'a list
- postorder :: 'a bt => 'a list
+ n_nodes :: "'a bt => nat"
+ n_leaves :: "'a bt => nat"
+ reflect :: "'a bt => 'a bt"
+ bt_map :: "('a => 'b) => ('a bt => 'b bt)"
+ preorder :: "'a bt => 'a list"
+ inorder :: "'a bt => 'a list"
+ postorder :: "'a bt => 'a list"
primrec
"n_nodes (Lf) = 0"
- "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
+ "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
primrec
"n_leaves (Lf) = Suc 0"
@@ -48,5 +51,56 @@
"postorder (Lf) = []"
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+
+text {* \medskip BT simplification *}
+
+lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
+ apply (induct t)
+ apply auto
+ done
+
+lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
+ apply (induct t)
+ apply auto
+ done
+
+text {*
+ The famous relationship between the numbers of leaves and nodes.
+*}
+
+lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
+ apply (induct t)
+ apply auto
+ done
+
+lemma reflect_reflect_ident: "reflect (reflect t) = t"
+ apply (induct t)
+ apply auto
+ done
+
+lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f 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 preorder_reflect: "preorder (reflect t) = rev (postorder t)"
+ apply (induct t)
+ apply simp_all
+ done
+
+lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
+ apply (induct t)
+ apply simp_all
+ done
+
+lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
+ apply (induct t)
+ apply simp_all
+ done
+
end
-