Why3_Int.thy 8.34 KB
Newer Older
Stefan Berghofer's avatar
Stefan Berghofer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
theory Why3_Int
imports Why3_Setup
begin

section {* Integers and the basic operators *}

why3_open "int/Int.xml"

why3_vc Comm by simp

why3_vc Comm1 by simp

why3_vc Assoc by simp

why3_vc Assoc1 by simp

why3_vc Unitary by simp

why3_vc Inv_def_l by simp

why3_vc Inv_def_r by simp

why3_vc Unit_def_l by simp

why3_vc Unit_def_r by simp

why3_vc Mul_distr_l by (simp add: ring_distribs)

why3_vc Mul_distr_r by (simp add: ring_distribs)

why3_vc infix_mn_def by simp

why3_vc NonTrivialRing by simp

why3_vc infix_lseq_def by auto

why3_vc Refl by simp

why3_vc Trans using assms by simp

why3_vc Total by auto

why3_vc Antisymm using assms by simp

why3_vc ZeroLessOne by simp

why3_vc CompatOrderAdd using assms by simp

why3_vc CompatOrderMult using assms by (rule mult_right_mono)

why3_end


section {* Absolute Value *}

why3_open "int/Abs.xml"

why3_vc abs_def by simp

why3_vc Abs_le by auto

why3_vc Abs_pos by simp

why3_end


section {* Minimum and Maximum *}

why3_open "int/MinMax.xml"

71
why3_vc Max_l using assms by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
72

73
why3_vc Max_comm by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
74

75
why3_vc Max_assoc by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
76

77
why3_vc Min_r using assms by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
78

79
why3_vc Min_comm by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
80

81
why3_vc Min_assoc by simp
Stefan Berghofer's avatar
Stefan Berghofer committed
82

83 84 85 86
why3_vc max_def by auto

why3_vc min_def by auto

Stefan Berghofer's avatar
Stefan Berghofer committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
why3_end


section {* Euclidean Division *}

definition ediv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "ediv" 70) where
  "a ediv b = sgn b * (a div \<bar>b\<bar>)"

definition emod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "emod" 70) where
  "a emod b = a mod \<bar>b\<bar>"

why3_open "int/EuclideanDivision.xml"
  constants
    div = ediv
    mod = emod

why3_vc Div_1 by (simp add: ediv_def)

why3_vc Div_1_left using assms by (simp add: ediv_def div_pos_pos_trivial)

why3_vc Div_inf using assms by (simp add: ediv_def div_pos_pos_trivial)

why3_vc Div_inf_neg
  using assms
  by (cases "x = y") (simp_all add: ediv_def
    zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial)

why3_vc Div_mod
Stefan Berghofer's avatar
Stefan Berghofer committed
115
  by (simp add: ediv_def emod_def mult.assoc [symmetric] abs_sgn)
Stefan Berghofer's avatar
Stefan Berghofer committed
116

Stefan Berghofer's avatar
Stefan Berghofer committed
117
why3_vc Div_mult using assms by (simp add: ediv_def add.commute)
Stefan Berghofer's avatar
Stefan Berghofer committed
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151

why3_vc Div_bound
proof -
  from assms show ?C1
    by (simp add: ediv_def pos_imp_zdiv_nonneg_iff)

  show ?C2
  proof (cases "x = 0")
    case False
    show ?thesis
    proof (cases "y = 1")
      case False
      with assms `x \<noteq> 0` have "x div y < x"
        by (simp add: int_div_less_self)
      with assms show ?thesis by (simp add: ediv_def)
    qed (simp add: ediv_def)
  qed (simp add: ediv_def)
qed

why3_vc Div_minus1_left
  using assms
  by (simp only: zdiv_zminus1_eq_if ediv_def)
    (simp add: div_pos_pos_trivial mod_pos_pos_trivial)

why3_vc Mod_0 by (simp add: emod_def)

why3_vc Mod_1 by (simp add: emod_def)

why3_vc Mod_1_left using assms by (simp add: emod_def mod_pos_pos_trivial)

why3_vc Mod_minus1_left
  using assms
  by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial)

Stefan Berghofer's avatar
Stefan Berghofer committed
152
why3_vc Mod_mult using assms by (simp add: emod_def add.commute)
Stefan Berghofer's avatar
Stefan Berghofer committed
153 154 155

why3_vc Mod_bound using assms by (simp_all add: emod_def)

156
why3_vc Div_unique using assms
157
 proof -
MARCHE Claude's avatar
MARCHE Claude committed
158 159 160 161 162 163 164
  have h0: "y \<noteq> 0" using assms by auto
  have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast
  have h2: "0 \<le> x emod y \<and> x emod y < y" using assms H1 h0 Mod_bound zabs_def
    by (metis abs_sgn monoid_mult_class.mult.right_neutral sgn_pos)
  have h3: "x - y < y * (x ediv y)" using h1 h2 by linarith
  have h4: "y * (x ediv y) \<le> x" using h1 h2 by linarith
  show ?thesis
165 166 167 168
  proof (cases "x ediv y > q")
   assume a:"q < x ediv y"
   have h5: "x ediv y \<ge> q + 1" using a by linarith
   have h6: "y * (x ediv y) >= y * (q + 1)" by (metis H1 h5 le_less mult_left_mono)
169
   have h7: "y * (x ediv y) >= q * y + y" by (metis Comm1 Mul_distr_l h6 monoid_mult_class.mult.right_neutral)
170 171 172
   thus "x ediv y = q" using H3 h1 h2 h7 by linarith
   next
   assume a:"\<not> q < x ediv y"
173
   show "x ediv y = q"
174 175 176
   proof (cases "x ediv y < q")
    assume b:"x ediv y < q"
    have h5: "x ediv y \<le> q - 1" using b by linarith
MARCHE Claude's avatar
MARCHE Claude committed
177
    have h6: "y * (x ediv y) <= y * (q - 1)" by (metis H1 h5 le_less mult_left_mono)
178
    have h7: "y * (x ediv y) <= q * y - y" by (metis Comm1 h6 int_distrib(4) monoid_mult_class.mult.right_neutral)
MARCHE Claude's avatar
MARCHE Claude committed
179 180
    thus "x ediv y = q" using H2 h3 h7 by linarith
    next
181 182 183 184 185
    assume b:"\<not> x ediv y < q"
    show ?thesis using a b by linarith
   qed
  qed
qed
Stefan Berghofer's avatar
Stefan Berghofer committed
186

187
why3_end
Stefan Berghofer's avatar
Stefan Berghofer committed
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222

section {* Computer Division *}

definition cdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cdiv" 70) where
  "a cdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"

definition cmod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cmod" 70) where
  "a cmod b = sgn a * (\<bar>a\<bar> mod \<bar>b\<bar>)"

why3_open "int/ComputerDivision.xml"
  constants
    div = cdiv
    mod = cmod

why3_vc Div_1 by (simp add: cdiv_def mult_sgn_abs)

why3_vc Div_inf using assms by (simp add: cdiv_def div_pos_pos_trivial)

why3_vc Div_sign_neg
  using assms
  by (cases "x = 0") (simp_all add: cdiv_def
    zdiv_zminus1_eq_if div_nonpos_pos_le0 pos_imp_zdiv_neg_iff)

why3_vc Div_sign_pos
  using assms
  by (cases "x = 0")
    (simp_all add: cdiv_def pos_imp_zdiv_nonneg_iff)

why3_vc Div_mod
proof -
  have "y * (sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>)) + sgn x * (\<bar>x\<bar> mod \<bar>y\<bar>) =
    sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>)"
    by (simp add: ring_distribs)
  then show ?thesis
    by (cases "x = 0") (simp_all add: cdiv_def cmod_def abs_sgn
223
      sgn_mult [symmetric] order.strict_iff_order)
Stefan Berghofer's avatar
Stefan Berghofer committed
224 225 226 227 228 229 230
qed

why3_vc Div_mult
proof (cases "y = 0")
  case False
  with assms show ?thesis
    by (cases "z = 0")
231
      (simp_all add: cdiv_def add.commute add_pos_pos)
Stefan Berghofer's avatar
Stefan Berghofer committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
qed simp

why3_vc Div_bound
proof -
  from assms show ?C1
    by (simp add: cdiv_def pos_imp_zdiv_nonneg_iff sgn_if)

  show ?C2
  proof (cases "x = 0")
    case False
    show ?thesis
    proof (cases "y = 1")
      case False
      with assms `x \<noteq> 0` have "x div y < x"
        by (simp add: int_div_less_self)
      with assms show ?thesis by (simp add: cdiv_def sgn_if)
    qed (simp add: cdiv_def sgn_if)
  qed (simp add: cdiv_def)
qed

why3_vc Mod_1 by (simp add: cmod_def)

why3_vc Mod_inf using assms by (simp add: cmod_def mod_pos_pos_trivial sgn_if)

why3_vc Mod_mult
proof (cases "y = 0")
  case False
  with assms show ?thesis
260
    by (cases "z = 0") (simp_all add: cmod_def add.commute add_pos_pos)
Stefan Berghofer's avatar
Stefan Berghofer committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288
qed simp

why3_vc Mod_bound
proof -
  from assms show ?C1
    by (auto simp add: cmod_def sgn_if intro: less_le_trans [of _ 0])

  from assms show ?C2
    by (auto simp add: cmod_def sgn_if intro: le_less_trans [of _ 0])
qed

why3_vc Mod_sign_neg using assms by (simp add: cmod_def sgn_if)

why3_vc Mod_sign_pos using assms by (simp add: cmod_def sgn_if)

why3_vc Rounds_toward_zero
proof (cases "x = 0")
  case False
  then have "\<bar>sgn x\<bar> = 1" by (simp add: sgn_if)
  have "sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) * y =
    sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>))" (is "?l = ?r")
    by simp
  then have "\<bar>?l\<bar> = \<bar>?r\<bar>" by (simp (no_asm_simp))
  also note abs_sgn [symmetric]
  also note abs_mult
  also have "\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) \<le> \<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>"
    by (rule add_increasing2) (simp_all add: assms)
  with assms have "\<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>)\<bar> \<le> \<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>\<bar>"
289
    by (simp add: pos_imp_zdiv_nonneg_iff)
Stefan Berghofer's avatar
Stefan Berghofer committed
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
  finally show ?thesis using `\<bar>sgn x\<bar> = 1`
    by (simp add: cdiv_def)
qed (simp add: cdiv_def)

why3_end


section {* Division by 2 *}

why3_open "int/Div2.xml"

why3_vc div2
  by (rule exI [of _ "x div 2"]) auto

why3_end


section {* Power of an integer to an integer *}

why3_open "int/Power.xml"

why3_vc Power_0 by simp

why3_vc Power_1 by simp

why3_vc Power_s using assms by (simp add: nat_add_distrib)

why3_vc Power_s_alt using assms by (simp add: nat_diff_distrib power_Suc [symmetric])

why3_vc Power_sum using assms by (simp add: nat_add_distrib power_add)

why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult)

323 324 325
why3_vc Power_comm1 by (simp add: power_mult_distrib)

why3_vc Power_comm2 by (simp add: power_mult_distrib)
Stefan Berghofer's avatar
Stefan Berghofer committed
326

Stefan Berghofer's avatar
Stefan Berghofer committed
327 328 329 330
why3_vc Power_non_neg using assms by simp

why3_vc Power_monotonic using assms by (simp add: power_increasing)

Stefan Berghofer's avatar
Stefan Berghofer committed
331 332 333
why3_end

end