src/HOL/Data_Structures/Tree234_Map.thy
 changeset 63636 6f38b7abb648 parent 63411 e051eea34990 child 67965 aaa31cd0caef
```     1.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Aug 07 12:10:49 2016 +0200
1.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Tue Aug 09 17:00:36 2016 +0200
1.3 @@ -127,12 +127,11 @@
1.4    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
1.6
1.7 -
1.8  lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
1.9    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
1.10  by(induction t rule: del.induct)
1.11 -  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
1.12 -(* 200 secs (2015) *)
1.13 +  (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits)
1.14 +(* 30 secs (2016) *)
1.15
1.16  lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
1.17    inorder(delete x t) = del_list x (inorder t)"
1.18 @@ -142,21 +141,18 @@
1.19  subsection \<open>Balancedness\<close>
1.20
1.21  lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
1.22 -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
1.23 +by (induct t) (auto, auto split!: if_split up\<^sub>i.split) (* 20 secs (2015) *)
1.24
1.25  lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
1.26  by (simp add: update_def bal_upd)
1.27
1.28 -
1.29  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
1.30  by(induction x t rule: del.induct)
1.31 -  (auto simp add: heights height_del_min split: prod.split)
1.32 -(* 20 secs (2015) *)
1.33 +  (auto simp add: heights height_del_min split!: if_split prod.split)
1.34
1.35  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
1.36  by(induction x t rule: del.induct)
1.37 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
1.38 -(* 100 secs (2015) *)
1.39 +  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
1.40
1.41  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"