# HG changeset patch
# User nipkow
# Date 1538922518 -7200
# Node ID 22fe10b4c0c6868863cb79c921febb056daa9355
# Parent  9dabb405a3baa3b2bdd9d2955e7e3742d0c1dec9
added Braun_Tree.thy

diff -r 9dabb405a3ba -r 22fe10b4c0c6 src/HOL/Data_Structures/Braun_Tree.thy
--- /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
diff -r 9dabb405a3ba -r 22fe10b4c0c6 src/HOL/Data_Structures/document/root.bib
--- 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}
 
diff -r 9dabb405a3ba -r 22fe10b4c0c6 src/HOL/ROOT
--- 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