int.why 5.77 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Oct 19, 2010 2 ``````theory Int `````` Jean-Christophe Filliâtre committed Mar 23, 2010 3 `````` `````` Andrei Paskevich committed Jun 29, 2011 4 5 `````` function zero : int = 0 function one : int = 1 `````` MARCHE Claude committed Oct 19, 2010 6 `````` `````` Andrei Paskevich committed Jun 29, 2011 7 8 9 `````` predicate (< ) int int predicate (> ) (x y : int) = y < x predicate (<=) (x y : int) = x < y \/ x = y `````` Andrei Paskevich committed Apr 02, 2010 10 `````` `````` Andrei Paskevich committed Jun 29, 2011 11 12 `````` clone export algebra.OrderedUnitaryCommutativeRing with type t = int, function zero = zero, function one = one, predicate (<=) = (<=) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 13 `````` `````` Jean-Christophe Filliâtre committed May 26, 2010 14 ``````end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 15 16 17 18 19 `````` theory Abs use import Int `````` Andrei Paskevich committed Jun 29, 2011 20 `````` function abs (x:int) : int = if x >= 0 then x else -x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 21 `````` `````` MARCHE Claude committed Sep 04, 2011 22 23 `````` lemma Abs_le: forall x y:int. abs x <= y <-> -y <= x <= y `````` Andrei Paskevich committed Jun 21, 2010 24 `````` lemma Abs_pos: forall x:int. abs x >= 0 `````` MARCHE Claude committed Mar 26, 2010 25 `````` `````` MARCHE Claude committed Sep 04, 2011 26 27 `````` lemma Abs_zero: forall x:int. abs x = 0 -> x = 0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 28 29 30 31 32 ``````end theory MinMax use import Int `````` Andrei Paskevich committed Jun 29, 2011 33 `````` clone export comparison.MinMax with type t = int, predicate ge = (>=) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 34 35 36 `````` end `````` Jean-Christophe Filliâtre committed Aug 01, 2011 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 48 ``````theory EuclideanDivision `````` MARCHE Claude committed Mar 26, 2010 49 50 51 52 `````` use import Int use import Abs `````` Andrei Paskevich committed Jun 29, 2011 53 54 `````` function div int int : int function mod int int : int `````` MARCHE Claude committed Mar 26, 2010 55 `````` `````` MARCHE Claude committed Oct 19, 2010 56 `````` axiom Div_mod: `````` Andrei Paskevich committed Jun 21, 2010 57 `````` forall x y:int. y <> 0 -> x = y * div x y + mod x y `````` MARCHE Claude committed Mar 26, 2010 58 `````` `````` MARCHE Claude committed Oct 19, 2010 59 `````` axiom Div_bound: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 60 `````` forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x `````` MARCHE Claude committed Oct 19, 2010 61 62 `````` axiom Mod_bound: `````` Andrei Paskevich committed Jun 21, 2010 63 `````` forall x y:int. y <> 0 -> 0 <= mod x y < abs y `````` MARCHE Claude committed Mar 26, 2010 64 `````` `````` Andrei Paskevich committed Jun 21, 2010 65 `````` lemma Mod_1: forall x:int. mod x 1 = 0 `````` MARCHE Claude committed Mar 26, 2010 66 `````` `````` Andrei Paskevich committed Jun 21, 2010 67 `````` lemma Div_1: forall x:int. div x 1 = x `````` MARCHE Claude committed Mar 26, 2010 68 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 69 70 71 ``````end theory ComputerDivision `````` MARCHE Claude committed Mar 26, 2010 72 73 74 75 `````` use import Int use import Abs `````` Andrei Paskevich committed Jun 29, 2011 76 77 `````` function div int int : int function mod int int : int `````` MARCHE Claude committed Mar 26, 2010 78 `````` `````` MARCHE Claude committed Oct 19, 2010 79 `````` axiom Div_mod: `````` Andrei Paskevich committed Jun 21, 2010 80 `````` forall x y:int. y <> 0 -> x = y * div x y + mod x y `````` MARCHE Claude committed Mar 26, 2010 81 `````` `````` MARCHE Claude committed Oct 19, 2010 82 `````` axiom Div_bound: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 83 `````` forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x `````` MARCHE Claude committed Oct 19, 2010 84 85 `````` axiom Mod_bound: `````` MARCHE Claude committed Jul 05, 2010 86 87 `````` forall x y:int. y <> 0 -> - abs y < mod x y < abs y `````` MARCHE Claude committed Oct 07, 2010 88 `````` axiom Div_sign_pos: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 89 `````` forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0 `````` MARCHE Claude committed Oct 07, 2010 90 91 `````` axiom Div_sign_neg: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 92 `````` forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0 `````` MARCHE Claude committed Oct 07, 2010 93 `````` `````` MARCHE Claude committed Jul 05, 2010 94 `````` axiom Mod_sign_pos: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 95 `````` forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0 `````` MARCHE Claude committed Jul 05, 2010 96 97 `````` axiom Mod_sign_neg: `````` Jean-Christophe Filliâtre committed Apr 18, 2011 98 `````` forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0 `````` MARCHE Claude committed Jul 05, 2010 99 100 101 `````` lemma Rounds_toward_zero: forall x y:int. y <> 0 -> abs (div x y * y) <= abs x `````` MARCHE Claude committed Mar 26, 2010 102 `````` `````` MARCHE Claude committed Mar 16, 2011 103 104 `````` lemma Div_1: forall x:int. div x 1 = x `````` Andrei Paskevich committed Jun 21, 2010 105 `````` lemma Mod_1: forall x:int. mod x 1 = 0 `````` MARCHE Claude committed Mar 26, 2010 106 `````` `````` MARCHE Claude committed Mar 16, 2011 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 `````` Jean-Christophe Filliâtre committed Jun 21, 2011 111 `````` lemma Div_mult: forall x y z:int [div (x * y + z) x]. `````` Jean-Christophe Filliâtre committed Apr 18, 2011 112 `````` x > 0 /\ y >= 0 /\ z >= 0 -> `````` MARCHE Claude committed Mar 16, 2011 113 114 `````` div (x * y + z) x = y + div z x `````` Jean-Christophe Filliâtre committed Jun 21, 2011 115 `````` lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. `````` Jean-Christophe Filliâtre committed Apr 18, 2011 116 `````` x > 0 /\ y >= 0 /\ z >= 0 -> `````` MARCHE Claude committed Mar 16, 2011 117 `````` mod (x * y + z) x = mod z x `````` MARCHE Claude committed Mar 26, 2010 118 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 119 120 ``````end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 121 ``````theory Exponentiation `````` Jean-Christophe Filliâtre committed Jun 25, 2010 122 123 `````` use import Int `````` Jean-Christophe Filliâtre committed Apr 08, 2011 124 `````` type t `````` Andrei Paskevich committed Jun 29, 2011 125 126 `````` function one : t function (*) t t : t `````` Jean-Christophe Filliâtre committed Jun 21, 2011 127 `````` `````` Andrei Paskevich committed Jun 29, 2011 128 `````` function power t int : t `````` Jean-Christophe Filliâtre committed Apr 08, 2011 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 `````` Andrei Paskevich committed Oct 26, 2010 133 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 134 135 136 ``````end theory Power `````` Jean-Christophe Filliâtre committed Jan 24, 2011 137 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 138 139 `````` use import Int `````` Jean-Christophe Filliâtre committed Jun 21, 2011 140 `````` clone export `````` Andrei Paskevich committed Jun 29, 2011 141 `````` Exponentiation with type t = int, function one = one, function (*) = (*) `````` Jean-Christophe Filliâtre committed Jan 24, 2011 142 `````` `````` Jean-Christophe Filliâtre committed Jan 25, 2011 143 144 `````` lemma Power_1 : forall x : int. power x 1 = x `````` Jean-Christophe Filliâtre committed Jan 24, 2011 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 `````` Jean-Christophe Filliâtre committed Jun 25, 2010 150 151 152 `````` end `````` 153 154 155 ``````theory NumOfParam type param `````` Jean-Christophe Filliâtre committed Jun 25, 2010 156 157 158 `````` use import Int `````` Andrei Paskevich committed Jun 29, 2011 159 `````` predicate pr param int `````` Jean-Christophe Filliâtre committed Jun 25, 2010 160 `````` `````` MARCHE Claude committed Apr 06, 2011 161 `````` (** number of [n] such that [a <= n < b] and [pr(p,n)] *) `````` Andrei Paskevich committed Jun 29, 2011 162 `````` function num_of (p : param) (a b : int) : int `````` Jean-Christophe Filliâtre committed Jun 25, 2010 163 `````` `````` MARCHE Claude committed Oct 19, 2010 164 165 `````` axiom Num_of_empty : forall p : param, a b : int. `````` 166 167 `````` b <= a -> num_of p a b = 0 `````` MARCHE Claude committed Oct 19, 2010 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 committed Oct 19, 2010 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 committed Apr 06, 2011 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 committed Oct 19, 2010 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 committed Apr 06, 2011 182 `````` (* by induction on c *) `````` Jean-Christophe Filliâtre committed Jun 25, 2010 183 `````` `````` MARCHE Claude committed Apr 06, 2011 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 : `````` Jean-Christophe Filliâtre committed Jul 04, 2010 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 committed Apr 06, 2011 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 *) `````` Jean-Christophe Filliâtre committed Jul 04, 2010 202 `````` `````` Jean-Christophe committed Apr 04, 2011 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 committed Apr 06, 2011 206 `````` (* by Num_of_append and num_of_increasing *) `````` Jean-Christophe committed Apr 04, 2011 207 `````` `````` Jean-Christophe Filliâtre committed Jun 25, 2010 208 209 ``````end `````` 210 ``````theory NumOf `````` Jean-Christophe Filliâtre committed Jun 25, 2010 211 `````` `````` Andrei Paskevich committed Jun 29, 2011 212 `````` predicate pr int `````` Jean-Christophe Filliâtre committed Jun 25, 2010 213 `````` `````` Andrei Paskevich committed Jun 29, 2011 214 `````` predicate pr0 () (n : int) = pr n `````` Jean-Christophe Filliâtre committed Jun 25, 2010 215 `````` `````` Andrei Paskevich committed Jun 29, 2011 216 `````` clone NumOfParam as N with type param = tuple0, predicate pr = pr0 `````` Jean-Christophe Filliâtre committed Jun 25, 2010 217 `````` `````` Andrei Paskevich committed Jun 29, 2011 218 `````` function num_of (a b : int) : int = N.num_of () a b `````` Jean-Christophe Filliâtre committed Jun 25, 2010 219 220 `````` end `````` Jean-Christophe Filliâtre committed Aug 18, 2010 221 `````` `````` Jean-Christophe Filliâtre committed Aug 03, 2011 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 `````` Jean-Christophe Filliâtre committed Aug 05, 2011 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 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 250 ``````theory Induction `````` Jean-Christophe Filliâtre committed Aug 05, 2011 251 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 252 253 `````` use import Int `````` Andrei Paskevich committed Jun 29, 2011 254 `````` predicate p int `````` Jean-Christophe Filliâtre committed Apr 08, 2011 255 `````` `````` MARCHE Claude committed Apr 10, 2011 256 `````` lemma Induction : `````` Jean-Christophe Filliâtre committed Apr 08, 2011 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 committed Jun 29, 2011 260 `````` function bound : int `````` MARCHE Claude committed Apr 10, 2011 261 262 `````` lemma Induction_bound : `````` Jean-Christophe Filliâtre committed Jun 21, 2011 263 `````` (forall n:int. bound <= n -> `````` MARCHE Claude committed Apr 10, 2011 264 265 266 `````` (forall k:int. bound <= k < n -> p k) -> p n) -> forall n:int. bound <= n -> p n `````` Jean-Christophe Filliâtre committed Apr 08, 2011 267 268 ``````end `````` Jean-Christophe Filliâtre committed Aug 18, 2010 269 ``````(* `````` MARCHE Claude committed Oct 19, 2010 270 ``````Local Variables: `````` Jean-Christophe Filliâtre committed Jan 24, 2011 271 ``````compile-command: "make -C .. theories/int.gui" `````` MARCHE Claude committed Oct 19, 2010 272 ``````End: `````` Jean-Christophe Filliâtre committed Aug 18, 2010 273 ``*)``