Tuned some proofs.
authorberghofe
Mon Oct 11 16:47:50 2004 +0200 (2004-10-11)
changeset 15239fb73c8154b19
parent 15238 cb559bd0b03c
child 15240 e1e6db03beee
Tuned some proofs.
src/HOL/Integ/Barith.thy
     1.1 --- a/src/HOL/Integ/Barith.thy	Mon Oct 11 10:52:18 2004 +0200
     1.2 +++ b/src/HOL/Integ/Barith.thy	Mon Oct 11 16:47:50 2004 +0200
     1.3 @@ -1,29 +1,32 @@
     1.4 -theory Barith = Presburger
     1.5 -files ("barith.ML") :
     1.6 +(*  Title:      HOL/Integ/Barith.thy
     1.7 +    ID:         $Id$
     1.8 +    Author:     Amine Chaieb, TU Muenchen
     1.9 +
    1.10 +Simple decision procedure for bounded arithmetic
    1.11 +*)
    1.12  
    1.13 -lemma imp_commute: "(PROP P ==> PROP Q
    1.14 -==> PROP R) == (PROP Q ==>
    1.15 -PROP P ==> PROP R)"
    1.16 +theory Barith
    1.17 +imports Presburger
    1.18 +files ("barith.ML")
    1.19 +begin
    1.20 +
    1.21 +lemma imp_commute: "(PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R) \<equiv>
    1.22 +  (PROP Q \<Longrightarrow> PROP P \<Longrightarrow> PROP R)"
    1.23  proof
    1.24 -  assume h1: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow>
    1.25 -PROP R"
    1.26 +  assume h1: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R"
    1.27    assume h2: "PROP Q"
    1.28    assume h3: "PROP P"
    1.29    from h3 h2 show "PROP R" by (rule h1)
    1.30  next
    1.31 -  assume h1: "PROP Q \<Longrightarrow> PROP P \<Longrightarrow>
    1.32 -PROP R"
    1.33 - assume h2: "PROP P"
    1.34 +  assume h1: "PROP Q \<Longrightarrow> PROP P \<Longrightarrow> PROP R"
    1.35 +  assume h2: "PROP P"
    1.36    assume h3: "PROP Q"
    1.37    from h3 h2 show "PROP R" by (rule h1)
    1.38  qed
    1.39  
    1.40 -lemma imp_simplify: "(PROP P \<Longrightarrow> PROP P
    1.41 -\<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow>
    1.42 -PROP Q)"
    1.43 +lemma imp_simplify: "(PROP P \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> PROP Q)"
    1.44  proof
    1.45 -  assume h1: "PROP P \<Longrightarrow> PROP P \<Longrightarrow>
    1.46 -PROP Q"
    1.47 +  assume h1: "PROP P \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
    1.48    assume h2: "PROP P"
    1.49    from h2 h2 show "PROP Q" by (rule h1)
    1.50  next
    1.51 @@ -35,47 +38,47 @@
    1.52  
    1.53  (* Abstraction of constants *)
    1.54  lemma abs_const: "(x::int) <= x \<and> x <= x"
    1.55 -by simp
    1.56 +  by simp
    1.57  
    1.58  (* Abstraction of Variables *)
    1.59  lemma abs_var: "l <= (x::int) \<and> x <= u \<Longrightarrow> l <= (x::int) \<and> x <= u"
    1.60 -by simp
    1.61 +  by simp
    1.62  
    1.63  
    1.64  (* Unary operators *)
    1.65  lemma abs_neg: "l <= (x::int) \<and> x <= u \<Longrightarrow>  -u <= -x \<and> -x <= -l"
    1.66 -by arith
    1.67 +  by arith
    1.68  
    1.69  
    1.70  (* Binary operations *)
    1.71  (* Addition*)
    1.72  lemma abs_add: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> 
    1.73    \<Longrightarrow>  l1 + l2 <= x1 + x2 \<and> x1 + x2 <= u1 + u2"
    1.74 -by arith
    1.75 +  by arith
    1.76  
    1.77  lemma abs_sub: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> 
    1.78    \<Longrightarrow>  l1 - u2 <= x1 - x2 \<and> x1 - x2 <= u1 - l2"
    1.79 -by arith
    1.80 +  by arith
    1.81  
    1.82  lemma abs_sub_x: "l <= (x::int) \<and> x <= u \<Longrightarrow> 0 <= x - x \<and> x - x <= 0"
    1.83 -by arith
    1.84 +  by arith
    1.85  
    1.86  (* For resolving the last step*)
    1.87  lemma subinterval: "\<lbrakk>l <= (e::int) \<and> e <= u ; l' <= l ; u <= u' \<rbrakk>
    1.88    \<Longrightarrow> l' <= e \<and> e <= u'"
    1.89 -by arith
    1.90 +  by arith
    1.91  
    1.92  lemma min_max_minus : "min (-a ::int) (-b) = - max a b"
    1.93 -by arith
    1.94 +  by arith
    1.95  
    1.96  lemma max_min_minus : " max (-a ::int) (-b) = - min a b"
    1.97 -by arith
    1.98 +  by arith
    1.99  
   1.100  lemma max_max_commute : "max (max (a::int) b) (max c d) = max (max a c) (max b d)"
   1.101 -by arith
   1.102 +  by arith
   1.103  
   1.104  lemma min_min_commute : "min (min (a::int) b) (min c d) = min (min a c) (min b d)"
   1.105 -by arith
   1.106 +  by arith
   1.107  
   1.108  lemma zintervals_min: "\<lbrakk> l1 <= (x1::int) \<and> x1<= u1 ; l2 <= x2 \<and> x2 <= u2 \<rbrakk> 
   1.109    \<Longrightarrow> min l1 l2 <= x1 \<and> x1 <= max u1 u2" by arith
   1.110 @@ -109,9 +112,9 @@
   1.111    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.112    and     l1_pos : "0 <= l1"
   1.113    and     l2_pos : "0 <= l2"
   1.114 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.115 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.116    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.117 -proof-
   1.118 +proof -
   1.119    from x1_lu have l1_le : "l1 <= x1" by simp
   1.120    from x1_lu have x1_le : "x1 <= u1" by simp
   1.121    from x2_lu have l2_le : "l2 <= x2" by simp
   1.122 @@ -148,61 +151,66 @@
   1.123  qed
   1.124  
   1.125  lemma min_le_I1 : "min (a::int) b <= a" by arith
   1.126 +
   1.127  lemma min_le_I2 : "min (a::int) b <= b" by arith
   1.128 +
   1.129  lemma zinterval_lneglpos :
   1.130    assumes  x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.131    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.132    and     l1_neg : "l1 <= 0"
   1.133    and x1_pos : "0 <= x1" 
   1.134    and     l2_pos : "0 <= l2"
   1.135 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.136 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.137    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.138 -
   1.139 -proof-
   1.140 -    from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp
   1.141 -    from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.142 -    from x1_lu x1_pos have u1_pos : "0 <= u1" by arith
   1.143 -    from x2_lu l2_pos have u2_pos : "0 <= u2" by arith
   1.144 -    from x2_lu have l2_le_u2 : "l2 <= u2" by arith
   1.145 -    from l2_le_u2 u1_pos 
   1.146 -     have u1l2_le_u1u2 : "u1*l2 <= u1*u2" by (simp add: zmult_zle_mono)
   1.147 -    have trv_0 : "(0::int) <= 0" by simp
   1.148 -    have "0*0 <= u1*l2" 
   1.149 -      by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos l2_pos])
   1.150 -    then have u1l2_pos : "0 <= u1*l2" by simp
   1.151 -      from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.152 -      from ml1_pos l2_pos have "0*0 <= (-l1)*l2" 
   1.153 -	by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos l2_pos])
   1.154 -      then have "0 <= -(l1*l2)" by simp  
   1.155 -      then have "0 - (-(l1*l2)) <= 0" by arith 
   1.156 -      then
   1.157 -      have l1l2_neg : "l1*l2 <= 0" by simp
   1.158 -      from ml1_pos u2_pos have "0*0 <= (-l1)*u2" 
   1.159 -	by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos])
   1.160 -      then have "0 <= -(l1*u2)" by simp  
   1.161 -      then have "0 - (-(l1*u2)) <= 0" by arith 
   1.162 -      then
   1.163 -      have l1u2_neg : "l1*u2 <= 0" by simp
   1.164 -      from l1l2_neg u1l2_pos have l1l2_le_u1l2: "l1*l2 <= u1*l2" by simp
   1.165 -      from l1u2_neg u1l2_pos have l1u2_le_u1l2 : "l1*u2 <= u1*l2" by simp
   1.166 -      from ml1_pos l2_le_u2 have "(-l1)*l2 <= (-l1)*u2"
   1.167 -	by (simp only: zmult_zle_mono) 
   1.168 -      then have l1u2_le_l1l2 : "l1*u2 <= l1*l2" by simp
   1.169 -      from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.170 -      have min1 : "l1*u2 = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" 
   1.171 -	by arith
   1.172 -      from u1l2_pos u1l2_le_u1u2 have "0 = min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by arith
   1.173 -      with l1u2_neg min1 have minth : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by simp
   1.174 -      from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.175 -      have max1 : "u1*u2 = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" 
   1.176 -	by arith
   1.177 -      from u1l2_pos u1l2_le_u1u2 have "u1*u2 = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by arith 
   1.178 -      with  max1 have "max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2)) = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by simp
   1.179 -      then have maxth : " max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2)) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" by simp
   1.180 -    have x1x2_0_u : "min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2)) <= x1 * x2 &
   1.181 -x1 * x2 <= max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.182 -      by (simp only: zinterval_lposlpos[OF x1_0_u1 x2_lu trv_0 l2_pos],simp)
   1.183 -      from minth maxth x1x2_0_u show ?thesis by (simp add: subinterval[OF _ minth maxth])
   1.184 +proof -
   1.185 +  from x1_lu x1_pos have x1_0_u1: "0 <= x1 \<and> x1 <= u1" by simp
   1.186 +  from l1_neg have ml1_pos: "0 <= -l1" by simp
   1.187 +  from x1_lu x1_pos have u1_pos: "0 <= u1" by arith
   1.188 +  from x2_lu l2_pos have u2_pos: "0 <= u2" by arith
   1.189 +  from x2_lu have l2_le_u2: "l2 <= u2" by arith
   1.190 +  from l2_le_u2 u1_pos
   1.191 +  have u1l2_le_u1u2: "u1*l2 <= u1*u2" by (rule zmult_zle_mono)
   1.192 +  have trv_0: "(0::int) <= 0" by simp
   1.193 +  from trv_0 trv_0 u1_pos l2_pos
   1.194 +  have "0*0 <= u1*l2" by (rule zmult_mono)
   1.195 +  then have u1l2_pos: "0 <= u1*l2" by simp
   1.196 +  from l1_neg have ml1_pos: "0 <= -l1" by simp
   1.197 +  from trv_0 trv_0 ml1_pos l2_pos have "0*0 <= (-l1)*l2"
   1.198 +    by (rule zmult_mono)
   1.199 +  then have "0 <= -(l1*l2)" by simp  
   1.200 +  then have "0 - (-(l1*l2)) <= 0" by arith 
   1.201 +  then have l1l2_neg: "l1*l2 <= 0" by simp
   1.202 +  from trv_0 trv_0 ml1_pos u2_pos have "0*0 <= (-l1)*u2"
   1.203 +    by (rule zmult_mono)
   1.204 +  then have "0 <= -(l1*u2)" by simp  
   1.205 +  then have "0 - (-(l1*u2)) <= 0" by arith 
   1.206 +  then have l1u2_neg: "l1*u2 <= 0" by simp
   1.207 +  from l1l2_neg u1l2_pos have l1l2_le_u1l2: "l1*l2 <= u1*l2" by simp
   1.208 +  from l1u2_neg u1l2_pos have l1u2_le_u1l2: "l1*u2 <= u1*l2" by simp
   1.209 +  from ml1_pos l2_le_u2 have "(-l1)*l2 <= (-l1)*u2"
   1.210 +    by (simp only: zmult_zle_mono) 
   1.211 +  then have l1u2_le_l1l2: "l1*u2 <= l1*l2" by simp
   1.212 +  from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.213 +  have min1: "l1*u2 = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" 
   1.214 +    by arith
   1.215 +  from u1l2_pos u1l2_le_u1u2 have "0 = min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))"
   1.216 +    by arith
   1.217 +  with l1u2_neg min1 have minth: "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <=
   1.218 +    min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by simp
   1.219 +  from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.220 +  have max1: "u1*u2 = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" 
   1.221 +    by arith
   1.222 +  from u1l2_pos u1l2_le_u1u2
   1.223 +  have "u1*u2 = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by arith 
   1.224 +  with max1 have "max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2)) =
   1.225 +    max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by simp
   1.226 +  then have maxth: " max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2)) <=
   1.227 +    max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" by simp
   1.228 +  from x1_0_u1 x2_lu trv_0 l2_pos
   1.229 +  have x1x2_0_u: "min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2)) <= x1 * x2 &
   1.230 +    x1 * x2 <= max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.231 +    by (rule zinterval_lposlpos)
   1.232 +  thus ?thesis using minth maxth by (rule subinterval)
   1.233  qed
   1.234  
   1.235  lemma zinterval_lneglneg :
   1.236 @@ -212,101 +220,100 @@
   1.237    and     x1_pos : "0 <= x1" 
   1.238    and     l2_neg : "l2 <= 0"
   1.239    and     x2_pos : "0 <= x2"
   1.240 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.241 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.242    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.243 +proof -
   1.244 +  from x1_lu x1_pos have x1_0_u1: "0 <= x1 \<and> x1 <= u1" by simp
   1.245 +  from l1_neg have ml1_pos: "0 <= -l1" by simp
   1.246 +  from l1_neg have l1_le0: "l1 <= 0" by simp
   1.247 +  from x1_lu x1_pos have u1_pos: "0 <= u1" by arith
   1.248 +  from x2_lu x2_pos have x2_0_u2: "0 <= x2 \<and> x2 <= u2" by simp
   1.249 +  from l2_neg have ml2_pos: "0 <= -l2" by simp
   1.250 +  from l2_neg have l2_le0: "l2 <= 0" by simp
   1.251 +  from x2_lu x2_pos have u2_pos: "0 <= u2" by arith
   1.252 +  have trv_0: "(0::int) <= 0" by simp
   1.253  
   1.254 -proof-
   1.255 -    from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp
   1.256 -    from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.257 -    from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.258 -    from x1_lu x1_pos have u1_pos : "0 <= u1" by arith
   1.259 -    from x2_lu x2_pos have x2_0_u2 : "0 <= x2 \<and> x2 <= u2" by simp
   1.260 -    from l2_neg have ml2_pos : "0 <= -l2" by simp
   1.261 -    from l2_neg have l2_le0 : "l2 <= 0" by simp
   1.262 -    from x2_lu x2_pos have u2_pos : "0 <= u2" by arith
   1.263 -    have trv_0 : "(0::int) <= 0" by simp
   1.264 -
   1.265 -    have x1x2_th1 : 
   1.266 -      "min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)) \<le> x1 * x2 \<and>
   1.267 -      x1 * x2 \<le> max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))"
   1.268 -      by (rule_tac  zinterval_lneglpos[OF x1_lu x2_0_u2 l1_le0 x1_pos trv_0])
   1.269 +  from x1_lu x2_0_u2 l1_le0 x1_pos trv_0
   1.270 +  have x1x2_th1: 
   1.271 +    "min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)) \<le> x1 * x2 \<and>
   1.272 +    x1 * x2 \<le> max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))"
   1.273 +    by (rule zinterval_lneglpos)
   1.274      
   1.275 -    have x1x2_eq_x2x1 : "x1*x2 = x2*x1" by (simp add: mult_ac)
   1.276 -    have
   1.277 -      "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x2 * x1 \<and>
   1.278 -      x2 * x1 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.279 -      by (rule_tac  zinterval_lneglpos[OF x2_lu x1_0_u1 l2_le0 x2_pos trv_0])
   1.280 +  have x1x2_eq_x2x1: "x1*x2 = x2*x1" by (simp add: mult_ac)
   1.281 +  from x2_lu x1_0_u1 l2_le0 x2_pos trv_0
   1.282 +  have
   1.283 +    "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x2 * x1 \<and>
   1.284 +    x2 * x1 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.285 +    by (rule zinterval_lneglpos)
   1.286      
   1.287 -    then have x1x2_th2 : 
   1.288 -      "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x1 * x2 \<and>
   1.289 -      x1 * x2 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.290 -      by (simp add: x1x2_eq_x2x1)
   1.291 +  then have x1x2_th2: 
   1.292 +    "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x1 * x2 \<and>
   1.293 +    x1 * x2 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.294 +    by (simp add: x1x2_eq_x2x1)
   1.295  
   1.296 -    from x1x2_th1 x1x2_th2 have x1x2_th3:
   1.297 -      "min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.298 -      (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))
   1.299 -      \<le> x1 * x2 \<and>
   1.300 -      x1 * x2
   1.301 -      \<le> max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.302 -      (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1)))"
   1.303 -      by (rule_tac zintervals_min[OF x1x2_th1 x1x2_th2])
   1.304 +  from x1x2_th1 x1x2_th2 have x1x2_th3:
   1.305 +    "min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.306 +    (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))
   1.307 +    \<le> x1 * x2 \<and>
   1.308 +    x1 * x2
   1.309 +    \<le> max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.310 +    (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1)))"
   1.311 +    by (rule zintervals_min)
   1.312  
   1.313 -    from ml1_pos u2_pos 
   1.314 -    have "0*0 <= -l1*u2" 
   1.315 -      by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos]) 
   1.316 -    then have l1u2_neg : "l1*u2 <= 0" by simp
   1.317 -    from l1u2_neg have min_l1u2_0 : "min (0) (l1*u2) = l1*u2" by arith
   1.318 -    from l1u2_neg have max_l1u2_0 : "max (0) (l1*u2) = 0" by arith
   1.319 -    from u1_pos u2_pos 
   1.320 -    have "0*0 <= u1*u2" 
   1.321 -      by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos u2_pos]) 
   1.322 -    then have u1u2_pos :"0 <= u1*u2" by simp
   1.323 -    from u1u2_pos have min_0_u1u2 : "min 0 (u1*u2) = 0" by arith
   1.324 -    from u1u2_pos have max_0_u1u2 : "max 0 (u1*u2) = u1*u2" by arith
   1.325 -    from ml2_pos u1_pos have "0*0 <= -l2*u1" 
   1.326 -      by (simp only: zmult_mono[OF trv_0 trv_0 ml2_pos u1_pos]) 
   1.327 -    then have l2u1_neg : "l2*u1 <= 0" by simp
   1.328 -    from l2u1_neg have min_l2u1_0 : "min 0 (l2*u1) = l2*u1" by arith
   1.329 -    from l2u1_neg have max_l2u1_0 : "max 0 (l2*u1) = 0" by arith
   1.330 -    from min_l1u2_0 min_0_u1u2 min_l2u1_0 
   1.331 -    have min_th1: 
   1.332 -      " min (l2*u1) (l1*u2) <= min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.333 -      (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))"
   1.334 -      by (simp add: min_commute mult_ac)
   1.335 -    from max_l1u2_0 max_0_u1u2 max_l2u1_0 
   1.336 -    have max_th1: "max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.337 -      (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))) <= u1*u2"
   1.338 -      by (simp add: max_commute mult_ac)
   1.339 -    have x1x2_th4: "min (l2*u1) (l1*u2) <= x1*x2 \<and> x1*x2 <= u1*u2" 
   1.340 -      by (rule_tac subinterval[OF x1x2_th3 min_th1 max_th1])
   1.341 +  from trv_0 trv_0 ml1_pos u2_pos 
   1.342 +  have "0*0 <= -l1*u2" by (rule zmult_mono) 
   1.343 +  then have l1u2_neg: "l1*u2 <= 0" by simp
   1.344 +  from l1u2_neg have min_l1u2_0: "min (0) (l1*u2) = l1*u2" by arith
   1.345 +  from l1u2_neg have max_l1u2_0: "max (0) (l1*u2) = 0" by arith
   1.346 +  from trv_0 trv_0 u1_pos u2_pos
   1.347 +  have "0*0 <= u1*u2" by (rule zmult_mono) 
   1.348 +  then have u1u2_pos: "0 <= u1*u2" by simp
   1.349 +  from u1u2_pos have min_0_u1u2: "min 0 (u1*u2) = 0" by arith
   1.350 +  from u1u2_pos have max_0_u1u2: "max 0 (u1*u2) = u1*u2" by arith
   1.351 +  from trv_0 trv_0 ml2_pos u1_pos have "0*0 <= -l2*u1" 
   1.352 +    by (rule zmult_mono) 
   1.353 +  then have l2u1_neg: "l2*u1 <= 0" by simp
   1.354 +  from l2u1_neg have min_l2u1_0: "min 0 (l2*u1) = l2*u1" by arith
   1.355 +  from l2u1_neg have max_l2u1_0: "max 0 (l2*u1) = 0" by arith
   1.356 +  from min_l1u2_0 min_0_u1u2 min_l2u1_0 
   1.357 +  have min_th1:
   1.358 +    "min (l2*u1) (l1*u2) <= min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.359 +    (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))"
   1.360 +    by (simp add: min_commute mult_ac)
   1.361 +  from max_l1u2_0 max_0_u1u2 max_l2u1_0 
   1.362 +  have max_th1: "max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.363 +    (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))) <= u1*u2"
   1.364 +    by (simp add: max_commute mult_ac)
   1.365 +  from x1x2_th3 min_th1 max_th1
   1.366 +  have x1x2_th4: "min (l2*u1) (l1*u2) <= x1*x2 \<and> x1*x2 <= u1*u2" 
   1.367 +    by (rule subinterval)
   1.368      
   1.369 -    have " min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) = min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1))" by (simp add: min_min_commute min_commute mult_ac) 
   1.370 -    moreover 
   1.371 -    have " min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1)) <= min (l1*u2) (l2*u1)" 
   1.372 -      by 
   1.373 -    (rule_tac min_le_I2 [of "(min (l1*l2) (u1*u2))" "(min (l1*u2) (l2*u1))"]) 
   1.374 -    ultimately have "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (l1*u2) (l2*u1)" by simp 
   1.375 -    then 
   1.376 -    have min_le1: "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <=min (l2*u1) (l1*u2)" 
   1.377 -      by (simp add: min_commute mult_ac)
   1.378 -    have "u1*u2 <= max (u1*l2) (u1*u2)" 
   1.379 -      by (rule_tac le_maxI2[of  "u1*u2" "u1*l2"]) 
   1.380 +  have "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) =
   1.381 +    min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1))"
   1.382 +    by (simp add: min_min_commute min_commute mult_ac) 
   1.383 +  moreover have "min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1)) <= min (l1*u2) (l2*u1)" 
   1.384 +    by (rule min_le_I2)
   1.385 +  ultimately have "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (l1*u2) (l2*u1)"
   1.386 +    by simp 
   1.387 +  then  have min_le1: "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <=min (l2*u1) (l1*u2)" 
   1.388 +    by (simp add: min_commute mult_ac)
   1.389 +  have "u1*u2 <= max (u1*l2) (u1*u2)" 
   1.390 +    by (rule le_maxI2) 
   1.391      
   1.392 -    moreover have "max (u1*l2) (u1*u2) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.393 -      by(rule_tac le_maxI2[of "(max (u1*l2) (u1*u2))" "(max (l1*l2) (l1*u2))"])
   1.394 -    then 
   1.395 -    have max_le1:"u1*u2 <= max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.396 -      by simp
   1.397 -    show ?thesis by (simp add: subinterval[OF x1x2_th4 min_le1 max_le1])
   1.398 -  qed
   1.399 +  moreover have "max (u1*l2) (u1*u2) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.400 +    by (rule le_maxI2)
   1.401 +  then have max_le1: "u1*u2 <= max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.402 +    by simp
   1.403 +  with x1x2_th4 min_le1 show ?thesis by (rule subinterval)
   1.404 +qed
   1.405  
   1.406  lemma zinterval_lpos:
   1.407    assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.408    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.409    and     l1_pos: "0 <= l1"
   1.410 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.411 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.412    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.413 -proof-
   1.414 +proof -
   1.415    from x1_lu have l1_le : "l1 <= x1" by simp
   1.416    from x1_lu have x1_le : "x1 <= u1" by simp
   1.417    from x2_lu have l2_le : "l2 <= x2" by simp
   1.418 @@ -314,172 +321,168 @@
   1.419    from x1_lu have l1_leu : "l1 <= u1" by arith
   1.420    from x2_lu have l2_leu : "l2 <= u2" by arith
   1.421    have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <0)" by arith
   1.422 -  moreover
   1.423 -  {
   1.424 +  thus ?thesis
   1.425 +  proof (elim disjE conjE)
   1.426      assume l2_pos: "0 <= l2"
   1.427 -    have ?thesis by (simp add: zinterval_lposlpos[OF x1_lu x2_lu l1_pos l2_pos])
   1.428 -  }
   1.429 -moreover
   1.430 -{
   1.431 -  assume  l2_neg : "l2 < 0" and x2_pos: "0<= x2"
   1.432 -  from l2_neg have l2_le_0 : "l2 <= 0" by arith
   1.433 -  thm zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos]
   1.434 -have th1 : 
   1.435 -  "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.436 -  x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" 
   1.437 -  by (simp add : zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos])
   1.438 -have mth1 : "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) = min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2))" 
   1.439 -  by (simp add: min_min_commute mult_ac)
   1.440 -have mth2: "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) = max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))"
   1.441 -  by (simp add: max_max_commute mult_ac)
   1.442 -have x1x2_th : "x2*x1 = x1*x2" by (simp add: mult_ac)
   1.443 -from th1 mth1 mth2 x1x2_th have 
   1.444 -   "min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2)) \<le> x1 * x2 \<and>
   1.445 -   x1 * x2 \<le> max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))"
   1.446 -by auto
   1.447 -    then have ?thesis by simp 
   1.448 -}
   1.449 -moreover
   1.450 -{
   1.451 -  assume x2_neg : "x2 <0" and u2_pos : "0 <= u2"
   1.452 -  from x2_lu x2_neg have mx2_mu2_ml2 : "-u2 <= -x2 \<and> -x2 <= -l2" by simp
   1.453 -  from u2_pos have mu2_neg : "-u2 <= 0" by simp
   1.454 -  from x2_neg have mx2_pos : "0 <= -x2" by simp
   1.455 -thm zinterval_lneglpos[OF mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos]
   1.456 -    have mx1x2_lu : 
   1.457 -"min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1))
   1.458 -\<le> - x2 * x1 \<and>
   1.459 -- x2 * x1 \<le> max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1))"      
   1.460 -      by (simp only: zinterval_lneglpos [OF  mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos],simp)
   1.461 -    have min_eq_mmax : 
   1.462 +    with x1_lu x2_lu l1_pos show ?thesis by (rule zinterval_lposlpos)
   1.463 +  next
   1.464 +    assume l2_neg: "l2 < 0" and x2_pos: "0<= x2"
   1.465 +    from l2_neg have l2_le_0 : "l2 <= 0" by arith
   1.466 +    from x2_lu x1_lu l2_le_0 x2_pos l1_pos
   1.467 +    have th1: 
   1.468 +      "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.469 +      x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" 
   1.470 +      by (rule zinterval_lneglpos)
   1.471 +    have mth1: "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) =
   1.472 +      min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2))" 
   1.473 +      by (simp add: min_min_commute mult_ac)
   1.474 +    have mth2: "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) =
   1.475 +      max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))"
   1.476 +      by (simp add: max_max_commute mult_ac)
   1.477 +    have x1x2_th: "x2*x1 = x1*x2" by (simp add: mult_ac)
   1.478 +    from th1 mth1 mth2 x1x2_th have 
   1.479 +      "min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2)) \<le> x1 * x2 \<and>
   1.480 +      x1 * x2 \<le> max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))"
   1.481 +      by auto
   1.482 +    thus ?thesis by simp
   1.483 +  next
   1.484 +    assume x2_neg: "x2 <0" and u2_pos: "0 <= u2"
   1.485 +    from x2_lu x2_neg have mx2_mu2_ml2: "-u2 <= -x2 \<and> -x2 <= -l2" by simp
   1.486 +    from u2_pos have mu2_neg: "-u2 <= 0" by simp
   1.487 +    from x2_neg have mx2_pos: "0 <= -x2" by simp
   1.488 +    from mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos
   1.489 +    have mx1x2_lu: 
   1.490 +      "min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1))
   1.491 +      \<le> - x2 * x1 \<and>
   1.492 +      - x2 * x1 \<le> max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1))"      
   1.493 +      by (rule zinterval_lneglpos)
   1.494 +    have min_eq_mmax: 
   1.495        "min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1)) = 
   1.496        - max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))" 
   1.497        by (simp add: min_max_minus max_min_minus)
   1.498 -    have max_eq_mmin : 
   1.499 +    have max_eq_mmin: 
   1.500        " max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1)) = 
   1.501        -min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))"
   1.502        by (simp add: min_max_minus max_min_minus)
   1.503      from mx1x2_lu min_eq_mmax max_eq_mmin 
   1.504      have "- max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))<= - x1 * x2 &
   1.505        - x1*x2 <=  -min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))" by (simp add: mult_ac)
   1.506 - then have ?thesis by (simp add: min_min_commute min_commute max_commute max_max_commute mult_ac) 
   1.507 -
   1.508 -}
   1.509 -moreover
   1.510 -{
   1.511 -  assume u2_neg : "u2 < 0"
   1.512 -  from x2_lu have mx2_lu : "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.513 -  from u2_neg have mu2_pos : "0 <= -u2" by arith
   1.514 -thm zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos]
   1.515 -have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.516 -\<le> x1 * - x2 \<and>
   1.517 -x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))
   1.518 -  " by (rule_tac zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos])
   1.519 -then have mx1x2_lu:
   1.520 -  "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) \<le> - x1 * x2 \<and>
   1.521 -- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))
   1.522 -  " by simp
   1.523 -moreover have "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) =- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2)) " 
   1.524 -  by (simp add: min_max_minus max_min_minus)
   1.525 -moreover 
   1.526 -have 
   1.527 -"max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) = - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))"
   1.528 - by (simp add: min_max_minus max_min_minus)
   1.529 -thm subinterval[OF mx1x2_lu]
   1.530 -ultimately have "- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2))\<le> - x1 * x2 \<and>
   1.531 -- x1 * x2 \<le> - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2)) " by simp
   1.532 - then have ?thesis by (simp add: max_commute min_commute)
   1.533 -}
   1.534 -ultimately show ?thesis by blast
   1.535 +    thus ?thesis by (simp add: min_min_commute min_commute max_commute max_max_commute mult_ac)
   1.536 +  next
   1.537 +    assume u2_neg: "u2 < 0"
   1.538 +    from x2_lu have mx2_lu: "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.539 +    from u2_neg have mu2_pos: "0 <= -u2" by arith
   1.540 +    from x1_lu mx2_lu l1_pos mu2_pos
   1.541 +    have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.542 +      \<le> x1 * - x2 \<and>
   1.543 +      x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))"
   1.544 +      by (rule zinterval_lposlpos)
   1.545 +    then have mx1x2_lu:
   1.546 +      "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) \<le> - x1 * x2 \<and>
   1.547 +      - x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))"
   1.548 +      by simp
   1.549 +    moreover have "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) =
   1.550 +      - max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2)) " 
   1.551 +      by (simp add: min_max_minus max_min_minus)
   1.552 +    moreover have
   1.553 +      "max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) =
   1.554 +      - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))"
   1.555 +      by (simp add: min_max_minus max_min_minus)
   1.556 +    ultimately have "- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2))\<le> - x1 * x2 \<and>
   1.557 +      - x1 * x2 \<le> - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2)) " by simp
   1.558 +    thus ?thesis by (simp add: max_commute min_commute)
   1.559 +  qed
   1.560  qed
   1.561  
   1.562  lemma zinterval_uneg :
   1.563  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.564    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.565    and     u1_neg: "u1 <= 0"
   1.566 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.567 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.568    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.569 -proof-
   1.570 +proof -
   1.571    from x1_lu  have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith
   1.572    from u1_neg have mu1_pos : "0 <= -u1" by arith
   1.573 -  thm zinterval_lpos [OF mx1_lu x2_lu mu1_pos]
   1.574 -  have mx1x2_lu : 
   1.575 +  with mx1_lu x2_lu have mx1x2_lu : 
   1.576      "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2))
   1.577      \<le> - x1 * x2 \<and> - x1 * x2 \<le> 
   1.578      max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))"
   1.579 -by (rule_tac zinterval_lpos [OF mx1_lu x2_lu mu1_pos])
   1.580 -moreover have 
   1.581 -  "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) = - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" by (simp add: min_max_minus max_min_minus)
   1.582 -moreover have 
   1.583 -  "max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) = - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))" by (simp add: min_max_minus max_min_minus)
   1.584 -ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))\<le> - x1 * x2 \<and> - x1 * x2 \<le>  - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))" by simp
   1.585 -then show ?thesis by (simp add: min_commute max_commute mult_ac)
   1.586 +    by (rule zinterval_lpos)
   1.587 +  moreover have 
   1.588 +    "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) =
   1.589 +    - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))"
   1.590 +    by (simp add: min_max_minus max_min_minus)
   1.591 +  moreover have 
   1.592 +    "max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) =
   1.593 +    - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))"
   1.594 +    by (simp add: min_max_minus max_min_minus)
   1.595 +  ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2)) \<le> - x1 * x2 \<and>
   1.596 +    - x1 * x2 \<le>  - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))" by simp
   1.597 +  then show ?thesis by (simp add: min_commute max_commute mult_ac)
   1.598  qed
   1.599  
   1.600  lemma zinterval_lnegxpos:
   1.601 -assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.602 +  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.603    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.604    and     l1_neg: "l1 <= 0"
   1.605    and     x1_pos: "0<= x1"
   1.606 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.607 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.608    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.609 -proof-
   1.610 +proof -
   1.611    have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <= 0)" by arith
   1.612 -  moreover
   1.613 -  {
   1.614 +  thus ?thesis
   1.615 +  proof (elim disjE conjE)
   1.616      assume l2_pos: "0 <= l2"
   1.617 -    thm zinterval_lpos [OF x2_lu x1_lu l2_pos]
   1.618 -    have 
   1.619 +    with x2_lu x1_lu have 
   1.620        "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.621        x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))"
   1.622 -      by (rule_tac zinterval_lpos [OF x2_lu x1_lu l2_pos])
   1.623 - moreover have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" by (simp add: mult_ac min_commute min_min_commute)
   1.624 -moreover have "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.625 -  by (simp add: mult_ac max_commute max_max_commute)
   1.626 -ultimately have ?thesis by (simp add: mult_ac)
   1.627 -
   1.628 -}
   1.629 -
   1.630 -moreover
   1.631 -{
   1.632 -  assume l2_neg: "l2 < 0" and x2_pos: " 0<= x2"
   1.633 -  from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.634 -  from l2_neg have l2_le0 : "l2 <= 0" by simp
   1.635 - have ?thesis by (simp add: zinterval_lneglneg [OF x1_lu x2_lu l1_le0 x1_pos l2_le0 x2_pos])
   1.636 -}
   1.637 -
   1.638 -moreover
   1.639 -{
   1.640 - assume x2_neg: "x2 <0" and u2_pos: "0 <= u2"
   1.641 - from x2_lu have mx2_lu: "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.642 - from x2_neg have mx2_pos: "0 <= -x2" by simp
   1.643 - from u2_pos have mu2_neg: "-u2 <= 0" by simp
   1.644 - from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.645 -thm zinterval_lneglneg [OF x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos]
   1.646 -have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.647 -\<le> x1 * - x2 \<and>
   1.648 -x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))" by (rule_tac zinterval_lneglneg [OF x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos])
   1.649 -then have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2))
   1.650 -\<le> - x1 * x2 \<and>
   1.651 -- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))" by simp
   1.652 -moreover have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) = - max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))" by (simp add: min_max_minus max_min_minus)
   1.653 -moreover have "max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) = - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" by (simp add: min_max_minus max_min_minus)
   1.654 -ultimately have "- max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))\<le> - x1 * x2 \<and>
   1.655 -- x1 * x2 \<le>  - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" by simp
   1.656 -
   1.657 -then have ?thesis by (simp add: min_commute max_commute mult_ac) 
   1.658 -}
   1.659 -
   1.660 -moreover
   1.661 -{
   1.662 - assume u2_neg: "u2 <= 0"
   1.663 - thm zinterval_uneg[OF x2_lu x1_lu u2_neg]
   1.664 -have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.665 -x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" by (rule_tac zinterval_uneg[OF x2_lu x1_lu u2_neg])
   1.666 -then have ?thesis by (simp add: mult_ac min_commute max_commute min_min_commute max_max_commute)
   1.667 -}
   1.668 -ultimately show ?thesis by blast
   1.669 -
   1.670 +      by (rule zinterval_lpos)
   1.671 +    moreover have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) =
   1.672 +      min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))"
   1.673 +      by (simp add: mult_ac min_commute min_min_commute)
   1.674 +    moreover have "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) =
   1.675 +      max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.676 +      by (simp add: mult_ac max_commute max_max_commute)
   1.677 +    ultimately show ?thesis by (simp add: mult_ac)
   1.678 +  next
   1.679 +    assume l2_neg: "l2 < 0" and x2_pos: " 0<= x2"
   1.680 +    from l1_neg have l1_le0: "l1 <= 0" by simp
   1.681 +    from l2_neg have l2_le0: "l2 <= 0" by simp
   1.682 +    from x1_lu x2_lu l1_le0 x1_pos l2_le0 x2_pos
   1.683 +    show ?thesis by (rule zinterval_lneglneg)
   1.684 +  next
   1.685 +    assume x2_neg: "x2 <0" and u2_pos: "0 <= u2"
   1.686 +    from x2_lu have mx2_lu: "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.687 +    from x2_neg have mx2_pos: "0 <= -x2" by simp
   1.688 +    from u2_pos have mu2_neg: "-u2 <= 0" by simp
   1.689 +    from l1_neg have l1_le0: "l1 <= 0" by simp
   1.690 +    from x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos
   1.691 +    have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.692 +      \<le> x1 * - x2 \<and>
   1.693 +      x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))"
   1.694 +      by (rule zinterval_lneglneg)
   1.695 +    then have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2))
   1.696 +      \<le> - x1 * x2 \<and>
   1.697 +      - x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))"
   1.698 +      by simp
   1.699 +    moreover have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) =
   1.700 +      - max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))"
   1.701 +      by (simp add: min_max_minus max_min_minus)
   1.702 +    moreover have "max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) =
   1.703 +      - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))"
   1.704 +      by (simp add: min_max_minus max_min_minus)
   1.705 +    ultimately have "- max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2)) \<le> - x1 * x2 \<and>
   1.706 +      - x1 * x2 \<le>  - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))"
   1.707 +      by simp
   1.708 +    thus ?thesis by (simp add: min_commute max_commute mult_ac) 
   1.709 +  next
   1.710 +    assume u2_neg: "u2 <= 0"
   1.711 +    with x2_lu x1_lu
   1.712 +    have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.713 +      x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))"
   1.714 +      by (rule zinterval_uneg)
   1.715 +    thus ?thesis by (simp add: mult_ac min_commute max_commute min_min_commute max_max_commute)
   1.716 +  qed
   1.717  qed
   1.718  
   1.719  lemma zinterval_xnegupos: 
   1.720 @@ -487,200 +490,167 @@
   1.721    and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.722    and     x1_neg: "x1 <= 0"
   1.723    and     u1_pos: "0<= u1"
   1.724 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.725 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.726    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.727 -proof-
   1.728 +proof -
   1.729    from x1_lu have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith 
   1.730    from u1_pos have mu1_neg : "-u1 <= 0" by simp
   1.731    from x1_neg have mx1_pos : "0 <= -x1" by simp
   1.732 -  thm zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ]
   1.733 +  with mx1_lu x2_lu mu1_neg
   1.734    have "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2))
   1.735 -\<le> - x1 * x2 \<and>
   1.736 -- x1 * x2 \<le> max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))"
   1.737 -    by (rule_tac zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ])
   1.738 -  moreover have 
   1.739 -    "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) = - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" 
   1.740 +    \<le> - x1 * x2 \<and>
   1.741 +    - x1 * x2 \<le> max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))"
   1.742 +    by (rule zinterval_lnegxpos)
   1.743 +  moreover have "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) =
   1.744 +    - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" 
   1.745      by (simp add: min_max_minus max_min_minus)
   1.746 -  moreover have 
   1.747 -    "max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) = - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.748 +  moreover have "max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) =
   1.749 +    - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.750      by (simp add: min_max_minus max_min_minus)
   1.751 -  ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))\<le> - x1 * x2 \<and>
   1.752 -- x1 * x2 \<le> - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.753 +  ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2)) \<le> - x1 * x2 \<and>
   1.754 +    - x1 * x2 \<le> - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.755      by simp
   1.756 -then show ?thesis by (simp add: mult_ac min_commute max_commute)
   1.757 +  then show ?thesis by (simp add: mult_ac min_commute max_commute)
   1.758  qed
   1.759  
   1.760  lemma abs_mul: 
   1.761 -  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.762 -  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.763 -  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.764 +  assumes x1_lu: "l1 <= (x1::int) \<and> x1 <= u1"
   1.765 +  and     x2_lu: "l2 <= (x2::int) \<and> x2 <= u2"
   1.766 +  shows "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.767    \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.768 -proof-
   1.769 +proof -
   1.770    have "(0 <= l1) \<or> (l1 <= 0 \<and> 0<= x1) \<or> (x1 <=0 \<and> 0 <= u1) \<or> (u1 <= 0)" 
   1.771      by arith
   1.772 -  moreover
   1.773 -  {
   1.774 +  thus ?thesis
   1.775 +  proof (elim disjE conjE)
   1.776      assume l1_pos: "0 <= l1"
   1.777 -    have ?thesis by (rule_tac zinterval_lpos [OF x1_lu x2_lu l1_pos])
   1.778 -  }
   1.779 -  
   1.780 -  moreover
   1.781 -  {
   1.782 -    assume l1_neg :"l1 <= 0" and x1_pos: "0<= x1"
   1.783 -    have ?thesis by (rule_tac zinterval_lnegxpos[OF x1_lu x2_lu l1_neg x1_pos])
   1.784 -  }
   1.785 -  
   1.786 -  moreover
   1.787 -  {
   1.788 -    assume x1_neg : "x1 <= 0" and u1_pos: "0 <= u1"
   1.789 -    have ?thesis by (rule_tac zinterval_xnegupos [OF x1_lu x2_lu x1_neg u1_pos])
   1.790 -  }
   1.791 -  
   1.792 -  moreover
   1.793 -  {
   1.794 +    with x1_lu x2_lu show ?thesis by (rule zinterval_lpos)
   1.795 +  next
   1.796 +    assume l1_neg: "l1 <= 0" and x1_pos: "0 <= x1"
   1.797 +    with x1_lu x2_lu show ?thesis by (rule zinterval_lnegxpos)
   1.798 +  next
   1.799 +    assume x1_neg: "x1 <= 0" and u1_pos: "0 <= u1"
   1.800 +    from x1_lu x2_lu x1_neg u1_pos show ?thesis by (rule zinterval_xnegupos)
   1.801 +  next
   1.802      assume u1_neg: "u1 <= 0"
   1.803 -    have ?thesis by (rule_tac zinterval_uneg [OF x1_lu x2_lu u1_neg])
   1.804 -  }
   1.805 -  
   1.806 -  ultimately show ?thesis by blast
   1.807 +    with x1_lu x2_lu show ?thesis by (rule zinterval_uneg)
   1.808 +  qed
   1.809  qed
   1.810  
   1.811  lemma mult_x_mono_lpos : 
   1.812 -assumes l_pos : "0 <= (l::int)"
   1.813 -  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.814 +  assumes l_pos : "0 <= (l::int)"
   1.815 +  and     x_lu : "l <= (x::int) \<and> x <= u"
   1.816    shows "l*l <= x*x \<and> x*x <= u*u"
   1.817 -
   1.818 -proof-
   1.819 +proof -
   1.820    from x_lu have x_l : "l <= x" by arith
   1.821 -  thm zmult_mono[OF l_pos l_pos x_l x_l]
   1.822 -  then have xx_l : "l*l <= x*x"
   1.823 -    by (simp add: zmult_mono[OF l_pos l_pos x_l x_l])
   1.824 +  from l_pos l_pos x_l x_l have xx_l : "l*l <= x*x"
   1.825 +    by (rule zmult_mono)
   1.826    moreover 
   1.827    from x_lu have x_u : "x <= u" by arith
   1.828    from l_pos x_l have x_pos : "0 <= x" by arith
   1.829 -  thm zmult_mono[OF x_pos x_pos x_u x_u]
   1.830 -  then have xx_u : "x*x <= u*u"
   1.831 -    by (simp add: zmult_mono[OF x_pos x_pos x_u x_u])
   1.832 -ultimately show ?thesis by simp
   1.833 +  from x_pos x_pos x_u x_u have xx_u : "x*x <= u*u"
   1.834 +    by (rule zmult_mono)
   1.835 +  ultimately show ?thesis by simp
   1.836  qed
   1.837  
   1.838  lemma mult_x_mono_luneg : 
   1.839 -assumes l_neg : "(l::int) <= 0"
   1.840 -  and   u_neg : "u <= 0"
   1.841 -  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.842 +  assumes l_neg: "(l::int) <= 0"
   1.843 +  and     u_neg: "u <= 0"
   1.844 +  and     x_lu: "l <= (x::int) \<and> x <= u"
   1.845    shows "u*u <= x*x \<and> x*x <= l*l"
   1.846 -
   1.847 -proof-
   1.848 -  from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith
   1.849 -  from u_neg have mu_pos : "0<= -u" by simp
   1.850 -  thm mult_x_mono_lpos[OF mu_pos mx_lu]
   1.851 -  have "- u * - u \<le> - x * - x \<and> - x * - x \<le> - l * - l"
   1.852 -    by (rule_tac mult_x_mono_lpos[OF mu_pos mx_lu])
   1.853 +proof -
   1.854 +  from u_neg have "0<= -u" by simp
   1.855 +  moreover from x_lu have "-u <= -x \<and> -x <= -l" by arith
   1.856 +  ultimately have "- u * - u \<le> - x * - x \<and> - x * - x \<le> - l * - l"
   1.857 +    by (rule mult_x_mono_lpos)
   1.858    then show ?thesis by simp
   1.859  qed
   1.860  
   1.861  lemma mult_x_mono_lxnegupos : 
   1.862 -assumes l_neg : "(l::int) <= 0"
   1.863 -  and   u_pos : "0 <= u"
   1.864 -  and   x_neg : "x <= 0"
   1.865 -  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.866 +  assumes l_neg: "(l::int) <= 0"
   1.867 +  and     u_pos: "0 <= u"
   1.868 +  and     x_neg: "x <= 0"
   1.869 +  and     x_lu: "l <= (x::int) \<and> x <= u"
   1.870    shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)"
   1.871 -proof-
   1.872 -  from x_lu x_neg have mx_0l : "0 <= - x \<and> - x <= - l" by arith
   1.873 -  have trv_0 : "(0::int) <= 0" by arith
   1.874 -  thm mult_x_mono_lpos[OF trv_0 mx_0l]
   1.875 -  have "0 * 0 \<le> - x * - x \<and> - x * - x \<le> - l * - l"
   1.876 -    by (rule_tac  mult_x_mono_lpos[OF trv_0 mx_0l])
   1.877 +proof -
   1.878 +  have "(0::int) <= 0" by arith
   1.879 +  moreover from x_lu x_neg have "0 <= - x \<and> - x <= - l" by arith
   1.880 +  ultimately have "0 * 0 \<le> - x * - x \<and> - x * - x \<le> - l * - l" 
   1.881 +    by (rule mult_x_mono_lpos)
   1.882    then have xx_0ll : "0 <= x*x \<and> x*x <= l*l" by simp
   1.883    have "l*l <= max (l*l) (u*u)" by (simp add: le_maxI1)
   1.884    with xx_0ll show ?thesis by arith
   1.885  qed
   1.886  
   1.887  lemma mult_x_mono_lnegupos : 
   1.888 -assumes l_neg : "(l::int) <= 0"
   1.889 -  and   u_pos : "0 <= u"
   1.890 -  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.891 +  assumes l_neg: "(l::int) <= 0"
   1.892 +  and     u_pos: "0 <= u"
   1.893 +  and     x_lu: "l <= (x::int) \<and> x <= u"
   1.894    shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)"
   1.895 -proof-
   1.896 -  have "0<= x \<or> x <= 0" by arith
   1.897 -moreover
   1.898 -{
   1.899 -  assume x_neg : "x <= 0"
   1.900 -  thm mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu]
   1.901 -  have ?thesis by (rule_tac mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu])
   1.902 -}
   1.903 -moreover
   1.904 +proof -
   1.905 +  have "0 <= x \<or> x <= 0" by arith
   1.906 +  thus ?thesis
   1.907 +  proof
   1.908 +    assume x_neg: "x <= 0"
   1.909 +    from l_neg u_pos x_neg x_lu show ?thesis by (rule mult_x_mono_lxnegupos)
   1.910 +  next
   1.911 +    assume x_pos: "0 <= x"
   1.912 +    from x_lu have mx_lu: "-u <= -x \<and> -x <= -l" by arith
   1.913 +    from x_pos have mx_neg: "-x <= 0" by simp
   1.914 +    from u_pos have mu_neg: "-u <= 0" by simp
   1.915 +    from x_lu x_pos have ml_pos: "0 <= -l" by simp
   1.916 +    from mu_neg ml_pos mx_neg mx_lu
   1.917 +    have "0 \<le> - x * - x \<and> - x * - x \<le> max (- u * - u) (- l * - l)"
   1.918 +      by (rule mult_x_mono_lxnegupos)
   1.919 +    thus ?thesis by (simp add: max_commute)
   1.920 +  qed
   1.921 +qed
   1.922  
   1.923 -{
   1.924 -  assume x_pos : "0 <= x"
   1.925 -  from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith
   1.926 -  from x_pos have mx_neg : "-x <= 0" by simp
   1.927 -  from u_pos have mu_neg : "-u <= 0" by simp
   1.928 -  from x_lu x_pos have ml_pos : "0 <= -l" by simp
   1.929 -  thm mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu]
   1.930 -  have "0 \<le> - x * - x \<and> - x * - x \<le> max (- u * - u) (- l * - l)"
   1.931 -    by (rule_tac mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu])
   1.932 -  then have ?thesis by (simp add: max_commute)
   1.933 -
   1.934 -}
   1.935 -ultimately show ?thesis by blast
   1.936 -
   1.937 -qed
   1.938  lemma abs_mul_x:
   1.939 -  assumes x_lu : "l <= (x::int) \<and> x <= u"
   1.940 -  shows 
   1.941 +  assumes x_lu: "l <= (x::int) \<and> x <= u"
   1.942 +  shows
   1.943    "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) <= x*x
   1.944    \<and> x*x <= (if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u)))"
   1.945 -proof-
   1.946 +proof -
   1.947    have "(0 <= l) \<or> (l < 0 \<and> u <= 0) \<or> (l < 0 \<and> 0 < u)" by arith 
   1.948 -  
   1.949 -  moreover
   1.950 -  {
   1.951 -    assume l_pos : "0 <= l"
   1.952 +  thus ?thesis
   1.953 +  proof (elim disjE conjE)
   1.954 +    assume l_pos: "0 <= l"
   1.955      from l_pos have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = l*l"
   1.956        by simp
   1.957 -    moreover from l_pos have "(if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u))) = u*u" by simp
   1.958 -    
   1.959 -    moreover have "l * l \<le> x * x \<and> x * x \<le> u * u" 
   1.960 -      by (rule_tac  mult_x_mono_lpos[OF l_pos x_lu])
   1.961 -    ultimately have ?thesis by simp 
   1.962 -  }
   1.963 -  
   1.964 -  moreover
   1.965 -  {
   1.966 -    assume l_neg : "l < 0"  and u_neg : "u <= 0"  
   1.967 -    from l_neg have l_le0 : "l <= 0" by simp
   1.968 +    moreover from l_pos have "(if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u))) = u*u"
   1.969 +      by simp
   1.970 +    moreover from l_pos x_lu have "l * l \<le> x * x \<and> x * x \<le> u * u" 
   1.971 +      by (rule mult_x_mono_lpos)
   1.972 +    ultimately show ?thesis by simp 
   1.973 +  next
   1.974 +    assume l_neg: "l < 0" and u_neg: "u <= 0"  
   1.975 +    from l_neg have l_le0: "l <= 0" by simp
   1.976      from l_neg u_neg have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = u*u"
   1.977        by simp
   1.978 -    moreover 
   1.979 -    from l_neg u_neg have "(if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u))) = l*l" by simp
   1.980 -    moreover 
   1.981 +    moreover
   1.982 +    from l_neg u_neg have "(if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u))) = l*l"
   1.983 +      by simp
   1.984 +    moreover from l_le0 u_neg x_lu
   1.985      have "u * u \<le> x * x \<and> x * x \<le> l * l" 
   1.986 -      by (rule_tac mult_x_mono_luneg[OF l_le0 u_neg x_lu])
   1.987 -    
   1.988 -    ultimately have ?thesis by simp 
   1.989 -  }
   1.990 -  moreover
   1.991 -  {
   1.992 -    assume l_neg : "l < 0" and u_pos: "0 < u"
   1.993 -    from l_neg have l_le0 : "l <= 0" by simp
   1.994 -    from u_pos have u_ge0 : "0 <= u" by simp
   1.995 +      by (rule mult_x_mono_luneg)
   1.996 +    ultimately show ?thesis by simp
   1.997 +  next
   1.998 +    assume l_neg: "l < 0" and u_pos: "0 < u"
   1.999 +    from l_neg have l_le0: "l <= 0" by simp
  1.1000 +    from u_pos have u_ge0: "0 <= u" by simp
  1.1001      from l_neg u_pos have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = 0"
  1.1002        by simp
  1.1003 -    moreover from l_neg u_pos have "(if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u))) = max (l*l) (u*u)" by simp
  1.1004 -    moreover have "0 \<le> x * x \<and> x * x \<le> max (l * l) (u * u)" 
  1.1005 -      by (rule_tac mult_x_mono_lnegupos[OF l_le0 u_ge0 x_lu])
  1.1006 -    
  1.1007 -    ultimately have ?thesis by simp 
  1.1008 -    
  1.1009 -  }
  1.1010 -  
  1.1011 -  ultimately show ?thesis by blast
  1.1012 +    moreover from l_neg u_pos have "(if 0 <= l then u*u else
  1.1013 +      if u <= 0 then l*l else (max (l*l) (u*u))) = max (l*l) (u*u)" by simp
  1.1014 +    moreover from l_le0 u_ge0 x_lu have "0 \<le> x * x \<and> x * x \<le> max (l * l) (u * u)" 
  1.1015 +      by (rule mult_x_mono_lnegupos)
  1.1016 +    ultimately show ?thesis by simp 
  1.1017 +  qed
  1.1018  qed
  1.1019  
  1.1020  
  1.1021 -use"barith.ML"
  1.1022 +use "barith.ML"
  1.1023  setup Barith.setup
  1.1024  
  1.1025  end
  1.1026 -