--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Sun Oct 07 16:28:38 2018 +0200
@@ -0,0 +1,50 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Braun Trees\<close>
+
+theory Braun_Tree
+imports "HOL-Library.Tree_Real"
+begin
+
+text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
+and later Hoogerwoord~\cite{Hoogerwoord} who gave them their name.\<close>
+
+fun braun :: "'a tree \<Rightarrow> bool" where
+"braun Leaf = True" |
+"braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
+
+text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close>
+
+lemma braun_unique: "\<lbrakk> braun (t1::unit tree); braun t2; size t1 = size t2 \<rbrakk> \<Longrightarrow> t1 = t2"
+proof (induction t1 arbitrary: t2)
+ case Leaf thus ?case by simp
+next
+ case (Node l1 _ r1)
+ from Node.prems(3) have "t2 \<noteq> Leaf" by auto
+ then obtain l2 x2 r2 where [simp]: "t2 = Node l2 x2 r2" by (meson neq_Leaf_iff)
+ with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by simp
+ thus ?case using Node.prems(1,2) Node.IH by auto
+qed
+
+text \<open>Braun trees are balanced:\<close>
+
+lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t"
+proof(induction t)
+ case Leaf show ?case by (simp add: balanced_def)
+next
+ case (Node l x r)
+ have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B")
+ using Node.prems by auto
+ thus ?case
+ proof
+ assume "?A"
+ thus ?thesis using Node
+ apply(simp add: balanced_def min_def max_def)
+ by (metis Node.IH balanced_optimal le_antisym le_refl)
+ next
+ assume "?B"
+ thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto
+ qed
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Data_Structures/document/root.bib Sat Oct 06 20:49:40 2018 +0200
+++ b/src/HOL/Data_Structures/document/root.bib Sun Oct 07 16:28:38 2018 +0200
@@ -28,6 +28,10 @@
year = {2016}
}
+@unpublished{BraunRem,author={W. Braun and Martin Rem},
+title="A logarithmic implementation of flexible arrays",
+note="Memorandum MR83/4. Eindhoven University of Techology",year=1983}
+
@phdthesis{Crane72,author={Clark A. Crane},
title={Linear Lists and Prorty Queues as Balanced Binary Trees},
school={Computer Science Department, Stanford University},year=1972}
@@ -42,6 +46,13 @@
title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
volume=4,number=1,pages={83--112},year=1982}}
+@inproceedings{Hoogerwoord,author={Rob R. Hoogerwoord},
+title="A logarithmic implementation of flexible arrays",
+editor={R. Bird and C. Morgan and J. Woodcock},
+booktitle={Mathematics of Program Construction, Second International Conference},
+publisher={Springer},series={LNCS},volume=669,year=1992,
+pages={191-207}}
+
@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
--- a/src/HOL/ROOT Sat Oct 06 20:49:40 2018 +0200
+++ b/src/HOL/ROOT Sun Oct 07 16:28:38 2018 +0200
@@ -222,6 +222,7 @@
Brother12_Map
AA_Map
Set2_Join_RBT
+ Braun_Tree
Trie
Leftist_Heap
Binomial_Heap