src/HOL/Data_Structures/Tree_Map.thy
changeset 61651 415e816d3f37
parent 61647 5121b9a57cce
child 61686 e6784939d645
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Fri Nov 13 12:43:54 2015 +0000
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Fri Nov 13 16:17:30 2015 +0100
     1.3 @@ -34,18 +34,10 @@
     1.4    "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     1.5  by (induction t) (auto simp: map_of_simps split: option.split)
     1.6  
     1.7 -
     1.8  lemma inorder_update:
     1.9    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    1.10  by(induction t) (auto simp: upd_list_simps)
    1.11  
    1.12 -
    1.13 -lemma del_minD:
    1.14 -  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
    1.15 -   x # inorder t' = inorder t"
    1.16 -by(induction t arbitrary: t' rule: del_min.induct)
    1.17 -  (auto simp: del_list_simps split: prod.splits if_splits)
    1.18 -
    1.19  lemma inorder_delete:
    1.20    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.21  by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)