lib/isabelle/Why3_Number.thy

   1 theory Why3_Number
   2 imports
   3   Why3_Int
   4   "HOL-Computational_Algebra.Primes"
   5 begin
   6
   7 section \<open> Parity properties \<close>
   8
   9 why3_open "number/Parity.xml"
  10
  11 why3_vc evenqtdef by arith
  12
  13 why3_vc oddqtdef by arith
  14
  15 why3_vc even_or_odd by auto
  16
  17 why3_vc even_not_odd using assms by simp
  18
  19 why3_vc odd_not_even using assms by simp
  20
  21 why3_vc even_odd using assms by simp
  22
  23 why3_vc odd_even using assms by simp
  24
  25 why3_vc even_even using assms by simp
  26
  27 why3_vc odd_odd using assms by simp
  28
  29 why3_vc even_2k by simp
  30
  31 why3_vc odd_2k1 by simp
  32
  33 why3_vc even_mod2
  34   by (auto simp add: evenqtdef cmod_def sgn_if minus_equation_iff [of n])
  35
  36 why3_end
  37
  38
  39 section \<open> Divisibility \<close>
  40
  41 why3_open "number/Divisibility.xml"
  42
  43 why3_vc dividesqtdef
  44   by (auto simp add: cmod_def sgn_if minus_equation_iff [of n])
  45
  46 why3_vc divides_refl by simp
  47
  48 why3_vc divides_1_n by simp
  49
  50 why3_vc divides_0 by simp
  51
  52 why3_vc divides_left using assms by simp
  53
  54 why3_vc divides_right using assms by simp
  55
  56 why3_vc divides_oppr using assms by simp
  57
  58 why3_vc divides_oppl using assms by simp
  59
  60 why3_vc divides_oppr_rev using assms by simp
  61
  62 why3_vc divides_oppl_rev using assms by simp
  63
  64 why3_vc divides_plusr using assms by simp
  65
  66 why3_vc divides_minusr using assms by simp
  67
  68 why3_vc divides_multl using assms by simp
  69
  70 why3_vc divides_multr using assms by simp
  71
  72 why3_vc divides_factorl by simp
  73
  74 why3_vc divides_factorr by simp
  75
  76 why3_vc divides_n_1 using assms by auto
  77
  78 why3_vc divides_antisym
  79   using assms
  80   by (auto dest: zdvd_antisym_abs)
  81
  82 why3_vc divides_trans using assms by (rule dvd_trans)
  83
  84 why3_vc divides_bounds using assms by (simp add: dvd_imp_le_int)
  85
  86 why3_vc mod_divides_euclidean
  87   using assms
  88   by (auto simp add: emod_def split: if_split_asm)
  89
  90 why3_vc divides_mod_euclidean
  91   using assms
  92   by (simp add: emod_def dvd_eq_mod_eq_0 zabs_def zmod_zminus2_eq_if)
  93
  94 why3_vc mod_divides_computer
  95   using assms
  96   by (auto simp add: cmod_def zabs_def sgn_0_0 zmod_zminus1_eq_if
  97     not_sym [OF less_imp_neq [OF pos_mod_bound]]
  98     split: if_split_asm)
  99
 100 why3_vc divides_mod_computer
 101   using assms
 102   by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def
 103     zmod_zminus1_eq_if zmod_zminus2_eq_if)
 104
 105 why3_vc even_divides ..
 106
 107 why3_vc odd_divides ..
 108
 109 why3_vc dividesqtspec
 110   by (simp add: dvd_def mult.commute)
 111
 112 why3_end
 113
 114
 115 section \<open> Greatest Common Divisor \<close>
 116
 117 why3_open "number/Gcd.xml"
 118
 119 why3_vc gcd_nonneg by simp
 120
 121 why3_vc gcd_def1 by simp
 122
 123 why3_vc gcd_def2 by simp
 124
 125 why3_vc gcd_def3 using assms by (rule gcd_greatest)
 126
 127 why3_vc gcd_unique using assms
 128   by (simp add: gcd_unique_int [symmetric])
 129
 130 why3_vc Comm by (rule gcd.commute)
 131
 132 why3_vc Assoc by (rule gcd.assoc)
 133
 134 why3_vc gcd_0_pos using assms by simp
 135
 136 why3_vc gcd_0_neg using assms by simp
 137
 138 why3_vc gcd_opp by simp
 139
 140 why3_vc gcd_euclid
 141   using gcd_add_mult [of a "- q" b]
 142   by (simp add: algebra_simps)
 143
 144 why3_vc Gcd_computer_mod
 145   using assms gcd_add_mult [of b "- 1" "a mod b"]
 146   by (simp add: cmod_def zabs_def gcd_red_int [symmetric] sgn_if algebra_simps del: gcd_mod_right)
 147     (simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod_right)
 148
 149 why3_vc Gcd_euclidean_mod
 150   using assms gcd_add_mult [of b "- 1" "a mod b"]
 151   by (simp add: emod_def zabs_def gcd_red_int [symmetric] algebra_simps del: gcd_mod_right)
 152     (simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod_right)
 153
 154 why3_vc gcd_mult using assms
 155   by (simp add: gcd_mult_distrib_int [symmetric])
 156
 157 why3_end
 158
 159
 160 section \<open> Prime numbers \<close>
 161
 162 why3_open "number/Prime.xml"
 163
 164 why3_vc primeqtdef
 165   by (auto simp add: prime_int_iff')
 166
 167 why3_vc not_prime_1 by simp
 168
 169 why3_vc prime_2 by simp
 170
 171 why3_vc prime_3 by simp
 172
 173 why3_vc prime_divisors
 174   using assms
 175   by (auto simp add: prime_int_altdef dest: spec [of _ "\<bar>d\<bar>"])
 176
 177 lemma small_divisors_aux:
 178   "1 < (n::nat) \<Longrightarrow> n < p \<Longrightarrow> n dvd p \<Longrightarrow> \<exists>d. prime d \<and> d * d \<le> p \<and> d dvd p"
 179 proof (induct n rule: less_induct)
 180   case (less n)
 181   then obtain m where "p = n * m" by (auto simp add: dvd_def)
 182   show ?case
 183   proof (cases "prime n")
 184     case True
 185     show ?thesis
 186     proof (cases "n \<le> m")
 187       case True
 188       with `p = n * m` `prime n`
 189       show ?thesis by auto
 190     next
 191       case False
 192       then have "m < n" by simp
 193       moreover from `n < p` `p = n * m` have "1 < m" by simp
 194       moreover from `1 < n` `n < p` `p = n * m` have "m < p" by simp
 195       moreover from `p = n * m` have "m dvd p" by simp
 196       ultimately show ?thesis by (rule less)
 197     qed
 198   next
 199     case False
 200     with `1 < n` obtain k where "k dvd n" "k \<noteq> 1" "k \<noteq> n"
 201       by (auto simp add: prime_nat_iff)
 202     with `1 < n` have "k \<le> n" by (simp add: dvd_imp_le)
 203     with `k \<noteq> n` have "k < n" by simp
 204     moreover from `k dvd n` `1 < n` have "k \<noteq> 0" by (rule_tac notI) simp
 205     with `k \<noteq> 1` have "1 < k" by simp
 206     moreover from `k < n` `n < p` have "k < p" by simp
 207     moreover from `k dvd n` `n dvd p` have "k dvd p" by (rule dvd_trans)
 208     ultimately show ?thesis by (rule less)
 209   qed
 210 qed
 211
 212 why3_vc small_divisors
 213   unfolding primeqtdef
 214 proof
 215   show "2 \<le> p" by fact
 216
 217   show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
 218   proof (intro strip)
 219     fix n
 220     assume "1 < n \<and> n < p"
 221     show "\<not> n dvd p"
 222     proof
 223       assume "n dvd p"
 224       with `1 < n \<and> n < p`
 225       have "1 < nat n" "nat n < nat p" "nat n dvd nat p"
 226         by (simp_all add: nat_dvd_iff)
 227       then have "\<exists>d. prime d \<and> d * d \<le> nat p \<and> d dvd (nat p)"
 228         by (rule small_divisors_aux)
 229       with `2 \<le> p` obtain d
 230         where d: "prime (int d)" "int d * int d \<le> p" "int d dvd p"
 231         by (auto simp add: int_dvd_int_iff [symmetric] le_nat_iff)
 232       from `prime (int d)` have "2 \<le> int d" by (simp add: prime_ge_2_int)
 233       then have "2 \<le> int d" by simp
 234       with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
 235         by (rule mult_mono) simp_all
 236       with d assms `2 \<le> int d` show False by auto
 237     qed
 238   qed
 239 qed
 240
 241 why3_vc even_prime
 242 proof -
 243   from `prime p` have "0 \<le> p" by (simp add: primeqtdef)
 244   from `prime p` have "2 \<le> p" by (simp add: prime_ge_2_int)
 245   with `prime p` `even p` `0 \<le> p` show ?thesis
 246     by (auto simp add: order_le_less prime_odd_int)
 247 qed
 248
 249 why3_vc odd_prime
 250 proof -
 251   from `prime p` have "2 \<le> p" by (simp add: prime_ge_2_int)
 252   with `prime p` `3 \<le> p` show ?thesis
 253     by (auto simp add: order_le_less prime_odd_int)
 254 qed
 255
 256 why3_end
 257
 258
 259 section \<open> Coprime numbers \<close>
 260
 261 why3_open "number/Coprime.xml"
 262
 263 why3_vc coprimeqtdef by (rule coprime_iff_gcd_eq_1)
 264
 265 why3_vc prime_coprime
 266 proof -
 267   have "(\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p) =
 268     (\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p)"
 269   proof
 270     assume H: "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
 271     show "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
 272     proof (intro strip)
 273       fix n
 274       assume H': "1 \<le> n \<and> n < p"
 275       {
 276         fix d
 277         assume "0 \<le> d" "d dvd n" "d dvd p"
 278         with H' have "d \<noteq> 0" by auto
 279         have "d = 1"
 280         proof (rule ccontr)
 281           assume "d \<noteq> 1"
 282           with `0 \<le> d` `d \<noteq> 0` have "1 < d" by simp
 283           moreover from `d dvd p` H' have "d \<le> p" by (auto dest: zdvd_imp_le)
 284           moreover from `d dvd n` H' have "d \<noteq> p" by (auto dest: zdvd_imp_le)
 285           ultimately show False using `d dvd p` H by auto
 286         qed
 287       }
 288       then show "coprime n p"
 289         by (auto simp add: coprime_iff_gcd_eq_1)
 290     qed
 291   next
 292     assume H: "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
 293     show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
 294     proof (intro strip notI)
 295       fix n
 296       assume H': "1 < n \<and> n < p" "n dvd p"
 297       then have "1 \<le> n \<and> n < p" by simp
 298       with H have "coprime n p" by simp
 299       with H' show False by (simp add: coprime_iff_gcd_eq_1)
 300     qed
 301   qed
 302   then show ?thesis by (simp add: primeqtdef)
 303 qed
 304
 305 why3_vc Gauss
 306 proof -
 307   from assms
 308   have "coprime a b" "a dvd c * b" by (simp_all add: mult.commute)
 309   then show ?thesis by (simp add: coprime_dvd_mult_left_iff)
 310 qed
 311
 312 why3_vc Euclid
 313   using assms
 314   by (simp add: prime_dvd_multD)
 315
 316 why3_vc gcd_coprime
 317 proof -
 318   have "gcd a (b * c) = gcd (b * c) a" by (simp add: gcd.commute)
 319   also from assms have "coprime a b" by (simp add: gcd.commute coprime_iff_gcd_eq_1)
 320   then have "gcd (b * c) a = gcd c a" by (simp add: gcd_mult_left_left_cancel)
 321   finally show ?thesis by (simp add: gcd.commute)
 322 qed
 323
 324 why3_end
 325
 326 end