Fixes to morePrecise

Fixed incosistent handling of fixed point exponent sign
morePrecise now correctly checks whether all values from a format fit into the other

hol4/Infra/MachineTypeScript.sml

@@ -4,7 +4,7 @@
   @author: Raphael Monat
   @maintainer: Heiko Becker
  **)
-open realTheory realLib;
+open realTheory realLib integerTheory;
 open RealSimpsTheory;
 open preambleFloVer;
 
@@ -16,7 +16,15 @@ val _ = List.app monadsyntax.enable_monad ["option"];
 
 
 Datatype:
-  mType = REAL | M16 | M32 | M64 | F num num bool (* first num is word length, second is fractional bits, bool is for sign of fractional bits *)
+  mType = REAL
+  (* Floating point formats *)
+  | M16 | M32 | M64
+  (* Fixed point formats:
+   * first num is word length,
+   * second is fractional bits,
+   * bool is for sign of fractional bits, inverse of the exponent sign with T <=> positive
+   *)
+  | F num num bool
 End
 
 Definition isFixedPoint_def :
@@ -181,9 +189,8 @@ QED
   REAL is real-valued evaluation, hence the most precise.
   All floating-point types are compared by
     mTypeToQ m1 <= mTypeToQ m2
-  All fixed-point types are compared by comparing only the word size
-  We consider a 32 bit fixed-point number to be more precise than a 16 bit
-  fixed-point number, no matter what the fractional bits may be.
+  All fixed-point types are compared by comparing the positions of the
+  least and most significant bits. It is equivalent to a subset check.
   For the moment, fixed-point and floating-point formats are incomparable.
  **)
 Definition isMorePrecise_def:
@@ -191,13 +198,8 @@ Definition isMorePrecise_def:
     case m1, m2 of
     | REAL, _ => T
     | F w1 f1 s1, F w2 f2 s2 =>
-                    if s1 then
-                      if s2 then
-                        (w2 ≤ w1 ∧ f2 ≤ f1)
-                      else
-                        (w2 ≤ w1)
-                    else if s2 then F
-                    else (w2 ≤ w1 ∧ f2 ≤ f1)
+      let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
+      &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2
     | F w f s, _ => F
     | _, F w f s=> F
     | M16, M16 => T
@@ -215,13 +217,8 @@ End
 Definition morePrecise_def:
   (morePrecise REAL _ = T) /\
   (morePrecise (F w1 f1 s1) (F w2 f2 s2) =
-               (if s1 then
-                  if s2 then
-                    (w2 ≤ w1 ∧ f2 ≤ f1)
-                  else
-                    (w2 ≤ w1)
-                else if s2 then F
-                else (w2 ≤ w1 ∧ f2 ≤ f1))) ∧
+    let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
+    &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2) /\
   (morePrecise (F w f s) _ = F) /\
   (morePrecise _ (F w f s) = F) /\
   (morePrecise M16 M16 = T) /\
@@ -241,7 +238,7 @@ Proof
   rpt strip_tac
   \\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
   \\ fs[morePrecise_def]
-  \\ every_case_tac \\ gs[]
+  \\ ntac 2 $ dxrule_all INT_LE_TRANS \\ simp[]
 QED
 
 Theorem isMorePrecise_morePrecise: