int.why 5.77 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
theory Int
3

Andrei Paskevich's avatar
Andrei Paskevich committed
4 5
  function zero : int = 0
  function one  : int = 1
MARCHE Claude's avatar
MARCHE Claude committed
6

Andrei Paskevich's avatar
Andrei Paskevich committed
7 8 9
  predicate (< ) int int
  predicate (> ) (x y : int) = y < x
  predicate (<=) (x y : int) = x < y \/ x = y
10

Andrei Paskevich's avatar
Andrei Paskevich committed
11 12
  clone export algebra.OrderedUnitaryCommutativeRing with type t = int,
    function zero = zero, function one = one, predicate (<=) = (<=)
13

14
end
15 16 17 18 19

theory Abs

  use import Int

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  function abs (x:int) : int = if x >= 0 then x else -x
21

22 23
  lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y

24
  lemma Abs_pos: forall x:int. abs x >= 0
MARCHE Claude's avatar
MARCHE Claude committed
25

26 27
  lemma Abs_zero: forall x:int. abs x = 0 -> x = 0

28 29 30 31 32
end

theory MinMax

  use import Int
Andrei Paskevich's avatar
Andrei Paskevich committed
33
  clone export comparison.MinMax with type t = int, predicate ge = (>=)
34 35 36

end

37 38 39 40 41 42 43 44 45 46 47
theory Lex2

  use import Int

  predicate lt_nat (x y: int) = 0 <= y /\ x < y

  clone export relations.Lex with type t1 = int, type t2 = int,
    predicate rel1 = lt_nat, predicate rel2 = lt_nat

end

48
theory EuclideanDivision
MARCHE Claude's avatar
MARCHE Claude committed
49 50 51 52

  use import Int
  use import Abs

Andrei Paskevich's avatar
Andrei Paskevich committed
53 54
  function div int int : int
  function mod int int : int
MARCHE Claude's avatar
MARCHE Claude committed
55

MARCHE Claude's avatar
MARCHE Claude committed
56
  axiom Div_mod:
57
    forall x y:int. y <> 0 -> x = y * div x y + mod x y
MARCHE Claude's avatar
MARCHE Claude committed
58

MARCHE Claude's avatar
MARCHE Claude committed
59
  axiom Div_bound:
60
    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
MARCHE Claude's avatar
MARCHE Claude committed
61 62

  axiom Mod_bound:
63
    forall x y:int. y <> 0 -> 0 <= mod x y < abs y
MARCHE Claude's avatar
MARCHE Claude committed
64

65
  lemma Mod_1: forall x:int. mod x 1 = 0
MARCHE Claude's avatar
MARCHE Claude committed
66

67
  lemma Div_1: forall x:int. div x 1 = x
MARCHE Claude's avatar
MARCHE Claude committed
68

69 70 71
end

theory ComputerDivision
MARCHE Claude's avatar
MARCHE Claude committed
72 73 74 75

  use import Int
  use import Abs

Andrei Paskevich's avatar
Andrei Paskevich committed
76 77
  function div int int : int
  function mod int int : int
MARCHE Claude's avatar
MARCHE Claude committed
78

MARCHE Claude's avatar
MARCHE Claude committed
79
  axiom Div_mod:
80
    forall x y:int. y <> 0 -> x = y * div x y + mod x y
MARCHE Claude's avatar
MARCHE Claude committed
81

MARCHE Claude's avatar
MARCHE Claude committed
82
  axiom Div_bound:
83
    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
MARCHE Claude's avatar
MARCHE Claude committed
84 85

  axiom Mod_bound:
MARCHE Claude's avatar
MARCHE Claude committed
86 87
    forall x y:int. y <> 0 -> - abs y < mod x y < abs y

MARCHE Claude's avatar
MARCHE Claude committed
88
  axiom Div_sign_pos:
89
    forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0
MARCHE Claude's avatar
MARCHE Claude committed
90 91

  axiom Div_sign_neg:
92
    forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0
MARCHE Claude's avatar
MARCHE Claude committed
93

MARCHE Claude's avatar
MARCHE Claude committed
94
  axiom Mod_sign_pos:
95
    forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0
MARCHE Claude's avatar
MARCHE Claude committed
96 97

  axiom Mod_sign_neg:
98
    forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0
MARCHE Claude's avatar
MARCHE Claude committed
99 100 101

  lemma Rounds_toward_zero:
    forall x y:int. y <> 0 -> abs (div x y * y) <= abs x
MARCHE Claude's avatar
MARCHE Claude committed
102

MARCHE Claude's avatar
MARCHE Claude committed
103 104
  lemma Div_1: forall x:int. div x 1 = x

105
  lemma Mod_1: forall x:int. mod x 1 = 0
MARCHE Claude's avatar
MARCHE Claude committed
106

MARCHE Claude's avatar
MARCHE Claude committed
107 108 109 110
  lemma Div_inf: forall x y:int. 0 <= x < y -> div x y = 0

  lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x

111
  lemma Div_mult: forall x y z:int [div (x * y + z) x].
112
          x > 0 /\ y >= 0 /\ z >= 0 ->
MARCHE Claude's avatar
MARCHE Claude committed
113 114
          div (x * y + z) x = y + div z x

115
  lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
116
          x > 0 /\ y >= 0 /\ z >= 0 ->
MARCHE Claude's avatar
MARCHE Claude committed
117
          mod (x * y + z) x = mod z x
MARCHE Claude's avatar
MARCHE Claude committed
118

119 120
end

121
theory Exponentiation
122 123
  use import Int

124
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
125 126
  function one : t
  function (*) t t : t
127

Andrei Paskevich's avatar
Andrei Paskevich committed
128
  function power t int : t
129 130 131 132

  axiom Power_0 : forall x: t. power x 0 = one

  axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n
133

134 135 136
end

theory Power
137

138 139
  use import Int

140
  clone export
Andrei Paskevich's avatar
Andrei Paskevich committed
141
    Exponentiation with type t = int, function one = one, function (*) = (*)
142

143 144
  lemma Power_1 : forall x : int. power x 1 = x

145 146 147 148 149
  lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m ->
    power x (n + m) = power x n * power x m

  lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
    power x (n * m) = power (power x n) m
150 151 152

end

153 154 155
theory NumOfParam

  type param
156 157 158

  use import Int

Andrei Paskevich's avatar
Andrei Paskevich committed
159
  predicate pr param int
160

MARCHE Claude's avatar
MARCHE Claude committed
161
  (** number of [n] such that [a <= n < b] and [pr(p,n)] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
162
  function num_of (p : param) (a b : int) : int
163

MARCHE Claude's avatar
MARCHE Claude committed
164 165
  axiom Num_of_empty :
    forall p : param, a b : int.
166 167
    b <= a -> num_of p a b = 0

MARCHE Claude's avatar
MARCHE Claude committed
168 169
  axiom Num_of_right_no_add :
    forall p : param, a b : int.
170
    a < b -> not pr p (b-1) -> num_of p a b = num_of p a (b-1)
MARCHE Claude's avatar
MARCHE Claude committed
171 172
  axiom Num_of_right_add :
    forall p : param, a b : int.
173 174
    a < b -> pr p (b-1) -> num_of p a b = 1 + num_of p a (b-1)

MARCHE Claude's avatar
MARCHE Claude committed
175 176 177 178 179
  lemma Num_of_non_negative :
    forall p : param, a b : int. 0 <= num_of p a b
    (* direct when a>=b, by induction on b when a <= b *)

  lemma Num_of_append :
MARCHE Claude's avatar
MARCHE Claude committed
180
    forall p : param, a b c : int.
181
    a <= b <= c -> num_of p a c = num_of p a b + num_of p b c
MARCHE Claude's avatar
MARCHE Claude committed
182
    (* by induction on c *)
183

MARCHE Claude's avatar
MARCHE Claude committed
184 185 186 187 188 189 190 191 192 193
  lemma Num_of_left_no_add :
    forall p : param, a b : int.
    a < b -> not pr p a -> num_of p a b = num_of p (a+1) b
    (* by Num_of_append *)
  lemma Num_of_left_add :
    forall p : param, a b : int.
    a < b -> pr p a -> num_of p a b = 1 + num_of p (a+1) b
    (* by Num_of_append *)

  lemma Empty :
194 195
    forall p : param, a b : int.
    (forall n : int. a <= n < b -> not pr p n) -> num_of p a b = 0
MARCHE Claude's avatar
MARCHE Claude committed
196 197 198 199 200 201
    (* by induction on b *)

  lemma num_of_increasing:
    forall p : param, i j k : int.
    i <= j <= k -> num_of p i j <= num_of p i k
    (* by Num_of_append and Num_of_non_negative *)
202

Jean-Christophe's avatar
Jean-Christophe committed
203 204 205
  lemma num_of_strictly_increasing:
    forall p : param, i j k l : int.
    i <= j <= k < l -> pr p k -> num_of p i j < num_of p i l
MARCHE Claude's avatar
MARCHE Claude committed
206
    (* by Num_of_append and num_of_increasing *)
Jean-Christophe's avatar
Jean-Christophe committed
207

208 209
end

210
theory NumOf
211

Andrei Paskevich's avatar
Andrei Paskevich committed
212
  predicate pr int
213

Andrei Paskevich's avatar
Andrei Paskevich committed
214
  predicate pr0 () (n : int) = pr n
215

Andrei Paskevich's avatar
Andrei Paskevich committed
216
  clone NumOfParam as N with type param = tuple0, predicate pr = pr0
217

Andrei Paskevich's avatar
Andrei Paskevich committed
218
  function num_of (a b : int) : int = N.num_of () a b
219 220

end
221

222 223 224 225 226 227 228 229 230 231 232
theory Fact "Factorial"

  use export Int

  function fact int : int

  axiom fact0: fact 0 = 1
  axiom factn: forall n:int. n >= 1 -> fact n = n * fact (n-1)

end

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
theory Iter

  use import Int

  type t
  function f t : t

  function iter int t : t

  axiom iter_0: forall x: t. iter 0 x = x
  axiom iter_s: forall k: int, x: t. 0 < k -> iter k x = iter (k-1) (f x)

  lemma iter_1: forall x: t. iter 1 x = f x
  lemma iter_s2: forall k: int, x: t. 0 < k -> iter k x = f (iter (k-1) x)

end

250
theory Induction
251

252 253
  use import Int

Andrei Paskevich's avatar
Andrei Paskevich committed
254
  predicate p int
255

256
  lemma Induction :
257 258 259
    (forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
    forall n:int. 0 <= n -> p n

Andrei Paskevich's avatar
Andrei Paskevich committed
260
  function bound : int
261 262

  lemma Induction_bound :
263
    (forall n:int. bound <= n ->
264 265 266
      (forall k:int. bound <= k < n -> p k) -> p n) ->
    forall n:int. bound <= n -> p n

267 268
end

269
(*
MARCHE Claude's avatar
MARCHE Claude committed
270
Local Variables:
271
compile-command: "make -C .. theories/int.gui"
MARCHE Claude's avatar
MARCHE Claude committed
272
End:
273
*)