stdlib/number.mlw

   1
   2 (** {1 Number theory} *)
   3
   4
   5 (** {2 Parity properties} *)
   6
   7 module Parity
   8
   9   use int.Int
  10
  11   predicate even (n: int) = exists k: int. n = 2 * k
  12   predicate odd (n: int) = exists k: int. n = 2 * k + 1
  13
  14   lemma even_or_odd: forall n: int. even n \/ odd n
  15
  16   lemma even_not_odd: forall n: int. even n -> not (odd n)
  17   lemma odd_not_even: forall n: int. odd n -> not (even n)
  18
  19   lemma even_odd: forall n: int. even n -> odd (n + 1)
  20   lemma odd_even: forall n: int. odd n -> even (n + 1)
  21
  22   lemma even_even: forall n: int. even n -> even (n + 2)
  23   lemma odd_odd: forall n: int. odd n -> odd (n + 2)
  24
  25   lemma even_2k: forall k: int. even (2 * k)
  26   lemma odd_2k1: forall k: int. odd (2 * k + 1)
  27
  28   use int.ComputerDivision
  29
  30   lemma even_mod2 :
  31     forall n:int. even n <-> mod n 2 = 0
  32
  33 end
  34
  35 (** {2 Divisibility} *)
  36
  37 module Divisibility
  38
  39   use export int.Int
  40   use int.ComputerDivision
  41
  42   let predicate divides (d:int) (n:int)
  43     ensures { result <-> exists q:int. n = q * d }
  44   = if d = 0 then n = 0 else mod n d = 0
  45
  46   lemma divides_refl: forall n:int. divides n n
  47   lemma divides_1_n : forall n:int. divides 1 n
  48   lemma divides_0   : forall n:int. divides n 0
  49
  50   lemma divides_left : forall a b c: int. divides a b -> divides (c*a) (c*b)
  51   lemma divides_right: forall a b c: int. divides a b -> divides (a*c) (b*c)
  52
  53   lemma divides_oppr: forall a b: int. divides a b -> divides a (-b)
  54   lemma divides_oppl: forall a b: int. divides a b -> divides (-a) b
  55   lemma divides_oppr_rev: forall a b: int. divides (-a) b -> divides a b
  56   lemma divides_oppl_rev: forall a b: int. divides a (-b) -> divides a b
  57
  58   lemma divides_plusr:
  59     forall a b c: int. divides a b -> divides a c -> divides a (b + c)
  60   lemma divides_minusr:
  61     forall a b c: int. divides a b -> divides a c -> divides a (b - c)
  62   lemma divides_multl:
  63     forall a b c: int. divides a b -> divides a (c * b)
  64   lemma divides_multr:
  65     forall a b c: int. divides a b -> divides a (b * c)
  66
  67   lemma divides_factorl: forall a b: int. divides a (b * a)
  68   lemma divides_factorr: forall a b: int. divides a (a * b)
  69
  70   lemma divides_n_1: forall n: int. divides n 1 -> n = 1 \/ n = -1
  71
  72   lemma divides_antisym:
  73     forall a b: int. divides a b -> divides b a -> a = b \/ a = -b
  74
  75   lemma divides_trans:
  76     forall a b c: int. divides a b -> divides b c -> divides a c
  77
  78   use int.Abs
  79
  80   lemma divides_bounds:
  81     forall a b: int. divides a b -> b <> 0 -> abs a <= abs b
  82
  83   use int.EuclideanDivision as ED
  84
  85   lemma mod_divides_euclidean:
  86     forall a b: int. b <> 0 -> ED.mod a b = 0 -> divides b a
  87   lemma divides_mod_euclidean:
  88     forall a b: int. b <> 0 -> divides b a -> ED.mod a b = 0
  89
  90   use int.ComputerDivision as CD
  91
  92   lemma mod_divides_computer:
  93     forall a b: int. b <> 0 -> CD.mod a b = 0 -> divides b a
  94   lemma divides_mod_computer:
  95     forall a b: int. b <> 0 -> divides b a -> CD.mod a b = 0
  96
  97   use Parity
  98
  99   lemma even_divides: forall a: int. even a <-> divides 2 a
 100   lemma odd_divides: forall a: int. odd a <-> not (divides 2 a)
 101
 102 end
 103
 104 (** {2 Greateast Common Divisor} *)
 105
 106 module Gcd
 107
 108   use export int.Int
 109   use Divisibility
 110
 111   function gcd int int : int
 112
 113   axiom gcd_nonneg: forall a b: int. 0 <= gcd a b
 114   axiom gcd_def1  : forall a b: int. divides (gcd a b) a
 115   axiom gcd_def2  : forall a b: int. divides (gcd a b) b
 116   axiom gcd_def3  :
 117     forall a b x: int. divides x a -> divides x b -> divides x (gcd a b)
 118   axiom gcd_unique:
 119     forall a b d: int.
 120     0 <= d -> divides d a -> divides d b ->
 121     (forall x: int. divides x a -> divides x b -> divides x d) ->
 122     d = gcd a b
 123
 124   (* gcd is associative commutative *)
 125
 126   clone algebra.AC with type t = int, function op = gcd
 127
 128   lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
 129   lemma gcd_0_neg: forall a: int. a <  0 -> gcd a 0 = -a
 130
 131   lemma gcd_opp: forall a b: int. gcd a b = gcd (-a) b
 132
 133   lemma gcd_euclid: forall a b q: int. gcd a b = gcd a (b - q * a)
 134
 135   use int.ComputerDivision as CD
 136
 137   lemma Gcd_computer_mod:
 138     forall a b: int [gcd b (CD.mod a b)].
 139     b <> 0 -> gcd b (CD.mod a b) = gcd a b
 140
 141   use int.EuclideanDivision as ED
 142
 143   lemma Gcd_euclidean_mod:
 144     forall a b: int [gcd b (ED.mod a b)].
 145     b <> 0 -> gcd b (ED.mod a b) = gcd a b
 146
 147   lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b
 148
 149 end
 150
 151 (** {2 Prime numbers} *)
 152
 153 module Prime
 154
 155   use export int.Int
 156   use Divisibility
 157
 158   predicate prime (p: int) =
 159     2 <= p /\ forall n: int. 1 < n < p -> not (divides n p)
 160
 161   lemma not_prime_1: not (prime 1)
 162   lemma prime_2    : prime 2
 163   lemma prime_3    : prime 3
 164
 165   lemma prime_divisors:
 166     forall p: int. prime p ->
 167     forall d: int. divides d p -> d = 1 \/ d = -1 \/ d = p \/ d = -p
 168
 169   lemma small_divisors:
 170     forall p: int. 2 <= p ->
 171     (forall d: int. 2 <= d -> prime d -> 1 < d*d <= p -> not (divides d p)) ->
 172     prime p
 173
 174   use Parity
 175
 176   lemma even_prime: forall p: int. prime p -> even p -> p = 2
 177
 178   lemma odd_prime: forall p: int. prime p -> p >= 3 -> odd p
 179
 180 end
 181
 182 (** {2 Coprime numbers} *)
 183
 184 module Coprime
 185
 186   use export int.Int
 187   use Divisibility
 188   use Gcd
 189
 190   predicate coprime (a b: int) = gcd a b = 1
 191
 192   use Prime
 193
 194   lemma prime_coprime:
 195     forall p: int.
 196     prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p
 197
 198   lemma Gauss:
 199     forall a b c:int. divides a (b*c) /\ coprime a b -> divides a c
 200
 201   lemma Euclid:
 202     forall p a b:int.
 203       prime p /\ divides p (a*b) -> divides p a \/ divides p b
 204
 205   lemma gcd_coprime:
 206     forall a b c. coprime a b -> gcd a (b*c) = gcd a c
 207
 208 end