blanchet@43197: (*  Title:      HOL/Metis_Examples/Binary_Tree.thy
blanchet@43197:     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@36487:     Author:     Jasmin Blanchette, TU Muenchen
paulson@23449: 
blanchet@43197: Metis example featuring binary trees.
paulson@23449: *)
paulson@23449: 
wenzelm@58889: section {* Metis Example Featuring Binary Trees *}
paulson@23449: 
blanchet@43197: theory Binary_Tree
haftmann@27104: imports Main
haftmann@27104: begin
paulson@23449: 
blanchet@50705: declare [[metis_new_skolem]]
blanchet@42103: 
blanchet@58310: datatype 'a bt =
paulson@23449:     Lf
paulson@23449:   | Br 'a  "'a bt"  "'a bt"
paulson@23449: 
haftmann@39246: primrec n_nodes :: "'a bt => nat" where
haftmann@39246:   "n_nodes Lf = 0"
haftmann@39246: | "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
haftmann@39246: 
haftmann@39246: primrec n_leaves :: "'a bt => nat" where
haftmann@39246:   "n_leaves Lf = Suc 0"
haftmann@39246: | "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
paulson@23449: 
haftmann@39246: primrec depth :: "'a bt => nat" where
haftmann@39246:   "depth Lf = 0"
haftmann@39246: | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
paulson@23449: 
haftmann@39246: primrec reflect :: "'a bt => 'a bt" where
haftmann@39246:   "reflect Lf = Lf"
haftmann@39246: | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
paulson@23449: 
haftmann@39246: primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
paulson@23449:   "bt_map f Lf = Lf"
haftmann@39246: | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
paulson@23449: 
haftmann@39246: primrec preorder :: "'a bt => 'a list" where
paulson@23449:   "preorder Lf = []"
haftmann@39246: | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
paulson@23449: 
haftmann@39246: primrec inorder :: "'a bt => 'a list" where
paulson@23449:   "inorder Lf = []"
haftmann@39246: | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
paulson@23449: 
haftmann@39246: primrec postorder :: "'a bt => 'a list" where
paulson@23449:   "postorder Lf = []"
haftmann@39246: | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
paulson@23449: 
haftmann@39246: primrec append :: "'a bt => 'a bt => 'a bt" where
haftmann@39246:   "append Lf t = t"
haftmann@39246: | "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
paulson@23449: 
paulson@23449: text {* \medskip BT simplification *}
paulson@23449: 
paulson@23449: lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
blanchet@36484: proof (induct t)
blanchet@36487:   case Lf thus ?case
blanchet@36487:   proof -
wenzelm@53015:     let "?p\<^sub>1 x\<^sub>1" = "x\<^sub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
wenzelm@53015:     have "\<not> ?p\<^sub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
wenzelm@53015:     hence "\<not> ?p\<^sub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
blanchet@36487:     thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
blanchet@36487:   qed
blanchet@36484: next
blanchet@36484:   case (Br a t1 t2) thus ?case
haftmann@57512:     by (metis n_leaves.simps(2) add.commute reflect.simps(2))
blanchet@36484: qed
paulson@23449: 
paulson@23449: lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
blanchet@36484: proof (induct t)
blanchet@36484:   case Lf thus ?case by (metis reflect.simps(1))
blanchet@36484: next
blanchet@36484:   case (Br a t1 t2) thus ?case
haftmann@57512:     by (metis add.commute n_nodes.simps(2) reflect.simps(2))
blanchet@36484: qed
paulson@23449: 
paulson@23449: lemma depth_reflect: "depth (reflect t) = depth t"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis depth.simps(1) reflect.simps(1))
haftmann@54864: by (metis depth.simps(2) max.commute reflect.simps(2))
paulson@23449: 
paulson@23449: text {*
blanchet@36484: The famous relationship between the numbers of leaves and nodes.
paulson@23449: *}
paulson@23449: 
paulson@23449: lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis n_leaves.simps(1) n_nodes.simps(1))
blanchet@36484: by auto
paulson@23449: 
paulson@23449: lemma reflect_reflect_ident: "reflect (reflect t) = t"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis reflect.simps(1))
blanchet@36484: proof -
blanchet@36484:   fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
blanchet@36484:   assume A1: "reflect (reflect t1) = t1"
blanchet@36484:   assume A2: "reflect (reflect t2) = t2"
blanchet@36484:   have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
blanchet@36484:     using A1 by (metis reflect.simps(2))
blanchet@36484:   hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
blanchet@36484:     by (metis reflect.simps(2))
blanchet@36484:   hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
blanchet@36484:     using A2 by metis
blanchet@36484:   thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
blanchet@36484: qed
paulson@23449: 
paulson@23449: lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
blanchet@43197: apply (rule ext)
paulson@23449: apply (induct_tac y)
blanchet@36484:  apply (metis bt_map.simps(1))
blanchet@36571: by (metis bt_map.simps(2))
paulson@23449: 
haftmann@39246: lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
paulson@23449: apply (induct t)
haftmann@39246:  apply (metis append.simps(1) bt_map.simps(1))
haftmann@39246: by (metis append.simps(2) bt_map.simps(2))
paulson@23449: 
paulson@23449: lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis bt_map.simps(1))
blanchet@36484: by (metis bt_map.simps(2) o_eq_dest_lhs)
paulson@23449: 
paulson@23449: lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis bt_map.simps(1) reflect.simps(1))
blanchet@36484: by (metis bt_map.simps(2) reflect.simps(2))
paulson@23449: 
paulson@23449: lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
blanchet@36484: apply (induct t)
blanchet@55465:  apply (metis bt_map.simps(1) list.map(1) preorder.simps(1))
blanchet@36484: by simp
paulson@23449: 
paulson@23449: lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
blanchet@36484: proof (induct t)
blanchet@36484:   case Lf thus ?case
blanchet@36484:   proof -
blanchet@55465:     have "map f [] = []" by (metis list.map(1))
blanchet@36484:     hence "map f [] = inorder Lf" by (metis inorder.simps(1))
blanchet@36484:     hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
blanchet@36484:     thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
blanchet@36484:   qed
blanchet@36484: next
blanchet@36484:   case (Br a t1 t2) thus ?case by simp
blanchet@36484: qed
paulson@23449: 
paulson@23449: lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
blanchet@36484: by simp
paulson@23449: 
paulson@23449: lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis bt_map.simps(1) depth.simps(1))
blanchet@36484: by simp
paulson@23449: 
paulson@23449: lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis bt_map.simps(1) n_leaves.simps(1))
blanchet@36484: proof -
blanchet@36484:   fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
blanchet@36484:   assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
blanchet@36484:   assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
blanchet@36484:   have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
blanchet@36484:     using A1 by (metis n_leaves.simps(2))
blanchet@36484:   hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
blanchet@36484:     by (metis bt_map.simps(2))
blanchet@36484:   hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
blanchet@36484:     using A2 by metis
blanchet@36484:   have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
blanchet@36484:     by (metis n_leaves.simps(2))
blanchet@36484:   thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
blanchet@36484:     using F1 by metis
blanchet@36484: qed
paulson@23449: 
paulson@23449: lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
blanchet@36484:               reflect.simps(1))
haftmann@39246: apply simp
haftmann@39246: done
paulson@23449: 
paulson@23449: lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
blanchet@36484: by simp
blanchet@36484: (* Slow:
blanchet@36484: by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
blanchet@36484:           reflect.simps(2) rev.simps(2) rev_append)
blanchet@36484: *)
paulson@23449: 
paulson@23449: lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
blanchet@36484: apply (induct t)
blanchet@36484:  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
blanchet@36484:               reflect.simps(1))
blanchet@36484: by (metis preorder_reflect reflect_reflect_ident rev_swap)
paulson@23449: 
paulson@23449: text {*
blanchet@36484: Analogues of the standard properties of the append function for lists.
paulson@23449: *}
paulson@23449: 
haftmann@39246: lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
blanchet@36484: apply (induct t1)
haftmann@39246:  apply (metis append.simps(1))
haftmann@39246: by (metis append.simps(2))
paulson@23449: 
haftmann@39246: lemma append_Lf2 [simp]: "append t Lf = t"
blanchet@36484: apply (induct t)
haftmann@39246:  apply (metis append.simps(1))
haftmann@39246: by (metis append.simps(2))
blanchet@36484: 
blanchet@36484: declare max_add_distrib_left [simp]
paulson@23449: 
haftmann@39246: lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
blanchet@36484: apply (induct t1)
haftmann@39246:  apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
blanchet@36484: by simp
paulson@23449: 
haftmann@39246: lemma n_leaves_append [simp]:
haftmann@39246:      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
blanchet@36484: apply (induct t1)
haftmann@39246:  apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
huffman@45502:               Suc_eq_plus1)
webertj@49962: by (simp add: distrib_right)
paulson@23449: 
haftmann@39246: lemma (*bt_map_append:*)
haftmann@39246:      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
blanchet@36484: apply (induct t1)
haftmann@39246:  apply (metis append.simps(1) bt_map.simps(1))
haftmann@39246: by (metis bt_map_append)
paulson@23449: 
paulson@23449: end