# HG changeset patch
# User nipkow
# Date 1589873596 -7200
# Node ID 1a884605a08b42dc65a40d52636ae31dfdf5f778
# Parent  b8d7b623e27429d6e4282aa6105ed74e518a3063
tuned

diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Tue May 19 09:33:16 2020 +0200
@@ -86,11 +86,14 @@
      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"
 
@@ -112,7 +115,7 @@
 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
 
 
@@ -143,7 +146,7 @@
   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:
@@ -163,7 +166,7 @@
 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
diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Tue May 19 09:33:16 2020 +0200
@@ -279,11 +279,13 @@
 "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>
@@ -468,7 +470,7 @@
 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:
@@ -484,7 +486,7 @@
     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
 
@@ -503,12 +505,12 @@
   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)
@@ -603,7 +605,7 @@
       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 *:
@@ -621,7 +623,7 @@
       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
 
@@ -644,12 +646,12 @@
   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)
diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Balance.thy	Tue May 19 09:33:16 2020 +0200
@@ -15,6 +15,7 @@
   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)"
@@ -52,7 +53,7 @@
       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'"
@@ -113,7 +114,7 @@
       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
@@ -149,7 +150,7 @@
       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
@@ -216,7 +217,7 @@
       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
diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/RBT_Set2.thy
--- a/src/HOL/Data_Structures/RBT_Set2.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/RBT_Set2.thy	Tue May 19 09:33:16 2020 +0200
@@ -35,6 +35,8 @@
 
 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)
@@ -43,7 +45,7 @@
 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)"
@@ -73,7 +75,7 @@
    (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
 
@@ -106,7 +108,7 @@
     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"
diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Tue May 19 09:33:16 2020 +0200
@@ -29,7 +29,7 @@
 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>"
 
@@ -227,7 +227,7 @@
 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
 
@@ -235,7 +235,7 @@
 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
 
@@ -291,7 +291,7 @@
 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
 
@@ -299,7 +299,7 @@
 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