diff --git a/src/HOL/Data_Structures/Interval_Tree.thy b/src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy
+++ b/src/HOL/Data_Structures/Interval_Tree.thy
@@ -1,298 +1,298 @@
 (* Author: Bohua Zhan, with modifications by Tobias Nipkow *)
 
 section \<open>Interval Trees\<close>
 
 theory Interval_Tree
 imports
   "HOL-Data_Structures.Cmp"
   "HOL-Data_Structures.List_Ins_Del"
   "HOL-Data_Structures.Isin2"
   "HOL-Data_Structures.Set_Specs"
 begin
 
 subsection \<open>Intervals\<close>
 
 text \<open>The following definition of intervals uses the \<^bold>\<open>typedef\<close> command
 to define the type of non-empty intervals as a subset of the type of pairs \<open>p\<close>
 where @{prop "fst p \<le> snd p"}:\<close>
 
 typedef (overloaded) 'a::linorder ivl =
   "{p :: 'a \<times> 'a. fst p \<le> snd p}" by auto
 
 text \<open>More precisely, @{typ "'a ivl"} is isomorphic with that subset via the function
 @{const Rep_ivl}. Hence the basic interval properties are not immediate but
 need simple proofs:\<close>
 
 definition low :: "'a::linorder ivl \<Rightarrow> 'a" where
 "low p = fst (Rep_ivl p)"
 
 definition high :: "'a::linorder ivl \<Rightarrow> 'a" where
 "high p = snd (Rep_ivl p)"
 
 lemma ivl_is_interval: "low p \<le> high p"
 by (metis Rep_ivl high_def low_def mem_Collect_eq)
 
 lemma ivl_inj: "low p = low q \<Longrightarrow> high p = high q \<Longrightarrow> p = q"
 by (metis Rep_ivl_inverse high_def low_def prod_eqI)
 
 text \<open>Now we can forget how exactly intervals were defined.\<close>
 
 
 instantiation ivl :: (linorder) linorder begin
 
 definition ivl_less: "(x < y) = (low x < low y | (low x = low y \<and> high x < high y))"
 definition ivl_less_eq: "(x \<le> y) = (low x < low y | (low x = low y \<and> high x \<le> high y))"
 
 instance proof
   fix x y z :: "'a ivl"
   show a: "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
     using ivl_less ivl_less_eq by force
   show b: "x \<le> x"
     by (simp add: ivl_less_eq)
   show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
     by (smt ivl_less_eq dual_order.trans less_trans)
   show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     using ivl_less_eq a ivl_inj ivl_less by fastforce
   show e: "x \<le> y \<or> y \<le> x"
     by (meson ivl_less_eq leI not_less_iff_gr_or_eq)
 qed end
 
 
 definition overlap :: "('a::linorder) ivl \<Rightarrow> 'a ivl \<Rightarrow> bool" where
 "overlap x y \<longleftrightarrow> (high x \<ge> low y \<and> high y \<ge> low x)"
 
 definition has_overlap :: "('a::linorder) ivl set \<Rightarrow> 'a ivl \<Rightarrow> bool" where
 "has_overlap S y \<longleftrightarrow> (\<exists>x\<in>S. overlap x y)"
 
 
 subsection \<open>Interval Trees\<close>
 
 type_synonym 'a ivl_tree = "('a ivl * 'a) tree"
 
 fun max_hi :: "('a::order_bot) ivl_tree \<Rightarrow> 'a" where
 "max_hi Leaf = bot" |
 "max_hi (Node _ (_,m) _) = m"
 
 definition max3 :: "('a::linorder) ivl \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
 "max3 a m n = max (high a) (max m n)"
 
 fun inv_max_hi :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
 "inv_max_hi Leaf \<longleftrightarrow> True" |
-"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (inv_max_hi l \<and> inv_max_hi r \<and> m = max3 a (max_hi l) (max_hi r))"
+"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (m = max3 a (max_hi l) (max_hi r) \<and> inv_max_hi l \<and> inv_max_hi r)"
 
 lemma max_hi_is_max:
   "inv_max_hi t \<Longrightarrow> a \<in> set_tree t \<Longrightarrow> high a \<le> max_hi t"
 by (induct t, auto simp add: max3_def max_def)
 
 lemma max_hi_exists:
   "inv_max_hi t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> \<exists>a\<in>set_tree t. high a = max_hi t"
 proof (induction t rule: tree2_induct)
   case Leaf
   then show ?case by auto
 next
   case N: (Node l v m r)
   then show ?case
   proof (cases l rule: tree2_cases)
     case Leaf
     then show ?thesis
       using N.prems(1) N.IH(2) by (cases r, auto simp add: max3_def max_def le_bot)
   next
     case Nl: Node
     then show ?thesis
     proof (cases r rule: tree2_cases)
       case Leaf
       then show ?thesis
         using N.prems(1) N.IH(1) Nl by (auto simp add: max3_def max_def le_bot)
     next
       case Nr: Node
       obtain p1 where p1: "p1 \<in> set_tree l" "high p1 = max_hi l"
         using N.IH(1) N.prems(1) Nl by auto
       obtain p2 where p2: "p2 \<in> set_tree r" "high p2 = max_hi r"
         using N.IH(2) N.prems(1) Nr by auto
       then show ?thesis
         using p1 p2 N.prems(1) by (auto simp add: max3_def max_def)
     qed
   qed
 qed
 
 
 subsection \<open>Insertion and Deletion\<close>
 
 definition node where
 [simp]: "node l a r = Node l (a, max3 a (max_hi l) (max_hi r)) r"
 
 fun insert :: "'a::{linorder,order_bot} ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree" where
 "insert x Leaf = Node Leaf (x, high x) Leaf" |
 "insert x (Node l (a, m) r) =
   (case cmp x a of
      EQ \<Rightarrow> Node l (a, m) r |
      LT \<Rightarrow> node (insert x l) a r |
      GT \<Rightarrow> node l a (insert x r))"
 
 lemma inorder_insert:
   "sorted (inorder t) \<Longrightarrow> inorder (insert x t) = ins_list x (inorder t)"
 by (induct t rule: tree2_induct) (auto simp: ins_list_simps)
 
 lemma inv_max_hi_insert:
   "inv_max_hi t \<Longrightarrow> inv_max_hi (insert x t)"
 by (induct t rule: tree2_induct) (auto simp add: max3_def)
 
 fun split_min :: "'a::{linorder,order_bot} ivl_tree \<Rightarrow> 'a ivl \<times> 'a ivl_tree" where
 "split_min (Node l (a, m) r) =
   (if l = Leaf then (a, r)
    else let (x,l') = split_min l in (x, node l' a r))"
 
 fun delete :: "'a::{linorder,order_bot} ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree" where
 "delete x Leaf = Leaf" |
 "delete x (Node l (a, m) r) =
   (case cmp x a of
      LT \<Rightarrow> node (delete x l) a r |
      GT \<Rightarrow> node l a (delete x r) |
      EQ \<Rightarrow> if r = Leaf then l else
            let (a', r') = split_min r in node l a' r')"
 
 lemma split_minD:
   "split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
 by (induct t arbitrary: t' rule: split_min.induct)
    (auto simp: sorted_lems split: prod.splits if_splits)
 
 lemma inorder_delete:
   "sorted (inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
 by (induct t)
    (auto simp: del_list_simps split_minD Let_def split: prod.splits)
 
 lemma inv_max_hi_split_min:
   "\<lbrakk> t \<noteq> Leaf;  inv_max_hi t \<rbrakk> \<Longrightarrow> inv_max_hi (snd (split_min t))"
 by (induct t) (auto split: prod.splits)
 
 lemma inv_max_hi_delete:
   "inv_max_hi t \<Longrightarrow> inv_max_hi (delete x t)"
 apply (induct t)
  apply simp
 using inv_max_hi_split_min by (fastforce simp add: Let_def split: prod.splits)
 
 
 subsection \<open>Search\<close>
 
 text \<open>Does interval \<open>x\<close> overlap with any interval in the tree?\<close>
 
 fun search :: "'a::{linorder,order_bot} ivl_tree \<Rightarrow> 'a ivl \<Rightarrow> bool" where
 "search Leaf x = False" |
 "search (Node l (a, m) r) x =
   (if overlap x a then True
    else if l \<noteq> Leaf \<and> max_hi l \<ge> low x then search l x
    else search r x)"
 
 lemma search_correct:
   "inv_max_hi t \<Longrightarrow> sorted (inorder t) \<Longrightarrow> search t x = has_overlap (set_tree t) x"
 proof (induction t rule: tree2_induct)
   case Leaf
   then show ?case by (auto simp add: has_overlap_def)
 next
   case (Node l a m r)
   have search_l: "search l x = has_overlap (set_tree l) x"
     using Node.IH(1) Node.prems by (auto simp: sorted_wrt_append)
   have search_r: "search r x = has_overlap (set_tree r) x"
     using Node.IH(2) Node.prems by (auto simp: sorted_wrt_append)
   show ?case
   proof (cases "overlap a x")
     case True
     thus ?thesis by (auto simp: overlap_def has_overlap_def)
   next
     case a_disjoint: False
     then show ?thesis
     proof cases
       assume [simp]: "l = Leaf"
       have search_eval: "search (Node l (a, m) r) x = search r x"
         using a_disjoint overlap_def by auto
       show ?thesis
         unfolding search_eval search_r
         by (auto simp add: has_overlap_def a_disjoint)
     next
       assume "l \<noteq> Leaf"
       then show ?thesis
       proof (cases "max_hi l \<ge> low x")
         case max_hi_l_ge: True
         have "inv_max_hi l"
           using Node.prems(1) by auto
         then obtain p where p: "p \<in> set_tree l" "high p = max_hi l"
           using \<open>l \<noteq> Leaf\<close> max_hi_exists by auto
         have search_eval: "search (Node l (a, m) r) x = search l x"
           using a_disjoint \<open>l \<noteq> Leaf\<close> max_hi_l_ge by (auto simp: overlap_def)
         show ?thesis
         proof (cases "low p \<le> high x")
           case True
           have "overlap p x"
             unfolding overlap_def using True p(2) max_hi_l_ge by auto
           then show ?thesis
             unfolding search_eval search_l
             using p(1) by(auto simp: has_overlap_def overlap_def)
         next
           case False
           have "\<not>overlap x rp" if asm: "rp \<in> set_tree r" for rp
           proof -
             have "low p \<le> low rp"
               using asm p(1) Node(4) by(fastforce simp: sorted_wrt_append ivl_less)
             then show ?thesis
               using False by (auto simp: overlap_def)
           qed
           then show ?thesis
             unfolding search_eval search_l
             using a_disjoint by (auto simp: has_overlap_def overlap_def)
         qed
       next
         case False
         have search_eval: "search (Node l (a, m) r) x = search r x"
           using a_disjoint False by (auto simp: overlap_def)
         have "\<not>overlap x lp" if asm: "lp \<in> set_tree l" for lp
           using asm False Node.prems(1) max_hi_is_max
           by (fastforce simp: overlap_def)
         then show ?thesis
           unfolding search_eval search_r
           using a_disjoint by (auto simp: has_overlap_def overlap_def)
       qed
     qed
   qed
 qed
 
 definition empty :: "'a ivl_tree" where
 "empty = Leaf"
 
 
 subsection \<open>Specification\<close>
 
 locale Interval_Set = Set +
   fixes has_overlap :: "'t \<Rightarrow> 'a::linorder ivl \<Rightarrow> bool"
   assumes set_overlap: "invar s \<Longrightarrow> has_overlap s x = Interval_Tree.has_overlap (set s) x"
 
 interpretation S: Interval_Set
   where empty = Leaf and insert = insert and delete = delete
   and has_overlap = search and isin = isin and set = set_tree
   and invar = "\<lambda>t. inv_max_hi t \<and> sorted (inorder t)"
 proof (standard, goal_cases)
   case 1
   then show ?case by auto
 next
   case 2
   then show ?case by (simp add: isin_set_inorder)
 next
   case 3
   then show ?case by(simp add: inorder_insert set_ins_list flip: set_inorder)
 next
   case 4
   then show ?case by(simp add: inorder_delete set_del_list flip: set_inorder)
 next
   case 5
   then show ?case by auto
 next
   case 6
   then show ?case by (simp add: inorder_insert inv_max_hi_insert sorted_ins_list)
 next
   case 7
   then show ?case by (simp add: inorder_delete inv_max_hi_delete sorted_del_list)
 next
   case 8
   then show ?case by (simp add: search_correct)
 qed
 
 end
diff --git a/src/HOL/Data_Structures/RBT_Set.thy b/src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy
+++ b/src/HOL/Data_Structures/RBT_Set.thy
@@ -1,322 +1,322 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>Red-Black Tree Implementation of Sets\<close>
 
 theory RBT_Set
 imports
   Complex_Main
   RBT
   Cmp
   Isin2
 begin
 
 definition empty :: "'a rbt" where
 "empty = Leaf"
 
 fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "ins x Leaf = R Leaf x Leaf" |
 "ins x (B l a r) =
   (case cmp x a of
      LT \<Rightarrow> baliL (ins x l) a r |
      GT \<Rightarrow> baliR l a (ins x r) |
      EQ \<Rightarrow> B l a r)" |
 "ins x (R l a r) =
   (case cmp x a of
     LT \<Rightarrow> R (ins x l) a r |
     GT \<Rightarrow> R l a (ins x r) |
     EQ \<Rightarrow> R l a r)"
 
 definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "insert x t = paint Black (ins x t)"
 
 fun color :: "'a rbt \<Rightarrow> color" where
 "color Leaf = Black" |
 "color (Node _ (_, c) _) = c"
 
 fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "del x Leaf = Leaf" |
 "del x (Node l (a, _) r) =
   (case cmp x a of
      LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
            then baldL (del x l) a r else R (del x l) a r |
      GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
            then baldR l a (del x r) else R l a (del x r) |
      EQ \<Rightarrow> join l r)"
 
 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "delete x t = paint Black (del x t)"
 
 
 subsection "Functional Correctness Proofs"
 
 lemma inorder_paint: "inorder(paint c t) = inorder t"
 by(cases t) (auto)
 
 lemma inorder_baliL:
   "inorder(baliL l a r) = inorder l @ a # inorder r"
 by(cases "(l,a,r)" rule: baliL.cases) (auto)
 
 lemma inorder_baliR:
   "inorder(baliR l a r) = inorder l @ a # inorder r"
 by(cases "(l,a,r)" rule: baliR.cases) (auto)
 
 lemma inorder_ins:
   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
 by(induction x t rule: ins.induct)
   (auto simp: ins_list_simps inorder_baliL inorder_baliR)
 
 lemma inorder_insert:
   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
 by (simp add: insert_def inorder_ins inorder_paint)
 
 lemma inorder_baldL:
   "inorder(baldL l a r) = inorder l @ a # inorder r"
 by(cases "(l,a,r)" rule: baldL.cases)
   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
 
 lemma inorder_baldR:
   "inorder(baldR l a r) = inorder l @ a # inorder r"
 by(cases "(l,a,r)" rule: baldR.cases)
   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
 
 lemma inorder_join:
   "inorder(join l r) = inorder l @ inorder r"
 by(induction l r rule: join.induct)
   (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
 
 lemma inorder_del:
  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
 by(induction x t rule: del.induct)
   (auto simp: del_list_simps inorder_join inorder_baldL inorder_baldR)
 
 lemma inorder_delete:
   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by (auto simp: delete_def inorder_del inorder_paint)
 
 
 subsection \<open>Structural invariants\<close>
 
 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
 by (cases c) auto
 
 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
 
 fun bheight :: "'a rbt \<Rightarrow> nat" where
 "bheight Leaf = 0" |
 "bheight (Node l (x, c) r) = (if c = Black then bheight l + 1 else bheight l)"
 
 fun invc :: "'a rbt \<Rightarrow> bool" where
 "invc Leaf = True" |
 "invc (Node l (a,c) r) =
-  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
+  ((c = Red \<longrightarrow> color l = Black \<and> color r = Black) \<and> invc l \<and> invc r)"
 
 text \<open>Weaker version:\<close>
 abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where
 "invc2 t \<equiv> invc(paint Black t)"
 
 fun invh :: "'a rbt \<Rightarrow> bool" where
 "invh Leaf = True" |
-"invh (Node l (x, c) r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
+"invh (Node l (x, c) r) = (bheight l = bheight r \<and> invh l \<and> invh r)"
 
 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
 by (cases t rule: tree2_cases) simp+
 
 definition rbt :: "'a rbt \<Rightarrow> bool" where
 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
 
 lemma color_paint_Black: "color (paint Black t) = Black"
 by (cases t) auto
 
 lemma paint2: "paint c2 (paint c1 t) = paint c2 t"
 by (cases t) auto
 
 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
 by (cases t) auto
 
 lemma invc_baliL:
   "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
 by (induct l a r rule: baliL.induct) auto
 
 lemma invc_baliR:
   "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
 by (induct l a r rule: baliR.induct) auto
 
 lemma bheight_baliL:
   "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
 by (induct l a r rule: baliL.induct) auto
 
 lemma bheight_baliR:
   "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
 by (induct l a r rule: baliR.induct) auto
 
 lemma invh_baliL: 
   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
 by (induct l a r rule: baliL.induct) auto
 
 lemma invh_baliR: 
   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
 by (induct l a r rule: baliR.induct) auto
 
 text \<open>All in one:\<close>
 
 lemma inv_baliR: "\<lbrakk> invh l; invh r; invc l; invc2 r; bheight l = bheight r \<rbrakk>
  \<Longrightarrow> invc (baliR l a r) \<and> invh (baliR l a r) \<and> bheight (baliR l a r) = Suc (bheight l)"
 by (induct l a r rule: baliR.induct) auto
 
 lemma inv_baliL: "\<lbrakk> invh l; invh r; invc2 l; invc r; bheight l = bheight r \<rbrakk>
  \<Longrightarrow> invc (baliL l a r) \<and> invh (baliL l a r) \<and> bheight (baliL l a r) = Suc (bheight l)"
 by (induct l a r rule: baliL.induct) auto
 
 subsubsection \<open>Insertion\<close>
 
 lemma invc_ins: "invc t \<longrightarrow> invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t))"
 by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
 
 lemma invh_ins: "invh t \<Longrightarrow> invh (ins x t) \<and> bheight (ins x t) = bheight t"
 by(induct x t rule: ins.induct)
   (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
 
 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
 by (simp add: invc_ins invh_ins color_paint_Black invh_paint rbt_def insert_def)
 
 text \<open>All in one:\<close>
 
 lemma inv_ins: "\<lbrakk> invc t; invh t \<rbrakk> \<Longrightarrow>
   invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t)) \<and>
   invh(ins x t) \<and> bheight (ins x t) = bheight t"
 by (induct x t rule: ins.induct) (auto simp: inv_baliL inv_baliR invc2I)
 
 theorem rbt_insert2: "rbt t \<Longrightarrow> rbt (insert x t)"
 by (simp add: inv_ins color_paint_Black invh_paint rbt_def insert_def)
 
 
 subsubsection \<open>Deletion\<close>
 
 lemma bheight_paint_Red:
   "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
 by (cases t) auto
 
 lemma invh_baldL_invc:
   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
    \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
 by (induct l a r rule: baldL.induct)
    (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
 
 lemma invh_baldL_Black: 
   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black \<rbrakk>
    \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
 by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
 
 lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
 by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
 
 lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
 by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint2 invc2I)
 
 lemma invh_baldR_invc:
   "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1;  invc l \<rbrakk>
   \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
 by(induct l a r rule: baldR.induct)
   (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
 
 lemma invc_baldR: "\<lbrakk>invc l; invc2 r; color l = Black\<rbrakk> \<Longrightarrow> invc (baldR l a r)"
 by (induct l a r rule: baldR.induct) (simp_all add: invc_baliL)
 
 lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)"
 by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint2 invc2I)
 
 lemma invh_join:
   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
   \<Longrightarrow> invh (join l r) \<and> bheight (join l r) = bheight l"
 by (induct l r rule: join.induct) 
    (auto simp: invh_baldL_Black split: tree.splits color.splits)
 
 lemma invc_join: 
   "\<lbrakk> invc l; invc r \<rbrakk> \<Longrightarrow>
   (color l = Black \<and> color r = Black \<longrightarrow> invc (join l r)) \<and> invc2 (join l r)"
 by (induct l r rule: join.induct)
    (auto simp: invc_baldL invc2I split: tree.splits color.splits)
 
 text \<open>All in one:\<close>
 
 lemma inv_baldL:
   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r; invc2 l; invc r \<rbrakk>
    \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r
   \<and> invc2 (baldL l a r) \<and> (color r = Black \<longrightarrow> invc (baldL l a r))"
 by (induct l a r rule: baldL.induct)
    (auto simp: inv_baliR invh_paint bheight_baliR bheight_paint_Red paint2 invc2I)
 
 lemma inv_baldR:
   "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1; invc l; invc2 r \<rbrakk>
    \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l
   \<and> invc2 (baldR l a r) \<and> (color l = Black \<longrightarrow> invc (baldR l a r))"
 by (induct l a r rule: baldR.induct)
    (auto simp: inv_baliL invh_paint bheight_baliL bheight_paint_Red paint2 invc2I)
 
 lemma inv_join:
   "\<lbrakk> invh l; invh r; bheight l = bheight r; invc l; invc r \<rbrakk>
   \<Longrightarrow> invh (join l r) \<and> bheight (join l r) = bheight l
   \<and> invc2 (join l r) \<and> (color l = Black \<and> color r = Black \<longrightarrow> invc (join l r))"
 by (induct l r rule: join.induct) 
    (auto simp: invh_baldL_Black inv_baldL invc2I split: tree.splits color.splits)
 
 lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r"
 by(cases t rule: tree2_cases) auto
 
 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
    invh (del x t) \<and>
    (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
     color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
 by(induct x t rule: del.induct)
   (auto simp: inv_baldL inv_baldR inv_join dest!: neq_LeafD)
 
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
 by (metis delete_def rbt_def color_paint_Black inv_del invc2I invh_paint)
 
 text \<open>Overall correctness:\<close>
 
 interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = rbt
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: empty_def)
 next
   case 2 thus ?case by(simp add: isin_set_inorder)
 next
   case 3 thus ?case by(simp add: inorder_insert)
 next
   case 4 thus ?case by(simp add: inorder_delete)
 next
   case 5 thus ?case by (simp add: rbt_def empty_def) 
 next
   case 6 thus ?case by (simp add: rbt_insert) 
 next
   case 7 thus ?case by (simp add: rbt_delete) 
 qed
 
 
 subsection \<open>Height-Size Relation\<close>
 
 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
 by(induction t) (auto split: if_split_asm)
 
 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
 by(auto simp: rbt_def dest: rbt_height_bheight_if)
 
 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
 by (induction t) auto
 
 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
 proof -
   have "2 powr (height t / 2) \<le> 2 powr bheight t"
     using rbt_height_bheight[OF assms] by (simp)
   also have "\<dots> \<le> size1 t" using assms
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
   hence "height t / 2 \<le> log 2 (size1 t)"
     by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed
 
 end
diff --git a/src/HOL/Data_Structures/Tree2.thy b/src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy
+++ b/src/HOL/Data_Structures/Tree2.thy
@@ -1,42 +1,42 @@
 section \<open>Augmented Tree (Tree2)\<close>
 
 theory Tree2
 imports "HOL-Library.Tree"
 begin
 
 text \<open>This theory provides the basic infrastructure for the type @{typ \<open>('a * 'b) tree\<close>}
 of augmented trees where @{typ 'a} is the key and @{typ 'b} some additional information.\<close>
 
 text \<open>IMPORTANT: Inductions and cases analyses on augmented trees need to use the following
 two rules explicitly. They generate nodes of the form @{term "Node l (a,b) r"}
 rather than @{term "Node l a r"} for trees of type @{typ "'a tree"}.\<close>
 
 lemmas tree2_induct = tree.induct[where 'a = "'a * 'b", split_format(complete)]
 
 lemmas tree2_cases = tree.exhaust[where 'a = "'a * 'b", split_format(complete)]
 
 fun inorder :: "('a*'b)tree \<Rightarrow> 'a list" where
 "inorder Leaf = []" |
 "inorder (Node l (a,_) r) = inorder l @ a # inorder r"
 
 fun set_tree :: "('a*'b) tree \<Rightarrow> 'a set" where
 "set_tree Leaf = {}" |
-"set_tree (Node l (a,_) r) = Set.insert a (set_tree l \<union> set_tree r)"
+"set_tree (Node l (a,_) r) = {a} \<union> set_tree l \<union> set_tree r"
 
 fun bst :: "('a::linorder*'b) tree \<Rightarrow> bool" where
 "bst Leaf = True" |
-"bst (Node l (a, _) r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"
+"bst (Node l (a, _) r) = ((\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x) \<and> bst l \<and> bst r)"
 
 lemma finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto
 
 lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
 lemma length_inorder[simp]: "length (inorder t) = size t"
 by (induction t) auto
 
 end
diff --git a/src/HOL/Data_Structures/Tree23.thy b/src/HOL/Data_Structures/Tree23.thy
--- a/src/HOL/Data_Structures/Tree23.thy
+++ b/src/HOL/Data_Structures/Tree23.thy
@@ -1,46 +1,46 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>2-3 Trees\<close>
 
 theory Tree23
 imports Main
 begin
 
 class height =
 fixes height :: "'a \<Rightarrow> nat"
 
 datatype 'a tree23 =
   Leaf ("\<langle>\<rangle>") |
   Node2 "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _\<rangle>") |
   Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _, _, _\<rangle>")
 
 fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
 "inorder Leaf = []" |
 "inorder(Node2 l a r) = inorder l @ a # inorder r" |
 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
 
 
 instantiation tree23 :: (type)height
 begin
 
 fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where
 "height Leaf = 0" |
 "height (Node2 l _ r) = Suc(max (height l) (height r))" |
 "height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
 
 instance ..
 
 end
 
 text \<open>Completeness:\<close>
 
 fun complete :: "'a tree23 \<Rightarrow> bool" where
 "complete Leaf = True" |
-"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node2 l _ r) = (height l = height r \<and> complete l & complete r)" |
 "complete (Node3 l _ m _ r) =
-  (complete l & complete m & complete r & height l = height m & height m = height r)"
+  (height l = height m & height m = height r & complete l & complete m & complete r)"
 
 lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
 by (induction t) auto
 
 end
diff --git a/src/HOL/Library/Tree.thy b/src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy
+++ b/src/HOL/Library/Tree.thy
@@ -1,455 +1,455 @@
 (* Author: Tobias Nipkow *)
 (* Todo: minimal ipl of almost complete trees *)
 
 section \<open>Binary Tree\<close>
 
 theory Tree
 imports Main
 begin
 
 datatype 'a tree =
   Leaf ("\<langle>\<rangle>") |
   Node "'a tree" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
 primrec left :: "'a tree \<Rightarrow> 'a tree" where
 "left (Node l v r) = l" |
 "left Leaf = Leaf"
 
 primrec right :: "'a tree \<Rightarrow> '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 \<Rightarrow> nat" where
 "size1 \<langle>\<rangle> = 1" |
 "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 
 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
 "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
-"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
+"subtrees (\<langle>l, a, r\<rangle>) = {\<langle>l, a, r\<rangle>} \<union> subtrees l \<union> subtrees r"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror \<langle>\<rangle> = Leaf" |
 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>"
 
 class height = fixes height :: "'a \<Rightarrow> 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 \<Rightarrow> nat" where
 "min_height Leaf = 0" |
 "min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
 
 fun complete :: "'a tree \<Rightarrow> bool" where
 "complete Leaf = True" |
-"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
+"complete (Node l x r) = (height l = height r \<and> complete l \<and> complete r)"
 
 text \<open>Almost complete:\<close>
 definition acomplete :: "'a tree \<Rightarrow> bool" where
 "acomplete t = (height t - min_height t \<le> 1)"
 
 text \<open>Weight balanced:\<close>
 fun wbalanced :: "'a tree \<Rightarrow> bool" where
 "wbalanced Leaf = True" |
 "wbalanced (Node l x r) = (abs(int(size l) - int(size r)) \<le> 1 \<and> wbalanced l \<and> wbalanced r)"
 
 text \<open>Internal path length:\<close>
 fun ipl :: "'a tree \<Rightarrow> nat" where
 "ipl Leaf = 0 " |
 "ipl (Node l _ r) = ipl l + size l + ipl r + size r"
 
 fun preorder :: "'a tree \<Rightarrow> 'a list" where
 "preorder \<langle>\<rangle> = []" |
 "preorder \<langle>l, x, r\<rangle> = x # preorder l @ preorder r"
 
 fun inorder :: "'a tree \<Rightarrow> 'a list" where
 "inorder \<langle>\<rangle> = []" |
 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r"
 
 text\<open>A linear version avoiding append:\<close>
 fun inorder2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "inorder2 \<langle>\<rangle> xs = xs" |
 "inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)"
 
 fun postorder :: "'a tree \<Rightarrow> 'a list" where
 "postorder \<langle>\<rangle> = []" |
 "postorder \<langle>l, x, r\<rangle> = postorder l @ postorder r @ [x]"
 
 text\<open>Binary Search Tree:\<close>
 fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where
 "bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True" |
 "bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow>
- 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)"
+ (\<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 \<Rightarrow> bool" where
 "bst \<equiv> bst_wrt (<)"
 
 fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where
 "heap Leaf = True" |
 "heap (Node l m r) =
-  (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+  ((\<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 \<longleftrightarrow> t = Leaf"
 by (rule tree.map_disc_iff)
 
 lemma eq_Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> 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 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma eq_0_size[simp]: "0 = size t \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
 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 = {} \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma eq_empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> 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 \<noteq> {}"
 by (cases t)(auto)
 
 lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t"
 by (cases t)(auto)
 
 lemma size_subtrees: "s \<in> subtrees t \<Longrightarrow> size s \<le> size t"
 by(induction t)(auto)
 
 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
 by (induction t)(auto)
 
 lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t"
 by (induction t) auto
 
 lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> 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 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma eq_0_height[simp]: "0 = height t \<longleftrightarrow> 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 \<le> size (t::'a tree)"
 by (induction t) auto
 
 lemma size1_height: "size1 t \<le> 2 ^ height (t::'a tree)"
 proof(induction t)
   case (Node l a r)
   show ?case
   proof (cases "height l \<le> height r")
     case True
     have "size1(Node l a r) = size1 l + size1 r" by simp
     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith
     also have "\<dots> \<le> 2 ^ height r + 2 ^ height r" using True by simp
     also have "\<dots> = 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 "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith
     also have "\<dots> \<le> 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 \<le> 2 ^ height (t::'a tree) - 1"
 using size1_height[of t, unfolded size1_size] by(arith)
 
 lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t"
 by (induction t) auto
 
 
 lemma min_height_le_height: "min_height t \<le> 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 \<le> size1 t"
 proof(induction t)
   case (Node l a r)
   have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
     by (simp add: min_def)
   also have "\<dots> \<le> 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 \<longleftrightarrow> (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 \<Longrightarrow> size1 t = 2 ^ height t"
 by (induction t) auto
 
 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
 using size1_if_complete[simplified size1_size] by fastforce
 
 lemma size1_height_if_incomplete:
   "\<not> complete t \<Longrightarrow> 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: "\<not> 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: "\<not> 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 \<longleftrightarrow> (height t = min_height t)"
 by(auto simp add: complete_iff_height)
 
 lemma min_height_size1_if_incomplete:
   "\<not> complete t \<Longrightarrow> 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: "\<not> 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: "\<not> 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 \<Longrightarrow> complete t"
 using  size1_height_if_incomplete by fastforce
 
 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
 using min_height_size1_if_incomplete by fastforce
 
 lemma complete_iff_size1: "complete t \<longleftrightarrow> 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) \<Longrightarrow> acomplete l"
 by(simp add: acomplete_def)
 
 lemma acomplete_subtreeR: "acomplete (Node l x r) \<Longrightarrow> acomplete r"
 by(simp add: acomplete_def)
 
 lemma acomplete_subtrees: "\<lbrakk> acomplete t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> 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 \<le> size t'" shows "height t \<le> height t'"
 proof (cases "complete t")
   case True
   have "(2::nat) ^ height t \<le> 2 ^ height t'"
   proof -
     have "2 ^ height t = size1 t"
       using True by (simp add: size1_if_complete)
     also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_size)
     also have "\<dots> \<le> 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 "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_size)
     also have "\<dots> \<le> 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: "\<lbrakk> wbalanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 = [] \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma eq_Nil_inorder[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
 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: "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> bst_wrt P t \<Longrightarrow> bst_wrt Q t"
 by (induction t) (auto)
 
 lemma bst_wrt_le_if_bst: "bst t \<Longrightarrow> bst_wrt (\<le>) t"
 using bst_wrt_mono less_imp_le by blast
 
 lemma bst_wrt_le_iff_sorted: "bst_wrt (\<le>) t \<longleftrightarrow> 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 \<longleftrightarrow> 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 = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>"
 by (induction t) simp_all
 
 lemma Leaf_mirror[simp]: "\<langle>\<rangle> = mirror t \<longleftrightarrow> t = \<langle>\<rangle>"
 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