src/HOL/Library/Tree.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68109 cebf36c14226 child 68998 818898556504 permissions -rw-r--r--
tuned equation
```     1 (* Author: Tobias Nipkow *)
```
```     2 (* Todo: minimal ipl of balanced trees *)
```
```     3
```
```     4 section \<open>Binary Tree\<close>
```
```     5
```
```     6 theory Tree
```
```     7 imports Main
```
```     8 begin
```
```     9
```
```    10 datatype 'a tree =
```
```    11   Leaf ("\<langle>\<rangle>") |
```
```    12   Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
```
```    13 datatype_compat tree
```
```    14
```
```    15 text\<open>Can be seen as counting the number of leaves rather than nodes:\<close>
```
```    16
```
```    17 definition size1 :: "'a tree \<Rightarrow> nat" where
```
```    18 "size1 t = size t + 1"
```
```    19
```
```    20 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
```
```    21 "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
```
```    22 "subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
```
```    23
```
```    24 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
```
```    25 "mirror \<langle>\<rangle> = Leaf" |
```
```    26 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>"
```
```    27
```
```    28 class height = fixes height :: "'a \<Rightarrow> nat"
```
```    29
```
```    30 instantiation tree :: (type)height
```
```    31 begin
```
```    32
```
```    33 fun height_tree :: "'a tree => nat" where
```
```    34 "height Leaf = 0" |
```
```    35 "height (Node t1 a t2) = max (height t1) (height t2) + 1"
```
```    36
```
```    37 instance ..
```
```    38
```
```    39 end
```
```    40
```
```    41 fun min_height :: "'a tree \<Rightarrow> nat" where
```
```    42 "min_height Leaf = 0" |
```
```    43 "min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
```
```    44
```
```    45 fun complete :: "'a tree \<Rightarrow> bool" where
```
```    46 "complete Leaf = True" |
```
```    47 "complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
```
```    48
```
```    49 definition balanced :: "'a tree \<Rightarrow> bool" where
```
```    50 "balanced t = (height t - min_height t \<le> 1)"
```
```    51
```
```    52 text \<open>Weight balanced:\<close>
```
```    53 fun wbalanced :: "'a tree \<Rightarrow> bool" where
```
```    54 "wbalanced Leaf = True" |
```
```    55 "wbalanced (Node l x r) = (abs(int(size l) - int(size r)) \<le> 1 \<and> wbalanced l \<and> wbalanced r)"
```
```    56
```
```    57 text \<open>Internal path length:\<close>
```
```    58 fun ipl :: "'a tree \<Rightarrow> nat" where
```
```    59 "ipl Leaf = 0 " |
```
```    60 "ipl (Node l _ r) = ipl l + size l + ipl r + size r"
```
```    61
```
```    62 fun preorder :: "'a tree \<Rightarrow> 'a list" where
```
```    63 "preorder \<langle>\<rangle> = []" |
```
```    64 "preorder \<langle>l, x, r\<rangle> = x # preorder l @ preorder r"
```
```    65
```
```    66 fun inorder :: "'a tree \<Rightarrow> 'a list" where
```
```    67 "inorder \<langle>\<rangle> = []" |
```
```    68 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r"
```
```    69
```
```    70 text\<open>A linear version avoiding append:\<close>
```
```    71 fun inorder2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
```
```    72 "inorder2 \<langle>\<rangle> xs = xs" |
```
```    73 "inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)"
```
```    74
```
```    75 fun postorder :: "'a tree \<Rightarrow> 'a list" where
```
```    76 "postorder \<langle>\<rangle> = []" |
```
```    77 "postorder \<langle>l, x, r\<rangle> = postorder l @ postorder r @ [x]"
```
```    78
```
```    79 text\<open>Binary Search Tree:\<close>
```
```    80 fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where
```
```    81 "bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True" |
```
```    82 "bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow>
```
```    83  bst_wrt P l \<and> bst_wrt P r \<and> (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x)"
```
```    84
```
```    85 abbreviation bst :: "('a::linorder) tree \<Rightarrow> bool" where
```
```    86 "bst \<equiv> bst_wrt (<)"
```
```    87
```
```    88 fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where
```
```    89 "heap Leaf = True" |
```
```    90 "heap (Node l m r) =
```
```    91   (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
```
```    92
```
```    93
```
```    94 subsection \<open>@{const map_tree}\<close>
```
```    95
```
```    96 lemma eq_map_tree_Leaf[simp]: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf"
```
```    97 by (rule tree.map_disc_iff)
```
```    98
```
```    99 lemma eq_Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> t = Leaf"
```
```   100 by (cases t) auto
```
```   101
```
```   102
```
```   103 subsection \<open>@{const size}\<close>
```
```   104
```
```   105 lemma size1_simps[simp]:
```
```   106   "size1 \<langle>\<rangle> = 1"
```
```   107   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
```
```   108 by (simp_all add: size1_def)
```
```   109
```
```   110 lemma size1_ge0[simp]: "0 < size1 t"
```
```   111 by (simp add: size1_def)
```
```   112
```
```   113 lemma eq_size_0[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
```
```   114 by(cases t) auto
```
```   115
```
```   116 lemma eq_0_size[simp]: "0 = size t \<longleftrightarrow> t = Leaf"
```
```   117 by(cases t) auto
```
```   118
```
```   119 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
```
```   120 by (cases t) auto
```
```   121
```
```   122 lemma size_map_tree[simp]: "size (map_tree f t) = size t"
```
```   123 by (induction t) auto
```
```   124
```
```   125 lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t"
```
```   126 by (simp add: size1_def)
```
```   127
```
```   128
```
```   129 subsection \<open>@{const set_tree}\<close>
```
```   130
```
```   131 lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
```
```   132 by (cases t) auto
```
```   133
```
```   134 lemma eq_empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> t = Leaf"
```
```   135 by (cases t) auto
```
```   136
```
```   137 lemma finite_set_tree[simp]: "finite(set_tree t)"
```
```   138 by(induction t) auto
```
```   139
```
```   140
```
```   141 subsection \<open>@{const subtrees}\<close>
```
```   142
```
```   143 lemma neq_subtrees_empty[simp]: "subtrees t \<noteq> {}"
```
```   144 by (cases t)(auto)
```
```   145
```
```   146 lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t"
```
```   147 by (cases t)(auto)
```
```   148
```
```   149 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
```
```   150 by (induction t)(auto)
```
```   151
```
```   152 lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t"
```
```   153 by (induction t) auto
```
```   154
```
```   155 lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t"
```
```   156 by (metis Node_notin_subtrees_if)
```
```   157
```
```   158
```
```   159 subsection \<open>@{const height} and @{const min_height}\<close>
```
```   160
```
```   161 lemma eq_height_0[simp]: "height t = 0 \<longleftrightarrow> t = Leaf"
```
```   162 by(cases t) auto
```
```   163
```
```   164 lemma eq_0_height[simp]: "0 = height t \<longleftrightarrow> t = Leaf"
```
```   165 by(cases t) auto
```
```   166
```
```   167 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
```
```   168 by (induction t) auto
```
```   169
```
```   170 lemma height_le_size_tree: "height t \<le> size (t::'a tree)"
```
```   171 by (induction t) auto
```
```   172
```
```   173 lemma size1_height: "size1 t \<le> 2 ^ height (t::'a tree)"
```
```   174 proof(induction t)
```
```   175   case (Node l a r)
```
```   176   show ?case
```
```   177   proof (cases "height l \<le> height r")
```
```   178     case True
```
```   179     have "size1(Node l a r) = size1 l + size1 r" by simp
```
```   180     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith
```
```   181     also have "\<dots> \<le> 2 ^ height r + 2 ^ height r" using True by simp
```
```   182     also have "\<dots> = 2 ^ height (Node l a r)"
```
```   183       using True by (auto simp: max_def mult_2)
```
```   184     finally show ?thesis .
```
```   185   next
```
```   186     case False
```
```   187     have "size1(Node l a r) = size1 l + size1 r" by simp
```
```   188     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith
```
```   189     also have "\<dots> \<le> 2 ^ height l + 2 ^ height l" using False by simp
```
```   190     finally show ?thesis using False by (auto simp: max_def mult_2)
```
```   191   qed
```
```   192 qed simp
```
```   193
```
```   194 corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
```
```   195 using size1_height[of t, unfolded size1_def] by(arith)
```
```   196
```
```   197 lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t"
```
```   198 by (induction t) auto
```
```   199
```
```   200
```
```   201 lemma min_height_le_height: "min_height t \<le> height t"
```
```   202 by(induction t) auto
```
```   203
```
```   204 lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
```
```   205 by (induction t) auto
```
```   206
```
```   207 lemma min_height_size1: "2 ^ min_height t \<le> size1 t"
```
```   208 proof(induction t)
```
```   209   case (Node l a r)
```
```   210   have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
```
```   211     by (simp add: min_def)
```
```   212   also have "\<dots> \<le> size1(Node l a r)" using Node.IH by simp
```
```   213   finally show ?case .
```
```   214 qed simp
```
```   215
```
```   216
```
```   217 subsection \<open>@{const complete}\<close>
```
```   218
```
```   219 lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)"
```
```   220 apply(induction t)
```
```   221  apply simp
```
```   222 apply (simp add: min_def max_def)
```
```   223 by (metis le_antisym le_trans min_height_le_height)
```
```   224
```
```   225 lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
```
```   226 by (induction t) auto
```
```   227
```
```   228 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
```
```   229 using size1_if_complete[simplified size1_def] by fastforce
```
```   230
```
```   231 lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
```
```   232 proof (induct "height t" arbitrary: t)
```
```   233   case 0 thus ?case by (simp)
```
```   234 next
```
```   235   case (Suc h)
```
```   236   hence "t \<noteq> Leaf" by auto
```
```   237   then obtain l a r where [simp]: "t = Node l a r"
```
```   238     by (auto simp: neq_Leaf_iff)
```
```   239   have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto)
```
```   240   have 3: "\<not> height l < h"
```
```   241   proof
```
```   242     assume 0: "height l < h"
```
```   243     have "size1 t = size1 l + size1 r" by simp
```
```   244     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
```
```   245       using size1_height[of l] size1_height[of r] by arith
```
```   246     also have " \<dots> < 2 ^ h + 2 ^ height r" using 0 by (simp)
```
```   247     also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 2 by (simp)
```
```   248     also have "\<dots> = 2 ^ (Suc h)" by (simp)
```
```   249     also have "\<dots> = size1 t" using Suc(2,3) by simp
```
```   250     finally have "size1 t < size1 t" .
```
```   251     thus False by (simp)
```
```   252   qed
```
```   253   have 4: "\<not> height r < h"
```
```   254   proof
```
```   255     assume 0: "height r < h"
```
```   256     have "size1 t = size1 l + size1 r" by simp
```
```   257     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
```
```   258       using size1_height[of l] size1_height[of r] by arith
```
```   259     also have " \<dots> < 2 ^ height l + 2 ^ h" using 0 by (simp)
```
```   260     also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 1 by (simp)
```
```   261     also have "\<dots> = 2 ^ (Suc h)" by (simp)
```
```   262     also have "\<dots> = size1 t" using Suc(2,3) by simp
```
```   263     finally have "size1 t < size1 t" .
```
```   264     thus False by (simp)
```
```   265   qed
```
```   266   from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+
```
```   267   hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r"
```
```   268     using Suc(3) size1_height[of l] size1_height[of r] by (auto)
```
```   269   with * Suc(1) show ?case by simp
```
```   270 qed
```
```   271
```
```   272 text\<open>The following proof involves \<open>\<ge>\<close>/\<open>>\<close> chains rather than the standard
```
```   273 \<open>\<le>\<close>/\<open><\<close> chains. To chain the elements together the transitivity rules \<open>xtrans\<close>
```
```   274 are used.\<close>
```
```   275
```
```   276 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
```
```   277 proof (induct "min_height t" arbitrary: t)
```
```   278   case 0 thus ?case by (simp add: size1_def)
```
```   279 next
```
```   280   case (Suc h)
```
```   281   hence "t \<noteq> Leaf" by auto
```
```   282   then obtain l a r where [simp]: "t = Node l a r"
```
```   283     by (auto simp: neq_Leaf_iff)
```
```   284   have 1: "h \<le> min_height l" and 2: "h \<le> min_height r" using Suc(2) by(auto)
```
```   285   have 3: "\<not> h < min_height l"
```
```   286   proof
```
```   287     assume 0: "h < min_height l"
```
```   288     have "size1 t = size1 l + size1 r" by simp
```
```   289     also note min_height_size1[of l]
```
```   290     also(xtrans) note min_height_size1[of r]
```
```   291     also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h"
```
```   292         using 0 by (simp add: diff_less_mono)
```
```   293     also(xtrans) have "(2::nat) ^ min_height r \<ge> 2 ^ h" using 2 by simp
```
```   294     also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
```
```   295     also have "\<dots> = size1 t" using Suc(2,3) by simp
```
```   296     finally show False by (simp add: diff_le_mono)
```
```   297   qed
```
```   298   have 4: "\<not> h < min_height r"
```
```   299   proof
```
```   300     assume 0: "h < min_height r"
```
```   301     have "size1 t = size1 l + size1 r" by simp
```
```   302     also note min_height_size1[of l]
```
```   303     also(xtrans) note min_height_size1[of r]
```
```   304     also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h"
```
```   305         using 0 by (simp add: diff_less_mono)
```
```   306     also(xtrans) have "(2::nat) ^ min_height l \<ge> 2 ^ h" using 1 by simp
```
```   307     also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
```
```   308     also have "\<dots> = size1 t" using Suc(2,3) by simp
```
```   309     finally show False by (simp add: diff_le_mono)
```
```   310   qed
```
```   311   from 1 2 3 4 have *: "min_height l = h" "min_height r = h" by linarith+
```
```   312   hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r"
```
```   313     using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto)
```
```   314   with * Suc(1) show ?case
```
```   315     by (simp add: complete_iff_height)
```
```   316 qed
```
```   317
```
```   318 lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t"
```
```   319 using complete_if_size1_height size1_if_complete by blast
```
```   320
```
```   321 text\<open>Better bounds for incomplete trees:\<close>
```
```   322
```
```   323 lemma size1_height_if_incomplete:
```
```   324   "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
```
```   325 by (meson antisym_conv complete_iff_size1 not_le size1_height)
```
```   326
```
```   327 lemma min_height_size1_if_incomplete:
```
```   328   "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
```
```   329 by (metis complete_if_size1_min_height le_less min_height_size1)
```
```   330
```
```   331
```
```   332 subsection \<open>@{const balanced}\<close>
```
```   333
```
```   334 lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l"
```
```   335 by(simp add: balanced_def)
```
```   336
```
```   337 lemma balanced_subtreeR: "balanced (Node l x r) \<Longrightarrow> balanced r"
```
```   338 by(simp add: balanced_def)
```
```   339
```
```   340 lemma balanced_subtrees: "\<lbrakk> balanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> balanced s"
```
```   341 using [[simp_depth_limit=1]]
```
```   342 by(induction t arbitrary: s)
```
```   343   (auto simp add: balanced_subtreeL balanced_subtreeR)
```
```   344
```
```   345 text\<open>Balanced trees have optimal height:\<close>
```
```   346
```
```   347 lemma balanced_optimal:
```
```   348 fixes t :: "'a tree" and t' :: "'b tree"
```
```   349 assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
```
```   350 proof (cases "complete t")
```
```   351   case True
```
```   352   have "(2::nat) ^ height t \<le> 2 ^ height t'"
```
```   353   proof -
```
```   354     have "2 ^ height t = size1 t"
```
```   355       using True by (simp add: complete_iff_height size1_if_complete)
```
```   356     also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_def)
```
```   357     also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height)
```
```   358     finally show ?thesis .
```
```   359   qed
```
```   360   thus ?thesis by (simp)
```
```   361 next
```
```   362   case False
```
```   363   have "(2::nat) ^ min_height t < 2 ^ height t'"
```
```   364   proof -
```
```   365     have "(2::nat) ^ min_height t < size1 t"
```
```   366       by(rule min_height_size1_if_incomplete[OF False])
```
```   367     also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_def)
```
```   368     also have "\<dots> \<le> 2 ^ height t'"  by(rule size1_height)
```
```   369     finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
```
```   370     thus ?thesis .
```
```   371   qed
```
```   372   hence *: "min_height t < height t'" by simp
```
```   373   have "min_height t + 1 = height t"
```
```   374     using min_height_le_height[of t] assms(1) False
```
```   375     by (simp add: complete_iff_height balanced_def)
```
```   376   with * show ?thesis by arith
```
```   377 qed
```
```   378
```
```   379
```
```   380 subsection \<open>@{const wbalanced}\<close>
```
```   381
```
```   382 lemma wbalanced_subtrees: "\<lbrakk> wbalanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> wbalanced s"
```
```   383 using [[simp_depth_limit=1]] by(induction t arbitrary: s) auto
```
```   384
```
```   385
```
```   386 subsection \<open>@{const ipl}\<close>
```
```   387
```
```   388 text \<open>The internal path length of a tree:\<close>
```
```   389
```
```   390 lemma ipl_if_complete_int:
```
```   391   "complete t \<Longrightarrow> int(ipl t) = (int(height t) - 2) * 2^(height t) + 2"
```
```   392 apply(induction t)
```
```   393  apply simp
```
```   394 apply simp
```
```   395 apply (simp add: algebra_simps size_if_complete of_nat_diff)
```
```   396 done
```
```   397
```
```   398
```
```   399 subsection "List of entries"
```
```   400
```
```   401 lemma eq_inorder_Nil[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
```
```   402 by (cases t) auto
```
```   403
```
```   404 lemma eq_Nil_inorder[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
```
```   405 by (cases t) auto
```
```   406
```
```   407 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
```
```   408 by (induction t) auto
```
```   409
```
```   410 lemma set_preorder[simp]: "set (preorder t) = set_tree t"
```
```   411 by (induction t) auto
```
```   412
```
```   413 lemma set_postorder[simp]: "set (postorder t) = set_tree t"
```
```   414 by (induction t) auto
```
```   415
```
```   416 lemma length_preorder[simp]: "length (preorder t) = size t"
```
```   417 by (induction t) auto
```
```   418
```
```   419 lemma length_inorder[simp]: "length (inorder t) = size t"
```
```   420 by (induction t) auto
```
```   421
```
```   422 lemma length_postorder[simp]: "length (postorder t) = size t"
```
```   423 by (induction t) auto
```
```   424
```
```   425 lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)"
```
```   426 by (induction t) auto
```
```   427
```
```   428 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)"
```
```   429 by (induction t) auto
```
```   430
```
```   431 lemma postorder_map: "postorder (map_tree f t) = map f (postorder t)"
```
```   432 by (induction t) auto
```
```   433
```
```   434 lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs"
```
```   435 by (induction t arbitrary: xs) auto
```
```   436
```
```   437
```
```   438 subsection \<open>Binary Search Tree\<close>
```
```   439
```
```   440 lemma bst_wrt_mono: "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> bst_wrt P t \<Longrightarrow> bst_wrt Q t"
```
```   441 by (induction t) (auto)
```
```   442
```
```   443 lemma bst_wrt_le_if_bst: "bst t \<Longrightarrow> bst_wrt (\<le>) t"
```
```   444 using bst_wrt_mono less_imp_le by blast
```
```   445
```
```   446 lemma bst_wrt_le_iff_sorted: "bst_wrt (\<le>) t \<longleftrightarrow> sorted (inorder t)"
```
```   447 apply (induction t)
```
```   448  apply(simp)
```
```   449 by (fastforce simp: sorted_append intro: less_imp_le less_trans)
```
```   450
```
```   451 lemma bst_iff_sorted_wrt_less: "bst t \<longleftrightarrow> sorted_wrt (<) (inorder t)"
```
```   452 apply (induction t)
```
```   453  apply simp
```
```   454 apply (fastforce simp: sorted_wrt_append)
```
```   455 done
```
```   456
```
```   457
```
```   458 subsection \<open>@{const heap}\<close>
```
```   459
```
```   460
```
```   461 subsection \<open>@{const mirror}\<close>
```
```   462
```
```   463 lemma mirror_Leaf[simp]: "mirror t = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>"
```
```   464 by (induction t) simp_all
```
```   465
```
```   466 lemma Leaf_mirror[simp]: "\<langle>\<rangle> = mirror t \<longleftrightarrow> t = \<langle>\<rangle>"
```
```   467 using mirror_Leaf by fastforce
```
```   468
```
```   469 lemma size_mirror[simp]: "size(mirror t) = size t"
```
```   470 by (induction t) simp_all
```
```   471
```
```   472 lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
```
```   473 by (simp add: size1_def)
```
```   474
```
```   475 lemma height_mirror[simp]: "height(mirror t) = height t"
```
```   476 by (induction t) simp_all
```
```   477
```
```   478 lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
```
```   479 by (induction t) simp_all
```
```   480
```
```   481 lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
```
```   482 by (induction t) simp_all
```
```   483
```
```   484 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
```
```   485 by (induction t) simp_all
```
```   486
```
```   487 lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)"
```
```   488 by (induction t) simp_all
```
```   489
```
```   490 lemma mirror_mirror[simp]: "mirror(mirror t) = t"
```
```   491 by (induction t) simp_all
```
```   492
```
```   493 end
```