a very simple decision procedure for a fragment of bounded arithmetic
authorchaieb
Wed Oct 06 13:58:56 2004 +0200 (2004-10-06)
changeset 15232388a6f431d83
parent 15231 96d5b6e2b6e4
child 15233 c55a12162944
a very simple decision procedure for a fragment of bounded arithmetic
src/HOL/Integ/Barith.thy
src/HOL/Integ/barith.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/Barith.thy	Wed Oct 06 13:58:56 2004 +0200
     1.3 @@ -0,0 +1,686 @@
     1.4 +theory Barith = Presburger
     1.5 +files ("barith.ML") :
     1.6 +
     1.7 +lemma imp_commute: "(PROP P ==> PROP Q
     1.8 +==> PROP R) == (PROP Q ==>
     1.9 +PROP P ==> PROP R)"
    1.10 +proof
    1.11 +  assume h1: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow>
    1.12 +PROP R"
    1.13 +  assume h2: "PROP Q"
    1.14 +  assume h3: "PROP P"
    1.15 +  from h3 h2 show "PROP R" by (rule h1)
    1.16 +next
    1.17 +  assume h1: "PROP Q \<Longrightarrow> PROP P \<Longrightarrow>
    1.18 +PROP R"
    1.19 + assume h2: "PROP P"
    1.20 +  assume h3: "PROP Q"
    1.21 +  from h3 h2 show "PROP R" by (rule h1)
    1.22 +qed
    1.23 +
    1.24 +lemma imp_simplify: "(PROP P \<Longrightarrow> PROP P
    1.25 +\<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow>
    1.26 +PROP Q)"
    1.27 +proof
    1.28 +  assume h1: "PROP P \<Longrightarrow> PROP P \<Longrightarrow>
    1.29 +PROP Q"
    1.30 +  assume h2: "PROP P"
    1.31 +  from h2 h2 show "PROP Q" by (rule h1)
    1.32 +next
    1.33 +  assume h: "PROP P \<Longrightarrow> PROP Q"
    1.34 +  assume "PROP P"
    1.35 +  then show "PROP Q" by (rule h)
    1.36 +qed
    1.37 +
    1.38 +
    1.39 +(* Abstraction of constants *)
    1.40 +lemma abs_const: "(x::int) <= x \<and> x <= x"
    1.41 +by simp
    1.42 +
    1.43 +(* Abstraction of Variables *)
    1.44 +lemma abs_var: "l <= (x::int) \<and> x <= u \<Longrightarrow> l <= (x::int) \<and> x <= u"
    1.45 +by simp
    1.46 +
    1.47 +
    1.48 +(* Unary operators *)
    1.49 +lemma abs_neg: "l <= (x::int) \<and> x <= u \<Longrightarrow>  -u <= -x \<and> -x <= -l"
    1.50 +by arith
    1.51 +
    1.52 +
    1.53 +(* Binary operations *)
    1.54 +(* Addition*)
    1.55 +lemma abs_add: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> 
    1.56 +  \<Longrightarrow>  l1 + l2 <= x1 + x2 \<and> x1 + x2 <= u1 + u2"
    1.57 +by arith
    1.58 +
    1.59 +lemma abs_sub: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> 
    1.60 +  \<Longrightarrow>  l1 - u2 <= x1 - x2 \<and> x1 - x2 <= u1 - l2"
    1.61 +by arith
    1.62 +
    1.63 +lemma abs_sub_x: "l <= (x::int) \<and> x <= u \<Longrightarrow> 0 <= x - x \<and> x - x <= 0"
    1.64 +by arith
    1.65 +
    1.66 +(* For resolving the last step*)
    1.67 +lemma subinterval: "\<lbrakk>l <= (e::int) \<and> e <= u ; l' <= l ; u <= u' \<rbrakk>
    1.68 +  \<Longrightarrow> l' <= e \<and> e <= u'"
    1.69 +by arith
    1.70 +
    1.71 +lemma min_max_minus : "min (-a ::int) (-b) = - max a b"
    1.72 +by arith
    1.73 +
    1.74 +lemma max_min_minus : " max (-a ::int) (-b) = - min a b"
    1.75 +by arith
    1.76 +
    1.77 +lemma max_max_commute : "max (max (a::int) b) (max c d) = max (max a c) (max b d)"
    1.78 +by arith
    1.79 +
    1.80 +lemma min_min_commute : "min (min (a::int) b) (min c d) = min (min a c) (min b d)"
    1.81 +by arith
    1.82 +
    1.83 +lemma zintervals_min: "\<lbrakk> l1 <= (x1::int) \<and> x1<= u1 ; l2 <= x2 \<and> x2 <= u2 \<rbrakk> 
    1.84 +  \<Longrightarrow> min l1 l2 <= x1 \<and> x1 <= max u1 u2" by arith
    1.85 +
    1.86 +lemma zmult_zle_mono: "(i::int) \<le> j \<Longrightarrow> 0 \<le> k \<Longrightarrow> k * i \<le> k * j"
    1.87 +  apply (erule order_le_less [THEN iffD1, THEN disjE, of "0::int"])
    1.88 +  apply (erule order_le_less [THEN iffD1, THEN disjE])
    1.89 +  apply (rule order_less_imp_le)
    1.90 +  apply (rule zmult_zless_mono2)
    1.91 +  apply simp_all
    1.92 +  done
    1.93 +  
    1.94 +lemma zmult_mono:
    1.95 +  assumes l1_pos : "0 <= l1"
    1.96 +  and l2_pos : "0 <= l2"
    1.97 +  and l1_le : "l1 <= (x1::int)"
    1.98 +  and l2_le : "l2 <= (x2::int)"
    1.99 +  shows "l1*l2 <= x1*x2"
   1.100 +proof -
   1.101 +  from l1_pos and l1_le have x1_pos: "0 \<le> x1" by (rule order_trans)
   1.102 +  from l1_le and l2_pos
   1.103 +  have "l2 * l1 \<le> l2 * x1" by (rule zmult_zle_mono)
   1.104 +  then have "l1 * l2 \<le> x1 * l2" by (simp add: mult_ac)
   1.105 +  also from l2_le and x1_pos
   1.106 +  have "x1 * l2 \<le> x1 * x2" by (rule zmult_zle_mono)
   1.107 +  finally show ?thesis .
   1.108 +qed
   1.109 +
   1.110 +lemma zinterval_lposlpos:
   1.111 +  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.112 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.113 +  and     l1_pos : "0 <= l1"
   1.114 +  and     l2_pos : "0 <= l2"
   1.115 +  shows conc : "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 +  from x1_lu have l1_le : "l1 <= x1" by simp
   1.119 +  from x1_lu have x1_le : "x1 <= u1" by simp
   1.120 +  from x2_lu have l2_le : "l2 <= x2" by simp
   1.121 +  from x2_lu have x2_le : "x2 <= u2" by simp
   1.122 +  from x1_lu have l1_leu : "l1 <= u1" by arith
   1.123 +  from x2_lu have l2_leu : "l2 <= u2" by arith
   1.124 +  from l1_pos l2_pos l1_le l2_le 
   1.125 +  have l1l2_le : "l1*l2 <= x1*x2" by (simp add: zmult_mono)
   1.126 +  from l1_pos x1_lu have x1_pos : "0 <= x1" by arith
   1.127 +  from l2_pos x2_lu have x2_pos : "0 <= x2" by arith
   1.128 +  from l1_pos x1_lu have u1_pos : "0 <= u1" by arith
   1.129 +  from l2_pos x2_lu have u2_pos : "0 <= u2" by arith
   1.130 +  from x1_pos x2_pos x1_le x2_le 
   1.131 +  have x1x2_le : "x1*x2 <= u1*u2" by (simp add: zmult_mono)
   1.132 +  from l2_leu l1_pos have l1l2_leu2 : "l1*l2 <= l1*u2" 
   1.133 +    by (simp add: zmult_zle_mono)
   1.134 +  from l1l2_leu2 have min1 : "l1*l2 = min (l1*l2) (l1*u2)" by arith
   1.135 +  from l2_leu u1_pos have u1l2_le : "u1*l2 <=u1*u2" by (simp add: zmult_zle_mono)
   1.136 +  from u1l2_le have min2 : "u1*l2 = min (u1*l2) (u1*u2)" by arith
   1.137 +  from l1_leu l2_pos have "l2*l1 <= l2*u1" by (simp add:zmult_zle_mono) 
   1.138 +  then have l1l2_le_u1l2 : "l1*l2 <= u1*l2" by (simp add: mult_ac)
   1.139 +  from min1 min2 l1l2_le_u1l2 have  min_th : 
   1.140 +    "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) = (l1*l2)" by arith
   1.141 +  from l1l2_leu2 have max1 : "l1*u2 = max (l1*l2) (l1*u2)" by arith
   1.142 +  from u1l2_le have max2 : "u1*u2 = max (u1*l2) (u1*u2)" by arith
   1.143 +  from l1_leu u2_pos have "u2*l1 <= u2*u1" by (simp add:zmult_zle_mono) 
   1.144 +  then have l1u2_le_u1u2 : "l1*u2 <= u1*u2" by (simp add: mult_ac)
   1.145 +  from max1 max2 l1u2_le_u1u2 have  max_th : 
   1.146 +    "max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2)) = (u1*u2)" by arith
   1.147 +  from min_th have min_th' :  "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= l1*l2" by arith
   1.148 +  from max_th have max_th' : "u1*u2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" by arith
   1.149 +  from min_th' max_th' l1l2_le x1x2_le 
   1.150 +  show ?thesis by simp
   1.151 +qed
   1.152 +
   1.153 +lemma min_le_I1 : "min (a::int) b <= a" by arith
   1.154 +lemma min_le_I2 : "min (a::int) b <= b" by arith
   1.155 +lemma zinterval_lneglpos :
   1.156 +  assumes  x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.157 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.158 +  and     l1_neg : "l1 <= 0"
   1.159 +  and x1_pos : "0 <= x1" 
   1.160 +  and     l2_pos : "0 <= l2"
   1.161 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.162 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.163 +
   1.164 +proof-
   1.165 +    from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp
   1.166 +    from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.167 +    from x1_lu x1_pos have u1_pos : "0 <= u1" by arith
   1.168 +    from x2_lu l2_pos have u2_pos : "0 <= u2" by arith
   1.169 +    from x2_lu have l2_le_u2 : "l2 <= u2" by arith
   1.170 +    from l2_le_u2 u1_pos 
   1.171 +     have u1l2_le_u1u2 : "u1*l2 <= u1*u2" by (simp add: zmult_zle_mono)
   1.172 +    have trv_0 : "(0::int) <= 0" by simp
   1.173 +    have "0*0 <= u1*l2" 
   1.174 +      by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos l2_pos])
   1.175 +    then have u1l2_pos : "0 <= u1*l2" by simp
   1.176 +      from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.177 +      from ml1_pos l2_pos have "0*0 <= (-l1)*l2" 
   1.178 +	by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos l2_pos])
   1.179 +      then have "0 <= -(l1*l2)" by simp  
   1.180 +      then have "0 - (-(l1*l2)) <= 0" by arith 
   1.181 +      then
   1.182 +      have l1l2_neg : "l1*l2 <= 0" by simp
   1.183 +      from ml1_pos u2_pos have "0*0 <= (-l1)*u2" 
   1.184 +	by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos])
   1.185 +      then have "0 <= -(l1*u2)" by simp  
   1.186 +      then have "0 - (-(l1*u2)) <= 0" by arith 
   1.187 +      then
   1.188 +      have l1u2_neg : "l1*u2 <= 0" by simp
   1.189 +      from l1l2_neg u1l2_pos have l1l2_le_u1l2: "l1*l2 <= u1*l2" by simp
   1.190 +      from l1u2_neg u1l2_pos have l1u2_le_u1l2 : "l1*u2 <= u1*l2" by simp
   1.191 +      from ml1_pos l2_le_u2 have "(-l1)*l2 <= (-l1)*u2"
   1.192 +	by (simp only: zmult_zle_mono) 
   1.193 +      then have l1u2_le_l1l2 : "l1*u2 <= l1*l2" by simp
   1.194 +      from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.195 +      have min1 : "l1*u2 = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" 
   1.196 +	by arith
   1.197 +      from u1l2_pos u1l2_le_u1u2 have "0 = min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by arith
   1.198 +      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.199 +      from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 
   1.200 +      have max1 : "u1*u2 = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" 
   1.201 +	by arith
   1.202 +      from u1l2_pos u1l2_le_u1u2 have "u1*u2 = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by arith 
   1.203 +      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.204 +      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.205 +    have x1x2_0_u : "min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2)) <= x1 * x2 &
   1.206 +x1 * x2 <= max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.207 +      by (simp only: zinterval_lposlpos[OF x1_0_u1 x2_lu trv_0 l2_pos],simp)
   1.208 +      from minth maxth x1x2_0_u show ?thesis by (simp add: subinterval[OF _ minth maxth])
   1.209 +qed
   1.210 +
   1.211 +lemma zinterval_lneglneg :
   1.212 +  assumes  x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.213 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.214 +  and     l1_neg : "l1 <= 0"
   1.215 +  and     x1_pos : "0 <= x1" 
   1.216 +  and     l2_neg : "l2 <= 0"
   1.217 +  and     x2_pos : "0 <= x2"
   1.218 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.219 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.220 +
   1.221 +proof-
   1.222 +    from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp
   1.223 +    from l1_neg have ml1_pos : "0 <= -l1" by simp
   1.224 +    from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.225 +    from x1_lu x1_pos have u1_pos : "0 <= u1" by arith
   1.226 +    from x2_lu x2_pos have x2_0_u2 : "0 <= x2 \<and> x2 <= u2" by simp
   1.227 +    from l2_neg have ml2_pos : "0 <= -l2" by simp
   1.228 +    from l2_neg have l2_le0 : "l2 <= 0" by simp
   1.229 +    from x2_lu x2_pos have u2_pos : "0 <= u2" by arith
   1.230 +    have trv_0 : "(0::int) <= 0" by simp
   1.231 +
   1.232 +    have x1x2_th1 : 
   1.233 +      "min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)) \<le> x1 * x2 \<and>
   1.234 +      x1 * x2 \<le> max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))"
   1.235 +      by (rule_tac  zinterval_lneglpos[OF x1_lu x2_0_u2 l1_le0 x1_pos trv_0])
   1.236 +    
   1.237 +    have x1x2_eq_x2x1 : "x1*x2 = x2*x1" by (simp add: mult_ac)
   1.238 +    have
   1.239 +      "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x2 * x1 \<and>
   1.240 +      x2 * x1 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.241 +      by (rule_tac  zinterval_lneglpos[OF x2_lu x1_0_u1 l2_le0 x2_pos trv_0])
   1.242 +    
   1.243 +    then have x1x2_th2 : 
   1.244 +      "min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x1 * x2 \<and>
   1.245 +      x1 * x2 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))"
   1.246 +      by (simp add: x1x2_eq_x2x1)
   1.247 +
   1.248 +    from x1x2_th1 x1x2_th2 have x1x2_th3:
   1.249 +      "min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.250 +      (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))
   1.251 +      \<le> x1 * x2 \<and>
   1.252 +      x1 * x2
   1.253 +      \<le> max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.254 +      (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1)))"
   1.255 +      by (rule_tac zintervals_min[OF x1x2_th1 x1x2_th2])
   1.256 +
   1.257 +    from ml1_pos u2_pos 
   1.258 +    have "0*0 <= -l1*u2" 
   1.259 +      by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos]) 
   1.260 +    then have l1u2_neg : "l1*u2 <= 0" by simp
   1.261 +    from l1u2_neg have min_l1u2_0 : "min (0) (l1*u2) = l1*u2" by arith
   1.262 +    from l1u2_neg have max_l1u2_0 : "max (0) (l1*u2) = 0" by arith
   1.263 +    from u1_pos u2_pos 
   1.264 +    have "0*0 <= u1*u2" 
   1.265 +      by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos u2_pos]) 
   1.266 +    then have u1u2_pos :"0 <= u1*u2" by simp
   1.267 +    from u1u2_pos have min_0_u1u2 : "min 0 (u1*u2) = 0" by arith
   1.268 +    from u1u2_pos have max_0_u1u2 : "max 0 (u1*u2) = u1*u2" by arith
   1.269 +    from ml2_pos u1_pos have "0*0 <= -l2*u1" 
   1.270 +      by (simp only: zmult_mono[OF trv_0 trv_0 ml2_pos u1_pos]) 
   1.271 +    then have l2u1_neg : "l2*u1 <= 0" by simp
   1.272 +    from l2u1_neg have min_l2u1_0 : "min 0 (l2*u1) = l2*u1" by arith
   1.273 +    from l2u1_neg have max_l2u1_0 : "max 0 (l2*u1) = 0" by arith
   1.274 +    from min_l1u2_0 min_0_u1u2 min_l2u1_0 
   1.275 +    have min_th1: 
   1.276 +      " min (l2*u1) (l1*u2) <= min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)))
   1.277 +      (min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))"
   1.278 +      by (simp add: min_commute mult_ac)
   1.279 +    from max_l1u2_0 max_0_u1u2 max_l2u1_0 
   1.280 +    have max_th1: "max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2)))
   1.281 +      (max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))) <= u1*u2"
   1.282 +      by (simp add: max_commute mult_ac)
   1.283 +    have x1x2_th4: "min (l2*u1) (l1*u2) <= x1*x2 \<and> x1*x2 <= u1*u2" 
   1.284 +      by (rule_tac subinterval[OF x1x2_th3 min_th1 max_th1])
   1.285 +    
   1.286 +    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.287 +    moreover 
   1.288 +    have " min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1)) <= min (l1*u2) (l2*u1)" 
   1.289 +      by 
   1.290 +    (rule_tac min_le_I2 [of "(min (l1*l2) (u1*u2))" "(min (l1*u2) (l2*u1))"]) 
   1.291 +    ultimately have "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (l1*u2) (l2*u1)" by simp 
   1.292 +    then 
   1.293 +    have min_le1: "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <=min (l2*u1) (l1*u2)" 
   1.294 +      by (simp add: min_commute mult_ac)
   1.295 +    have "u1*u2 <= max (u1*l2) (u1*u2)" 
   1.296 +      by (rule_tac le_maxI2[of  "u1*u2" "u1*l2"]) 
   1.297 +    
   1.298 +    moreover have "max (u1*l2) (u1*u2) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.299 +      by(rule_tac le_maxI2[of "(max (u1*l2) (u1*u2))" "(max (l1*l2) (l1*u2))"])
   1.300 +    then 
   1.301 +    have max_le1:"u1*u2 <= max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" 
   1.302 +      by simp
   1.303 +    show ?thesis by (simp add: subinterval[OF x1x2_th4 min_le1 max_le1])
   1.304 +  qed
   1.305 +
   1.306 +lemma zinterval_lpos:
   1.307 +  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.308 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.309 +  and     l1_pos: "0 <= l1"
   1.310 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.311 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.312 +proof-
   1.313 +  from x1_lu have l1_le : "l1 <= x1" by simp
   1.314 +  from x1_lu have x1_le : "x1 <= u1" by simp
   1.315 +  from x2_lu have l2_le : "l2 <= x2" by simp
   1.316 +  from x2_lu have x2_le : "x2 <= u2" by simp
   1.317 +  from x1_lu have l1_leu : "l1 <= u1" by arith
   1.318 +  from x2_lu have l2_leu : "l2 <= u2" by arith
   1.319 +  have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <0)" by arith
   1.320 +  moreover
   1.321 +  {
   1.322 +    assume l2_pos: "0 <= l2"
   1.323 +    have ?thesis by (simp add: zinterval_lposlpos[OF x1_lu x2_lu l1_pos l2_pos])
   1.324 +  }
   1.325 +moreover
   1.326 +{
   1.327 +  assume  l2_neg : "l2 < 0" and x2_pos: "0<= x2"
   1.328 +  from l2_neg have l2_le_0 : "l2 <= 0" by arith
   1.329 +  thm zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos]
   1.330 +have th1 : 
   1.331 +  "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.332 +  x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" 
   1.333 +  by (simp add : zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos])
   1.334 +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.335 +  by (simp add: min_min_commute mult_ac)
   1.336 +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.337 +  by (simp add: max_max_commute mult_ac)
   1.338 +have x1x2_th : "x2*x1 = x1*x2" by (simp add: mult_ac)
   1.339 +from th1 mth1 mth2 x1x2_th have 
   1.340 +   "min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2)) \<le> x1 * x2 \<and>
   1.341 +   x1 * x2 \<le> max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))"
   1.342 +by auto
   1.343 +    then have ?thesis by simp 
   1.344 +}
   1.345 +moreover
   1.346 +{
   1.347 +  assume x2_neg : "x2 <0" and u2_pos : "0 <= u2"
   1.348 +  from x2_lu x2_neg have mx2_mu2_ml2 : "-u2 <= -x2 \<and> -x2 <= -l2" by simp
   1.349 +  from u2_pos have mu2_neg : "-u2 <= 0" by simp
   1.350 +  from x2_neg have mx2_pos : "0 <= -x2" by simp
   1.351 +thm zinterval_lneglpos[OF mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos]
   1.352 +    have mx1x2_lu : 
   1.353 +"min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1))
   1.354 +\<le> - x2 * x1 \<and>
   1.355 +- x2 * x1 \<le> max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1))"      
   1.356 +      by (simp only: zinterval_lneglpos [OF  mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos],simp)
   1.357 +    have min_eq_mmax : 
   1.358 +      "min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1)) = 
   1.359 +      - max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))" 
   1.360 +      by (simp add: min_max_minus max_min_minus)
   1.361 +    have max_eq_mmin : 
   1.362 +      " max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1)) = 
   1.363 +      -min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))"
   1.364 +      by (simp add: min_max_minus max_min_minus)
   1.365 +    from mx1x2_lu min_eq_mmax max_eq_mmin 
   1.366 +    have "- max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))<= - x1 * x2 &
   1.367 +      - x1*x2 <=  -min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))" by (simp add: mult_ac)
   1.368 + then have ?thesis by (simp add: min_min_commute min_commute max_commute max_max_commute mult_ac) 
   1.369 +
   1.370 +}
   1.371 +moreover
   1.372 +{
   1.373 +  assume u2_neg : "u2 < 0"
   1.374 +  from x2_lu have mx2_lu : "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.375 +  from u2_neg have mu2_pos : "0 <= -u2" by arith
   1.376 +thm zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos]
   1.377 +have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.378 +\<le> x1 * - x2 \<and>
   1.379 +x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))
   1.380 +  " by (rule_tac zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos])
   1.381 +then have mx1x2_lu:
   1.382 +  "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) \<le> - x1 * x2 \<and>
   1.383 +- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))
   1.384 +  " by simp
   1.385 +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.386 +  by (simp add: min_max_minus max_min_minus)
   1.387 +moreover 
   1.388 +have 
   1.389 +"max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) = - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))"
   1.390 + by (simp add: min_max_minus max_min_minus)
   1.391 +thm subinterval[OF mx1x2_lu]
   1.392 +ultimately have "- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2))\<le> - x1 * x2 \<and>
   1.393 +- x1 * x2 \<le> - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2)) " by simp
   1.394 + then have ?thesis by (simp add: max_commute min_commute)
   1.395 +}
   1.396 +ultimately show ?thesis by blast
   1.397 +qed
   1.398 +
   1.399 +lemma zinterval_uneg :
   1.400 +assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.401 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.402 +  and     u1_neg: "u1 <= 0"
   1.403 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.404 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.405 +proof-
   1.406 +  from x1_lu  have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith
   1.407 +  from u1_neg have mu1_pos : "0 <= -u1" by arith
   1.408 +  thm zinterval_lpos [OF mx1_lu x2_lu mu1_pos]
   1.409 +  have mx1x2_lu : 
   1.410 +    "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2))
   1.411 +    \<le> - x1 * x2 \<and> - x1 * x2 \<le> 
   1.412 +    max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))"
   1.413 +by (rule_tac zinterval_lpos [OF mx1_lu x2_lu mu1_pos])
   1.414 +moreover have 
   1.415 +  "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.416 +moreover have 
   1.417 +  "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.418 +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.419 +then show ?thesis by (simp add: min_commute max_commute mult_ac)
   1.420 +qed
   1.421 +
   1.422 +lemma zinterval_lnegxpos:
   1.423 +assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.424 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.425 +  and     l1_neg: "l1 <= 0"
   1.426 +  and     x1_pos: "0<= x1"
   1.427 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.428 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.429 +proof-
   1.430 +  have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <= 0)" by arith
   1.431 +  moreover
   1.432 +  {
   1.433 +    assume l2_pos: "0 <= l2"
   1.434 +    thm zinterval_lpos [OF x2_lu x1_lu l2_pos]
   1.435 +    have 
   1.436 +      "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.437 +      x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))"
   1.438 +      by (rule_tac zinterval_lpos [OF x2_lu x1_lu l2_pos])
   1.439 + 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.440 +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.441 +  by (simp add: mult_ac max_commute max_max_commute)
   1.442 +ultimately have ?thesis by (simp add: mult_ac)
   1.443 +
   1.444 +}
   1.445 +
   1.446 +moreover
   1.447 +{
   1.448 +  assume l2_neg: "l2 < 0" and x2_pos: " 0<= x2"
   1.449 +  from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.450 +  from l2_neg have l2_le0 : "l2 <= 0" by simp
   1.451 + have ?thesis by (simp add: zinterval_lneglneg [OF x1_lu x2_lu l1_le0 x1_pos l2_le0 x2_pos])
   1.452 +}
   1.453 +
   1.454 +moreover
   1.455 +{
   1.456 + assume x2_neg: "x2 <0" and u2_pos: "0 <= u2"
   1.457 + from x2_lu have mx2_lu: "-u2 <= -x2 \<and> -x2 <= -l2" by arith
   1.458 + from x2_neg have mx2_pos: "0 <= -x2" by simp
   1.459 + from u2_pos have mu2_neg: "-u2 <= 0" by simp
   1.460 + from l1_neg have l1_le0 : "l1 <= 0" by simp
   1.461 +thm zinterval_lneglneg [OF x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos]
   1.462 +have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2))
   1.463 +\<le> x1 * - x2 \<and>
   1.464 +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.465 +then have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2))
   1.466 +\<le> - x1 * x2 \<and>
   1.467 +- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))" by simp
   1.468 +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.469 +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.470 +ultimately have "- max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))\<le> - x1 * x2 \<and>
   1.471 +- x1 * x2 \<le>  - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" by simp
   1.472 +
   1.473 +then have ?thesis by (simp add: min_commute max_commute mult_ac) 
   1.474 +}
   1.475 +
   1.476 +moreover
   1.477 +{
   1.478 + assume u2_neg: "u2 <= 0"
   1.479 + thm zinterval_uneg[OF x2_lu x1_lu u2_neg]
   1.480 +have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and>
   1.481 +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.482 +then have ?thesis by (simp add: mult_ac min_commute max_commute min_min_commute max_max_commute)
   1.483 +}
   1.484 +ultimately show ?thesis by blast
   1.485 +
   1.486 +qed
   1.487 +
   1.488 +lemma zinterval_xnegupos: 
   1.489 +assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.490 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.491 +  and     x1_neg: "x1 <= 0"
   1.492 +  and     u1_pos: "0<= u1"
   1.493 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.494 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.495 +proof-
   1.496 +  from x1_lu have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith 
   1.497 +  from u1_pos have mu1_neg : "-u1 <= 0" by simp
   1.498 +  from x1_neg have mx1_pos : "0 <= -x1" by simp
   1.499 +  thm zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ]
   1.500 +  have "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2))
   1.501 +\<le> - x1 * x2 \<and>
   1.502 +- x1 * x2 \<le> max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))"
   1.503 +    by (rule_tac zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ])
   1.504 +  moreover have 
   1.505 +    "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) = - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" 
   1.506 +    by (simp add: min_max_minus max_min_minus)
   1.507 +  moreover have 
   1.508 +    "max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) = - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.509 +    by (simp add: min_max_minus max_min_minus)
   1.510 +  ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))\<le> - x1 * x2 \<and>
   1.511 +- x1 * x2 \<le> - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" 
   1.512 +    by simp
   1.513 +then show ?thesis by (simp add: mult_ac min_commute max_commute)
   1.514 +qed
   1.515 +
   1.516 +lemma abs_mul: 
   1.517 +  assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1"
   1.518 +  and     x2_lu : "l2 <= (x2::int) \<and> x2 <= u2"
   1.519 +  shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 
   1.520 +  \<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))"
   1.521 +proof-
   1.522 +  have "(0 <= l1) \<or> (l1 <= 0 \<and> 0<= x1) \<or> (x1 <=0 \<and> 0 <= u1) \<or> (u1 <= 0)" 
   1.523 +    by arith
   1.524 +  moreover
   1.525 +  {
   1.526 +    assume l1_pos: "0 <= l1"
   1.527 +    have ?thesis by (rule_tac zinterval_lpos [OF x1_lu x2_lu l1_pos])
   1.528 +  }
   1.529 +  
   1.530 +  moreover
   1.531 +  {
   1.532 +    assume l1_neg :"l1 <= 0" and x1_pos: "0<= x1"
   1.533 +    have ?thesis by (rule_tac zinterval_lnegxpos[OF x1_lu x2_lu l1_neg x1_pos])
   1.534 +  }
   1.535 +  
   1.536 +  moreover
   1.537 +  {
   1.538 +    assume x1_neg : "x1 <= 0" and u1_pos: "0 <= u1"
   1.539 +    have ?thesis by (rule_tac zinterval_xnegupos [OF x1_lu x2_lu x1_neg u1_pos])
   1.540 +  }
   1.541 +  
   1.542 +  moreover
   1.543 +  {
   1.544 +    assume u1_neg: "u1 <= 0"
   1.545 +    have ?thesis by (rule_tac zinterval_uneg [OF x1_lu x2_lu u1_neg])
   1.546 +  }
   1.547 +  
   1.548 +  ultimately show ?thesis by blast
   1.549 +qed
   1.550 +
   1.551 +lemma mult_x_mono_lpos : 
   1.552 +assumes l_pos : "0 <= (l::int)"
   1.553 +  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.554 +  shows "l*l <= x*x \<and> x*x <= u*u"
   1.555 +
   1.556 +proof-
   1.557 +  from x_lu have x_l : "l <= x" by arith
   1.558 +  thm zmult_mono[OF l_pos l_pos x_l x_l]
   1.559 +  then have xx_l : "l*l <= x*x"
   1.560 +    by (simp add: zmult_mono[OF l_pos l_pos x_l x_l])
   1.561 +  moreover 
   1.562 +  from x_lu have x_u : "x <= u" by arith
   1.563 +  from l_pos x_l have x_pos : "0 <= x" by arith
   1.564 +  thm zmult_mono[OF x_pos x_pos x_u x_u]
   1.565 +  then have xx_u : "x*x <= u*u"
   1.566 +    by (simp add: zmult_mono[OF x_pos x_pos x_u x_u])
   1.567 +ultimately show ?thesis by simp
   1.568 +qed
   1.569 +
   1.570 +lemma mult_x_mono_luneg : 
   1.571 +assumes l_neg : "(l::int) <= 0"
   1.572 +  and   u_neg : "u <= 0"
   1.573 +  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.574 +  shows "u*u <= x*x \<and> x*x <= l*l"
   1.575 +
   1.576 +proof-
   1.577 +  from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith
   1.578 +  from u_neg have mu_pos : "0<= -u" by simp
   1.579 +  thm mult_x_mono_lpos[OF mu_pos mx_lu]
   1.580 +  have "- u * - u \<le> - x * - x \<and> - x * - x \<le> - l * - l"
   1.581 +    by (rule_tac mult_x_mono_lpos[OF mu_pos mx_lu])
   1.582 +  then show ?thesis by simp
   1.583 +qed
   1.584 +
   1.585 +lemma mult_x_mono_lxnegupos : 
   1.586 +assumes l_neg : "(l::int) <= 0"
   1.587 +  and   u_pos : "0 <= u"
   1.588 +  and   x_neg : "x <= 0"
   1.589 +  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.590 +  shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)"
   1.591 +proof-
   1.592 +  from x_lu x_neg have mx_0l : "0 <= - x \<and> - x <= - l" by arith
   1.593 +  have trv_0 : "(0::int) <= 0" by arith
   1.594 +  thm mult_x_mono_lpos[OF trv_0 mx_0l]
   1.595 +  have "0 * 0 \<le> - x * - x \<and> - x * - x \<le> - l * - l"
   1.596 +    by (rule_tac  mult_x_mono_lpos[OF trv_0 mx_0l])
   1.597 +  then have xx_0ll : "0 <= x*x \<and> x*x <= l*l" by simp
   1.598 +  have "l*l <= max (l*l) (u*u)" by (simp add: le_maxI1)
   1.599 +  with xx_0ll show ?thesis by arith
   1.600 +qed
   1.601 +
   1.602 +lemma mult_x_mono_lnegupos : 
   1.603 +assumes l_neg : "(l::int) <= 0"
   1.604 +  and   u_pos : "0 <= u"
   1.605 +  and   x_lu : "l <= (x::int) \<and> x <= u"
   1.606 +  shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)"
   1.607 +proof-
   1.608 +  have "0<= x \<or> x <= 0" by arith
   1.609 +moreover
   1.610 +{
   1.611 +  assume x_neg : "x <= 0"
   1.612 +  thm mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu]
   1.613 +  have ?thesis by (rule_tac mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu])
   1.614 +}
   1.615 +moreover
   1.616 +
   1.617 +{
   1.618 +  assume x_pos : "0 <= x"
   1.619 +  from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith
   1.620 +  from x_pos have mx_neg : "-x <= 0" by simp
   1.621 +  from u_pos have mu_neg : "-u <= 0" by simp
   1.622 +  from x_lu x_pos have ml_pos : "0 <= -l" by simp
   1.623 +  thm mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu]
   1.624 +  have "0 \<le> - x * - x \<and> - x * - x \<le> max (- u * - u) (- l * - l)"
   1.625 +    by (rule_tac mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu])
   1.626 +  then have ?thesis by (simp add: max_commute)
   1.627 +
   1.628 +}
   1.629 +ultimately show ?thesis by blast
   1.630 +
   1.631 +qed
   1.632 +lemma abs_mul_x:
   1.633 +  assumes x_lu : "l <= (x::int) \<and> x <= u"
   1.634 +  shows 
   1.635 +  "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) <= x*x
   1.636 +  \<and> x*x <= (if 0 <= l then u*u  else if u <= 0 then l*l else (max (l*l) (u*u)))"
   1.637 +proof-
   1.638 +  have "(0 <= l) \<or> (l < 0 \<and> u <= 0) \<or> (l < 0 \<and> 0 < u)" by arith 
   1.639 +  
   1.640 +  moreover
   1.641 +  {
   1.642 +    assume l_pos : "0 <= l"
   1.643 +    from l_pos have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = l*l"
   1.644 +      by simp
   1.645 +    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.646 +    
   1.647 +    moreover have "l * l \<le> x * x \<and> x * x \<le> u * u" 
   1.648 +      by (rule_tac  mult_x_mono_lpos[OF l_pos x_lu])
   1.649 +    ultimately have ?thesis by simp 
   1.650 +  }
   1.651 +  
   1.652 +  moreover
   1.653 +  {
   1.654 +    assume l_neg : "l < 0"  and u_neg : "u <= 0"  
   1.655 +    from l_neg have l_le0 : "l <= 0" by simp
   1.656 +    from l_neg u_neg have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = u*u"
   1.657 +      by simp
   1.658 +    moreover 
   1.659 +    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.660 +    moreover 
   1.661 +    have "u * u \<le> x * x \<and> x * x \<le> l * l" 
   1.662 +      by (rule_tac mult_x_mono_luneg[OF l_le0 u_neg x_lu])
   1.663 +    
   1.664 +    ultimately have ?thesis by simp 
   1.665 +  }
   1.666 +  moreover
   1.667 +  {
   1.668 +    assume l_neg : "l < 0" and u_pos: "0 < u"
   1.669 +    from l_neg have l_le0 : "l <= 0" by simp
   1.670 +    from u_pos have u_ge0 : "0 <= u" by simp
   1.671 +    from l_neg u_pos have "(if 0 <= l then l*l  else if u <= 0 then u*u else 0) = 0"
   1.672 +      by simp
   1.673 +    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.674 +    moreover have "0 \<le> x * x \<and> x * x \<le> max (l * l) (u * u)" 
   1.675 +      by (rule_tac mult_x_mono_lnegupos[OF l_le0 u_ge0 x_lu])
   1.676 +    
   1.677 +    ultimately have ?thesis by simp 
   1.678 +    
   1.679 +  }
   1.680 +  
   1.681 +  ultimately show ?thesis by blast
   1.682 +qed
   1.683 +
   1.684 +
   1.685 +use"barith.ML"
   1.686 +setup Barith.setup
   1.687 +
   1.688 +end
   1.689 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/barith.ML	Wed Oct 06 13:58:56 2004 +0200
     2.3 @@ -0,0 +1,290 @@
     2.4 +(**************************************************************)
     2.5 +(*                                                            *)
     2.6 +(*                                                            *)
     2.7 +(*          Trying to implement an Bounded arithmetic         *)
     2.8 +(*                                                            *)
     2.9 +(*                                                            *)
    2.10 +(**************************************************************)
    2.11 +  
    2.12 +signature BARITH = 
    2.13 +sig
    2.14 +  val barith_tac : int -> tactic
    2.15 +  val setup      : (theory -> theory) list
    2.16 +  
    2.17 +end;
    2.18 +
    2.19 +
    2.20 +structure Barith =
    2.21 +struct
    2.22 +
    2.23 +(* Theorems we use from Barith.thy*)
    2.24 +val abs_const = thm "abs_const";
    2.25 +val abs_var = thm "abs_var";
    2.26 +val abs_neg = thm "abs_neg";
    2.27 +val abs_add = thm "abs_add";
    2.28 +val abs_sub = thm "abs_sub";
    2.29 +val abs_sub_x = thm "abs_sub_x";
    2.30 +val abs_mul = thm "abs_mul";
    2.31 +val abs_mul_x = thm "abs_mul_x";
    2.32 +val subinterval = thm "subinterval";
    2.33 +val imp_commute = thm "imp_commute";
    2.34 +val imp_simplify = thm "imp_simplify";
    2.35 +
    2.36 +exception NORMCONJ of string;
    2.37 +
    2.38 +fun interval_of_conj t = case t of
    2.39 + Const("op &",_) $
    2.40 +  (Const("op <=",_) $ l1 $(x as Free(xn,xT)))$
    2.41 +  (Const("op <=",_) $ y $ u1) => 
    2.42 +      if (x = y andalso type_of x = HOLogic.intT) 
    2.43 +        then (x,(l1,u1)) 
    2.44 +        else raise 
    2.45 +	  (NORMCONJ "Not in normal form -- not the same variable")
    2.46 +| Const("op &",_) $(Const("op <=",_) $ y $ u1)$
    2.47 +  (Const("op <=",_) $ l1 $(x as Free(xn,xT))) =>
    2.48 +      if (x = y andalso type_of x = HOLogic.intT) 
    2.49 +        then (x,(l1,u1)) 
    2.50 +        else raise 
    2.51 +	  (NORMCONJ "Not in normal form -- not the same variable")
    2.52 +|(Const("op <=",_) $ l $(x as Free(xn,xT))) => (x,(l,x))
    2.53 +|(Const("op <=",_) $ (x as Free(xn,xT))$ u) => (x,(x,u))
    2.54 +|_ => raise (NORMCONJ "Not in normal form - unknown conjunct");
    2.55 +
    2.56 +
    2.57 +(* The input to this function should be a list *)
    2.58 +(*of meta-implications of the following form:*)
    2.59 +(* l1 <= x1 & x1 <= u1 ==> ... ==> ln <= xn & xn <= un*)
    2.60 +(* the output will be a list of Var*interval*)
    2.61 +
    2.62 +val iT = HOLogic.intT;
    2.63 +fun maxterm t1 t2 = Const("HOL.max",iT --> iT --> iT)$t1$t2;
    2.64 +fun minterm t1 t2 = Const("HOL.min",iT --> iT --> iT)$t1$t2;
    2.65 +
    2.66 +fun intervals_of_premise p =  
    2.67 +  let val ps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems p)
    2.68 +      fun tight [] = []
    2.69 +         |tight ((x,(l,u))::ls) = 
    2.70 +	   let val ls' = tight ls in
    2.71 +	     case assoc (ls',x) of
    2.72 +	      None => (x,(l,u))::ls'
    2.73 +	     |Some (l',u') => let val ln = if (CooperDec.is_numeral l) andalso (CooperDec.is_numeral l') then CooperDec.mk_numeral (Int.min (CooperDec.dest_numeral l,CooperDec.dest_numeral l')) else (maxterm l l')
    2.74 +		 val un = if (CooperDec.is_numeral u) andalso (CooperDec.is_numeral u') then CooperDec.mk_numeral (Int.min (CooperDec.dest_numeral u,CooperDec.dest_numeral u')) else (minterm u u')
    2.75 +		   in (x,(ln,un))::(filter (fn p => fst p = x) ls')
    2.76 +		   end
    2.77 +           end 
    2.78 +  in tight (map interval_of_conj ps)
    2.79 +end ;
    2.80 +
    2.81 +fun exp_of_concl p = case p of
    2.82 +  Const("op &",_) $
    2.83 +  (Const("op <=",_) $ l $ e)$
    2.84 +  (Const("op <=",_) $ e' $ u) => 
    2.85 +     if e = e' then [(e,(Some l,Some u))]
    2.86 +     else raise NORMCONJ "Conclusion not in normal form-- different exp in conj"
    2.87 +|Const("op &",_) $
    2.88 +  (Const("op <=",_) $ e' $ u)$
    2.89 +  (Const("op <=",_) $ l $ e) => 
    2.90 +     if e = e' then [(e,(Some l,Some u))] 
    2.91 +     else raise NORMCONJ "Conclusion not in normal form-- different exp in conj"
    2.92 +|(Const("op <=",_) $ e $ u) =>
    2.93 +  if (CooperDec.is_numeral u) then [(e,(None,Some u))]
    2.94 +  else 
    2.95 +    if (CooperDec.is_numeral e) then [(u,(Some e,None))] 
    2.96 +    else raise NORMCONJ "Bounds has to be numerals" 
    2.97 +|(Const("op &",_)$a$b) => (exp_of_concl a) @ (exp_of_concl b)
    2.98 +|_ => raise NORMCONJ "Conclusion not in normal form---unknown connective";
    2.99 +
   2.100 +
   2.101 +fun strip_problem p = 
   2.102 +let 
   2.103 +  val is = intervals_of_premise p
   2.104 +  val e = exp_of_concl ((HOLogic.dest_Trueprop o Logic.strip_imp_concl) p)
   2.105 +in (is,e)
   2.106 +end;
   2.107 +
   2.108 +
   2.109 +
   2.110 +
   2.111 +(*Abstract interpretation of Intervals over theorems *)
   2.112 +exception ABSEXP of string;
   2.113 +
   2.114 +fun decomp_absexp sg is e = case e of
   2.115 + Free(xn,_) => ([], fn [] => case assoc (is,e) of 
   2.116 +   Some (l,u) => instantiate' [] 
   2.117 +     (map (fn a => Some (cterm_of sg a)) [l,e,u]) abs_var
   2.118 +  |_ => raise ABSEXP ("No Interval for Variable   " ^ xn) )
   2.119 +|Const("op +",_) $ e1 $ e2 => 
   2.120 +  ([e1,e2], fn [th1,th2] => [th1,th2] MRS abs_add)
   2.121 +|Const("op -",_) $ e1 $ e2 => 
   2.122 +  if e1 = e2 then 
   2.123 +    ([e1],fn [th] => th RS abs_sub_x)
   2.124 +  else
   2.125 +    ([e1,e2], fn [th1,th2] => [th1,th2] MRS abs_sub)
   2.126 +|Const("op *",_) $ e1 $ e2 => 
   2.127 +  if e1 = e2 then 
   2.128 +    ([e1],fn [th] => th RS abs_mul_x)
   2.129 +  else
   2.130 +  ([e1,e2], fn [th1,th2] => [th1,th2] MRS abs_mul)
   2.131 +|Const("op uminus",_) $ e' => 
   2.132 +  ([e'], fn [th] => th RS abs_neg)
   2.133 +|_ => if CooperDec.is_numeral e then
   2.134 +    ([], fn [] => instantiate' [] [Some (cterm_of sg e)] abs_const) 
   2.135 +        else raise ABSEXP "Unknown arithmetical expression";
   2.136 +
   2.137 +fun absexp sg is (e,(lo,uo)) = case (lo,uo) of
   2.138 +  (Some l, Some u) =>
   2.139 +  let 
   2.140 +    val th1 = CooperProof.thm_of sg (decomp_absexp sg is) e
   2.141 +    val th2 = instantiate' [] [None,None,None,Some (cterm_of sg l),Some (cterm_of sg u)] subinterval
   2.142 +    val ss = (simpset_of (theory "Presburger")) addsimps [max_def,min_def]
   2.143 +    val my_ss = HOL_basic_ss addsimps [imp_commute, imp_simplify]
   2.144 +    val th' = th1
   2.145 +    val th = th' RS th2
   2.146 +  in th
   2.147 +  end 
   2.148 +|(None, Some u) => 
   2.149 +  let 
   2.150 +    val th1 = CooperProof.thm_of sg (decomp_absexp sg is) e
   2.151 +    val Const("op &",_)$
   2.152 +      (Const("op <=",_)$l$_)$_= (HOLogic.dest_Trueprop o concl_of) th1
   2.153 +    val th2 = instantiate' [] [None,None,None,Some (cterm_of sg l),Some (cterm_of sg u)] subinterval
   2.154 +    val ss = (simpset_of (theory "Presburger")) addsimps [max_def,min_def]
   2.155 +    val my_ss = HOL_basic_ss addsimps [imp_commute, imp_simplify]
   2.156 +    val th' = th1
   2.157 +    val th = th' RS th2
   2.158 +  in th RS conjunct2
   2.159 +  end 
   2.160 +
   2.161 +|(Some l, None) => let 
   2.162 +    val th1 = CooperProof.thm_of sg (decomp_absexp sg is) e
   2.163 +    val Const("op &",_)$_$
   2.164 +      (Const("op <=",_)$_$u)= (HOLogic.dest_Trueprop o concl_of) th1
   2.165 +    val th2 = instantiate' [] [None,None,None,Some (cterm_of sg l),Some (cterm_of sg u)] subinterval
   2.166 +    val ss = (simpset_of (theory "Presburger")) addsimps [max_def,min_def]
   2.167 +    val my_ss = HOL_basic_ss addsimps [imp_commute, imp_simplify]
   2.168 +    val th' = th1
   2.169 +    val th = th' RS th2
   2.170 +  in th RS conjunct1
   2.171 +  end 
   2.172 +
   2.173 +|(None,None) => raise ABSEXP "No bounds for conclusion";
   2.174 +
   2.175 +fun free_occ e = case e of
   2.176 + Free(_,i) => if i = HOLogic.intT then 1 else 0
   2.177 +|f$a => (free_occ f) + (free_occ a)
   2.178 +|Abs(_,_,p) => free_occ p
   2.179 +|_ => 0;
   2.180 +
   2.181 +
   2.182 +(*
   2.183 +fun simp_exp sg p = 
   2.184 +  let val (is,(e,(l,u))) = strip_problem p
   2.185 +      val th = absexp sg is (e,(l,u))
   2.186 +      val _ = prth th
   2.187 +  in (th, free_occ e)
   2.188 +end;
   2.189 +*)
   2.190 +
   2.191 +fun simp_exp sg p = 
   2.192 +  let val (is,es) = strip_problem p
   2.193 +      val ths = map (absexp sg is) es
   2.194 +      val n = foldr (fn ((e,(_,_)),x) => (free_occ e) + x) (es,0)
   2.195 +  in (ths, n)
   2.196 +end;
   2.197 +
   2.198 +
   2.199 +
   2.200 +(* ============================ *)
   2.201 +(*      The barith Tactic       *)
   2.202 +(* ============================ *)
   2.203 +
   2.204 +(*
   2.205 +fun barith_tac i = ObjectLogic.atomize_tac i THEN (fn st =>
   2.206 +  let
   2.207 +    fun assm_tac n j = REPEAT_DETERM_N n ((assume_tac j) ORELSE (simple_arith_tac j))
   2.208 +    val g = BasisLibrary.List.nth (prems_of st, i - 1)
   2.209 +    val sg = sign_of_thm st
   2.210 +    val ss = (simpset_of (the_context())) addsimps [max_def,min_def]
   2.211 +    val (th,n) = simp_exp sg g
   2.212 +  in (rtac th i 
   2.213 +	THEN assm_tac n i  
   2.214 +	THEN (TRY (REPEAT_DETERM_N 2 (simp_tac ss i)))) st
   2.215 +end);
   2.216 +
   2.217 +*)
   2.218 +
   2.219 +
   2.220 +fun barith_tac i = ObjectLogic.atomize_tac i THEN (fn st =>
   2.221 +  let
   2.222 +    fun assm_tac n j = REPEAT_DETERM_N n ((assume_tac j) ORELSE (simple_arith_tac j))
   2.223 +    val g = BasisLibrary.List.nth (prems_of st, i - 1)
   2.224 +    val sg = sign_of_thm st
   2.225 +    val ss = (simpset_of (theory "Barith")) addsimps [max_def,min_def]
   2.226 +    val (ths,n) = simp_exp sg g
   2.227 +    val cn = length ths - 1
   2.228 +    fun conjIs thn j = EVERY (map (rtac conjI) (j upto (thn + j - 1)))
   2.229 +    fun thtac thms j = EVERY (map 
   2.230 +	(fn t => rtac t j THEN assm_tac n j  
   2.231 +	THEN (TRY (REPEAT_DETERM_N 2 (simp_tac ss j)))) thms)
   2.232 +  in ((conjIs cn i) THEN (thtac ths i)) st
   2.233 +end);
   2.234 +
   2.235 +fun barith_args meth =
   2.236 + let val parse_flag = 
   2.237 +         Args.$$$ "no_quantify" >> K (apfst (K false))
   2.238 +      || Args.$$$ "abs" >> K (apsnd (K true));
   2.239 + in
   2.240 +   Method.simple_args 
   2.241 +  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") []
   2.242 + >>
   2.243 +    curry (foldl op |>) (true, false))
   2.244 +    (fn (q,a) => fn _ => meth 1)
   2.245 +  end;
   2.246 +
   2.247 +fun barith_method i = Method.METHOD (fn facts =>
   2.248 +  Method.insert_tac facts 1 THEN barith_tac i)
   2.249 +
   2.250 +val setup =
   2.251 +  [Method.add_method ("barith",
   2.252 +     Method.no_args (barith_method 1),
   2.253 +     "VERY simple decision procedure for bounded arithmetic")];
   2.254 +
   2.255 +
   2.256 +(* End of Structure *)
   2.257 +end;
   2.258 +
   2.259 +(* Test *)
   2.260 +(*
   2.261 +open Barith;
   2.262 +
   2.263 +Goal "-1 <= (x::int) & x <= 1 ==> 0 <= (y::int) & y <= 5 + 7 ==> -13 <= x*x + y*x & x*x + y*x <= 20";
   2.264 +by(barith_tac 1);
   2.265 +
   2.266 +Goal "-1 <= (x::int) & x <= 1 ==> 0 <= (y::int) & y <= 5 + 7 ==> 0 <= x - x  + y & x - x  + y<= 12";
   2.267 +by(barith_tac 1);
   2.268 +
   2.269 +Goal "-1 <= (x::int) & x <= 1 ==> 0 <= (y::int) & y <= 5 + 7 ==> 0 <= x - x  + x*x & x - x  + x*x<= 1";
   2.270 +by(barith_tac 1);
   2.271 +
   2.272 +Goal "(x::int) <= 1& 1 <= x ==> 0 <= (y::int) & y <= 5 + 7 ==> 0 <= x - x  + x*x & x - x  + x*x<= 1";
   2.273 +by(barith_tac 1);
   2.274 +
   2.275 +Goal "(x::int) <= 1& 1 <= x ==> (t::int) <= 8 ==>(x::int) <= 2& 0 <= x ==> 0 <= (y::int) & y <= 5 + 7 ==> 0 <= x - x  + x*x & x - x  + x*x<= 1";
   2.276 +by(barith_tac 1);
   2.277 +
   2.278 +Goal "-1 <= (x::int) & x <= 1 ==> 0 <= (y::int) & y <= 5 + 7 ==> -4 <= x - x  + x*x";
   2.279 +by(barith_tac 1);
   2.280 +
   2.281 +Goal "[|(0::int) <= x & x <= 5 ; 0 <= (y::int) & y <= 7|]==> (0 <= x*x*x & x*x*x <= 125 ) & (0 <= x*x & x*x <= 100) & (0 <= x*x + x & x*x + x <= 30) & (0<= x*y & x*y <= 35)";
   2.282 +by (barith_tac 1);
   2.283 +*)
   2.284 +
   2.285 +
   2.286 +(*
   2.287 +val st = topthm();
   2.288 +val sg = sign_of_thm st; 
   2.289 +val g = BasisLibrary.List.nth (prems_of st, 0);
   2.290 +val (ths,n) = simp_exp sg g;
   2.291 +fun assm_tac n j = REPEAT_DETERM_N n ((assume_tac j) ORELSE (simple_arith_tac j));
   2.292 +
   2.293 +*)