Move prelude to be last import as recommended by CakeML devs

hol4/AbbrevsScript.sml

 (**
   This file contains some type abbreviations, to ease writing.
  **)
+open realTheory realLib sptreeTheory
+open MachineTypeTheory
 open preamble
-open realTheory realLib sptreeTheory MachineTypeTheory
 
 val _ = new_theory "Abbrevs";
 (**

hol4/CertificateCheckerScript.sml

@@ -4,13 +4,13 @@
   validator and the error bound validator. Running this function on the encoded
   analysis result gives the desired theorem as shown in the soundness theorem.
 **)
-open preamble;
-
 open simpLib realTheory realLib RealArith RealSimpsTheory
 open AbbrevsTheory ExpressionsTheory DaisyTactics ExpressionAbbrevsTheory
      ErrorBoundsTheory IntervalArithTheory IntervalValidationTheory
      ErrorValidationTheory ssaPrgsTheory FPRangeValidatorTheory
 
+open preamble;
+
 val _ = new_theory "CertificateChecker";
 val _ = temp_overload_on("abs",``real$abs``);
 

hol4/CommandsScript.sml

 (**
  Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
  **)
-open preamble
 open simpLib realTheory realLib RealArith
 open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory MachineTypeTheory
+open preamble
 
 val _ = new_theory "Commands";
 

hol4/DaisyMapScript.sml

-open preamble
 open MachineTypeTheory ExpressionAbbrevsTheory DaisyTactics
+open preamble
 
 val _ = new_theory "DaisyMap";
 

hol4/EnvironmentsScript.sml

-open preamble
 open simpLib realTheory realLib RealArith sptreeTheory
 open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyTactics DaisyMapTheory
+open preamble
 
 val _ = new_theory "Environments";
 

hol4/ErrorBoundsScript.sml

@@ -3,10 +3,10 @@ Proofs of general bounds on the error of arithmetic Expressions.
 This shortens soundness proofs later.
 Bounds are explained in section 5, Deriving Computable Error Bounds
 **)
-open preamble
 open simpLib realTheory realLib RealArith
-open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
-open ExpressionAbbrevsTheory EnvironmentsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
+     MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
+open preamble
 
 val _ = new_theory "ErrorBounds";
 

hol4/ErrorValidationScript.sml

@@ -6,11 +6,12 @@
    encoded in the analysis result. The validator is used in the file
    CertificateChecker.v to build the complete checker.
  **)
-open preamble
 open simpLib realTheory realLib RealArith pred_setTheory
-open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
-open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory
-open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory DaisyMapTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
+     MachineTypeTheory ExpressionAbbrevsTheory ErrorBoundsTheory
+     IntervalArithTheory TypingTheory IntervalValidationTheory
+     EnvironmentsTheory CommandsTheory ssaPrgsTheory DaisyMapTheory;
+open preamble
 
 val _ = new_theory "ErrorValidation";
 

hol4/ExpressionAbbrevsScript.sml

@@ -2,8 +2,8 @@
   Some abbreviations that require having defined expressions beforehand
   If we would put them in the Abbrevs file, this would create a circular dependency which HOL4 cannot resolve.
 **)
-open preamble
 open ExpressionsTheory
+open preamble
 
 val _ = new_theory "ExpressionAbbrevs"
 

hol4/ExpressionsScript.sml

 (**
   Formalization of the base expression language for the daisy framework
  **)
-open preamble miscTheory
-open realTheory realLib sptreeTheory
-open AbbrevsTheory MachineTypeTheory
-open DaisyTactics
-
-val _ = ParseExtras.temp_tight_equality()
+open miscTheory realTheory realLib sptreeTheory
+open AbbrevsTheory MachineTypeTheory DaisyTactics
+open preamble
 
 val _ = new_theory "Expressions";
 

hol4/FPRangeValidatorScript.sml

@@ -8,13 +8,11 @@
   value according to IEEE 754.
 
 **)
-open preamble
-
 open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
-
 open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithTheory
      ExpressionsTheory DaisyTactics IntervalValidationTheory ErrorValidationTheory
      CommandsTheory EnvironmentsTheory ssaPrgsTheory
+open preamble
 
 val _ = new_theory "FPRangeValidator";
 

hol4/IEEE_connectionScript.sml

-open preamble
-
 open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
-
 open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics
      CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
      TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
      CommandsTheory ssaPrgsTheory EnvironmentsTheory DaisyMapTheory
+open preamble
 
 val _ = new_theory "IEEE_connection";
 

hol4/Infra/MachineTypeScript.sml

@@ -4,8 +4,8 @@
   @author: Raphael Monat
   @maintainer: Heiko Becker
  **)
-open preamble miscTheory
-open realTheory realLib sptreeTheory
+open miscTheory realTheory realLib sptreeTheory
+open preamble
 
 val _ = new_theory "MachineType";
 

hol4/IntervalArithScript.sml

@@ -2,9 +2,9 @@
   Formalization of real valued interval arithmetic
   Used in soundness proofs for error bound validator.
 **)
-open preamble
 open realTheory realLib RealArith
 open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
+open preamble
 
 val _ = new_theory "IntervalArith";
 

hol4/IntervalValidationScript.sml

@@ -5,11 +5,11 @@
     The computation is done using our formalized interval arithmetic.
     The function is used in CertificateChecker.v to build the full checker.
 **)
-open preamble
 open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
 open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
      ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
      sptreeLib sptreeTheory DaisyMapTheory
+open preamble
 
 val _ = new_theory "IntervalValidation";
 

hol4/RealSimpsScript.sml

-open preamble
 open RealArith
 open realTheory realLib
-val _ = ParseExtras.temp_tight_equality()
+open preamble
+  (*
+val _ = ParseExtras.temp_tight_equality() *)
 
 val _ = new_theory "RealSimps";
 

hol4/TypingScript.sml

-open preamble miscTheory
-open DaisyTactics
-open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
+open miscTheory realTheory realLib sptreeTheory
+open ExpressionsTheory MachineTypeTheory  DaisyTactics
      IntervalValidationTheory CommandsTheory DaisyMapTheory
+open preamble
 
 val _ = new_theory "Typing";
 

cakeml @ 78a58694

-Subproject commit daa2d5c014fffca8301ddca1a17592d13b452455
+Subproject commit 78a58694402dc04c3291458d9c91eb1daef723d7

hol4/daisyParserScript.sml

-open preamble
 open AbbrevsTheory MachineTypeTheory ExpressionsTheory CommandsTheory DaisyMapTheory
+open preamble
 
 val _ = new_theory "daisyParser";
 

hol4/ssaPrgsScript.sml

@@ -5,9 +5,9 @@
   Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
   the program with the predicate with the set of free and defined variables
 **)
-open preamble
 open pred_setSyntax pred_setTheory
 open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory DaisyTactics CommandsTheory MachineTypeTheory
+open preamble
 
 val _ = new_theory "ssaPrgs";
 

hol4/test.sml

+
+open CertificateCheckerTheory daisyParserTheory
+
+val test = EVAL ``(case (dParse (lex "Let Var 4 MTYPE 64 + * Var 0 Var 0 Var 1 Let Var 5 MTYPE 32 Cast MTYPE 32 + Var 0 * Var 1 Var 1 Ret + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64 GAMMA Var 0 MTYPE 64 Var 1 MTYPE 32 Var 4 MTYPE 64 Var 5 MTYPE 32 PRE ? Var 0 ~5#1 5#1 ? Var 1 ~5#1 5#1 ABS ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? + * Var 0 Var 0 Var 1 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? * Var 0 Var 0 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#16777216  ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? Cast MTYPE 32 + Var 0 * Var 1 Var 1 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? + Var 0 * Var 1 Var 1 ~30#1 30#1 190147601533197042302697458892825#42535295865117307932921825928971026432 ? Var 0 ~5#1 5#1 5#9007199254740992 ? * Var 1 Var 1 ~25#1 25#1 21110624511590425#4722366482869645213696 ? Var 1 ~5#1 5#1 5#16777216 ? Var 1 ~5#1 5#1 5#16777216  ? + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~1630#1 3050#1 139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425#285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736 ? * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  ~779#1 1681#1 773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~851#1 1369#1 172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009#372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992")) of
+|   SOME ((f, P, M, Gamma), l) => CertificateCheckerCmd f M P Gamma
+|   _ => F) = T``;
+  EVAL_TAC
+  fs[sptreeTheory.lookup_def]
+  conj_tac \\ EVAL_TAC
+  >- (fs[sptreeTheory.lookup_def]
+    \\ rpt strip_tac
+    \\ fs[sptreeTheory.lookup_def]
+    \\ EVAL_TAC)
+  rpt ( EVAL_TAC\\ fs[realTheory.REAL_INV_1OVER])
+  EVAL_TAC
+  EVAL_TAC
+
+SIMP_RULE std_ss [