src/HOL/Data_Structures/Brother12_Map.thy
changeset 67040 c1b87d15774a
parent 63411 e051eea34990
child 67406 23307fd33906
     1.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Thu Nov 09 10:24:00 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Fri Nov 10 22:05:30 2017 +0100
     1.3 @@ -126,61 +126,58 @@
     1.4    { case 1
     1.5      then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
     1.6        lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
     1.7 -    { assume "x < a"
     1.8 -      have ?case
     1.9 -      proof cases
    1.10 -        assume "l \<in> B h"
    1.11 -        from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
    1.12 -        show ?thesis using `x<a` by(simp)
    1.13 -      next
    1.14 -        assume "l \<notin> B h"
    1.15 -        hence "l \<in> U h" "r \<in> B h" using lr by auto
    1.16 -        from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
    1.17 -        show ?thesis using `x<a` by(simp)
    1.18 -      qed
    1.19 -    } moreover
    1.20 -    { assume "x > a"
    1.21 -      have ?case
    1.22 +    have ?case if "x < a"
    1.23 +    proof cases
    1.24 +      assume "l \<in> B h"
    1.25 +      from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
    1.26 +      show ?thesis using `x<a` by(simp)
    1.27 +    next
    1.28 +      assume "l \<notin> B h"
    1.29 +      hence "l \<in> U h" "r \<in> B h" using lr by auto
    1.30 +      from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
    1.31 +      show ?thesis using `x<a` by(simp)
    1.32 +    qed
    1.33 +    moreover
    1.34 +    have ?case if "x > a"
    1.35 +    proof cases
    1.36 +      assume "r \<in> B h"
    1.37 +      from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
    1.38 +      show ?thesis using `x>a` by(simp)
    1.39 +    next
    1.40 +      assume "r \<notin> B h"
    1.41 +      hence "l \<in> B h" "r \<in> U h" using lr by auto
    1.42 +      from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
    1.43 +      show ?thesis using `x>a` by(simp)
    1.44 +    qed
    1.45 +    moreover
    1.46 +    have ?case if [simp]: "x=a"
    1.47 +    proof (cases "del_min r")
    1.48 +      case None
    1.49 +      show ?thesis
    1.50        proof cases
    1.51          assume "r \<in> B h"
    1.52 -        from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
    1.53 -        show ?thesis using `x>a` by(simp)
    1.54 +        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
    1.55        next
    1.56          assume "r \<notin> B h"
    1.57 -        hence "l \<in> B h" "r \<in> U h" using lr by auto
    1.58 -        from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
    1.59 -        show ?thesis using `x>a` by(simp)
    1.60 +        hence "r \<in> U h" using lr by auto
    1.61 +        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    1.62        qed
    1.63 -    } moreover
    1.64 -    { assume [simp]: "x=a"
    1.65 -      have ?case
    1.66 -      proof (cases "del_min r")
    1.67 -        case None
    1.68 -        show ?thesis
    1.69 -        proof cases
    1.70 -          assume "r \<in> B h"
    1.71 -          with del_minNoneN0[OF this None] lr show ?thesis by(simp)
    1.72 -        next
    1.73 -          assume "r \<notin> B h"
    1.74 -          hence "r \<in> U h" using lr by auto
    1.75 -          with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    1.76 -        qed
    1.77 +    next
    1.78 +      case [simp]: (Some br')
    1.79 +      obtain b r' where [simp]: "br' = (b,r')" by fastforce
    1.80 +      show ?thesis
    1.81 +      proof cases
    1.82 +        assume "r \<in> B h"
    1.83 +        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
    1.84 +        show ?thesis by simp
    1.85        next
    1.86 -        case [simp]: (Some br')
    1.87 -        obtain b r' where [simp]: "br' = (b,r')" by fastforce
    1.88 -        show ?thesis
    1.89 -        proof cases
    1.90 -          assume "r \<in> B h"
    1.91 -          from del_min_type(1)[OF this] n2_type3[OF lr(1)]
    1.92 -          show ?thesis by simp
    1.93 -        next
    1.94 -          assume "r \<notin> B h"
    1.95 -          hence "l \<in> B h" and "r \<in> U h" using lr by auto
    1.96 -          from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
    1.97 -          show ?thesis by simp
    1.98 -        qed
    1.99 +        assume "r \<notin> B h"
   1.100 +        hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.101 +        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.102 +        show ?thesis by simp
   1.103        qed
   1.104 -    } ultimately show ?case by auto                         
   1.105 +    qed
   1.106 +    ultimately show ?case by auto                         
   1.107    }
   1.108    { case 2 with Suc.IH(1) show ?case by auto }
   1.109  qed auto