src/HOL/Data_Structures/Brother12_Set.thy
changeset 68020 6aade817bee5
parent 67965 aaa31cd0caef
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -92,14 +92,14 @@
     1.4    N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
     1.5  "n2 t1 a1 t2 = N2 t1 a1 t2"
     1.6  
     1.7 -fun del_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
     1.8 -"del_min N0 = None" |
     1.9 -"del_min (N1 t) =
    1.10 -  (case del_min t of
    1.11 +fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
    1.12 +"split_min N0 = None" |
    1.13 +"split_min (N1 t) =
    1.14 +  (case split_min t of
    1.15       None \<Rightarrow> None |
    1.16       Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
    1.17 -"del_min (N2 t1 a t2) =
    1.18 -  (case del_min t1 of
    1.19 +"split_min (N2 t1 a t2) =
    1.20 +  (case split_min t1 of
    1.21       None \<Rightarrow> Some (a, N1 t2) |
    1.22       Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
    1.23  
    1.24 @@ -110,7 +110,7 @@
    1.25    (case cmp x a of
    1.26       LT \<Rightarrow> n2 (del x l) a r |
    1.27       GT \<Rightarrow> n2 l a (del x r) |
    1.28 -     EQ \<Rightarrow> (case del_min r of
    1.29 +     EQ \<Rightarrow> (case split_min r of
    1.30                None \<Rightarrow> N1 l |
    1.31                Some (b, r') \<Rightarrow> n2 l b r'))"
    1.32  
    1.33 @@ -189,15 +189,15 @@
    1.34  lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
    1.35  by(cases "(l,a,r)" rule: n2.cases) (auto)
    1.36  
    1.37 -lemma inorder_del_min:
    1.38 -  "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
    1.39 -  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
    1.40 +lemma inorder_split_min:
    1.41 +  "t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
    1.42 +  (split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
    1.43  by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
    1.44  
    1.45  lemma inorder_del:
    1.46    "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    1.47  by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
    1.48 -     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
    1.49 +     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
    1.50  
    1.51  lemma inorder_delete:
    1.52    "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.53 @@ -331,15 +331,15 @@
    1.54  apply(erule exE bexE conjE imageE | simp | erule disjE)+
    1.55  done
    1.56  
    1.57 -lemma del_minNoneN0: "\<lbrakk>t \<in> B h; del_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
    1.58 +lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
    1.59  by (cases t) (auto split: option.splits)
    1.60  
    1.61 -lemma del_minNoneN1 : "\<lbrakk>t \<in> U h; del_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
    1.62 -by (cases h) (auto simp: del_minNoneN0  split: option.splits)
    1.63 +lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
    1.64 +by (cases h) (auto simp: split_minNoneN0  split: option.splits)
    1.65  
    1.66 -lemma del_min_type:
    1.67 -  "t \<in> B h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
    1.68 -  "t \<in> U h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
    1.69 +lemma split_min_type:
    1.70 +  "t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
    1.71 +  "t \<in> U h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
    1.72  proof (induction h arbitrary: t a t')
    1.73    case (Suc h)
    1.74    { case 1
    1.75 @@ -347,12 +347,12 @@
    1.76        t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
    1.77        by auto
    1.78      show ?case
    1.79 -    proof (cases "del_min t1")
    1.80 +    proof (cases "split_min t1")
    1.81        case None
    1.82        show ?thesis
    1.83        proof cases
    1.84          assume "t1 \<in> B h"
    1.85 -        with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
    1.86 +        with split_minNoneN0[OF this None] 1 show ?thesis by(auto)
    1.87        next
    1.88          assume "t1 \<notin> B h"
    1.89          thus ?thesis using 1 None by (auto)
    1.90 @@ -376,9 +376,9 @@
    1.91    { case 2
    1.92      then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
    1.93      show ?case
    1.94 -    proof (cases "del_min t1")
    1.95 +    proof (cases "split_min t1")
    1.96        case None
    1.97 -      with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
    1.98 +      with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
    1.99      next
   1.100        case [simp]: (Some bt')
   1.101        obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
   1.102 @@ -421,16 +421,16 @@
   1.103      qed
   1.104      moreover
   1.105      have ?case if [simp]: "x=a"
   1.106 -    proof (cases "del_min r")
   1.107 +    proof (cases "split_min r")
   1.108        case None
   1.109        show ?thesis
   1.110        proof cases
   1.111          assume "r \<in> B h"
   1.112 -        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.113 +        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.114        next
   1.115          assume "r \<notin> B h"
   1.116          hence "r \<in> U h" using lr by auto
   1.117 -        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.118 +        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.119        qed
   1.120      next
   1.121        case [simp]: (Some br')
   1.122 @@ -438,12 +438,12 @@
   1.123        show ?thesis
   1.124        proof cases
   1.125          assume "r \<in> B h"
   1.126 -        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.127 +        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.128          show ?thesis by simp
   1.129        next
   1.130          assume "r \<notin> B h"
   1.131          hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.132 -        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.133 +        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.134          show ?thesis by simp
   1.135        qed
   1.136      qed