pvs-common.gen 7.41 KB
Newer Older
1

Jean-Christophe's avatar
Jean-Christophe committed
2 3 4
unknown "unfinished" "\"\\0\""
unknown "untried" "\"\\0\""
valid "succeeded"
5 6
time "why3cpulimit time : %s s"

7
(*transformation "inline_trivial"*)
8
transformation "eliminate_builtin"
9 10

(* PVS does not support mutual recursion *)
11
transformation "eliminate_mutual_recursion"
12
(* though we could do better, we only use recursion on one argument *)
13 14
transformation "eliminate_non_struct_recursion"

15 16
transformation "eliminate_epsilon"

17
(* PVS only has simple patterns *)
18
transformation "compile_match"
19
transformation "eliminate_projections"
20 21 22 23 24 25 26 27 28

transformation "simplify_formula"

theory BuiltIn
  syntax type   int   "int"
  syntax type   real  "real"
  syntax predicate  (=)   "(%1 = %2)"
end

29 30 31 32 33
theory HighOrd
  syntax type (->) "[%1 -> %2]"
  syntax function (@) "%1(%2)"
end

34 35 36
theory map.Map

  syntax function get "%1(%2)"
37 38 39 40
  syntax function ([]) "%1(%2)"

  syntax function set    "(%1 WITH [(%2) |-> %3])"
  syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
41 42 43 44

  remove prop Select_eq
  remove prop Select_neq

MARCHE Claude's avatar
MARCHE Claude committed
45 46
end

47
theory Bool
48 49 50 51
  syntax type bool   "bool"

  syntax function True  "TRUE"
  syntax function False "FALSE"
52 53 54
end

theory bool.Bool
55 56 57 58 59

  syntax function andb  "(%1 AND %2)"
  syntax function orb   "(%1 OR %2)"
  syntax function xorb  "(%1 XOR %2)"
  syntax function notb  "(NOT %1)"
60
  syntax function implb "(%1 => %2)"
61 62 63 64 65 66 67 68

end

theory int.Int

  syntax function zero "0"
  syntax function one  "1"

69 70 71 72
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function ( * ) "(%1 * %2)"
  syntax function (-_)  "(-%1)"
73 74 75 76 77 78

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

79 80 81 82 83 84 85
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
86 87
  remove prop Mul_distr_l
  remove prop Mul_distr_r
88
  remove prop Comm
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 115 116 117
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne

end

theory int.Abs

  syntax function abs "abs(%1)"

  remove prop Abs_pos

end

theory int.MinMax

  syntax function min "min(%1, %2)"
  syntax function max "max(%1, %2)"

end

theory real.Real

118 119
  syntax function zero "0"
  syntax function one  "1"
120

121 122 123 124
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function (-_)  "(-%1)"
  syntax function ( * ) "(%1 * %2)"
125
  (* / and inv are defined in the realization *)
126

127 128 129 130
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
131

132 133 134 135 136 137 138
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
139 140
  remove prop Mul_distr_l
  remove prop Mul_distr_r
141
  remove prop Comm
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
  remove prop Unitary
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div

end

158 159 160 161
theory real.MinMax
  syntax function min "min(%1, %2)"
  syntax function max "max(%1, %2)"

162 163
  remove prop Max_l
  remove prop Min_r
164 165 166 167
  remove prop Max_comm
  remove prop Min_comm
  remove prop Max_assoc
  remove prop Min_assoc
168 169
end

170 171
theory real.RealInfix

172 173 174 175
  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function (-._) "(-%1)"
  syntax function ( *.) "(%1 * %2)"
176 177
  syntax function (/.)  "real@Real.infix_sl(%1, %2)"
  syntax function inv   "real@Real.inv(%1)"
178

179 180 181 182
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"
183 184 185 186 187

end

theory real.Abs

188
  syntax function abs "abs(%1)"
189 190 191 192 193 194 195 196

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

197
  syntax function from_int "(%1 :: real)"
198 199 200 201 202 203 204 205 206 207

  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

end

Jean-Christophe's avatar
Jean-Christophe committed
208 209 210 211 212 213 214 215 216 217 218
theory real.PowerReal

  syntax function pow "(%1 ^ %2)"

  remove prop Pow_x_zero
  remove prop Pow_x_one
  remove prop Pow_one_y

end

(***
219 220
theory real.Square

221
  syntax function sqrt "SQRT(%1)"
222 223 224 225 226

end

theory real.ExpLog

227 228
  syntax function exp "EXP(%1)"
  syntax function log "LOG(%1)"
229 230 231 232 233

end

theory real.Trigonometry

234 235
  syntax function cos "COS(%1)"
  syntax function sin "SIN(%1)"
236 237 238

  syntax function pi "PI"

239
  syntax function tan "TAN(%1)"
240 241

end
Jean-Christophe's avatar
Jean-Christophe committed
242
***)
Jean-Christophe's avatar
Jean-Christophe committed
243

244 245 246 247 248 249 250 251 252 253 254
theory option.Option
  syntax type option "lift[%1]"

  syntax function None "bottom"
  syntax function Some "up(%1)"
end

theory list.List

  syntax type list "list[%1]"

255
  syntax function Nil  "(null :: %t0)"
256 257 258 259 260 261 262 263 264 265 266 267
  syntax function Cons "cons(%1, %2)"

end

theory list.Length
  syntax function length "length(%1)"
  remove prop Length_nonnegative
  remove prop Length_nil
end

theory list.Mem
  syntax predicate mem "member(%1, %2)"
268

269 270 271 272 273 274 275 276 277 278 279 280 281
end

theory list.Nth
  syntax function nth
    "IF 0 <= %1 AND %1 < length(%2) THEN up(nth(%2, %1)) ELSE bottom ENDIF"
end

theory list.Append
  syntax function (++) "append(%1, %2)"

  remove prop Append_assoc
  remove prop Append_l_nil
  remove prop Append_length
Jean-Christophe's avatar
Jean-Christophe committed
282 283 284
  (* FIXME? the following are not part of PVS prelude *)
  remove prop mem_append
  remove prop mem_decomp
285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
end

theory list.Reverse
  syntax function reverse "reverse(%1)"
end

theory set.Set
  syntax type set "set[%1]"

  syntax predicate mem "member(%1, %2)"
  remove prop      extensionality

  syntax predicate subset "subset?(%1, %2)"
  remove prop      subset_trans

  syntax function  empty    "(emptyset :: %t0)"
  syntax predicate is_empty "empty?(%1)"
302
  remove prop      empty_def
303 304

  syntax function add "add(%1, %2)"
305
  remove prop     add_def
306 307 308
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
309
  remove prop     remove_def
310 311 312
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
313
  remove prop     union_def
314 315

  syntax function inter "intersection(%1, %2)"
316
  remove prop     inter_def
317 318

  syntax function diff "difference(%1, %2)"
319
  remove prop     diff_def
320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337
  remove prop     subset_diff

  (* TODO: choose *)

  syntax function all "fullset"
end

theory set.Fset
  syntax type set "finite_set[%1]"

  syntax predicate mem "member(%1, %2)"
  remove prop      extensionality

  syntax predicate subset "subset?(%1, %2)"
  remove prop      subset_trans

  syntax function  empty    "(emptyset :: %t0)"
  syntax predicate is_empty "empty?(%1)"
338
  remove prop      empty_def
339 340

  syntax function add "add(%1, %2)"
341
  remove prop     add_def
342 343 344
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
345
  remove prop     remove_def
346 347 348
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
349
  remove prop     union_def
350 351

  syntax function inter "intersection(%1, %2)"
352
  remove prop     inter_def
353 354

  syntax function diff "difference(%1, %2)"
355
  remove prop     diff_def
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
  remove prop     subset_diff

  (* TODO: choose *)

  syntax function cardinal "Card(%1)"
  remove prop     cardinal_nonneg
  remove prop     cardinal_empty
  remove prop     cardinal_add
  remove prop     cardinal_remove
  remove prop     cardinal_subset
  remove prop     cardinal1

  (* TODO: nth *)
end

Jean-Christophe's avatar
Jean-Christophe committed
371 372 373
(* this file has an extension .aux rather than .gen
   since it should not be distributed *)
import "pvs-realizations.aux"