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