src/HOL/ex/BT.thy
 author haftmann Wed Sep 08 19:21:46 2010 +0200 (2010-09-08) changeset 39246 9e58f0499f57 parent 23236 91d71bde1112 child 49962 a8cc904a6820 permissions -rw-r--r--
modernized primrec
 clasohm@1476 1 (* Title: HOL/ex/BT.thy clasohm@1476 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory lcp@1167 3 Copyright 1995 University of Cambridge lcp@1167 4 paulson@20711 5 Binary trees lcp@1167 6 *) lcp@1167 7 wenzelm@11024 8 header {* Binary trees *} wenzelm@11024 9 haftmann@16417 10 theory BT imports Main begin lcp@1167 11 wenzelm@11024 12 datatype 'a bt = wenzelm@11024 13 Lf wenzelm@11024 14 | Br 'a "'a bt" "'a bt" wenzelm@11024 15 haftmann@39246 16 primrec n_nodes :: "'a bt => nat" where haftmann@39246 17 "n_nodes Lf = 0" haftmann@39246 18 | "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" haftmann@39246 19 haftmann@39246 20 primrec n_leaves :: "'a bt => nat" where haftmann@39246 21 "n_leaves Lf = Suc 0" haftmann@39246 22 | "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" lcp@1167 23 haftmann@39246 24 primrec depth :: "'a bt => nat" where haftmann@39246 25 "depth Lf = 0" haftmann@39246 26 | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" lcp@1167 27 haftmann@39246 28 primrec reflect :: "'a bt => 'a bt" where haftmann@39246 29 "reflect Lf = Lf" haftmann@39246 30 | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" paulson@19478 31 haftmann@39246 32 primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where berghofe@1896 33 "bt_map f Lf = Lf" haftmann@39246 34 | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" lcp@1167 35 haftmann@39246 36 primrec preorder :: "'a bt => 'a list" where paulson@19478 37 "preorder Lf = []" haftmann@39246 38 | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" lcp@1167 39 haftmann@39246 40 primrec inorder :: "'a bt => 'a list" where paulson@19478 41 "inorder Lf = []" haftmann@39246 42 | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" lcp@1167 43 haftmann@39246 44 primrec postorder :: "'a bt => 'a list" where paulson@19478 45 "postorder Lf = []" haftmann@39246 46 | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" lcp@1167 47 haftmann@39246 48 primrec append :: "'a bt => 'a bt => 'a bt" where haftmann@23236 49 "append Lf t = t" haftmann@39246 50 | "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" wenzelm@11024 51 wenzelm@11024 52 text {* \medskip BT simplification *} wenzelm@11024 53 wenzelm@11024 54 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" wenzelm@11024 55 apply (induct t) wenzelm@11024 56 apply auto wenzelm@11024 57 done wenzelm@11024 58 wenzelm@11024 59 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" wenzelm@11024 60 apply (induct t) wenzelm@11024 61 apply auto wenzelm@11024 62 done wenzelm@11024 63 paulson@19478 64 lemma depth_reflect: "depth (reflect t) = depth t" paulson@20711 65 apply (induct t) paulson@20711 66 apply auto paulson@19478 67 done paulson@19478 68 wenzelm@11024 69 text {* wenzelm@11024 70 The famous relationship between the numbers of leaves and nodes. wenzelm@11024 71 *} wenzelm@11024 72 wenzelm@11024 73 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" wenzelm@11024 74 apply (induct t) wenzelm@11024 75 apply auto wenzelm@11024 76 done wenzelm@11024 77 wenzelm@11024 78 lemma reflect_reflect_ident: "reflect (reflect t) = t" wenzelm@11024 79 apply (induct t) wenzelm@11024 80 apply auto wenzelm@11024 81 done wenzelm@11024 82 wenzelm@11024 83 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" wenzelm@11024 84 apply (induct t) wenzelm@11024 85 apply simp_all wenzelm@11024 86 done wenzelm@11024 87 paulson@19526 88 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" paulson@19526 89 apply (induct t) paulson@19526 90 apply simp_all paulson@19526 91 done paulson@19526 92 wenzelm@11024 93 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" wenzelm@11024 94 apply (induct t) wenzelm@11024 95 apply simp_all wenzelm@11024 96 done wenzelm@11024 97 paulson@19526 98 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" paulson@19526 99 apply (induct t) paulson@19526 100 apply simp_all paulson@19526 101 done paulson@19526 102 paulson@19526 103 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" paulson@19526 104 apply (induct t) paulson@19526 105 apply simp_all paulson@19526 106 done paulson@19526 107 paulson@19526 108 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" paulson@19526 109 apply (induct t) paulson@19526 110 apply (simp_all add: left_distrib) paulson@19526 111 done paulson@19526 112 wenzelm@11024 113 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" wenzelm@11024 114 apply (induct t) wenzelm@11024 115 apply simp_all wenzelm@11024 116 done wenzelm@11024 117 wenzelm@11024 118 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" wenzelm@11024 119 apply (induct t) wenzelm@11024 120 apply simp_all wenzelm@11024 121 done wenzelm@11024 122 wenzelm@11024 123 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" wenzelm@11024 124 apply (induct t) wenzelm@11024 125 apply simp_all wenzelm@11024 126 done wenzelm@11024 127 paulson@19478 128 text {* paulson@19478 129 Analogues of the standard properties of the append function for lists. paulson@19478 130 *} paulson@19478 131 paulson@19478 132 lemma append_assoc [simp]: haftmann@23236 133 "append (append t1 t2) t3 = append t1 (append t2 t3)" paulson@19478 134 apply (induct t1) paulson@19478 135 apply simp_all paulson@19478 136 done paulson@19478 137 haftmann@23236 138 lemma append_Lf2 [simp]: "append t Lf = t" paulson@19478 139 apply (induct t) paulson@19478 140 apply simp_all paulson@19478 141 done paulson@19478 142 haftmann@23236 143 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" paulson@19478 144 apply (induct t1) paulson@19478 145 apply (simp_all add: max_add_distrib_left) paulson@19478 146 done paulson@19478 147 paulson@19478 148 lemma n_leaves_append [simp]: haftmann@23236 149 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" paulson@19478 150 apply (induct t1) paulson@19478 151 apply (simp_all add: left_distrib) paulson@19478 152 done paulson@19478 153 paulson@19526 154 lemma bt_map_append: haftmann@23236 155 "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" paulson@19526 156 apply (induct t1) paulson@19526 157 apply simp_all paulson@19526 158 done paulson@19526 159 lcp@1167 160 end