unnecessary precondition
authornipkow
Fri Nov 13 16:17:30 2015 +0100 (2015-11-13)
changeset 61651415e816d3f37
parent 61650 2be10c63a0ab
child 61652 90c65a811257
unnecessary precondition
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
     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)
     2.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Nov 13 12:43:54 2015 +0000
     2.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Fri Nov 13 16:17:30 2015 +0100
     2.3 @@ -50,8 +50,7 @@
     2.4  
     2.5  
     2.6  lemma del_minD:
     2.7 -  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
     2.8 -   x # inorder t' = inorder t"
     2.9 +  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
    2.10  by(induction t arbitrary: t' rule: del_min.induct)
    2.11    (auto simp: sorted_lems split: prod.splits if_splits)
    2.12