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.5  by(simp add: update_def inorder_upd)
     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)"
    1.42  by(simp add: delete_def bal_tree\<^sub>d_del)