src/HOL/Data_Structures/Brother12_Map.thy
changeset 68020 6aade817bee5
parent 67965 aaa31cd0caef
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4    (case cmp x a of
     1.5       LT \<Rightarrow> n2 (del x l) (a,b) r |
     1.6       GT \<Rightarrow> n2 l (a,b) (del x r) |
     1.7 -     EQ \<Rightarrow> (case del_min r of
     1.8 +     EQ \<Rightarrow> (case split_min r of
     1.9                None \<Rightarrow> N1 l |
    1.10                Some (ab, r') \<Rightarrow> n2 l ab r'))"
    1.11  
    1.12 @@ -84,7 +84,7 @@
    1.13  lemma inorder_del:
    1.14    "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    1.15  by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
    1.16 -     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
    1.17 +     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
    1.18  
    1.19  lemma inorder_delete:
    1.20    "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.21 @@ -151,16 +151,16 @@
    1.22      qed
    1.23      moreover
    1.24      have ?case if [simp]: "x=a"
    1.25 -    proof (cases "del_min r")
    1.26 +    proof (cases "split_min r")
    1.27        case None
    1.28        show ?thesis
    1.29        proof cases
    1.30          assume "r \<in> B h"
    1.31 -        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
    1.32 +        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
    1.33        next
    1.34          assume "r \<notin> B h"
    1.35          hence "r \<in> U h" using lr by auto
    1.36 -        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    1.37 +        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    1.38        qed
    1.39      next
    1.40        case [simp]: (Some br')
    1.41 @@ -168,12 +168,12 @@
    1.42        show ?thesis
    1.43        proof cases
    1.44          assume "r \<in> B h"
    1.45 -        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
    1.46 +        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
    1.47          show ?thesis by simp
    1.48        next
    1.49          assume "r \<notin> B h"
    1.50          hence "l \<in> B h" and "r \<in> U h" using lr by auto
    1.51 -        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
    1.52 +        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
    1.53          show ?thesis by simp
    1.54        qed
    1.55      qed