src/HOL/Data_Structures/Tree_Set.thy
changeset 68020 6aade817bee5
parent 67965 aaa31cd0caef
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -27,9 +27,9 @@
     1.4       EQ \<Rightarrow> Node l a r |
     1.5       GT \<Rightarrow> Node l a (insert x r))"
     1.6  
     1.7 -fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
     1.8 -"del_min (Node l a r) =
     1.9 -  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
    1.10 +fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    1.11 +"split_min (Node l a r) =
    1.12 +  (if l = Leaf then (a,r) else let (x,l') = split_min l in (x, Node l' a r))"
    1.13  
    1.14  fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    1.15  "delete x Leaf = Leaf" |
    1.16 @@ -37,7 +37,7 @@
    1.17    (case cmp x a of
    1.18       LT \<Rightarrow>  Node (delete x l) a r |
    1.19       GT \<Rightarrow>  Node l a (delete x r) |
    1.20 -     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    1.21 +     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = split_min r in Node l a' r')"
    1.22  
    1.23  
    1.24  subsection "Functional Correctness Proofs"
    1.25 @@ -50,14 +50,14 @@
    1.26  by(induction t) (auto simp: ins_list_simps)
    1.27  
    1.28  
    1.29 -lemma del_minD:
    1.30 -  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
    1.31 -by(induction t arbitrary: t' rule: del_min.induct)
    1.32 +lemma split_minD:
    1.33 +  "split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
    1.34 +by(induction t arbitrary: t' rule: split_min.induct)
    1.35    (auto simp: sorted_lems split: prod.splits if_splits)
    1.36  
    1.37  lemma inorder_delete:
    1.38    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.39 -by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
    1.40 +by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
    1.41  
    1.42  interpretation Set_by_Ordered
    1.43  where empty = Leaf and isin = isin and insert = insert and delete = delete