diff --git a/src/HOL/Data_Structures/AVL_Bal_Set.thy b/src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy
@@ -1,195 +1,198 @@
 (* Author: Tobias Nipkow *)
 
 section "AVL Tree with Balance Factors (1)"
 
 theory AVL_Bal_Set
 imports
   Cmp
   Isin2
 begin
 
 text \<open>This version detects height increase/decrease from above via the change in balance factors.\<close>
 
 datatype bal = Lh | Bal | Rh
 
 type_synonym 'a tree_bal = "('a * bal) tree"
 
 text \<open>Invariant:\<close>
 
 fun avl :: "'a tree_bal \<Rightarrow> bool" where
 "avl Leaf = True" |
 "avl (Node l (a,b) r) =
   ((case b of
     Bal \<Rightarrow> height r = height l |
     Lh \<Rightarrow> height l = height r + 1 |
     Rh \<Rightarrow> height r = height l + 1)
   \<and> avl l \<and> avl r)"
 
 
 subsection \<open>Code\<close>
 
 fun is_bal where
 "is_bal (Node l (a,b) r) = (b = Bal)"
 
 fun incr where
 "incr t t' = (t = Leaf \<or> is_bal t \<and> \<not> is_bal t')"
 
 fun rot2 where
 "rot2 A a B c C = (case B of
   (Node B\<^sub>1 (b, bb) B\<^sub>2) \<Rightarrow>
     let b\<^sub>1 = if bb = Rh then Lh else Bal;
         b\<^sub>2 = if bb = Lh then Rh else Bal
     in Node (Node A (a,b\<^sub>1) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,b\<^sub>2) C))"
 
 fun balL :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
 "balL AB c bc C = (case bc of
      Bal \<Rightarrow> Node AB (c,Lh) C |
      Rh \<Rightarrow> Node AB (c,Bal) C |
      Lh \<Rightarrow> (case AB of
        Node A (a,Lh) B \<Rightarrow> Node A (a,Bal) (Node B (c,Bal) C) |
        Node A (a,Bal) B \<Rightarrow> Node A (a,Rh) (Node B (c,Lh) C) |
        Node A (a,Rh) B \<Rightarrow> rot2 A a B c C))"
 
 fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
 "balR A a ba BC = (case ba of
      Bal \<Rightarrow> Node A (a,Rh) BC |
      Lh \<Rightarrow> Node A (a,Bal) BC |
      Rh \<Rightarrow> (case BC of
        Node B (c,Rh) C \<Rightarrow> Node (Node A (a,Bal) B) (c,Bal) C |
        Node B (c,Bal) C \<Rightarrow> Node (Node A (a,Rh) B) (c,Lh) C |
        Node B (c,Lh) C \<Rightarrow> rot2 A a B c C))"
 
 fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
 "insert x Leaf = Node Leaf (x, Bal) Leaf" |
 "insert x (Node l (a, b) r) = (case cmp x a of
    EQ \<Rightarrow> Node l (a, b) r |
    LT \<Rightarrow> let l' = insert x l in if incr l l' then balL l' a b r else Node l' (a,b) r |
    GT \<Rightarrow> let r' = insert x r in if incr r r' then balR l a b r' else Node l (a,b) r')"
 
 fun decr where
 "decr t t' = (t \<noteq> Leaf \<and> (t' = Leaf \<or> \<not> is_bal t \<and> is_bal t'))"
 
 fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal * 'a" where
 "split_max (Node l (a, ba) r) =
   (if r = Leaf then (l,a)
    else let (r',a') = split_max r;
             t' = if decr r r' then balL l a ba r' else Node l (a,ba) r'
         in (t', a'))"
 
 fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
 "delete _ Leaf = Leaf" |
 "delete x (Node l (a, ba) r) =
   (case cmp x a of
      EQ \<Rightarrow> if l = Leaf then r
            else let (l', a') = split_max l in
                 if decr l l' then balR l' a' ba r else Node l' (a',ba) r |
      LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
      GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
 
+
+subsection \<open>Proofs\<close>
+
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
 lemmas splits = if_splits tree.splits bal.splits
 
-subsection \<open>Proofs\<close>
+declare Let_def [simp]
 
 subsubsection "Proofs about insertion"
 
 lemma avl_insert: "avl t \<Longrightarrow>
   avl(insert x t) \<and>
   height(insert x t) = height t + (if incr t (insert x t) then 1 else 0)"
 apply(induction x t rule: insert.induct)
 apply(auto split!: splits)
 done
 
 text \<open>The following two auxiliary lemma merely simplify the proof of \<open>inorder_insert\<close>.\<close>
 
 lemma [simp]: "[] \<noteq> ins_list x xs"
 by(cases xs) auto
 
 lemma [simp]: "avl t \<Longrightarrow> insert x t \<noteq> \<langle>l, (a, Rh), \<langle>\<rangle>\<rangle> \<and> insert x t \<noteq> \<langle>\<langle>\<rangle>, (a, Lh), r\<rangle>"
 by(drule avl_insert[of _ x]) (auto split: splits)
 
 theorem inorder_insert:
   "\<lbrakk> avl t;  sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
 apply(induction t)
-apply (auto simp: ins_list_simps Let_def split!: splits)
+apply (auto simp: ins_list_simps split!: splits)
 done
 
 
 subsubsection "Proofs about deletion"
 
 lemma inorder_balR:
   "\<lbrakk> ba = Rh \<longrightarrow> r \<noteq> Leaf; avl r \<rbrakk>
   \<Longrightarrow> inorder (balR l a ba r) = inorder l @ a # inorder r"
 by (auto split: splits)
 
 lemma inorder_balL:
   "\<lbrakk> ba = Lh \<longrightarrow> l \<noteq> Leaf; avl l \<rbrakk>
    \<Longrightarrow> inorder (balL l a ba r) = inorder l @ a # inorder r"
 by (auto split: splits)
 
 lemma height_1_iff: "avl t \<Longrightarrow> height t = Suc 0 \<longleftrightarrow> (\<exists>x. t = Node Leaf (x,Bal) Leaf)"
 by(cases t) (auto split: splits prod.splits)
 
 lemma avl_split_max:
   "\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
    avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
 apply(induction t arbitrary: t' a rule: split_max_induct)
  apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
 apply(fastforce)+
 done
 
 lemma avl_delete: "avl t \<Longrightarrow>
   avl (delete x t) \<and>
   height t = height (delete x t) + (if decr t (delete x t) then 1 else 0)"
 apply(induction x t rule: delete.induct)
- apply(auto simp: max_absorb1 max_absorb2 Let_def height_1_iff dest: avl_split_max split!: splits prod.splits)
+ apply(auto simp: max_absorb1 max_absorb2 height_1_iff dest: avl_split_max split!: splits prod.splits)
 done
 
 lemma inorder_split_maxD:
   "\<lbrakk> split_max t = (t',a); t \<noteq> Leaf; avl t \<rbrakk> \<Longrightarrow>
    inorder t' @ [a] = inorder t"
 apply(induction t arbitrary: t' rule: split_max.induct)
  apply(fastforce split!: splits prod.splits)
 apply simp
 done
 
 lemma neq_Leaf_if_height_neq_0: "height t \<noteq> 0 \<Longrightarrow> t \<noteq> Leaf"
 by auto
 
 lemma split_max_Leaf: "\<lbrakk> t \<noteq> Leaf; avl t \<rbrakk> \<Longrightarrow> split_max t = (\<langle>\<rangle>, x) \<longleftrightarrow> t = Node Leaf (x,Bal) Leaf"
 by(cases t) (auto split: splits prod.splits)
 
 theorem inorder_delete:
   "\<lbrakk> avl t; sorted(inorder t) \<rbrakk>  \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
 apply(induction t rule: tree2_induct)
-apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD Let_def
+apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD
                  split_max_Leaf neq_Leaf_if_height_neq_0
            simp del: balL.simps balR.simps split!: splits prod.splits)
 done
 
 
 subsubsection \<open>Set Implementation\<close>
 
 interpretation S: Set_by_Ordered
 where empty = Leaf and isin = isin
   and insert = insert
   and delete = delete
   and inorder = inorder and inv = avl
 proof (standard, goal_cases)
   case 1 show ?case by (simp)
 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)
 next
   case 6 thus ?case by (simp add: avl_insert)
 next
   case 7 thus ?case by (simp add: avl_delete)
 qed
 
 end
diff --git a/src/HOL/Data_Structures/Array_Braun.thy b/src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy
+++ b/src/HOL/Data_Structures/Array_Braun.thy
@@ -1,668 +1,670 @@
 (* Author: Tobias Nipkow, with contributions by Thomas Sewell *)
 
 section "Arrays via Braun Trees"
 
 theory Array_Braun
 imports
   Array_Specs
   Braun_Tree
 begin
 
 subsection "Array"
 
 fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where
 "lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"
 
 fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "update1 n x Leaf = Node Leaf x Leaf" |
 "update1 n x (Node l a r) =
   (if n=1 then Node l x r else
    if even n then Node (update1 (n div 2) x l) a r
             else Node l a (update1 (n div 2) x r))"
 
 fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "adds [] n t = t" |
 "adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"
 
 fun list :: "'a tree \<Rightarrow> 'a list" where
 "list Leaf = []" |
 "list (Node l x r) = x # splice (list l) (list r)"
 
 
 subsubsection "Functional Correctness"
 
 lemma size_list: "size(list t) = size t"
 by(induction t)(auto)
 
 lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)"
 by auto arith
 
 lemma nth_splice: "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk>
   \<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"
 apply(induction xs ys arbitrary: n rule: splice.induct)
 apply (auto simp: nth_Cons' minus1_div2)
 done
 
 lemma div2_in_bounds:
   "\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow>
    (odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"
 by auto arith
 
 declare upt_Suc[simp del]
 
 
 paragraph \<open>\<^const>\<open>lookup1\<close>\<close>
 
 lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
 proof(induction t arbitrary: i)
   case Leaf thus ?case by simp
 next
   case Node
   thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"]
     by (auto simp: nth_splice minus1_div2 size_list)
 qed
 
 lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
 by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
 
 
 paragraph \<open>\<^const>\<open>update1\<close>\<close>
 
 lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case Node thus ?case using div2_in_bounds[OF Node.prems] by simp
 qed
 
 lemma braun_update1: "\<lbrakk>braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> braun(update1 n x t)"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case Node thus ?case
     using div2_in_bounds[OF Node.prems] by (simp add: size_update1)
 qed
 
 lemma lookup1_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow>
   lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)"
 proof(induction t arbitrary: m n)
   case Leaf
   then show ?case by simp
 next
   have aux: "\<lbrakk> odd n; odd m \<rbrakk> \<Longrightarrow> n div 2 = (m::nat) div 2 \<longleftrightarrow> m=n" for m n
     using odd_two_times_div_two_succ by fastforce
   case Node
   thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux)
 qed
 
 lemma list_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
 by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)
 
 text \<open>A second proof of @{thm list_update1}:\<close>
 
 lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n - Suc 0 = m \<longleftrightarrow> n = m+1"
 by arith
 
 lemma list_update_splice:
   "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow>
   (splice xs ys) [n := x] =
   (if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"
 by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)
 
 lemma list_update2: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
 proof(induction t arbitrary: n)
   case Leaf thus ?case by simp
 next
   case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
     by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
 qed
 
 
 paragraph \<open>\<^const>\<open>adds\<close>\<close>
 
 lemma splice_last: shows
   "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
 and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
 by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
 
 lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]"
 by(induction t)(auto simp: splice_last size_list)
 
 lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1"
 by(induction t arbitrary: m)(auto)
 
 lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)"
 by(induction t)(auto simp: size_add_hi)
 
 lemma size_braun_adds:
   "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)"
 by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)
 
 lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs"
 by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)
 
 
 subsubsection "Array Implementation"
 
 interpretation A: Array
 where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
 and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
 and len = "\<lambda>(t,l). l"
 and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
 and invar = "\<lambda>(t,l). braun t \<and> l = size t"
 and list = "\<lambda>(t,l). list t"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)
 next
   case 2 thus ?case by (simp add: list_update1 split: prod.splits)
 next
   case 3 thus ?case by (simp add: size_list split: prod.splits)
 next
   case 4 thus ?case by (simp add: list_adds)
 next
   case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits)
 next
   case 6 thus ?case by (simp add: size_braun_adds split: prod.splits)
 qed
 
 
 subsection "Flexible Array"
 
 fun add_lo where
 "add_lo x Leaf = Node Leaf x Leaf" |
 "add_lo x (Node l a r) = Node (add_lo a r) x l"
 
 fun merge where
 "merge Leaf r = r" |
 "merge (Node l a r) rr = Node rr a (merge l r)"
 
 fun del_lo where
 "del_lo Leaf = Leaf" |
 "del_lo (Node l a r) = merge l r"
 
 fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "del_hi n Leaf = Leaf" |
 "del_hi n (Node l x r) =
   (if n = 1 then Leaf
    else if even n
        then Node (del_hi (n div 2) l) x r
        else Node l x (del_hi (n div 2) r))"
 
 
 subsubsection "Functional Correctness"
 
 
 paragraph \<open>\<^const>\<open>add_lo\<close>\<close>
 
 lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
 by(induction t arbitrary: a) auto
 
 lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)"
 by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
 
 
 paragraph \<open>\<^const>\<open>del_lo\<close>\<close>
 
 lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
 by (induction l r rule: merge.induct) auto
 
 lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
 by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)
 
 lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)"
 by (cases t) (simp_all add: list_merge)
 
 lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
 by (cases t) (simp_all add: braun_merge)
 
 
 paragraph \<open>\<^const>\<open>del_hi\<close>\<close>
 
 lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
 by(cases t) simp_all
 
 lemma butlast_splice: "butlast (splice xs ys) =
   (if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"
 by(induction xs ys rule: splice.induct) (auto)
 
 lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)"
 apply(induction t arbitrary: st)
 by(auto simp: list_Nil_iff size_list butlast_splice)
 
 lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)"
 apply(induction t arbitrary: st)
 by(auto simp: list_del_hi simp flip: size_list)
 
 
 subsubsection "Flexible Array Implementation"
 
 interpretation AF: Array_Flex
 where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
 and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
 and len = "\<lambda>(t,l). l"
 and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
 and invar = "\<lambda>(t,l). braun t \<and> l = size t"
 and list = "\<lambda>(t,l). list t"
 and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"
 and del_lo = "\<lambda>(t,l). (del_lo t, l-1)"
 and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"
 and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: list_add_lo split: prod.splits)
 next
   case 2 thus ?case by (simp add: list_del_lo split: prod.splits)
 next
   case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits)
 next
   case 4 thus ?case by (simp add: list_del_hi split: prod.splits)
 next
   case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits)
 next
   case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits)
 next
   case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits)
 next
   case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits)
 qed
 
 
 subsection "Faster"
 
 
 subsubsection \<open>Size\<close>
 
 fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
 "diff Leaf _ = 0" |
 "diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
 
 fun size_fast :: "'a tree \<Rightarrow> nat" where
 "size_fast Leaf = 0" |
 "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
 
+declare Let_def[simp]
+
 lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
 by(induction t arbitrary: n) auto
 
 lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
-by(induction t) (auto simp add: Let_def diff)
+by(induction t) (auto simp add: diff)
 
 
 subsubsection \<open>Initialization with 1 element\<close>
 
 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
 "braun_of_naive x n = (if n=0 then Leaf
   else let m = (n-1) div 2
        in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
        else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
 
 fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
 "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
   else let (s,t) = braun2_of x ((n-1) div 2)
        in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"
 
 definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
 "braun_of x n = fst (braun2_of x n)"
 
 declare braun2_of.simps [simp del]
 
 lemma braun2_of_size_braun: "braun2_of x n = (s,t) \<Longrightarrow> size s = n \<and> size t = n+1 \<and> braun s \<and> braun t"
 proof(induction x n arbitrary: s t rule: braun2_of.induct)
   case (1 x n)
   then show ?case
     by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+
 qed
 
 lemma braun2_of_replicate:
   "braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x"
 proof(induction x n arbitrary: s t rule: braun2_of.induct)
   case (1 x n)
   have "x # replicate m x = replicate (m+1) x" for m by simp
   with 1 show ?case
     apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]
         simp del: replicate.simps(2) split: prod.splits if_splits)
     by presburger+
 qed
 
 corollary braun_braun_of: "braun(braun_of x n)"
 unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
 
 corollary list_braun_of: "list(braun_of x n) = replicate n x"
 unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
 
 
 subsubsection "Proof Infrastructure"
 
 text \<open>Originally due to Thomas Sewell.\<close>
 
 paragraph \<open>\<open>take_nths\<close>\<close>
 
 fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "take_nths i k [] = []" |
 "take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
   else take_nths (i - 1) k xs)"
 
 text \<open>This is the more concise definition but seems to complicate the proofs:\<close>
 
 lemma take_nths_eq_nths: "take_nths i k xs = nths xs (\<Union>n. {n*2^k + i})"
 proof(induction xs arbitrary: i)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs)
   show ?case
   proof cases
     assume [simp]: "i = 0"
     have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}"
       apply (auto simp del: mult_Suc)
       by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc)
     thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons)
   next
     assume [arith]: "i \<noteq> 0"
     have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}"
       apply auto
       by (metis diff_Suc_Suc diff_zero)
     thus ?thesis by (simp add: Cons.IH nths_Cons)
   qed
 qed
 
 lemma take_nths_drop:
   "take_nths i k (drop j xs) = take_nths (i + j) k xs"
 by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
 
 lemma take_nths_00:
   "take_nths 0 0 xs = xs"
 by (induct xs; simp)
 
 lemma splice_take_nths:
   "splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
 by (induct xs; simp)
 
 lemma take_nths_take_nths:
   "take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
 by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
 
 lemma take_nths_empty:
   "(take_nths i k xs = []) = (length xs \<le> i)"
 by (induction xs arbitrary: i k) auto
 
 lemma hd_take_nths:
   "i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i"
 by (induction xs arbitrary: i k) auto
 
 lemma take_nths_01_splice:
   "\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow>
    take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
    take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
 by (induct xs arbitrary: ys; case_tac ys; simp)
 
 lemma length_take_nths_00:
   "length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or>
    length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
 by (induct xs) auto
 
 
 paragraph \<open>\<open>braun_list\<close>\<close>
 
 fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where
 "braun_list Leaf xs = (xs = [])" |
 "braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
     braun_list l (take_nths 1 1 xs) \<and>
     braun_list r (take_nths 2 1 xs))"
 
 lemma braun_list_eq:
   "braun_list t xs = (braun t \<and> xs = list t)"
 proof (induct t arbitrary: xs)
   case Leaf
   show ?case by simp
 next
   case Node
   show ?case
     using length_take_nths_00[of xs] splice_take_nths[of xs]
     by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice)
 qed
 
 
 subsubsection \<open>Converting a list of elements into a Braun tree\<close>
 
 fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where
 "nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
 "nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
 "nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
 "nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
 "nodes ls [] rs = []"
 
 fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where
 "brauns k xs = (if xs = [] then [] else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
    in nodes ts ys (drop (2^k) ts))"
 
 declare brauns.simps[simp del]
 
 definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
 "brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
 
 fun t_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
 "t_brauns k xs = (if xs = [] then 0 else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
    in 4 * min (2^k) (length xs) + t_brauns (k+1) zs)"
 
 
 paragraph "Functional correctness"
 
 text \<open>The proof is originally due to Thomas Sewell.\<close>
 
 lemma length_nodes:
   "length (nodes ls xs rs) = length xs"
 by (induct ls xs rs rule: nodes.induct; simp)
 
 lemma nth_nodes:
   "i < length xs \<Longrightarrow> nodes ls xs rs ! i =
   Node (if i < length ls then ls ! i else Leaf) (xs ! i)
     (if i < length rs then rs ! i else Leaf)"
 by (induct ls xs rs arbitrary: i rule: nodes.induct;
     simp add: nth_Cons split: nat.split)
 
 theorem length_brauns:
   "length (brauns k xs) = min (length xs) (2 ^ k)"
 proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
-  case (less xs) thus ?case by (simp add: brauns.simps[of k xs] Let_def length_nodes)
+  case (less xs) thus ?case by (simp add: brauns.simps[of k xs] length_nodes)
 qed
 
 theorem brauns_correct:
   "i < min (length xs) (2 ^ k) \<Longrightarrow> braun_list (brauns k xs ! i) (take_nths i k xs)"
 proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length])
   case (less xs)
   have "xs \<noteq> []" using less.prems by auto
   let ?zs = "drop (2^k) xs"
   let ?ts = "brauns (Suc k) ?zs"
   from less.hyps[of ?zs _ "Suc k"]
   have IH: "\<lbrakk> j = i + 2 ^ k;  i < min (length ?zs) (2 ^ (k+1)) \<rbrakk> \<Longrightarrow>
     braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j
     using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
   show ?case
     using less.prems
-    by (auto simp: brauns.simps[of k xs] Let_def nth_nodes take_nths_take_nths
+    by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths
                    IH take_nths_empty hd_take_nths length_brauns)
 qed
 
 corollary brauns1_correct:
   "braun (brauns1 xs) \<and> list (brauns1 xs) = xs"
 using brauns_correct[of 0 xs 0]
 by (simp add: brauns1_def braun_list_eq take_nths_00)
 
 
 paragraph "Running Time Analysis"
 
 theorem t_brauns:
   "t_brauns k xs = 4 * length xs"
 proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
   case (less xs)
   show ?case
   proof cases
     assume "xs = []"
-    thus ?thesis by(simp add: Let_def)
+    thus ?thesis by(simp)
   next
     assume "xs \<noteq> []"
     let ?zs = "drop (2^k) xs"
     have "t_brauns k xs = t_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
-     using \<open>xs \<noteq> []\<close> by(simp add: Let_def)
+     using \<open>xs \<noteq> []\<close> by(simp)
     also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
       using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
       by (simp)
     also have "\<dots> = 4 * length xs"
       by(simp)
     finally show ?case .
   qed
 qed
 
 
 subsubsection \<open>Converting a Braun Tree into a List of Elements\<close>
 
 text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>
 
 function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
 "list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts in
   if us = [] then [] else
   map value us @ list_fast_rec (map left us @ map right us))"
 by (pat_completeness, auto)
 
 lemma list_fast_rec_term1: "ts \<noteq> [] \<Longrightarrow> Leaf \<notin> set ts \<Longrightarrow>
   sum_list (map (size o left) ts) + sum_list (map (size o right) ts) < sum_list (map size ts)"
   apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter')
   apply (rule sum_list_strict_mono; clarsimp?)
   apply (case_tac x; simp)
   done
 
 lemma list_fast_rec_term: "us \<noteq> [] \<Longrightarrow> us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<Longrightarrow>
   sum_list (map (size o left) us) + sum_list (map (size o right) us) < sum_list (map size ts)"
   apply (rule order_less_le_trans, rule list_fast_rec_term1, simp_all)
   apply (rule sum_list_filter_le_nat)
   done
 
 termination
   apply (relation "measure (sum_list o map size)")
    apply simp
   apply (simp add: list_fast_rec_term)
   done
 
 declare list_fast_rec.simps[simp del]
 
 definition list_fast :: "'a tree \<Rightarrow> 'a list" where
 "list_fast t = list_fast_rec [t]"
 
 function t_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
 "t_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
   in length ts + (if us = [] then 0 else
   5 * length us + t_list_fast_rec (map left us @ map right us)))"
 by (pat_completeness, auto)
 
 termination
   apply (relation "measure (sum_list o map size)")
    apply simp
   apply (simp add: list_fast_rec_term)
   done
 
 declare t_list_fast_rec.simps[simp del]
 
 paragraph "Functional Correctness"
 
 lemma list_fast_rec_all_Leaf:
   "\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []"
 by (simp add: filter_empty_conv list_fast_rec.simps)
 
 lemma take_nths_eq_single:
   "length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)"
 by (induction xs arbitrary: i n; simp add: drop_Cons')
 
 lemma braun_list_Nil:
   "braun_list t [] = (t = Leaf)"
 by (cases t; simp)
 
 lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow>
   braun_list t xs =
  (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
     braun_list l (take_nths 1 1 xs) \<and>
     braun_list r (take_nths 2 1 xs))"
 by(cases t; simp)
 
 theorem list_fast_rec_correct:
   "\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk>
     \<Longrightarrow> list_fast_rec ts = xs"
 proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length])
   case (less xs)
   show ?case
   proof (cases "length xs < 2 ^ k")
     case True
     from less.prems True have filter:
       "\<exists>n. ts = map (\<lambda>x. Node Leaf x Leaf) xs @ replicate n Leaf"
       apply (rule_tac x="length ts - length xs" in exI)
       apply (clarsimp simp: list_eq_iff_nth_eq)
       apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
       done
     thus ?thesis
-      by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf Let_def)
+      by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
   next
     case False
     with less.prems(2) have *:
       "\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
          \<and> value (ts ! i) = xs ! i
          \<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
          \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
                  \<longrightarrow> braun_list (right (ts ! i)) ys)"
       by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
                      algebra_simps)
     have 1: "map value ts = take (2 ^ k) xs"
       using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
     have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
       using less.prems(1) False
       by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
                simp: nth_append * take_nths_drop algebra_simps)
     from less.prems(1) False show ?thesis
-      by (auto simp: list_fast_rec.simps[of ts] 1 2 Let_def * all_set_conv_all_nth)
+      by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth)
   qed
 qed
 
 corollary list_fast_correct:
   "braun t \<Longrightarrow> list_fast t = list t"
 by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
 
 paragraph "Running Time Analysis"
 
 lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
   (\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
 by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
 
 theorem t_list_fast_rec_ub:
   "t_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
 proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"])
   case (less ts)
   let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts"
   show ?case
   proof cases
     assume "?us = []"
     thus ?thesis using t_list_fast_rec.simps[of ts]
-      by(simp add: Let_def sum_list_Suc)
+      by(simp add: sum_list_Suc)
     next
     assume "?us \<noteq> []"
     let ?children = "map left ?us @ map right ?us"
     have "t_list_fast_rec ts = t_list_fast_rec ?children + 5 * length ?us + length ts"
-     using \<open>?us \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp add: Let_def)
+     using \<open>?us \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp)
     also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
       using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
       by (simp)
     also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts"
       by(simp add: sum_list_Suc o_def)
     also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"
       by(simp add: sum_tree_list_children)
     also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"
       by(simp add: sum_list_filter_le_nat)
     also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"
       by(simp add: sum_list_Suc)
     finally show ?case .
   qed
 qed
 
 end
\ No newline at end of file
diff --git a/src/HOL/Data_Structures/Balance.thy b/src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy
+++ b/src/HOL/Data_Structures/Balance.thy
@@ -1,246 +1,247 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>Creating Balanced Trees\<close>
 
 theory Balance
 imports
   "HOL-Library.Tree_Real"
 begin
 
 fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where
 "bal n xs = (if n=0 then (Leaf,xs) else
  (let m = n div 2;
       (l, ys) = bal m xs;
       (r, zs) = bal (n-1-m) (tl ys)
   in (Node l (hd ys) r, zs)))"
 
 declare bal.simps[simp del]
+declare Let_def[simp]
 
 definition bal_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree" where
 "bal_list n xs = fst (bal n xs)"
 
 definition balance_list :: "'a list \<Rightarrow> 'a tree" where
 "balance_list xs = bal_list (length xs) xs"
 
 definition bal_tree :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "bal_tree n t = bal_list n (inorder t)"
 
 definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where
 "balance_tree t = bal_tree (size t) t"
 
 lemma bal_simps:
   "bal 0 xs = (Leaf, xs)"
   "n > 0 \<Longrightarrow>
    bal n xs =
   (let m = n div 2;
       (l, ys) = bal m xs;
       (r, zs) = bal (n-1-m) (tl ys)
   in (Node l (hd ys) r, zs))"
 by(simp_all add: bal.simps)
 
 lemma bal_inorder:
   "\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk>
   \<Longrightarrow> xs = inorder t @ zs \<and> size t = n"
 proof(induction n xs arbitrary: t zs rule: bal.induct)
   case (1 n xs) show ?case
   proof cases
     assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps)
   next
     assume [arith]: "n \<noteq> 0"
     let ?m = "n div 2" let ?m' = "n - 1 - ?m"
     from "1.prems"(2) obtain l r ys where
       b1: "bal ?m xs = (l,ys)" and
       b2: "bal ?m' (tl ys) = (r,zs)" and
       t: "t = \<langle>l, hd ys, r\<rangle>"
-      by(auto simp: Let_def bal_simps split: prod.splits)
+      by(auto simp: bal_simps split: prod.splits)
     have IH1: "xs = inorder l @ ys \<and> size l = ?m"
       using b1 "1.prems"(1) by(intro "1.IH"(1)) auto
     have IH2: "tl ys = inorder r @ zs \<and> size r = ?m'"
       using b1 b2 IH1 "1.prems"(1) by(intro "1.IH"(2)) auto
     show ?thesis using t IH1 IH2  "1.prems"(1) hd_Cons_tl[of ys] by fastforce
   qed
 qed
 
 corollary inorder_bal_list[simp]:
   "n \<le> length xs \<Longrightarrow> inorder(bal_list n xs) = take n xs"
 unfolding bal_list_def
 by (metis (mono_tags) prod.collapse[of "bal n xs"] append_eq_conv_conj bal_inorder length_inorder)
 
 corollary inorder_balance_list[simp]: "inorder(balance_list xs) = xs"
 by(simp add: balance_list_def)
 
 corollary inorder_bal_tree:
   "n \<le> size t \<Longrightarrow> inorder(bal_tree n t) = take n (inorder t)"
 by(simp add: bal_tree_def)
 
 corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t"
 by(simp add: balance_tree_def inorder_bal_tree)
 
 
 text\<open>The length/size lemmas below do not require the precondition @{prop"n \<le> length xs"}
 (or  @{prop"n \<le> size t"}) that they come with. They could take advantage of the fact
 that @{term "bal xs n"} yields a result even if @{prop "n > length xs"}.
 In that case the result will contain one or more occurrences of @{term "hd []"}.
 However, this is counter-intuitive and does not reflect the execution
 in an eager functional language.\<close>
 
 lemma bal_length: "\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> length zs = length xs - n"
 using bal_inorder by fastforce
 
 corollary size_bal_list[simp]: "n \<le> length xs \<Longrightarrow> size(bal_list n xs) = n"
 unfolding bal_list_def using bal_inorder prod.exhaust_sel by blast
 
 corollary size_balance_list[simp]: "size(balance_list xs) = length xs"
 by (simp add: balance_list_def)
 
 corollary size_bal_tree[simp]: "n \<le> size t \<Longrightarrow> size(bal_tree n t) = n"
 by(simp add: bal_tree_def)
 
 corollary size_balance_tree[simp]: "size(balance_tree t) = size t"
 by(simp add: balance_tree_def)
 
 lemma min_height_bal:
   "\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)"
 proof(induction n xs arbitrary: t zs rule: bal.induct)
   case (1 n xs)
   show ?case
   proof cases
     assume "n = 0" thus ?thesis using "1.prems"(2) by (simp add: bal_simps)
   next
     assume [arith]: "n \<noteq> 0"
     let ?m = "n div 2" let ?m' = "n - 1 - ?m"
     from "1.prems" obtain l r ys where
       b1: "bal ?m xs = (l,ys)" and
       b2: "bal ?m' (tl ys) = (r,zs)" and
       t: "t = \<langle>l, hd ys, r\<rangle>"
-      by(auto simp: bal_simps Let_def split: prod.splits)
+      by(auto simp: bal_simps split: prod.splits)
     let ?hl = "nat (floor(log 2 (?m + 1)))"
     let ?hr = "nat (floor(log 2 (?m' + 1)))"
     have IH1: "min_height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
     have IH2: "min_height r = ?hr"
       using "1.prems"(1) bal_length[OF _ b1] b1 b2 by(intro "1.IH"(2)) auto
     have "(n+1) div 2 \<ge> 1" by arith
     hence 0: "log 2 ((n+1) div 2) \<ge> 0" by simp
     have "?m' \<le> ?m" by arith
     hence le: "?hr \<le> ?hl" by(simp add: nat_mono floor_mono)
     have "min_height t = min ?hl ?hr + 1" by (simp add: t IH1 IH2)
     also have "\<dots> = ?hr + 1" using le by (simp add: min_absorb2)
     also have "?m' + 1 = (n+1) div 2" by linarith
     also have "nat (floor(log 2 ((n+1) div 2))) + 1
        = nat (floor(log 2 ((n+1) div 2) + 1))"
       using 0 by linarith
     also have "\<dots> = nat (floor(log 2 (n + 1)))"
       using floor_log2_div2[of "n+1"] by (simp add: log_mult)
     finally show ?thesis .
   qed
 qed
 
 lemma height_bal:
   "\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>"
 proof(induction n xs arbitrary: t zs rule: bal.induct)
   case (1 n xs) show ?case
   proof cases
     assume "n = 0" thus ?thesis
       using "1.prems" by (simp add: bal_simps)
   next
     assume [arith]: "n \<noteq> 0"
     let ?m = "n div 2" let ?m' = "n - 1 - ?m"
     from "1.prems" obtain l r ys where
       b1: "bal ?m xs = (l,ys)" and
       b2: "bal ?m' (tl ys) = (r,zs)" and
       t: "t = \<langle>l, hd ys, r\<rangle>"
-      by(auto simp: bal_simps Let_def split: prod.splits)
+      by(auto simp: bal_simps split: prod.splits)
     let ?hl = "nat \<lceil>log 2 (?m + 1)\<rceil>"
     let ?hr = "nat \<lceil>log 2 (?m' + 1)\<rceil>"
     have IH1: "height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
     have IH2: "height r = ?hr"
       using b1 b2 bal_length[OF _ b1] "1.prems"(1) by(intro "1.IH"(2)) auto
     have 0: "log 2 (?m + 1) \<ge> 0" by simp
     have "?m' \<le> ?m" by arith
     hence le: "?hr \<le> ?hl"
       by(simp add: nat_mono ceiling_mono del: nat_ceiling_le_eq)
     have "height t = max ?hl ?hr + 1" by (simp add: t IH1 IH2)
     also have "\<dots> = ?hl + 1" using le by (simp add: max_absorb1)
     also have "\<dots> = nat \<lceil>log 2 (?m + 1) + 1\<rceil>" using 0 by linarith
     also have "\<dots> = nat \<lceil>log 2 (n + 1)\<rceil>"
       using ceiling_log2_div2[of "n+1"] by (simp)
     finally show ?thesis .
   qed
 qed
 
 lemma balanced_bal:
   assumes "n \<le> length xs" "bal n xs = (t,ys)" shows "balanced t"
 unfolding balanced_def
 using height_bal[OF assms] min_height_bal[OF assms]
 by linarith
 
 lemma height_bal_list:
   "n \<le> length xs \<Longrightarrow> height (bal_list n xs) = nat \<lceil>log 2 (n + 1)\<rceil>"
 unfolding bal_list_def by (metis height_bal prod.collapse)
 
 lemma height_balance_list:
   "height (balance_list xs) = nat \<lceil>log 2 (length xs + 1)\<rceil>"
 by (simp add: balance_list_def height_bal_list)
 
 corollary height_bal_tree:
   "n \<le> size t \<Longrightarrow> height (bal_tree n t) = nat\<lceil>log 2 (n + 1)\<rceil>"
 unfolding bal_list_def bal_tree_def
 by (metis bal_list_def height_bal_list length_inorder)
 
 corollary height_balance_tree:
   "height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>"
 by (simp add: bal_tree_def balance_tree_def height_bal_list)
 
 corollary balanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> balanced (bal_list n xs)"
 unfolding bal_list_def by (metis  balanced_bal prod.collapse)
 
 corollary balanced_balance_list[simp]: "balanced (balance_list xs)"
 by (simp add: balance_list_def)
 
 corollary balanced_bal_tree[simp]: "n \<le> size t \<Longrightarrow> balanced (bal_tree n t)"
 by (simp add: bal_tree_def)
 
 corollary balanced_balance_tree[simp]: "balanced (balance_tree t)"
 by (simp add: balance_tree_def)
 
 lemma wbalanced_bal: "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> wbalanced t"
 proof(induction n xs arbitrary: t ys rule: bal.induct)
   case (1 n xs)
   show ?case
   proof cases
     assume "n = 0"
     thus ?thesis using "1.prems"(2) by(simp add: bal_simps)
   next
     assume [arith]: "n \<noteq> 0"
     with "1.prems" obtain l ys r zs where
       rec1: "bal (n div 2) xs = (l, ys)" and
       rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and
       t: "t = \<langle>l, hd ys, r\<rangle>"
-      by(auto simp add: bal_simps Let_def split: prod.splits)
+      by(auto simp add: bal_simps split: prod.splits)
     have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl _ rec1] "1.prems"(1) by linarith
     have "wbalanced r"
       using rec1 rec2 bal_length[OF _ rec1] "1.prems"(1) by(intro "1.IH"(2)) auto
     with l t bal_length[OF _ rec1] "1.prems"(1) bal_inorder[OF _ rec1] bal_inorder[OF _ rec2]
     show ?thesis by auto
   qed
 qed
 
 text\<open>An alternative proof via @{thm balanced_if_wbalanced}:\<close>
 lemma "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> balanced t"
 by(rule balanced_if_wbalanced[OF wbalanced_bal])
 
 lemma wbalanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> wbalanced (bal_list n xs)"
 by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal)
 
 lemma wbalanced_balance_list[simp]: "wbalanced (balance_list xs)"
 by(simp add: balance_list_def)
 
 lemma wbalanced_bal_tree[simp]: "n \<le> size t \<Longrightarrow> wbalanced (bal_tree n t)"
 by(simp add: bal_tree_def)
 
 lemma wbalanced_balance_tree: "wbalanced (balance_tree t)"
 by (simp add: balance_tree_def)
 
 hide_const (open) bal
 
 end
diff --git a/src/HOL/Data_Structures/RBT_Set2.thy b/src/HOL/Data_Structures/RBT_Set2.thy
--- a/src/HOL/Data_Structures/RBT_Set2.thy
+++ b/src/HOL/Data_Structures/RBT_Set2.thy
@@ -1,144 +1,146 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>Alternative Deletion in Red-Black Trees\<close>
 
 theory RBT_Set2
 imports RBT_Set
 begin
 
 text \<open>This is a conceptually simpler version of deletion. Instead of the tricky \<open>join\<close>
 function this version follows the standard approach of replacing the deleted element
 (in function \<open>del\<close>) by the minimal element in its right subtree.\<close>
 
 fun split_min :: "'a rbt \<Rightarrow> 'a \<times> 'a rbt" where
 "split_min (Node l (a, _) r) =
   (if l = Leaf then (a,r)
    else let (x,l') = split_min l
         in (x, if color l = Black then baldL l' a r else R l' a r))"
 
 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> let l' = del x l in if l \<noteq> Leaf \<and> color l = Black
            then baldL l' a r else R l' a r |
      GT \<Rightarrow> let r' = del x r in if r \<noteq> Leaf \<and> color r = Black
            then baldR l a r' else R l a r' |
      EQ \<Rightarrow> if r = Leaf then l else let (a',r') = split_min r in
            if color r = Black then baldR l a' r' else R l a' r')"
 
 text \<open>The first two \<open>let\<close>s speed up the automatic proof of \<open>inv_del\<close> below.\<close>
 
 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "delete x t = paint Black (del x t)"
 
 
 subsection "Functional Correctness Proofs"
 
+declare Let_def[simp]
+
 lemma split_minD:
   "split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
 by(induction t arbitrary: t' rule: split_min.induct)
   (auto simp: inorder_baldL sorted_lems split: prod.splits if_splits)
 
 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_baldL inorder_baldR split_minD Let_def split: prod.splits)
+  (auto simp: del_list_simps inorder_baldL inorder_baldR split_minD split: prod.splits)
 
 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_Red[simp]: "(c \<noteq> Red) = (c = Black)"
 by (cases c) auto
 
 
 subsubsection \<open>Deletion\<close>
 
 lemma inv_split_min: "\<lbrakk> split_min t = (x,t'); t \<noteq> Leaf; invh t; invc t \<rbrakk> \<Longrightarrow>
    invh t' \<and>
    (color t = Red \<longrightarrow> bheight t' = bheight t \<and> invc t') \<and>
    (color t = Black \<longrightarrow> bheight t' = bheight t - 1 \<and> invc2 t')"
 apply(induction t arbitrary: x t' rule: split_min.induct)
 apply(auto simp: inv_baldR inv_baldL invc2I dest!: neq_LeafD
            split: if_splits prod.splits)
 done
 
 text \<open>An automatic proof. It is quite brittle, e.g. inlining the \<open>let\<close>s in @{const del} breaks it.\<close>
 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
    invh (del x t) \<and>
    (color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and>
    (color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
 apply(induction x t rule: del.induct)
-apply(auto simp: inv_baldR inv_baldL invc2I Let_def dest!: inv_split_min dest: neq_LeafD
+apply(auto simp: inv_baldR inv_baldL invc2I dest!: inv_split_min dest: neq_LeafD
            split!: prod.splits if_splits)
 done
 
 text\<open>A structured proof where one can see what is used in each case.\<close>
 lemma inv_del2: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
    invh (del x t) \<and>
    (color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and>
    (color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
 proof(induction x t rule: del.induct)
   case (1 x)
   then show ?case by simp
 next
   case (2 x l a c r)
   note if_split[split del]
   show ?case
   proof cases
     assume "x < a"
     show ?thesis
     proof cases (* For readability; could be automated more: *)
       assume *: "l \<noteq> Leaf \<and> color l = Black"
       hence "bheight l > 0" using neq_LeafD[of l] by auto
       thus ?thesis using \<open>x < a\<close> "2.IH"(1) "2.prems" inv_baldL[of "del x l"] * by(auto)
     next
       assume "\<not>(l \<noteq> Leaf \<and> color l = Black)"
       thus ?thesis using \<open>x < a\<close> "2.prems" "2.IH"(1) by(auto)
     qed
   next (* more automation: *)
     assume "\<not> x < a"
     show ?thesis
     proof cases
       assume "x > a"
       show ?thesis using \<open>a < x\<close> "2.IH"(2) "2.prems" neq_LeafD[of r] inv_baldR[of _ "del x r"]
-          by(auto simp: Let_def split: if_split)
+          by(auto split: if_split)
     
     next
       assume "\<not> x > a"
       show ?thesis using "2.prems" \<open>\<not> x < a\<close> \<open>\<not> x > a\<close>
           by(auto simp: inv_baldR invc2I dest!: inv_split_min dest: neq_LeafD split: prod.split if_split)
     qed
   qed
 qed
 
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
 by (metis delete_def rbt_def color_paint_Black inv_del 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
 
 
 end
diff --git a/src/HOL/Data_Structures/Set2_Join.thy b/src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy
+++ b/src/HOL/Data_Structures/Set2_Join.thy
@@ -1,356 +1,356 @@
 (* Author: Tobias Nipkow *)
 
 section "Join-Based Implementation of Sets"
 
 theory Set2_Join
 imports
   Isin2
 begin
 
 text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
 \<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
 All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
 and an element \<open>x\<close> such that \<open>l < x < r\<close>.
 
 The theory is based on theory \<^theory>\<open>HOL-Data_Structures.Tree2\<close> where nodes have an additional field.
 This field is ignored here but it means that this theory can be instantiated
 with red-black trees (see theory \<^file>\<open>Set2_Join_RBT.thy\<close>) and other balanced trees.
 This approach is very concrete and fixes the type of trees.
 Alternatively, one could assume some abstract type \<^typ>\<open>'t\<close> of trees with suitable decomposition
 and recursion operators on it.\<close>
 
 locale Set2_Join =
 fixes join :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree"
 fixes inv :: "('a*'b) tree \<Rightarrow> bool"
 assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r"
 assumes bst_join: "bst (Node l (a, b) r) \<Longrightarrow> bst (join l a r)"
 assumes inv_Leaf: "inv \<langle>\<rangle>"
 assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l a r)"
 assumes inv_Node: "\<lbrakk> inv (Node l (a,b) r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
 begin
 
-declare set_join [simp]
+declare set_join [simp] Let_def[simp]
 
 subsection "\<open>split_min\<close>"
 
 fun split_min :: "('a*'b) tree \<Rightarrow> 'a \<times> ('a*'b) tree" where
 "split_min (Node l (a, _) r) =
   (if l = Leaf then (a,r) else let (m,l') = split_min l in (m, join l' a r))"
 
 lemma split_min_set:
   "\<lbrakk> split_min t = (m,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> m \<in> set_tree t \<and> set_tree t = {m} \<union> set_tree t'"
 proof(induction t arbitrary: t' rule: tree2_induct)
   case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
 next
   case Leaf thus ?case by simp
 qed
 
 lemma split_min_bst:
   "\<lbrakk> split_min t = (m,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x \<in> set_tree t'. m < x)"
 proof(induction t arbitrary: t' rule: tree2_induct)
   case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
 next
   case Leaf thus ?case by simp
 qed
 
 lemma split_min_inv:
   "\<lbrakk> split_min t = (m,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
 proof(induction t arbitrary: t' rule: tree2_induct)
   case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
 next
   case Leaf thus ?case by simp
 qed
 
 
 subsection "\<open>join2\<close>"
 
 definition join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
 "join2 l r = (if r = Leaf then l else let (m,r') = split_min r in join l m r')"
 
 lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
 by(simp add: join2_def split_min_set split: prod.split)
 
 lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
   \<Longrightarrow> bst (join2 l r)"
 by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
 
 lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
 by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
 
 
 subsection "\<open>split\<close>"
 
 fun split :: "('a*'b)tree \<Rightarrow> 'a \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where
 "split Leaf k = (Leaf, False, Leaf)" |
 "split (Node l (a, _) r) x =
   (case cmp x a of
      LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
      GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
      EQ \<Rightarrow> (l, True, r))"
 
 lemma split: "split t x = (l,xin,r) \<Longrightarrow> bst t \<Longrightarrow>
   set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}
   \<and> (xin = (x \<in> set_tree t)) \<and> bst l \<and> bst r"
 proof(induction t arbitrary: l xin r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
   case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
 qed
 
 lemma split_inv: "split t x = (l,xin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
 proof(induction t arbitrary: l xin r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
   case Node
   thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
 qed
 
 declare split.simps[simp del]
 
 
 subsection "\<open>insert\<close>"
 
 definition insert :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
 "insert x t = (let (l,_,r) = split t x in join l x r)"
 
 lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = {x} \<union> set_tree t"
 by(auto simp add: insert_def split split: prod.split)
 
 lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
 by(auto simp add: insert_def bst_join dest: split split: prod.split)
 
 lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
 by(force simp: insert_def inv_join dest: split_inv split: prod.split)
 
 
 subsection "\<open>delete\<close>"
 
 definition delete :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
 "delete x t = (let (l,_,r) = split t x in join2 l r)"
 
 lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
 by(auto simp: delete_def split split: prod.split)
 
 lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
 by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
 
 lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
 by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
 
 
 subsection "\<open>union\<close>"
 
 fun union :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
 "union t1 t2 =
   (if t1 = Leaf then t2 else
    if t2 = Leaf then t1 else
    case t1 of Node l1 (a, _) r1 \<Rightarrow>
    let (l2,_ ,r2) = split t2 a;
        l' = union l1 l2; r' = union r1 r2
    in join l' a r')"
 
 declare union.simps [simp del]
 
 lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
 proof(induction t1 t2 rule: union.induct)
   case (1 t1 t2)
   then show ?case
     by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
 qed
 
 lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
 proof(induction t1 t2 rule: union.induct)
   case (1 t1 t2)
   thus ?case
     by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
         split: tree.split prod.split)
 qed
 
 lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
 proof(induction t1 t2 rule: union.induct)
   case (1 t1 t2)
   thus ?case
     by(auto simp:union.simps[of t1 t2] inv_join split_inv
         split!: tree.split prod.split dest: inv_Node)
 qed
 
 subsection "\<open>inter\<close>"
 
 fun inter :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
 "inter t1 t2 =
   (if t1 = Leaf then Leaf else
    if t2 = Leaf then Leaf else
    case t1 of Node l1 (a, _) r1 \<Rightarrow>
    let (l2,ain,r2) = split t2 a;
        l' = inter l1 l2; r' = inter r1 r2
    in if ain then join l' a r' else join2 l' r')"
 
 declare inter.simps [simp del]
 
 lemma set_tree_inter:
   "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
 proof(induction t1 t2 rule: inter.induct)
   case (1 t1 t2)
   show ?case
   proof (cases t1 rule: tree2_cases)
     case Leaf thus ?thesis by (simp add: inter.simps)
   next
     case [simp]: (Node l1 a _ r1)
     show ?thesis
     proof (cases "t2 = Leaf")
       case True thus ?thesis by (simp add: inter.simps)
     next
       case False
       let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
       have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
       obtain l2 ain r2 where sp: "split t2 a = (l2,ain,r2)" using prod_cases3 by blast
       let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if ain then {a} else {}"
       have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
            **: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
         using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
       have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
         using "1.IH"(1)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
       have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
         using "1.IH"(2)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
       have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {a}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
         by(simp add: t2)
       also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
         using * ** by auto
       also have "\<dots> = set_tree (inter t1 t2)"
       using IHl IHr sp inter.simps[of t1 t2] False by(simp)
       finally show ?thesis by simp
     qed
   qed
 qed
 
 lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
 proof(induction t1 t2 rule: inter.induct)
   case (1 t1 t2)
   thus ?case
-    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
+    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split
         intro!: bst_join bst_join2 split: tree.split prod.split)
 qed
 
 lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
 proof(induction t1 t2 rule: inter.induct)
   case (1 t1 t2)
   thus ?case
-    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv
         split!: tree.split prod.split dest: inv_Node)
 qed
 
 subsection "\<open>diff\<close>"
 
 fun diff :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
 "diff t1 t2 =
   (if t1 = Leaf then Leaf else
    if t2 = Leaf then t1 else
    case t2 of Node l2 (a, _) r2 \<Rightarrow>
    let (l1,_,r1) = split t1 a;
        l' = diff l1 l2; r' = diff r1 r2
    in join2 l' r')"
 
 declare diff.simps [simp del]
 
 lemma set_tree_diff:
   "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
 proof(induction t1 t2 rule: diff.induct)
   case (1 t1 t2)
   show ?case
   proof (cases t2 rule: tree2_cases)
     case Leaf thus ?thesis by (simp add: diff.simps)
   next
     case [simp]: (Node l2 a _ r2)
     show ?thesis
     proof (cases "t1 = Leaf")
       case True thus ?thesis by (simp add: diff.simps)
     next
       case False
       let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
       obtain l1 ain r1 where sp: "split t1 a = (l1,ain,r1)" using prod_cases3 by blast
       let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if ain then {a} else {}"
       have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
            **: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
         using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
       have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
         using "1.IH"(1)[OF False _ _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
       have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
         using "1.IH"(2)[OF False _ _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
       have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {a})"
         by(simp add: t1)
       also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
         using ** by auto
       also have "\<dots> = set_tree (diff t1 t2)"
       using IHl IHr sp diff.simps[of t1 t2] False by(simp)
       finally show ?thesis by simp
     qed
   qed
 qed
 
 lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
 proof(induction t1 t2 rule: diff.induct)
   case (1 t1 t2)
   thus ?case
-    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
+    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split
         intro!: bst_join bst_join2 split: tree.split prod.split)
 qed
 
 lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
 proof(induction t1 t2 rule: diff.induct)
   case (1 t1 t2)
   thus ?case
-    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv
         split!: tree.split prod.split dest: inv_Node)
 qed
 
 text \<open>Locale \<^locale>\<open>Set2_Join\<close> implements locale \<^locale>\<open>Set2\<close>:\<close>
 
 sublocale Set2
 where empty = Leaf and insert = insert and delete = delete and isin = isin
 and union = union and inter = inter and diff = diff
 and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
 proof (standard, goal_cases)
   case 1 show ?case by (simp)
 next
   case 2 thus ?case by(simp add: isin_set_tree)
 next
   case 3 thus ?case by (simp add: set_tree_insert)
 next
   case 4 thus ?case by (simp add: set_tree_delete)
 next
   case 5 thus ?case by (simp add: inv_Leaf)
 next
   case 6 thus ?case by (simp add: bst_insert inv_insert)
 next
   case 7 thus ?case by (simp add: bst_delete inv_delete)
 next
   case 8 thus ?case by(simp add: set_tree_union)
 next
   case 9 thus ?case by(simp add: set_tree_inter)
 next
   case 10 thus ?case by(simp add: set_tree_diff)
 next
   case 11 thus ?case by (simp add: bst_union inv_union)
 next
   case 12 thus ?case by (simp add: bst_inter inv_inter)
 next
   case 13 thus ?case by (simp add: bst_diff inv_diff)
 qed
 
 end
 
 interpretation unbal: Set2_Join
 where join = "\<lambda>l x r. Node l (x, ()) r" and inv = "\<lambda>t. True"
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
   case 2 thus ?case by simp
 next
   case 3 thus ?case by simp
 next
   case 4 thus ?case by simp
 next
   case 5 thus ?case by simp
 qed
 
 end
\ No newline at end of file