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
```