pvs-common.gen 7.39 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
(*transformation "simplify_recursive_definition"*)
13
(* though we could do better, we only use recursion on one argument *)
14 15
transformation "eliminate_non_struct_recursion"

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

transformation "simplify_formula"

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

28 29 30 31
theory map.Map
  syntax type  map "[%1 -> %2]"

  syntax function get "%1(%2)"
32 33 34 35
  syntax function ([]) "%1(%2)"

  syntax function set    "(%1 WITH [(%2) |-> %3])"
  syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
36 37 38 39

  remove prop Select_eq
  remove prop Select_neq

40
  syntax function const "(LAMBDA (x:%v0): %1)"
41 42 43
  remove prop Const
end

44
theory Bool
45 46 47 48
  syntax type bool   "bool"

  syntax function True  "TRUE"
  syntax function False "FALSE"
49 50 51
end

theory bool.Bool
52 53 54 55 56

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

end

theory int.Int

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

66 67 68 69
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function ( * ) "(%1 * %2)"
  syntax function (-_)  "(-%1)"
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112

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

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  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

113 114
  syntax function zero "0"
  syntax function one  "1"
115

116 117 118 119
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function (-_)  "(-%1)"
  syntax function ( * ) "(%1 * %2)"
120
(*
121 122
  syntax function ( / ) "(%1 / %2)"
  syntax function inv   "(1 / %1)"
123
*)
124

125 126 127 128
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  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

153 154 155 156 157 158 159 160 161 162
theory real.MinMax
  syntax function min "min(%1, %2)"
  syntax function max "max(%1, %2)"

  remove prop Max_is_ge
  remove prop Max_is_some
  remove prop Min_is_le
  remove prop Min_is_some
end

163 164
theory real.RealInfix

165 166 167 168
  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function (-._) "(-%1)"
  syntax function ( *.) "(%1 * %2)"
169
  (* syntax function (/.)  "(%1 / %2)" *)
170

171 172 173 174
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"
175 176 177 178 179

end

theory real.Abs

180
  syntax function abs "abs(%1)"
181 182 183 184 185 186 187 188

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

189
  syntax function from_int "(%1 :: real)"
190 191 192 193 194 195 196 197 198 199

  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
200 201 202 203 204 205 206 207 208 209 210
theory real.PowerReal

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

  remove prop Pow_x_zero
  remove prop Pow_x_one
  remove prop Pow_one_y

end

(***
211 212
theory real.Square

213
  syntax function sqrt "SQRT(%1)"
214 215 216 217 218

end

theory real.ExpLog

219 220
  syntax function exp "EXP(%1)"
  syntax function log "LOG(%1)"
221 222 223 224 225

end

theory real.Trigonometry

226 227
  syntax function cos "COS(%1)"
  syntax function sin "SIN(%1)"
228 229 230

  syntax function pi "PI"

231
  syntax function tan "TAN(%1)"
232 233

end
Jean-Christophe's avatar
Jean-Christophe committed
234
***)
Jean-Christophe's avatar
Jean-Christophe committed
235

236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
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]"

  syntax function Nil  "null"
  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)"
Jean-Christophe's avatar
Jean-Christophe committed
260
  
261 262 263 264 265 266 267 268 269 270 271 272 273
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
274 275 276
  (* FIXME? the following are not part of PVS prelude *)
  remove prop mem_append
  remove prop mem_decomp
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
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)"
  remove prop      empty_def1

  syntax function add "add(%1, %2)"
  remove prop     add_def1
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
  remove prop     remove_def1
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
  remove prop     union_def1

  syntax function inter "intersection(%1, %2)"
  remove prop     inter_def1

  syntax function diff "difference(%1, %2)"
  remove prop     diff_def1
  remove prop     subset_diff

  (* TODO: choose *)

  syntax function all "fullset"
  remove prop     all_def
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)"
  remove prop      empty_def1

  syntax function add "add(%1, %2)"
  remove prop     add_def1
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
  remove prop     remove_def1
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
  remove prop     union_def1

  syntax function inter "intersection(%1, %2)"
  remove prop     inter_def1

  syntax function diff "difference(%1, %2)"
  remove prop     diff_def1
  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
364 365 366
(* this file has an extension .aux rather than .gen
   since it should not be distributed *)
import "pvs-realizations.aux"