src/HOL/Data_Structures/Brother12_Set.thy
changeset 67040 c1b87d15774a
parent 66453 cc19f7ca2ed6
child 67406 23307fd33906
     1.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Thu Nov 09 10:24:00 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Fri Nov 10 22:05:30 2017 +0100
     1.3 @@ -258,9 +258,9 @@
     1.4      then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
     1.5        t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h"
     1.6        by auto
     1.7 -    { assume "x < a"
     1.8 -      hence "?case \<longleftrightarrow> n2 (ins x t1) a t2 \<in> Bp (Suc h)" by simp
     1.9 -      also have "\<dots>"
    1.10 +    have ?case if "x < a"
    1.11 +    proof -
    1.12 +      have "n2 (ins x t1) a t2 \<in> Bp (Suc h)"
    1.13        proof cases
    1.14          assume "t1 \<in> B h"
    1.15          with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
    1.16 @@ -269,12 +269,12 @@
    1.17          hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto
    1.18          show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
    1.19        qed
    1.20 -      finally have ?case .
    1.21 -    }
    1.22 +      with `x < a` show ?case by simp
    1.23 +    qed
    1.24      moreover
    1.25 -    { assume "a < x"
    1.26 -      hence "?case \<longleftrightarrow> n2 t1 a (ins x t2) \<in> Bp (Suc h)" by simp
    1.27 -      also have "\<dots>"
    1.28 +    have ?case if "a < x"
    1.29 +    proof -
    1.30 +      have "n2 t1 a (ins x t2) \<in> Bp (Suc h)"
    1.31        proof cases
    1.32          assume "t2 \<in> B h"
    1.33          with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
    1.34 @@ -283,12 +283,14 @@
    1.35          hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto
    1.36          show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
    1.37        qed
    1.38 -    }
    1.39 -    moreover 
    1.40 -    { assume "x = a"
    1.41 +      with `a < x` show ?case by simp
    1.42 +    qed
    1.43 +    moreover
    1.44 +    have ?case if "x = a"
    1.45 +    proof -
    1.46        from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B)
    1.47 -      hence "?case" using `x = a` by simp
    1.48 -    }
    1.49 +      thus "?case" using `x = a` by simp
    1.50 +    qed
    1.51      ultimately show ?case by auto
    1.52    next
    1.53      case 2 thus ?case using Suc(1) n1_type by fastforce }
    1.54 @@ -398,61 +400,58 @@
    1.55    { case 1
    1.56      then obtain l a r where [simp]: "t = N2 l a r" and
    1.57        lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
    1.58 -    { assume "x < a"
    1.59 -      have ?case
    1.60 -      proof cases
    1.61 -        assume "l \<in> B h"
    1.62 -        from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
    1.63 -        show ?thesis using `x<a` by(simp)
    1.64 -      next
    1.65 -        assume "l \<notin> B h"
    1.66 -        hence "l \<in> U h" "r \<in> B h" using lr by auto
    1.67 -        from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
    1.68 -        show ?thesis using `x<a` by(simp)
    1.69 -      qed
    1.70 -    } moreover
    1.71 -    { assume "x > a"
    1.72 -      have ?case
    1.73 +    have ?case if "x < a"
    1.74 +    proof cases
    1.75 +      assume "l \<in> B h"
    1.76 +      from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
    1.77 +      show ?thesis using `x<a` by(simp)
    1.78 +    next
    1.79 +      assume "l \<notin> B h"
    1.80 +      hence "l \<in> U h" "r \<in> B h" using lr by auto
    1.81 +      from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
    1.82 +      show ?thesis using `x<a` by(simp)
    1.83 +    qed
    1.84 +    moreover
    1.85 +    have ?case if "x > a"
    1.86 +    proof cases
    1.87 +      assume "r \<in> B h"
    1.88 +      from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
    1.89 +      show ?thesis using `x>a` by(simp)
    1.90 +    next
    1.91 +      assume "r \<notin> B h"
    1.92 +      hence "l \<in> B h" "r \<in> U h" using lr by auto
    1.93 +      from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
    1.94 +      show ?thesis using `x>a` by(simp)
    1.95 +    qed
    1.96 +    moreover
    1.97 +    have ?case if [simp]: "x=a"
    1.98 +    proof (cases "del_min r")
    1.99 +      case None
   1.100 +      show ?thesis
   1.101        proof cases
   1.102          assume "r \<in> B h"
   1.103 -        from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
   1.104 -        show ?thesis using `x>a` by(simp)
   1.105 +        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.106        next
   1.107          assume "r \<notin> B h"
   1.108 -        hence "l \<in> B h" "r \<in> U h" using lr by auto
   1.109 -        from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
   1.110 -        show ?thesis using `x>a` by(simp)
   1.111 +        hence "r \<in> U h" using lr by auto
   1.112 +        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.113        qed
   1.114 -    } moreover
   1.115 -    { assume [simp]: "x=a"
   1.116 -      have ?case
   1.117 -      proof (cases "del_min r")
   1.118 -        case None
   1.119 -        show ?thesis
   1.120 -        proof cases
   1.121 -          assume "r \<in> B h"
   1.122 -          with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.123 -        next
   1.124 -          assume "r \<notin> B h"
   1.125 -          hence "r \<in> U h" using lr by auto
   1.126 -          with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.127 -        qed
   1.128 +    next
   1.129 +      case [simp]: (Some br')
   1.130 +      obtain b r' where [simp]: "br' = (b,r')" by fastforce
   1.131 +      show ?thesis
   1.132 +      proof cases
   1.133 +        assume "r \<in> B h"
   1.134 +        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.135 +        show ?thesis by simp
   1.136        next
   1.137 -        case [simp]: (Some br')
   1.138 -        obtain b r' where [simp]: "br' = (b,r')" by fastforce
   1.139 -        show ?thesis
   1.140 -        proof cases
   1.141 -          assume "r \<in> B h"
   1.142 -          from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.143 -          show ?thesis by simp
   1.144 -        next
   1.145 -          assume "r \<notin> B h"
   1.146 -          hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.147 -          from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.148 -          show ?thesis by simp
   1.149 -        qed
   1.150 +        assume "r \<notin> B h"
   1.151 +        hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.152 +        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.153 +        show ?thesis by simp
   1.154        qed
   1.155 -    } ultimately show ?case by auto
   1.156 +    qed
   1.157 +    ultimately show ?case by auto
   1.158    }
   1.159    { case 2 with Suc.IH(1) show ?case by auto }
   1.160  qed auto