ExpressionsScript.sml 15.3 KB
Newer Older
1 2 3 4 5
(**
  Formalization of the base expression language for the daisy framework
 **)
open preamble miscTheory
open realTheory realLib sptreeTheory
6
open AbbrevsTheory MachineTypeTheory
7
open DaisyTactics
8

9 10
val _ = ParseExtras.temp_tight_equality()

11
val _ = new_theory "Expressions";
12

13
val _ = temp_overload_on("abs",``real$abs``);
14
(**
15
  EXPRESSIONS WILL use binary operators.
16 17 18
  Define them first
**)
val _ = Datatype `
19
  binop = Plus | Sub | Mult | Div`;
20 21 22 23 24 25

(**
  Next define an evaluation function for binary operators.
  Errors are added on the expression evaluation level later
*)
val evalBinop_def = Define `
26 27 28 29
  evalBinop Plus v1 v2 = v1 + v2 /\
  evalBinop Sub  v1 v2 = v1 - v2 /\
  evalBinop Mult v1 v2 = v1 * v2 /\
  evalBinop Div  v1 v2 = v1 / (v2:real)`;
30 31 32 33 34 35

(**
Expressions will use unary operators.
Define them first
**)
val _ = Datatype `
36
  unop = Neg | Inv`
37 38 39 40 41 42

(**
Define evaluation for unary operators on reals.
Errors are added in the expression evaluation level later
**)
val evalUnop_def = Define `
43 44
  evalUnop Neg v = - v /\
  evalUnop Inv v = inv(v:real)`
45

46
(**
47 48
  Define Expressions parametric over some value type 'v.
  Will ease reasoning about different instantiations later.
49 50 51
**)
val _ = Datatype `
  exp = Var num
52
      | Const mType 'v
53
      | Unop unop exp
54
      | Binop binop exp exp
Nikita Zyuzin's avatar
Nikita Zyuzin committed
55
      | Fma exp exp exp
56 57
      | Downcast mType exp`

Nikita Zyuzin's avatar
Nikita Zyuzin committed
58 59 60 61 62 63 64
(**
  Define evaluation of FMA (fused multiply-add) on reals
  Errors are added on the expression evaluation level later
**)
val evalFma_def = Define `
  evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`

65
val toREval_def = Define `
Heiko Becker's avatar
Heiko Becker committed
66
  toREval e :real exp =
67
    case e of
Heiko Becker's avatar
Heiko Becker committed
68 69
      | (Var n) => Var n
      | (Const m n) => Const M0 n
Nikita Zyuzin's avatar
Nikita Zyuzin committed
70
      | (Unop u e1) => Unop u (toREval e1)
Heiko Becker's avatar
Heiko Becker committed
71
      | (Binop bop e1 e2) => Binop bop (toREval e1) (toREval e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
72
      | (Fma e1 e2 e3) => Fma (toREval e1) (toREval e2) (toREval e3)
Heiko Becker's avatar
Heiko Becker committed
73
      | (Downcast m e1) => (toREval e1)`;
74 75 76 77 78

(**
  Define a perturbation function to ease writing of basic definitions
**)
val perturb_def = Define `
79
  perturb (r:real) (e:real) = r * (1 + e)`
80 81

(**
82 83 84 85
Define expression evaluation relation parametric by an "error" epsilon.
The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
86 87
**)
val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
88 89
  (!E defVars m x v.
     defVars x = SOME m /\
90
     E x = SOME v ==>
91 92
     eval_exp E defVars (Var x) v m) /\
  (!E defVars m n delta.
93
      abs delta <= (mTypeToQ m) ==>
94 95 96 97 98
     eval_exp E defVars (Const m n) (perturb n delta) m) /\
  (!E defVars m f1 v1.
     eval_exp E defVars f1 v1 m ==>
     eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m) /\
  (!E defVars m f1 v1 delta.
99
     abs delta <= (mTypeToQ m) /\
100
     (v1 <> 0) /\
101 102
     eval_exp E defVars f1 v1 m ==>
     eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m) /\
103 104 105 106 107
  (!E defVars m m1 f1 v1 delta.
     isMorePrecise m1 m /\
     abs delta <= (mTypeToQ m) /\
     eval_exp E defVars f1 v1 m1 ==>
     eval_exp E defVars (Downcast m f1) (perturb v1 delta) m) /\
108
  (!E defVars m1 m2 b f1 f2 v1 v2 delta.
109
     abs delta <= (mTypeToQ (join m1 m2)) /\
110 111
     eval_exp E defVars f1 v1 m1 /\
     eval_exp E defVars f2 v2 m2 /\
112
     ((b = Div) ==> (v2 <> 0)) ==>
Nikita Zyuzin's avatar
Nikita Zyuzin committed
113 114 115 116 117 118 119
     eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2)) /\
  (!E defVars m1 m2 m3 f1 f2 f3 v1 v2 v3 delta.
     abs delta <= (mTypeToQ (join3 m1 m2 m3)) /\
     eval_exp E defVars f1 v1 m1 /\
     eval_exp E defVars f2 v2 m2 /\
     eval_exp E defVars f3 v3 m3 ==>
     eval_exp E defVars (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3))`;
120

='s avatar
= committed
121
val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases);
122

123 124 125
(**
  Generate a better case lemma
**)
126 127
val eval_exp_cases =
  map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
128
    [``eval_exp E defVars (Var v) res m``,
129
     ``eval_exp E defVars (Const m1 n) res m2``,
130 131
     ``eval_exp E defVars (Unop u e) res m``,
     ``eval_exp E defVars (Binop n e1 e2) res m``,
Nikita Zyuzin's avatar
Nikita Zyuzin committed
132
     ``eval_exp E defVars (Fma e1 e2 e3) res m``,
133
     ``eval_exp E defVars (Downcast m1 e1) res m2``]
134 135
  |> LIST_CONJ |> curry save_thm "eval_exp_cases";

Nikita Zyuzin's avatar
Nikita Zyuzin committed
136
val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist, Fma_dist] = CONJ_LIST 7 eval_exp_rules;
137 138 139 140 141
save_thm ("Var_load", Var_load);
save_thm ("Const_dist", Const_dist);
save_thm ("Unop_neg", Unop_neg);
save_thm ("Unop_inv", Unop_inv);
save_thm ("Binop_dist", Binop_dist);
Nikita Zyuzin's avatar
Nikita Zyuzin committed
142
save_thm ("Fma_dist", Fma_dist);
143
save_thm ("Downcast_dist", Downcast_dist);
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
(**
  Show some simpler (more general) rule lemmata
**)

val Const_dist' = store_thm (
  "Const_dist'",
  ``!m n delta v m' E Gamma.
      (abs delta) <= (mTypeToQ m) /\
      v = perturb n delta /\
      m' = m ==>
      eval_exp E Gamma (Const m n) v m'``,
  fs [Const_dist]);

val Unop_neg' = store_thm (
  "Unop_neg'",
  ``!m f1 v1 v m' E Gamma.
      eval_exp E Gamma f1 v1 m /\
      v = evalUnop Neg v1 /\
      m' = m ==>
      eval_exp E Gamma (Unop Neg f1) v m'``,
  fs [Unop_neg]);

val Unop_inv' = store_thm (
  "Unop_inv'",
  ``!m f1 v1 delta v m' E Gamma.
      (abs delta) <= (mTypeToQ m) /\
      eval_exp E Gamma f1 v1 m /\
      (v1 <> 0) /\
      v = perturb (evalUnop Inv v1) delta /\
      m' = m ==>
      eval_exp E Gamma (Unop Inv f1) v m'``,
  fs [Unop_inv]);

val Downcast_dist' = store_thm ("Downcast_dist'",
  ``!m m1 f1 v1 delta v m' E Gamma.
      isMorePrecise m1 m /\
      (abs delta) <= (mTypeToQ m) /\
      eval_exp E Gamma f1 v1 m1 /\
      v = perturb v1 delta /\
      m' = m ==>
      eval_exp E Gamma (Downcast m f1) v m'``,
  rpt strip_tac
  \\ rw []
  \\ match_mp_tac Downcast_dist
  \\ qexists_tac `m1` \\ fs[]);

val Binop_dist' = store_thm ("Binop_dist'",
  ``!m1 m2 op f1 f2 v1 v2 delta v m' E Gamma.
      (abs delta) <= (mTypeToQ m') /\
      eval_exp E Gamma f1 v1 m1 /\
      eval_exp E Gamma f2 v2 m2 /\
      ((op = Div) ==> (v2 <> 0)) /\
      v = perturb (evalBinop op v1 v2) delta /\
      m' = join m1 m2 ==>
      eval_exp E Gamma (Binop op f1 f2) v m'``,
  fs [Binop_dist]);

Nikita Zyuzin's avatar
Nikita Zyuzin committed
202 203 204 205 206 207 208 209 210 211 212
val Fma_dist' = store_thm ("Fma_dist'",
  ``!m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma.
      (abs delta) <= (mTypeToQ m') /\
      eval_exp E Gamma f1 v1 m1 /\
      eval_exp E Gamma f2 v2 m2 /\
      eval_exp E Gamma f3 v3 m3 /\
      v = perturb (evalFma v1 v2 v3) delta /\
      m' = join3 m1 m2 m3 ==>
      eval_exp E Gamma (Fma f1 f2 f3) v m'``,
  fs [Fma_dist]);

213 214 215 216 217 218 219 220 221 222
(**
  Define the set of "used" variables of an expression to be the set of variables
  occuring in it
**)
val usedVars_def = Define `
  usedVars (e: 'a exp) :num_set =
    case e of
      | Var x => insert x () (LN)
      | Unop u e1 => usedVars e1
      | Binop b e1 e2 => union (usedVars e1) (usedVars e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
223
      | Fma e1 e2 e3 => union (usedVars e1) (union (usedVars e2) (usedVars e3))
224
      | Downcast m e1 => usedVars e1
225 226 227 228 229
      | _ => LN`;

(**
  If |delta| <= 0 then perturb v delta is exactly v.
**)
230 231 232 233
val delta_0_deterministic = store_thm("delta_0_deterministic",
  ``!(v:real) (delta:real). abs delta <= 0 ==> perturb v delta = v``,
  fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);

='s avatar
= committed
234
val delta_M0_deterministic = store_thm("delta_M0_deterministic",
235 236
  ``!(v:real) (delta:real). abs delta <= mTypeToQ M0 ==> perturb v delta = v``,
  fs [mTypeToQ_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
='s avatar
= committed
237

Heiko Becker's avatar
Heiko Becker committed
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
val toRMap_def = Define `
  toRMap (d:num -> mType option) (n:num) : mType option =
    case d n of
      | SOME m => SOME M0
      | NONE => NONE`;

val toRMap_eval_M0 = store_thm (
  "toRMap_eval_M0",
  ``!f v E Gamma m.
      eval_exp E (toRMap Gamma) (toREval f) v m ==> m = M0``,
  Induct \\ simp[Once toREval_def] \\ fs[eval_exp_cases, toRMap_def]
  \\ rpt strip_tac \\ fs[]
  >- (every_case_tac \\ fs[])
  >- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
  >- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
  >- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
      \\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
Nikita Zyuzin's avatar
Nikita Zyuzin committed
255 256 257 258 259
      \\ rveq \\ fs[join_def])
  >- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
      \\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
      \\ `m3 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
      \\ rveq \\ fs[join3_def] \\ fs[join_def]));
Heiko Becker's avatar
Heiko Becker committed
260

261 262 263
(**
Evaluation with 0 as machine epsilon is deterministic
**)
264
val meps_0_deterministic = store_thm("meps_0_deterministic",
265
  ``!(f: real exp) v1:real v2:real E defVars.
Heiko Becker's avatar
Heiko Becker committed
266 267
      eval_exp E (toRMap defVars) (toREval f) v1 M0 /\
      eval_exp E (toRMap defVars) (toREval f) v2 M0 ==>
268
      v1 = v2``,
269
  Induct_on `f`
270
  >- (rw [toREval_def] \\ fs [eval_exp_cases])
271 272 273 274 275 276 277 278
  >- (rw [toREval_def]
      \\ fs [eval_exp_cases, mTypeToQ_def, delta_0_deterministic])
  >- (rw []
      \\ rpt (
           qpat_x_assum `eval_exp _ _ (toREval _) _ _`
             (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
      \\ Cases_on `u` \\ fs [eval_exp_cases] \\ rw []
      \\ fs [eval_exp_cases]
279
      >- (res_tac \\ fs [REAL_NEG_EQ])
280
      >- (res_tac \\ fs [mTypeToQ_def, delta_0_deterministic]))
281 282 283 284 285 286
  >- (rw[]
      \\ rename1 `Binop b f1 f2`
      \\ rpt (
           qpat_x_assum `eval_exp _ _ (toREval _) _ _`
            (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
      \\ Cases_on `b` \\ fs [eval_exp_cases]
Heiko Becker's avatar
Heiko Becker committed
287
      \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule  toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
288 289 290 291 292
      \\ rw[]
      \\ rename1 `eval_exp E _ (toREval f1) vf11 M0`
      \\ rename1 `eval_exp E _ (toREval f1) vf12 m1`
      \\ rename1 `eval_exp E _ (toREval f2) vf21 M0`
      \\ rename1 `eval_exp _ _ (toREval f2) vf22 m2`
Heiko Becker's avatar
Heiko Becker committed
293
      \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\  fs [])
294 295 296 297 298 299
      \\ rw []
      \\ fs [join_def, mTypeToQ_def, delta_0_deterministic]
      \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf21`,`vf22`] ASSUME_TAC thm)
      \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf11`,`vf12`] ASSUME_TAC thm)
      \\ res_tac
      \\ rw[])
Nikita Zyuzin's avatar
Nikita Zyuzin committed
300 301 302 303 304 305 306 307 308 309 310 311 312 313
  >- (rw[]
      \\ rpt (
           qpat_x_assum `eval_exp _ _ (toREval _) _ _`
            (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
      \\ fs [eval_exp_cases]
      \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule  toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
      \\ `m3 = M0` by (irule  toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
      \\ `m1' = M0 /\ m2' = M0` by (conj_tac \\ irule  toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
      \\ `m3' = M0` by (irule  toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
      \\ rw[]
      \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v3`,`v3'`, `E`, `defVars`] ASSUME_TAC thm)
      \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v2'`,`v2''`, `E`, `defVars`] ASSUME_TAC thm)
      \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v1'`,`v1''`, `E`, `defVars`] ASSUME_TAC thm)
      \\ fs [join3_def, join_def, mTypeToQ_def, delta_0_deterministic])
314 315
  >- (rw[]
      \\ rpt (
Heiko Becker's avatar
Heiko Becker committed
316
           qpat_x_assum `eval_exp _ _ (toREval (Downcast _ _)) _ _`
317 318 319
            (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
      \\ fs [eval_exp_cases]
      \\ res_tac));
320

321
(**
322
Helping lemmas. Needed in soundness proof.
323
For each evaluation of using an arbitrary epsilon, we can replace it by
324
evaluating the subExpressions and then binding the result values to different
325
variables in the Environment.
326 327
**)
val binary_unfolding = store_thm("binary_unfolding",
328 329 330 331 332 333 334 335 336 337
  ``!(b:binop) (f1:(real)exp) (f2:(real)exp) E Gamma (v:real) v1 v2 m1 m2 delta.
      (b = Div ==> (v2 <> 0)) /\
      (abs delta) <= (mTypeToQ (join m1 m2)) /\
      eval_exp E Gamma f1 v1 m1 /\
      eval_exp E Gamma f2 v2 m2 /\
      eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2) ==>
      eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
        (updDefVars 2 m2 (updDefVars 1 m1 Gamma))
        (Binop b (Var 1) (Var 2)) (perturb (evalBinop b v1 v2) delta) (join m1 m2)``,
  fs [updEnv_def,updDefVars_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
338 339
  \\ metis_tac []);

340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
val fma_unfolding = store_thm("fma_unfolding",
  ``!(f1:(real)exp) (f2:(real)exp) (f3:(real)exp) E Gamma (v:real) v1 v2 v3 m1 m2 m3 delta.
      (abs delta) <= (mTypeToQ (join3 m1 m2 m3)) /\
      eval_exp E Gamma f1 v1 m1 /\
      eval_exp E Gamma f2 v2 m2 /\
      eval_exp E Gamma f3 v3 m3 /\
      eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3) ==>
      eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
        (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
        (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3)``,
  fs [updEnv_def,updDefVars_def,join3_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
  \\ rpt strip_tac
  \\ qexists_tac `delta'`
  \\ conj_tac \\ fs[]);

355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
val eval_eq_env = store_thm (
  "eval_eq_env",
  ``!e E1 E2 Gamma v m.
      (!x. E1 x = E2 x) /\
      eval_exp E1 Gamma e v m ==>
      eval_exp E2 Gamma e v m``,
  Induct \\ rpt strip_tac \\ fs[eval_exp_cases]
  >- (`E1 n = E2 n` by (first_x_assum irule)
      \\ fs[])
  >- (qexists_tac `delta'` \\ fs[])
  >- (rveq \\ qexists_tac `v1` \\ fs[]
      \\ first_x_assum drule \\ disch_then irule \\ fs[])
  >- (rveq \\ qexists_tac `v1` \\ fs[]
      \\ qexists_tac `delta'` \\ fs[]
      \\ first_x_assum drule \\ disch_then irule \\ fs[])
  >- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`]
      \\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[])
Nikita Zyuzin's avatar
Nikita Zyuzin committed
372 373
  >- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta'`]
      \\ fs[] \\ prove_tac [])
374 375 376
  >- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[]
      \\ first_x_assum drule \\ disch_then irule \\ fs[]));

377 378 379 380 381 382 383 384 385 386 387
(* (** *)
(*   Analogous lemma for unary expressions *)
(* **) *)
(* val unary_unfolding = store_thm("unary_unfolding", *)
(* ``!(u:unop) (e1:(real)exp) (m:mType) E defVars (v:real). *)
(*        (eval_exp E defVars (Unop Inv e1) v m <=> *)
(*        (?(v1:real). *)
(*           eval_exp E defVars e1 v1 m /\ *)
(*           eval_exp (updEnv 1 v1 emptyEnv) (updDefVars 1 m defVars) (Unop Inv (Var 1)) v m))``, *)
(*   fs [updEnv_def, updDefVars_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS] *)
(*   \\ metis_tac []); *)
388

389
(*
390
  Using the parametric Expressions, define boolean Expressions for conditionals
391
*)
392 393 394
(* val _ = Datatype ` *)
(*   bexp = Leq ('v exp) ('v exp) *)
(*        | Less ('v exp) ('v exp)` *)
395 396 397 398

(*
  Define evaluation of boolean expressions
*)
399 400 401 402 403 404 405 406 407
(* val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln ` *)
(*   (!E defVars e1 e2 v1 v2 m. *)
(*       eval_exp E defVars e1 v1 m /\ *)
(*       eval_exp E defVars e2 v2 m ==> *)
(*       bval E defVars m (Leq e1 e2) (v1 <= v2))/\ *)
(*   (!E defVars e1 e2 v1 v2 m. *)
(*       eval_exp E defVars e1 v1 m /\ *)
(*       eval_exp E defVars e2 v2 m ==> *)
(*       bval E defVars m (Less e1 e2) (v1 < v2))`; *)
408

409 410 411 412 413 414 415 416 417 418 419
(* val bval_exp_cases = *)
(*   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases]) *)
(*     [``bval E defVars m (Leq e1 e2) res``, *)
(*      ``bval E defVars m (Less e1 e2) res``] *)
(*   |> LIST_CONJ |> curry save_thm "bval_exp_cases"; *)

(* (** *)
(*   Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
(* val _ = overload_on("Gr",``\(e1:('v)exp). \(e2:('v)exp). Less e2 e1``); *)
(* val _ = overload_on("Greq",``\(e1:('v)exp). \(e2:('v)exp). Leq e2 e1``); *)
420 421

val _ = export_theory();