IEEE_connectionScript.sml 34.2 KB
Newer Older
1
2
open preamble

3
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
4

5
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics CertificateCheckerTheory
6
open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
7

8
val _ = new_theory "IEEE_connection";
9

Heiko Becker's avatar
Heiko Becker committed
10
11
val _ = temp_overload_on("abs",``real$abs``);

Heiko Becker's avatar
Heiko Becker committed
12
val dmode_def = Define `dmode = roundTiesToEven`;
13

14
val eval_exp_float_def = Define `
Heiko Becker's avatar
Heiko Becker committed
15
16
  (eval_exp_float (Var n) E = E n) /\
  (eval_exp_float (Const m v) E = SOME v) /\
17
18
19
20
21
  (eval_exp_float (Unop Neg e) E =
    case eval_exp_float e E of
      | SOME v => SOME (fp64_negate v)
      | _ => NONE) /\
  (eval_exp_float (Unop Inv e) E = NONE) /\
Heiko Becker's avatar
Heiko Becker committed
22
23
  (eval_exp_float (Binop b e1 e2) E =
    (case (eval_exp_float e1 E), (eval_exp_float e2 E) of
24
       | SOME v1, SOME v2 =>
Heiko Becker's avatar
Heiko Becker committed
25
26
27
28
29
          (case b of
             | Plus => SOME (fp64_add dmode v1 v2)
             | Sub => SOME (fp64_sub dmode v1 v2)
             | Mult => SOME (fp64_mul dmode v1 v2)
             | Div => SOME (fp64_div dmode v1 v2))
30
31
       | _, _ => NONE) /\
  (eval_exp_float (Downcast m e) E = NONE))`;
32
33
34
35
36
37
38
39
40
41
42
43
44
45

val toRExp_def = Define `
  (toRExp ((Var v):word64 exp) = Var v) /\
  (toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\
  (toRExp (Unop u e1) = Unop u (toRExp e1)) /\
  (toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\
  (toRExp (Downcast m e1) = Downcast m (toRExp e1))`;

val toREnv_def = Define `
  toREnv (E:num -> word64 option) (x:num):real option =
    case E x of
      | NONE => NONE
      | SOME v => SOME (float_to_real (fp64_to_float v))`;

Heiko Becker's avatar
Heiko Becker committed
46
47
48
49
50
val toWordEnv_def = Define `
  toWordEnv E = \x. case E x of
                      | SOME v => SOME (float_to_fp64 (real_to_float dmode v))
                      | NONE => NONE`;

51
52
53
54
55
56
57
val Binop_to_Rop_def = Define `
  Binop_to_Rop (b:binop) :real->real->real =
    case b of
      | Plus => $+
      | Sub => $-
      | Mult => $*
      | Div => $/ `;
58

59
60
61
62
val f64_plus_preserves_finite = store_thm ("f64_plus_preserves_finite",
  ``!f1 f2.
      fp64_isFinite (fp64_add dmode f1 f2) ==>
      fp64_isFinite f1 /\ fp64_isFinite f2 ``,
Heiko Becker's avatar
Heiko Becker committed
63
64
65
66
  rw [fp64_isFinite_def, fp64_add_def, fp64_to_float_float_to_fp64,
      float_add_def, float_is_finite_def]
  \\ Cases_on `float_value (fp64_to_float f1)`
  \\ Cases_on `float_value (fp64_to_float f2)`
67
68
69
70
71
72
  \\ fs [float_values]);

val f64_sub_preserves_finite = store_thm ("f64_plus_preserves_finite",
  ``!f1 f2.
      fp64_isFinite (fp64_sub dmode f1 f2) ==>
      fp64_isFinite f1 /\ fp64_isFinite f2 ``,
Heiko Becker's avatar
Heiko Becker committed
73
74
  rw [fp64_isFinite_def, fp64_sub_def, fp64_to_float_float_to_fp64,
      float_sub_def, float_is_finite_def]
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
  \\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
  \\ fs [float_values]
  \\ Cases_on `float_value (float_negate (fp64_to_float f2))`
  \\ fs [float_values]
  \\ `(fp64_to_float f2).Exponent = UINT_MAXw`
    by (fs [float_value_def]
        \\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
        \\ Cases_on `(fp64_to_float f2).Significand = 0w`
        \\ fs [])
  \\ `(fp64_to_float f2).Significand = 0w`
    by (fs [float_value_def]
        \\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
        \\ Cases_on `(fp64_to_float f2).Significand = 0w`
        \\ fs [])
  \\ fs [float_negate_def, float_value_def]);

val f64_mul_preserves_finite = store_thm ("f64_plus_preserves_finite",
  ``!f1 f2.
      fp64_isFinite (fp64_mul dmode f1 f2) ==>
      fp64_isFinite f1 /\ fp64_isFinite f2 ``,
Heiko Becker's avatar
Heiko Becker committed
95
96
  rw [fp64_isFinite_def, fp64_mul_def, fp64_to_float_float_to_fp64,
      float_mul_def, float_is_finite_def]
97
98
99
100
101
102
103
104
105
106
  \\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
  \\ fs [float_values]
  \\ Cases_on `r = 0`
  \\ fs [float_values]);

val f64_div_preserves_finite = store_thm ("f64_plus_preserves_finite",
  ``!f1 f2.
      fp64_isFinite (fp64_div dmode f1 f2) /\
      (float_value (fp64_to_float f2) = Infinity ==> F)==>
      fp64_isFinite f1 /\ fp64_isFinite f2 ``,
Heiko Becker's avatar
Heiko Becker committed
107
108
  rw [fp64_isFinite_def, fp64_div_def, fp64_to_float_float_to_fp64,
      float_div_def, float_is_finite_def]
109
110
111
112
113
  \\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
  \\ fs [float_values]
  \\ Cases_on `r = 0`
  \\ fs [float_values]);

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
val threshold_64_bit_lt_maxValue = store_thm ("threshold_64_bit_lt_maxValue",
  ``maxValue M64 < threshold (:52 # 11)``,
  fs[threshold_def, maxValue_def, maxExponent_def]
  \\ once_rewrite_tac [GSYM REAL_MUL_RID]
  \\ once_rewrite_tac [GSYM REAL_MUL_ASSOC]
  \\ irule REAL_LT_LMUL_IMP
  \\ fs[]
  \\ once_rewrite_tac [real_sub]
  \\ once_rewrite_tac [GSYM REAL_LT_ADDNEG2]
  \\ once_rewrite_tac [REAL_NEGNEG]
  \\ once_rewrite_tac [RealArith.REAL_ARITH ``2:real = 1+1``]
  \\ irule REAL_LT_IADD
  \\ once_rewrite_tac [GSYM REAL_INV1]
  \\ irule REAL_LT_INV \\ fs[]);

val normalValue_implies_normalization = store_thm ("validFloatValue_implies_normalization",
  ``!v.
      normal v M64 ==>
      normalizes (:52 #11) v``,
  rpt strip_tac
  \\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_def,
        minExponentPos_def, wordsTheory.INT_MIN_def, wordsTheory.dimindex_11,
        wordsTheory.UINT_MAX_def, wordsTheory.dimword_11]
  \\ irule REAL_LET_TRANS
  \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);

val normalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
  ``!v.
      normal v M64 ==>
      float_is_finite ((real_to_float dmode v):(52 , 11) float)``,
  rpt strip_tac
  \\ fs [real_to_float_def, normal_def, dmode_def]
  \\ irule float_round_finite
  \\ irule REAL_LET_TRANS
  \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);

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
val normal_value_is_float_value = store_thm (
  "normal_value_is_float_value",
  ``!ff.
      normal (float_to_real ((ff):(52,11) float)) M64 ==>
      float_value ff = Float (float_to_real ff)``,
  rpt strip_tac
  \\rewrite_tac[float_value_def]
  \\rw_thm_asm `normal _ _` normal_def
  \\fs[float_to_real_def]
  \\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_def, minExponentPos_def]
   >-( Cases_on `ff.Sign` \\ fs[]
  \\ Cases_on `n` \\ fs[]
  \\ Cases_on `n'` \\ fs[])
  >- (Cases_on `ff.Sign` \\ fs[]
      \\ Cases_on `n` \\ fs[]
      \\ TRY (Cases_on `n'` \\ fs[])
      \\ Cases_on `ff.Significand` \\ fs[]
      \\ Cases_on `n` \\ fs[]
      \\ qpat_x_assum `abs _ <= _` MP_TAC
      \\ qmatch_abbrev_tac `abs (cst1 * cst2) <= cst3 ==> _`
      \\ strip_tac
      >- (`abs (cst1 * cst2) = cst1 * cst2`
             by (once_rewrite_tac[ABS_REFL]
                 \\ irule REAL_LE_MUL
                 \\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
                 \\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
                 \\ fs[]
                 \\ irule REAL_LE_ADD \\ fs[]
                 \\ irule REAL_LE_MUL \\ fs[]
                 \\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
          \\ rw_asm_star `abs _ = _`
          \\ `cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
          \\ irule REAL_LE_TRANS
          \\ qexists_tac `cst1 * cst2` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1:real = cst1 * 1``]
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1 * cst2 * 1 = cst1 * cst2:real``]
          \\ irule REAL_LE_LMUL_IMP
          \\ unabbrev_all_tac \\ fs[]
          \\ once_rewrite_tac [REAL_LE_ADDR]
          \\ once_rewrite_tac [real_div]
          \\ irule REAL_LE_MUL \\ fs[]
          \\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[])
     \\ `abs (cst1 * cst2) = -(cst1 * cst2)`
             by (once_rewrite_tac[abs]
                 \\ `~ (0 <= cst1 * cst2)` suffices_by (fs[] )
                 \\ unabbrev_all_tac
                 \\ once_rewrite_tac [REAL_MUL_LNEG]
                 \\ fs[]
                 \\ qmatch_abbrev_tac `~ (cst1 * cst2 <= 0:real)`
                 \\ once_rewrite_tac [REAL_NOT_LE]
                 \\ irule REAL_LT_MUL
                 \\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
                 \\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
                 \\ irule REAL_LT_ADD \\ fs[]
                 \\ irule REAL_LT_MUL \\ fs[]
                 \\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
          \\ rw_asm_star `abs _ = _`
          \\ `- cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
          \\ irule REAL_LE_TRANS
          \\ qexists_tac `- (cst1 * cst2)` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``-cst1:real = -cst1 * 1``]
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``- (cst1 * cst2) * 1 = - cst1 * cst2:real``]
          \\ irule REAL_LE_LMUL_IMP
          \\ unabbrev_all_tac \\ fs[]
          \\ once_rewrite_tac [REAL_LE_ADDR]
          \\ once_rewrite_tac [real_div]
          \\ irule REAL_LE_MUL \\ fs[]
          \\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[]));

Heiko Becker's avatar
Heiko Becker committed
219
220
221
222
223
224
225
226
227
val validValue_gives_float_value = store_thm ("validValue_gives_float_value",
  ``!ff:(52,11) float.
      validFloatValue (float_to_real ff) M64 ==>
      float_value ff = Float (float_to_real ff)``,
  rpt strip_tac \\ fs[validFloatValue_def]
  >- (irule normal_value_is_float_value \\ fs[])
  \\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
  \\ every_case_tac \\ fs[]);

228
229
230
231
232
233
234
235
236
val normalTranslatedValue_implies_finiteness = store_thm ("normalTranslatedValue_implies_finiteness",
  ``!ff:double.
      normal (float_to_real ff) M64 ==>
      float_is_finite ff``,
  rpt strip_tac
  \\ fs[float_is_finite_def]
  \\ qspec_then `ff` impl_subgoal_tac normal_value_is_float_value
  \\ fs[]);

237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
val zero_value_implies_finiteness = store_thm ("zero_value_implies_finiteness",
  ``!v. v= 0 ==> float_is_finite ((real_to_float dmode v))``,
  rpt strip_tac \\ rveq
  \\ fs[real_to_float_def, dmode_def]
  \\ irule float_round_finite
  \\ fs[threshold_is_positive]
);

val validFPRanges_implies_finiteness = store_thm ("validFPRanges_gives_finiteness",
  ``!v.
      validFloatValue v M64 ==>
      fp64_isFinite (float_to_fp64 (real_to_float dmode v))``,
  rpt strip_tac
  \\ fs[validFloatValue_def, fp64_isFinite_def, fp64_to_float_float_to_fp64,
        zero_value_implies_finiteness, normalValue_implies_finiteness]);
252

Heiko Becker's avatar
Heiko Becker committed
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
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
val finite_float_implies_threshold = Q.prove (
  `!f:(α , β) float.
      float_is_finite f ==>
      ~(float_to_real f  -threshold (:α # β)) /\
      ~(float_to_real f  threshold (:α # β)) `,
  rpt strip_tac
  \\ drule lift_ieeeTheory.float_to_real_threshold
  \\ simp[realTheory.abs]
  \\ every_case_tac
  \\ strip_tac \\ RealArith.REAL_ASM_ARITH_TAC);

val round_float_to_real_id = Q.prove(
  `!f.
     float_is_finite f /\
     float_is_normal f /\
     ~ float_is_zero f ==>
     round roundTiesToEven (float_to_real f) = f`,
  rw[]
  \\ qpat_assum `float_is_finite _` mp_tac
  \\ qpat_assum `float_is_normal _` mp_tac
  \\ rewrite_tac [float_is_finite_def, float_is_normal_def]
  \\ rewrite_tac [float_value_def]
  \\ simp[]
  \\ strip_tac
  \\ once_rewrite_tac [round_def]
  \\ fs[finite_float_implies_threshold]
  \\ once_rewrite_tac [closest_such_def]
  \\ SELECT_ELIM_TAC
  \\ rw[]
  >- (qexists_tac `f`
      \\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS]
      \\ Cases_on `f = b` \\ fs[]
      \\ first_x_assum (qspec_then `f` mp_tac)
      \\ fs[realTheory.REAL_SUB_REFL]
      \\ strip_tac
      \\ fs[float_to_real_eq]
      \\ rfs[])
  \\ CCONTR_TAC
  \\ fs[is_closest_def, IN_DEF]
  \\ qpat_x_assum `!x._ ` mp_tac
  \\ first_x_assum (qspec_then `f` mp_tac)
  \\ fs[realTheory.REAL_SUB_REFL]
  \\ rpt strip_tac
  \\ fs[float_to_real_eq]
  \\ rfs[]);

val real_to_float_id = Q.store_thm ("real_to_float_id",
  `!f.
     float_is_finite f /\
     float_is_normal f /\
     ~ float_is_zero f ==>
     real_to_float dmode (float_to_real f) = f`,
rpt strip_tac
\\ fs[dmode_def, real_to_float_def, float_round_def, round_float_to_real_id]);

308
val real_to_float_float_id = Q.prove (
Heiko Becker's avatar
Heiko Becker committed
309
310
311
312
313
  `!f.
     fp64_isFinite f /\
     fp64_isNormal f /\
     ~ fp64_isZero f ==>
     float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f`,
314
rpt strip_tac
Heiko Becker's avatar
Heiko Becker committed
315
316
317
\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
\\ fs[real_to_float_id]
\\ fs[float_to_fp64_fp64_to_float]);
318

319
320
321
322
323
324
325
326
val float_to_real_real_to_float_zero_id = store_thm ("float_to_real_real_to_float_zero_id",
  ``float_to_real (real_to_float roundTiesToEven 0) = 0``,
  once_rewrite_tac[real_to_float_def]
  \\ `float_round roundTiesToEven F 0 = (float_plus_zero(:α#β))`
       by  (irule round_roundTiesToEven_is_plus_zero
            \\ fs[ulp_def, ULP_def])
  \\ fs[float_to_real_def, float_plus_zero_def]);

Heiko Becker's avatar
Heiko Becker committed
327
328
329
330
331
332
333
334
335
val div_eq0_general = store_thm ("div_eq0_general",
  ``!a b:real. b <> 0 ==> (a / b = 0 <=> a = 0)``,
  rpt strip_tac \\ Cases_on `0 < b` \\ fs[div_eq0]
  \\ `0 < -b` by RealArith.REAL_ASM_ARITH_TAC
  \\ `a/ -b = 0 <=> a = 0` by fs[div_eq0]
  \\ fs[real_div]
  \\ Cases_on `a = 0` \\ fs[]
  \\ Cases_on `inv b = 0` \\ fs[REAL_INV_NZ]);

336
337
338
339
340
341
342
343
val float_to_real_round_zero_is_zero = store_thm (
  "float_to_real_round_zero_is_zero",
  ``!ff P.
      2 * abs ff <=  ulp ((:α#β) :(α#β) itself) ==>
      float_to_real ((float_round roundTiesToEven P ff):(α, β) float) = 0``,
  rpt strip_tac \\ Cases_on `P`
  \\ fs [round_roundTiesToEven_is_plus_zero,
         round_roundTiesToEven_is_minus_zero, zero_to_real]);
Heiko Becker's avatar
Heiko Becker committed
344

Heiko Becker's avatar
Heiko Becker committed
345
346
347
348
349
350
351
352
353
354
355
356
357
358
val noDowncast_def = Define `
  (noDowncast (Var v) = T) /\
  (noDowncast (Const _ _) = T) /\
  (noDowncast (Unop _ e) = noDowncast e) /\
  (noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
  (noDowncast (Downcast _ _) = F)`;

val is64BitEval_def = Define `
  (is64BitEval ((Const m c):real exp) = (m = M64)) /\
  (is64BitEval (Unop _ e) = is64BitEval e) /\
  (is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
  (is64BitEval (Downcast m e) = is64BitEval e) /\
  (is64BitEval ((Var v):real exp) = T)`;

Heiko Becker's avatar
Heiko Becker committed
359
360
361
val flushToZero_def = Define `
  flushToZero e E Gamma v m = (eval_exp e E Gamma v m /\ 0 <= abs v /\ abs v <= 0 (* FIXME *) ==> eval_exp e E Gamma 0 m)`;

Heiko Becker's avatar
Heiko Becker committed
362
363
364
365
366
367
368
369
370
371
372
373
374
375
val typeMap_eq_typeExp = Q.prove(`!e. typeMap Gamma e e = typeExpression Gamma e`,
Induct \\ fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] );

val typing_is_64bit = store_thm("typing_is_64bit",
  ``!e.
      noDowncast e /\ is64BitEval e /\ (!v. v IN domain(usedVars e) ==> Gamma v = SOME M64) ==>
      (typeMap Gamma e) e  = SOME M64``
Induct
\\ rpt strip_tac \\ simp[Once typeMap_def] \\ fs[is64BitEval_def, noDowncast_def]
>- (first_x_assum irule \\ fs[usedVars_def])
>- (fs [Once typeExpression_def]
    \\ first_x_assum irule
>- (

Heiko Becker's avatar
Heiko Becker committed
376
val bstep_gives_IEEE2 = store_thm ("bstep_gives_IEEE2",
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
  ``!(e:word64 exp) E1 E2 Gamma vR A P fVars dVars .
      typeCheck (toRExp e) Gamma (\_. SOME M64) /\
      approxEnv E1 Gamma A fVars dVars (toREnv E2) /\
      validIntervalbounds (toRExp e) A P dVars /\
      validErrorbound (toRExp e) (\_. SOME M64) A dVars /\
      FPRangeValidator (toRExp e) A (\_. SOME M64) /\
      eval_exp (toREnv E2) Gamma (toRExp e) vR M64 /\
      domain (usedVars (toRExp e)) DIFF domain dVars  domain fVars 
      (v.
        v  domain fVars 
        vR. E1 v = SOME vR  FST (P v)  vR  vR  SND (P v)) 
      (v. v  domain fVars  v  domain dVars  m. Gamma v = SOME m) 
      (v.
      v  domain dVars 
      vR.
      E1 v = SOME vR  FST (FST (A (Var v)))  vR 
                  vR  SND (FST (A (Var v)))) ==>
      ?v.
        eval_exp_float e E2 = SOME v /\
        eval_exp (toREnv E2) Gamma (toRExp e) (float_to_real (fp64_to_float v)) M64``,
Heiko Becker's avatar
Heiko Becker committed
397
  Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
398
  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
399
  \\ once_rewrite_tac [eval_exp_float_def]
400
  >- (once_rewrite_tac [toREnv_def]
401
      \\ fs[validFloatValue_def]
Heiko Becker's avatar
Heiko Becker committed
402
      \\ rveq
403
404
405
406
      \\ fs[eval_exp_cases, fp64_to_float_float_to_fp64, dmode_def,
            float_to_real_real_to_float_zero_id]
      \\ fs[toREnv_def]
      \\ Cases_on `E2 n` \\ fs[])
407
408
409
  >- (rveq \\ fs[eval_exp_cases]
      \\ once_rewrite_tac [fp64_to_float_def]
      \\ qexists_tac `0:real` \\ fs[perturb_def, mTypeToQ_pos])
Heiko Becker's avatar
Heiko Becker committed
410
  >- (simp [eval_exp_cases, eval_exp_float_def]
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
      \\ Cases_on `A (Unop u (toRExp e))`
      \\ Cases_on `u` \\ TRY (fs[eval_exp_float_def, Once validErrorbound_def] \\ FAIL_TAC "")
      \\ fs[eval_exp_float_def]
      \\ first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (rw_thm_asm `typeCheck _ _ _` typeCheck_def
          \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
          \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
          \\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
          \\ fs[]
          \\ Cases_on `A (Unop Neg (toRExp e))` \\ Cases_on ` A (toRExp e)` \\ fs[]
          \\ every_case_tac \\ fs[]
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ fs[])
      \\ fs[fp64_negate_def, fp64_to_float_float_to_fp64]
      \\ qexists_tac `float_to_real (fp64_to_float v)` \\ fs[]
      \\ fs[evalUnop_def, float_to_real_negate])
427
  >- (rename1 `Binop b (toRExp e1) (toRExp e2)`
428
429
430
431
432
433
434
435
436
437
438
439
440
441
      \\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
      \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ fs[]
      \\ `(\_. SOME M64) (toRExp e1) = SOME m1 /\ (\_. SOME M64) (toRExp e2) = SOME m2`
           by (conj_tac \\ irule typingSoundnessExp \\ fs[]
               \\ rpt (asm_exists_tac \\ fs[]))
      \\ `m1 = M64 /\ m2 = M64` by fs[]
      \\ rveq
      \\ ntac 2 (first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`] assume_tac))
      \\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
          \\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
          \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
          \\ Cases_on `A (toRExp e2)` \\ fs[]
442
          \\ fs[]
443
444
445
446
447
448
449
450
451
452
453
          \\ conj_tac
          >- (Cases_on `IVlo (widenInterval q r) = 0` \\ fs[])
          \\ conj_tac \\ fs[]
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
      \\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
          \\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
          \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
          \\ Cases_on `A (toRExp e2)` \\ fs[]
454
          \\ fs[]
455
456
457
458
459
          \\ conj_tac
          >- (Cases_on `IVlo (widenInterval q r) = 0` \\ fs[])
          \\ conj_tac \\ fs[]
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
Heiko Becker's avatar
Heiko Becker committed
460
      \\ fs[]
461
      \\ rename1 `eval_exp_float e1 _ = SOME vF1`
462
      \\ rename1 `eval_exp_float e2 _ = SOME vF2`
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
      \\ `?nR2. eval_exp E1 (toRMap Gamma) (toREval (toRExp e2)) nR2 M0 /\
             FST (FST (A (toRExp e2))) <= nR2 /\ nR2 <= SND (FST (A (toRExp e2)))`
           by (irule validIntervalbounds_sound
               \\ qexistsl_tac [`P`, `dVars`, `fVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ fs[]
               \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
               \\ fs [DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac \\ first_x_assum irule
               \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
      \\ `!vF2 m2. eval_exp (toREnv E2) Gamma (toRExp e2) vF2 m2 ==>
            abs (nR2 - vF2) <= SND (A (toRExp e2))`
            by (drule validErrorbound_sound
                \\ rpt (disch_then drule)
                \\ disch_then
                     (qspecl_then
                        [`nR2`, `SND (A (toRExp e2))`, `P`,
                         `FST (FST (A (toRExp e2)))`,
                         `SND (FST (A (toRExp e2))) `] destruct)
                \\ fs[]
                \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
                \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
                \\ Cases_on `A (Binop b (toRExp e1)(toRExp e2))`
                \\ fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
                \\ fs [DIFF_DEF, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule
                \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
      \\ `contained (float_to_real (fp64_to_float vF2)) (widenInterval (FST (FST (A (toRExp e2))), SND (FST (A (toRExp e2)))) (SND(A (toRExp e2))))`
           by (irule distance_gives_iv
               \\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
               \\ first_x_assum irule
               \\ qexists_tac `M64` \\ fs[])

      \\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
           by (strip_tac
               \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
               \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))`
               \\ Cases_on `A (toRExp e1)` \\ Cases_on `A (toRExp e2)`
               \\ rename1 `A (toRExp e2) = (iv_e2, err2)`
               \\ rveq
               \\ fs[IVhi_def, IVlo_def, widenInterval_def, contained_def]
               >- (CCONTR_TAC \\ fs[] \\ rveq
                   \\ `0 < 0:real`
                        by (irule REAL_LET_TRANS
                            \\ qexists_tac `SND iv_e2 + err2` \\ fs[])
                   \\ fs[])
               \\ CCONTR_TAC \\ fs[] \\ rveq
               \\ `0 < 0:real`
                    by (irule REAL_LTE_TRANS
                        \\ qexists_tac `FST iv_e2 - err2` \\ fs[])
               \\ fs[])
514
515
516
      \\ `validFloatValue
            (evalBinop b (float_to_real (fp64_to_float vF1))
             (float_to_real (fp64_to_float vF2))) M64`
517
                by (drule FPRangeValidator_sound
518
519
520
521
522
523
524
525
526
527
                    \\ disch_then
                         (qspecl_then
                            [`(Binop b (toRExp e1) (toRExp e2))`,
                             `evalBinop b (float_to_real (fp64_to_float vF1))
                                           (float_to_real (fp64_to_float vF2))`,
                             `M64`, `\_. SOME M64`, `P`] irule)
                    \\ fs[]
                    \\ qexistsl_tac [`P`, `e1`, `e2`]
                    \\ fs[]
                    \\ simp[typeCheck_def, eval_exp_cases]
528
                    \\ rewrite_tac [CONJ_ASSOC]
529
                    \\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
530
531
                    \\ qexists_tac `0:real`
                    \\ Cases_on `b` \\ fs[perturb_def, evalBinop_def, mTypeToQ_pos])
532
      \\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
533
534
535
536
537
538
           by (drule FPRangeValidator_sound
               \\ disch_then
                    (qspecl_then
                       [`toRExp e1`,
                        `float_to_real (fp64_to_float vF1)`,
                         `M64`, `\_. SOME M64`, `P`] irule)
539
               \\ fs[]
540
541
542
543
544
545
546
547
548
549
               \\ qexistsl_tac [`P`, `e1`] \\ fs[]
               \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
               \\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
               \\ Cases_on `A (toRExp e2)` \\ fs[]
               \\ conj_tac \\ fs[SUBSET_DEF, DIFF_DEF]
               >- (rpt strip_tac \\ first_x_assum irule
                   \\ simp[Once usedVars_def, domain_union] \\ fs[])
               \\ Cases_on `IVlo (widenInterval q r) = 0` \\ fs[])
550
      \\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
551
552
553
554
555
556
            by (drule FPRangeValidator_sound
               \\ disch_then
                    (qspecl_then
                       [`toRExp e2`,
                        `float_to_real (fp64_to_float vF2)`,
                         `M64`, `\_. SOME M64`, `P`] irule)
557
               \\ fs[]
558
559
560
561
562
563
564
565
566
567
568
               \\ qexistsl_tac [`P`, `e2`] \\ fs[]
               \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
               \\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
               \\ Cases_on `A (toRExp e2)` \\ fs[]
               \\ conj_tac \\ fs[SUBSET_DEF, DIFF_DEF]
               >- (rpt strip_tac \\ first_x_assum irule
                   \\ simp[Once usedVars_def, domain_union] \\ fs[])
               \\ Cases_on `IVlo (widenInterval q r) = 0` \\ fs[])
      \\ simp[eval_exp_cases]
Heiko Becker's avatar
Heiko Becker committed
569
      \\ Cases_on `b` \\ fs[]
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
      \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                       `float_to_real (fp64_to_float vF2)`] \\ fs[]
      \\ rw_thm_asm `validFloatValue (evalBinop _ _ _) M64` validFloatValue_def
      \\ fs[]
      >- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_add_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                     normalTranslatedValue_implies_finiteness,
                     normalValue_implies_normalization,
                     GSYM float_is_zero_to_real, float_is_finite])
           \\ fs[dmode_def]
           \\ rename1 `abs err <= _`
           \\ qexists_tac `err`
           \\ fs[perturb_def, evalBinop_def]
           \\ fs[mTypeToQ_def, join_def])
      >- (fs[REAL_LNEG_UNIQ, evalBinop_def]
590
591
592
593
594
          \\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
          \\ fs[float_add_def]
          \\ fs[join_def]
          \\ qexists_tac `0:real` \\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
          \\ fs[validFloatValue_def, normal_value_is_float_value, float_round_with_flags_def]
595
          >- (`2 * abs (0:real) <= ulp (:52 #11)`
596
                   by (fs[ulp_def, ULP_def])
597
              \\ fs [float_to_real_round_zero_is_zero])
598
599
600
          >- (`float_to_real (fp64_to_float vF1) = 0`
                 by (fs[])
              \\ fs[normal_def]
601
              \\ qpat_x_assum `0 = - float_to_real _` (fn thm => fs[GSYM thm])
602
603
604
605
              \\ `0 < 0:real` suffices_by (fs[])
              \\ irule REAL_LTE_TRANS
              \\ qexists_tac `minValue M64`
              \\ fs[minValue_def, minExponentPos_def, REAL_INV_1OVER])
606
          >- (`- float_to_real (fp64_to_float vF2) = 0`
607
608
                by fs[]
              \\ `float_to_real (fp64_to_float vF2) = 0`
609
                    by (rpt (qpat_x_assum `!x. _` kall_tac) \\ RealArith.REAL_ASM_ARITH_TAC)
610
611
612
613
              \\ fs[normal_def] \\ `0 < 0:real` suffices_by (fs[])
              \\ irule REAL_LTE_TRANS
              \\ qexists_tac `minValue M64`
              \\ fs[minValue_def, minExponentPos_def, REAL_INV_1OVER])
614
         \\ `float_to_real (fp64_to_float vF1) = 0:real` by fs[]
615
616
617
618
619
         \\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
         \\ Cases_on `float_value (fp64_to_float vF1)`
         \\ Cases_on `float_value (fp64_to_float vF2)` \\ fs[]
         \\ `2 * abs (0:real) <= ulp (:52#11)`
               by (fs[ulp_def, ULP_def])
620
621
         \\ Cases_on `((fp64_to_float vF1).Sign = (fp64_to_float vF2).Sign 
                      (fp64_to_float vF2).Sign = 1w)`
622
623
         \\ fs [round_roundTiesToEven_is_plus_zero,
                round_roundTiesToEven_is_minus_zero, float_values])
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
      >- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_sub_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                     normalTranslatedValue_implies_finiteness,
                     normalValue_implies_normalization,
                     GSYM float_is_zero_to_real, float_is_finite])
           \\ fs[dmode_def]
           \\ rename1 `abs err <= _`
           \\ qexists_tac `err`
           \\ fs[perturb_def, evalBinop_def]
           \\ fs[mTypeToQ_def, join_def])
      >- (pop_assum MP_TAC
          \\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def]
          \\ fs[fp64_sub_def, dmode_def, fp64_to_float_float_to_fp64]
          \\ fs[float_sub_def]
          \\ fs[join_def]
          \\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
          \\ fs[validFloatValue_def, normal_value_is_float_value, float_round_with_flags_def]
646
          >- (strip_tac
647
648
              \\ `2 * abs (0:real) <= ulp (:52 #11)`
                   by (fs[ulp_def, ULP_def])
649
650
              \\ fs[float_to_real_round_zero_is_zero]
              \\ qexists_tac `0` \\ fs[mTypeToQ_def])
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
          >- (strip_tac
              \\ fs[normal_def]
              \\ `0 < 0:real` suffices_by (fs[])
              \\ irule REAL_LTE_TRANS
              \\ qexists_tac `minValue M64`
              \\ fs[minValue_def, minExponentPos_def, REAL_INV_1OVER])
          >- (disch_then (fn thm => assume_tac (GSYM thm))
              \\ fs[normal_def] \\ `0 < 0:real` suffices_by (fs[])
              \\ irule REAL_LTE_TRANS
              \\ qexists_tac `minValue M64`
              \\ fs[minValue_def, minExponentPos_def, REAL_INV_1OVER])
         \\ qexists_tac `0`
         \\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
         \\ Cases_on `float_value (fp64_to_float vF1)`
         \\ Cases_on `float_value (fp64_to_float vF2)` \\ fs[]
         \\ `2 * abs (0:real) <= ulp (:52#11)`
               by (fs[ulp_def, ULP_def])
668
669
         \\ Cases_on `((fp64_to_float vF1).Sign  (fp64_to_float vF2).Sign 
                      (fp64_to_float vF1).Sign = 1w)`
670
671
         \\ fs [round_roundTiesToEven_is_plus_zero,
                round_roundTiesToEven_is_minus_zero, float_values, join_def, mTypeToQ_pos])
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
      >- (fs[fp64_mul_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_mul_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                     normalTranslatedValue_implies_finiteness,
                     normalValue_implies_normalization,
                     GSYM float_is_zero_to_real, float_is_finite])
           \\ fs[dmode_def]
           \\ rename1 `abs err <= _`
           \\ qexists_tac `err`
           \\ fs[perturb_def, evalBinop_def]
           \\ fs[mTypeToQ_def, join_def])
Heiko Becker's avatar
Heiko Becker committed
687
688
689
690
691
692
693
694
      >- (fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def,
             GSYM float_is_zero_to_real, float_is_zero_def,
             join_def]
            THENL [ Cases_on `float_value (fp64_to_float vF1)`,
                    Cases_on `float_value (fp64_to_float vF2)`]
             \\ fs[validValue_gives_float_value]
             \\ fs[float_round_with_flags_def, dmode_def,
                   fp64_to_float_float_to_fp64, perturb_def]
695
             \\ Cases_on `(fp64_to_float vF1).Sign  (fp64_to_float vF2).Sign`
Heiko Becker's avatar
Heiko Becker committed
696
697
698
699
700
             \\ `2 * abs (0:real) <= ulp (:52#11)`
               by (fs[ulp_def, ULP_def])
             \\ fs [round_roundTiesToEven_is_plus_zero,
                    round_roundTiesToEven_is_minus_zero, zero_to_real]
             \\ qexists_tac `0` \\ fs[mTypeToQ_pos])
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
      >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_div_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                     normalTranslatedValue_implies_finiteness,
                     normalValue_implies_normalization,
                     GSYM float_is_zero_to_real, float_is_finite])
           \\ fs[dmode_def]
           \\ rename1 `abs err <= _`
           \\ qexists_tac `err`
           \\ fs[perturb_def, evalBinop_def]
           \\ fs[mTypeToQ_def, join_def]
           \\ CCONTR_TAC \\ fs[float_is_zero_to_real])
Heiko Becker's avatar
Heiko Becker committed
717
718
      >- (fs[evalBinop_def]
          \\ `float_to_real (fp64_to_float vF1) = 0`
719
720
721
722
723
               by (qspecl_then
                     [`float_to_real (fp64_to_float vF1)`,
                      `float_to_real (fp64_to_float vF2)`]
                     impl_subgoal_tac (GSYM div_eq0_general)
                   \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
724
725
726
727
728
729
730
          \\ fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64,
                float_div_def]
          \\ rw_thm_asm `float_to_real (fp64_to_float vF1) = 0` (GSYM float_is_zero_to_real)
          \\ fs[float_is_zero_def]
          \\ Cases_on `float_value (fp64_to_float vF1)`
          \\ fs[validValue_gives_float_value]
          \\ simp [float_round_with_flags_def]
731
          \\ Cases_on `(fp64_to_float vF1).Sign  (fp64_to_float vF2).Sign`
Heiko Becker's avatar
Heiko Becker committed
732
733
734
735
736
          \\ `2 * abs (0:real) <= ulp (:52#11)`
                 by (fs[ulp_def, ULP_def])
          \\ fs [round_roundTiesToEven_is_plus_zero,
                 round_roundTiesToEven_is_minus_zero, zero_to_real]
          \\ qexists_tac `0` \\ fs[mTypeToQ_pos, perturb_def, join_def]))
737
738
739
740
  >- (cheat));

val final_thm = store_thm (
  "final_thm",
741
742
  ``!(e:word64 exp) (absenv:analysisResult) (P:precond) E1 E2 defVars fVars.
      approxEnv E1 defVars absenv fVars LN (toREnv E2) /\
743
744
745
746
747
748
749
750
      (!v.
          v IN (domain fVars) ==>
          ?vR.
            (E1 v = SOME vR) /\
            FST (P v) <= vR /\ vR <= SND (P v)) /\
      (domain (usedVars (toRExp e))) SUBSET (domain fVars) /\
      (!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\
      CertificateChecker (toRExp e) absenv P defVars ==>
751
      ?vR vF. (* m, currently = M64 *)
752
        eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
753
754
       eval_exp_float e E2 = SOME vF /\
       eval_exp (toREnv E2) defVars (toRExp e) (float_to_real (fp64_to_float vF)) M64 /\
Heiko Becker's avatar
Heiko Becker committed
755
756
       abs (vR - (float_to_real (fp64_to_float vF))) <=
             (SND (absenv (toRExp e)))``,
757
758
759
760
761
  rpt strip_tac
  \\ drule Certificate_checking_is_sound
  \\ rpt (disch_then drule)
  \\ strip_tac \\ asm_exists_tac
  \\ fs[]
762
763
764
765
766
  \\ qspecl_then [`e`, `E1`, `E2`, `defVars`, `vR`, `absenv`, `P`, `fVars`, `LN`]
       destruct
       bstep_gives_IEEE2
  \\ fs[CertificateChecker_def]
  >- (cheat (* Massaging *))
767
768
  \\ res_tac \\ fs[]);

Heiko Becker's avatar
Heiko Becker committed
769
val _ = export_theory ();