Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 15 kB

Quelle Tree.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)
(* Todo: minimal ipl of almost complete trees *)

section \<open>Binary Tree\<close>

theory Tree
imports Main
begin

datatype 'a tree =
  Leaf (\<open>\<langle>\<rangle>\<close>) |
  Node "'a tree" ("value": 'a) "'a tree" (\(\indent=1 notation=\mixfix Node\\\_,/ _,/ _\)\)
datatype_compat tree

primrec left :: "'a tree \ 'a tree" where
"left (Node l v r) = l" |
"left Leaf = Leaf"

primrec right :: "'a tree \ 'a tree" where
"right (Node l v r) = r" |
"right Leaf = Leaf"

text\<open>Counting the number of leaves rather than nodes:\<close>

fun size1 :: "'a tree \ nat" where
"size1 \\ = 1" |
"size1 \l, x, r\ = size1 l + size1 r"

fun subtrees :: "'a tree \ 'a tree set" where
"subtrees \\ = {\\}" |
"subtrees (\l, a, r\) = {\l, a, r\} \ subtrees l \ subtrees r"

fun mirror :: "'a tree \ 'a tree" where
"mirror \\ = Leaf" |
"mirror \l,x,r\ = \mirror r, x, mirror l\"

class height = fixes height :: "'a \ nat"

instantiation tree :: (type)height
begin

fun height_tree :: "'a tree => nat" where
"height Leaf = 0" |
"height (Node l a r) = max (height l) (height r) + 1"

instance ..

end

fun min_height :: "'a tree \ nat" where
"min_height Leaf = 0" |
"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"

fun complete :: "'a tree \ bool" where
"complete Leaf = True" |
"complete (Node l x r) = (height l = height r \ complete l \ complete r)"

text \<open>Almost complete:\<close>
definition acomplete :: "'a tree \ bool" where
"acomplete t = (height t - min_height t \ 1)"

text \<open>Weight balanced:\<close>
fun wbalanced :: "'a tree \ bool" where
"wbalanced Leaf = True" |
"wbalanced (Node l x r) = (abs(int(size l) - int(size r)) \ 1 \ wbalanced l \ wbalanced r)"

text \<open>Internal path length:\<close>
fun ipl :: "'a tree \ nat" where
"ipl Leaf = 0 " |
"ipl (Node l _ r) = ipl l + size l + ipl r + size r"

fun preorder :: "'a tree \ 'a list" where
"preorder \\ = []" |
"preorder \l, x, r\ = x # preorder l @ preorder r"

fun inorder :: "'a tree \ 'a list" where
"inorder \\ = []" |
"inorder \l, x, r\ = inorder l @ [x] @ inorder r"

text\<open>A linear version avoiding append:\<close>
fun inorder2 :: "'a tree \ 'a list \ 'a list" where
"inorder2 \\ xs = xs" |
"inorder2 \l, x, r\ xs = inorder2 l (x # inorder2 r xs)"

fun postorder :: "'a tree \ 'a list" where
"postorder \\ = []" |
"postorder \l, x, r\ = postorder l @ postorder r @ [x]"

text\<open>Binary Search Tree:\<close>
fun bst_wrt :: "('a \ 'a \ bool) \ 'a tree \ bool" where
"bst_wrt P \\ \ True" |
"bst_wrt P \l, a, r\ \
(\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x) \<and> bst_wrt P l \<and> bst_wrt P r"

abbreviation bst :: "('a::linorder) tree \ bool" where
"bst \ bst_wrt (<)"

fun (in linorder) heap :: "'a tree \ bool" where
"heap Leaf = True" |
"heap (Node l m r) =
  ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"

subsection \<open>\<^const>\<open>map_tree\<close>\<close>

lemma eq_map_tree_Leaf[simp]: "map_tree f t = Leaf \ t = Leaf"
by (rule tree.map_disc_iff)

lemma eq_Leaf_map_tree[simp]: "Leaf = map_tree f t \ t = Leaf"
by (cases t) auto

subsection \<open>\<^const>\<open>size\<close>\<close>

lemma size1_size: "size1 t = size t + 1"
by (induction t) simp_all

lemma size1_ge0[simp]: "0 < size1 t"
by (simp add: size1_size)

lemma eq_size_0[simp]: "size t = 0 \ t = Leaf"
by(cases t) auto

lemma eq_0_size[simp]: "0 = size t \ t = Leaf"
by(cases t) auto

lemma neq_Leaf_iff: "(t \ \\) = (\l a r. t = \l, a, r\)"
by (cases t) auto

lemma size_map_tree[simp]: "size (map_tree f t) = size t"
by (induction t) auto

lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t"
by (simp add: size1_size)

subsection \<open>\<^const>\<open>set_tree\<close>\<close>

lemma eq_set_tree_empty[simp]: "set_tree t = {} \ t = Leaf"
by (cases t) auto

lemma eq_empty_set_tree[simp]: "{} = set_tree t \ t = Leaf"
by (cases t) auto

lemma finite_set_tree[simp]: "finite(set_tree t)"
by(induction t) auto

subsection \<open>\<^const>\<open>subtrees\<close>\<close>

lemma neq_subtrees_empty[simp]: "subtrees t \ {}"
by (cases t)(auto)

lemma neq_empty_subtrees[simp]: "{} \ subtrees t"
by (cases t)(auto)

lemma size_subtrees: "s \ subtrees t \ size s \ size t"
by(induction t)(auto)

lemma set_treeE: "a \ set_tree t \ \l r. \l, a, r\ \ subtrees t"
by (induction t)(auto)

lemma Node_notin_subtrees_if[simp]: "a \ set_tree t \ Node l a r \ subtrees t"
by (induction t) auto

lemma in_set_tree_if: "\l, a, r\ \ subtrees t \ a \ set_tree t"
by (metis Node_notin_subtrees_if)

subsection \<open>\<^const>\<open>height\<close> and \<^const>\<open>min_height\<close>\<close>

lemma eq_height_0[simp]: "height t = 0 \ t = Leaf"
by(cases t) auto

lemma eq_0_height[simp]: "0 = height t \ t = Leaf"
by(cases t) auto

lemma height_map_tree[simp]: "height (map_tree f t) = height t"
by (induction t) auto

lemma height_le_size_tree: "height t \ size (t::'a tree)"
by (induction t) auto

lemma size1_height: "size1 t \ 2 ^ height (t::'a tree)"
proof(induction t)
  case (Node l a r)
  show ?case
  proof (cases "height l \ height r")
    case True
    have "size1(Node l a r) = size1 l + size1 r" by simp
    also have "\ \ 2 ^ height l + 2 ^ height r" using Node.IH by arith
    also have "\ \ 2 ^ height r + 2 ^ height r" using True by simp
    also have "\ = 2 ^ height (Node l a r)"
      using True by (auto simp: max_def mult_2)
    finally show ?thesis .
  next
    case False
    have "size1(Node l a r) = size1 l + size1 r" by simp
    also have "\ \ 2 ^ height l + 2 ^ height r" using Node.IH by arith
    also have "\ \ 2 ^ height l + 2 ^ height l" using False by simp
    finally show ?thesis using False by (auto simp: max_def mult_2)
  qed
qed simp

corollary size_height: "size t \ 2 ^ height (t::'a tree) - 1"
using size1_height[of t, unfolded size1_size] by(arith)

lemma height_subtrees: "s \ subtrees t \ height s \ height t"
by (induction t) auto

lemma min_height_le_height: "min_height t \ height t"
by(induction t) auto

lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
by (induction t) auto

lemma min_height_size1: "2 ^ min_height t \ size1 t"
proof(induction t)
  case (Node l a r)
  have "(2::nat) ^ min_height (Node l a r) \ 2 ^ min_height l + 2 ^ min_height r"
    by (simp add: min_def)
  also have "\ \ size1(Node l a r)" using Node.IH by simp
  finally show ?case .
qed simp

subsection \<open>\<^const>\<open>complete\<close>\<close>

lemma complete_iff_height: "complete t \ (min_height t = height t)"
apply(induction t)
apply simp
apply (simp add: min_def max_def)
by (metis le_antisym le_trans min_height_le_height)

lemma size1_if_complete: "complete t \ size1 t = 2 ^ height t"
by (induction t) auto

lemma size_if_complete: "complete t \ size t = 2 ^ height t - 1"
using size1_if_complete[simplified size1_size] by fastforce

lemma size1_height_if_incomplete:
  "\ complete t \ size1 t < 2 ^ height t"
proof(induction t)
  case Leaf thus ?case by simp
next
  case (Node l x r)
  have 1: ?case if h: "height l < height r"
    using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
    by(auto simp: max_def simp del: power_strict_increasing_iff)
  have 2: ?case if h: "height l > height r"
    using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
    by(auto simp: max_def simp del: power_strict_increasing_iff)
  have 3: ?case if h: "height l = height r" and c: "\ complete l"
    using h size1_height[of r] Node.IH(1)[OF c] by(simp)
  have 4: ?case if h: "height l = height r" and c: "\ complete r"
    using h size1_height[of l] Node.IH(2)[OF c] by(simp)
  from 1 2 3 4 Node.prems show ?case apply (simp add: max_def) by linarith
qed

lemma complete_iff_min_height: "complete t \ (height t = min_height t)"
by(auto simp add: complete_iff_height)

lemma min_height_size1_if_incomplete:
  "\ complete t \ 2 ^ min_height t < size1 t"
proof(induction t)
  case Leaf thus ?case by simp
next
  case (Node l x r)
  have 1: ?case if h: "min_height l < min_height r"
    using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
    by(auto simp: max_def simp del: power_strict_increasing_iff)
  have 2: ?case if h: "min_height l > min_height r"
    using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
    by(auto simp: max_def simp del: power_strict_increasing_iff)
  have 3: ?case if h: "min_height l = min_height r" and c: "\ complete l"
    using h min_height_size1[of r] Node.IH(1)[OF c] by(simp add: complete_iff_min_height)
  have 4: ?case if h: "min_height l = min_height r" and c: "\ complete r"
    using h min_height_size1[of l] Node.IH(2)[OF c] by(simp add: complete_iff_min_height)
  from 1 2 3 4 Node.prems show ?case
    by (fastforce simp: complete_iff_min_height[THEN iffD1])
qed

lemma complete_if_size1_height: "size1 t = 2 ^ height t \ complete t"
using  size1_height_if_incomplete by fastforce

lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \ complete t"
using min_height_size1_if_incomplete by fastforce

lemma complete_iff_size1: "complete t \ size1 t = 2 ^ height t"
using complete_if_size1_height size1_if_complete by blast

subsection \<open>\<^const>\<open>acomplete\<close>\<close>

lemma acomplete_subtreeL: "acomplete (Node l x r) \ acomplete l"
by(simp add: acomplete_def)

lemma acomplete_subtreeR: "acomplete (Node l x r) \ acomplete r"
by(simp add: acomplete_def)

lemma acomplete_subtrees: "\ acomplete t; s \ subtrees t \ \ acomplete s"
using [[simp_depth_limit=1]]
by(induction t arbitrary: s)
  (auto simp add: acomplete_subtreeL acomplete_subtreeR)

text\<open>Balanced trees have optimal height:\<close>

lemma acomplete_optimal:
fixes t :: "'a tree" and t' :: "'b tree"
assumes "acomplete t" "size t \ size t'" shows "height t \ height t'"
proof (cases "complete t")
  case True
  have "(2::nat) ^ height t \ 2 ^ height t'"
  proof -
    have "2 ^ height t = size1 t"
      using True by (simp add: size1_if_complete)
    also have "\ \ size1 t'" using assms(2) by(simp add: size1_size)
    also have "\ \ 2 ^ height t'" by (rule size1_height)
    finally show ?thesis .
  qed
  thus ?thesis by (simp)
next
  case False
  have "(2::nat) ^ min_height t < 2 ^ height t'"
  proof -
    have "(2::nat) ^ min_height t < size1 t"
      by(rule min_height_size1_if_incomplete[OF False])
    also have "\ \ size1 t'" using assms(2) by (simp add: size1_size)
    also have "\ \ 2 ^ height t'" by(rule size1_height)
    finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
    thus ?thesis .
  qed
  hence *: "min_height t < height t'" by simp
  have "min_height t + 1 = height t"
    using min_height_le_height[of t] assms(1) False
    by (simp add: complete_iff_height acomplete_def)
  with * show ?thesis by arith
qed

subsection \<open>\<^const>\<open>wbalanced\<close>\<close>

lemma wbalanced_subtrees: "\ wbalanced t; s \ subtrees t \ \ wbalanced s"
using [[simp_depth_limit=1]] by(induction t arbitrary: s) auto

subsection \<open>\<^const>\<open>ipl\<close>\<close>

text \<open>The internal path length of a tree:\<close>

lemma ipl_if_complete_int:
  "complete t \ int(ipl t) = (int(height t) - 2) * 2^(height t) + 2"
apply(induction t)
apply simp
apply simp
apply (simp add: algebra_simps size_if_complete of_nat_diff)
done

subsection "List of entries"

lemma eq_inorder_Nil[simp]: "inorder t = [] \ t = Leaf"
by (cases t) auto

lemmas eq_Nil_inorder[simp] = eq_inorder_Nil[THEN eq_iff_swap]

lemma set_inorder[simp]: "set (inorder t) = set_tree t"
by (induction t) auto

lemma preorder_eq_Nil_iff[simp]: "(preorder t = []) = (t = \\)"
by (cases t) auto

lemmas Nil_eq_preorder_iff [simp] = preorder_eq_Nil_iff[THEN eq_iff_swap]

lemma preorder_eq_Cons_iff:
  "preorder t = x # xs \ (\ l r. t = \l, x, r\ \ xs = preorder l @ preorder r)"
by (cases t) auto

lemmas Cons_eq_preorder_iff = preorder_eq_Cons_iff[THEN eq_iff_swap]

lemma set_preorder[simp]: "set (preorder t) = set_tree t"
by (induction t) auto

lemma set_postorder[simp]: "set (postorder t) = set_tree t"
by (induction t) auto

lemma length_preorder[simp]: "length (preorder t) = size t"
by (induction t) auto

lemma length_inorder[simp]: "length (inorder t) = size t"
by (induction t) auto

lemma length_postorder[simp]: "length (postorder t) = size t"
by (induction t) auto

lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)"
by (induction t) auto

lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)"
by (induction t) auto

lemma postorder_map: "postorder (map_tree f t) = map f (postorder t)"
by (induction t) auto

lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs"
by (induction t arbitrary: xs) auto

subsection \<open>Binary Search Tree\<close>

lemma bst_wrt_mono: "(\x y. P x y \ Q x y) \ bst_wrt P t \ bst_wrt Q t"
by (induction t) (auto)

lemma bst_wrt_le_if_bst: "bst t \ bst_wrt (\) t"
using bst_wrt_mono less_imp_le by blast

lemma bst_wrt_le_iff_sorted: "bst_wrt (\) t \ sorted (inorder t)"
apply (induction t)
apply(simp)
by (fastforce simp: sorted_append intro: less_imp_le less_trans)

lemma bst_iff_sorted_wrt_less: "bst t \ sorted_wrt (<) (inorder t)"
apply (induction t)
apply simp
apply (fastforce simp: sorted_wrt_append)
done

subsection \<open>\<^const>\<open>heap\<close>\<close>

subsection \<open>\<^const>\<open>mirror\<close>\<close>

lemma mirror_Leaf[simp]: "mirror t = \\ \ t = \\"
by (induction t) simp_all

lemma Leaf_mirror[simp]: "\\ = mirror t \ t = \\"
using mirror_Leaf by fastforce

lemma size_mirror[simp]: "size(mirror t) = size t"
by (induction t) simp_all

lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
by (simp add: size1_size)

lemma height_mirror[simp]: "height(mirror t) = height t"
by (induction t) simp_all

lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
by (induction t) simp_all

lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
by (induction t) simp_all

lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
by (induction t) simp_all

lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)"
by (induction t) simp_all

lemma mirror_mirror[simp]: "mirror(mirror t) = t"
by (induction t) simp_all

end

quality95%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.