src/HOL/Data_Structures/RBT_Set.thy
changeset 61231 cc6969542f8d
parent 61224 759b5299a9f2
child 61428 5e1938107371
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Sep 22 17:13:13 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Sep 23 09:14:22 2015 +0200
     1.3 @@ -35,29 +35,27 @@
     1.4  
     1.5  lemma inorder_bal:
     1.6    "inorder(bal l a r) = inorder l @ a # inorder r"
     1.7 -by(induction l a r rule: bal.induct) (auto simp: sorted_lems)
     1.8 +by(induction l a r rule: bal.induct) (auto)
     1.9  
    1.10  lemma inorder_insert:
    1.11    "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
    1.12 -by(induction a t rule: insert.induct) (auto simp: ins_simps inorder_bal)
    1.13 +by(induction a t rule: insert.induct) (auto simp: ins_list_simps inorder_bal)
    1.14  
    1.15  lemma inorder_red: "inorder(red t) = inorder t"
    1.16 -by(induction t) (auto simp: sorted_lems)
    1.17 +by(induction t) (auto)
    1.18  
    1.19  lemma inorder_balL:
    1.20    "inorder(balL l a r) = inorder l @ a # inorder r"
    1.21 -by(induction l a r rule: balL.induct)
    1.22 -  (auto simp: sorted_lems inorder_bal inorder_red)
    1.23 +by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_red)
    1.24  
    1.25  lemma inorder_balR:
    1.26    "inorder(balR l a r) = inorder l @ a # inorder r"
    1.27 -by(induction l a r rule: balR.induct)
    1.28 -  (auto simp: sorted_lems inorder_bal inorder_red)
    1.29 +by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_red)
    1.30  
    1.31  lemma inorder_combine:
    1.32    "inorder(combine l r) = inorder l @ inorder r"
    1.33  by(induction l r rule: combine.induct)
    1.34 -  (auto simp: sorted_lems inorder_balL inorder_balR split: tree.split color.split)
    1.35 +  (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    1.36  
    1.37  lemma inorder_delete:
    1.38   "sorted(inorder t) \<Longrightarrow>  inorder(delete x t) = del_list x (inorder t)" and
    1.39 @@ -66,7 +64,7 @@
    1.40   "sorted(inorder r) \<Longrightarrow>  inorder(deleteR x l a r) =
    1.41      inorder l @ a # del_list x (inorder r)"
    1.42  by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
    1.43 -  (auto simp: del_simps inorder_combine inorder_balL inorder_balR)
    1.44 +  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    1.45  
    1.46  interpretation Set_by_Ordered
    1.47  where empty = Leaf and isin = isin and insert = insert and delete = delete