1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
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
260
261
262
263
264
265
266
267
268
269
|
(* Why driver for Mathematica *)
prelude "(* this is a prelude for Mathematica *)"
printer "mathematica"
filename "%f-%t-%g.m"
valid "\\bTrue\\b"
unknown "\\bFalse\\b" "\\bFalse\\b"
time "why3cpulimit time : %s s"
(* Performed introductions depending on whether counterexamples are
requested, as said by the meta "get_counterexmp". When this meta
set, this transformation introduces the model variables that are
still embedded in the goal. When it is not set, it removes all
these unused-ce-related variables, even in the context. *)
transformation "counterexamples_dependent_intros"
transformation "inline_trivial"
transformation "inline_all"
transformation "eliminate_builtin"
(*transformation "eliminate_definition"*)
(*transformation "eliminate_recursion"*)
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_if"*)
transformation "eliminate_epsilon"
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
transformation "eliminate_literal"
transformation "eliminate_let"
(*transformation "split_premise"*)
transformation "simplify_formula"
(*transformation "simplify_unknown_lsymbols"*)
transformation "simplify_trivial_quantification"
(*transformation "introduce_premises"*)
(*transformation "instantiate_predicate"*)
(*transformation "abstract_unknown_lsymbols"*)
theory BuiltIn
syntax type int "Integers"
syntax type real "Reals"
syntax predicate (=) "(%1 == %2)"
meta "encoding:kept" type int
end
(* int *)
theory int.Int
prelude "(* this is a prelude for Mathematica integer arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop 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
meta "encoding:kept" type int
end
theory int.Abs
syntax function abs "Abs[%1]"
end
theory int.EuclideanDivision
syntax function div "Quotient[%1, %2]"
syntax function mod "Mod[%1, %2]"
remove prop Mod_bound
remove prop Div_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
meta "encoding:kept" type int
end
(* real *)
theory real.Real
prelude "(* this is a prelude for Mathematica real arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1 / %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
remove prop add_div
remove prop sub_div
remove prop neg_div
remove prop assoc_mul_div
remove prop assoc_div_mul
remove prop assoc_div_div
remove prop CompatOrderMult
(*meta "encoding:kept" type real*)
end
theory real.Abs
syntax function abs "Abs[%1]"
end
theory real.MinMax
syntax function min "Min[%1, %2]"
syntax function max "Max[%1, %2]"
end
theory real.Square
syntax function sqr "Power[%1,2]"
syntax function sqrt "Sqrt[%1]"
end
theory real.ExpLog
syntax function exp "Exp[%1]"
syntax function e "E"
syntax function log "Log[%1]"
syntax function log2 "Log[2, %1]"
syntax function log10 "Log[10, %1]"
remove prop Exp_zero
remove prop Exp_sum
remove prop Log_one
remove prop Log_mul
remove prop Log_exp
remove prop Exp_log
end
theory real.PowerInt
syntax function power "Power[%1, %2]"
end
theory real.PowerReal
syntax function pow "Power[%1, %2]"
end
theory real.Trigonometry
syntax function cos "Cos[%1]"
syntax function sin "Sin[%1]"
syntax function tan "Tan[%1]"
syntax function atan "ArcTan[%1]"
syntax function pi "Pi"
end
theory real.Hyperbolic
syntax function sinh "Sinh[%1]"
syntax function cosh "Cosh[%1]"
syntax function tanh "Tanh[%1]"
syntax function asinh "ArcSinh[%1]"
syntax function acosh "ArcCosh[%1]"
syntax function atanh "ArcTanh[%1]"
end
theory real.FromInt
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory Bool
syntax type bool "Bool"
syntax function True "True"
syntax function False "False"
meta "encoding:kept" type bool
end
theory bool.Bool
syntax function andb "(%1 && %2)"
syntax function orb "(%1 || %2)"
syntax function xorb "Xor[%1, %2]"
syntax function notb "(! %1)"
syntax function implb "Implies[%1, %2]"
end
|
