From 0e964525af8a3c9592147ee0dcbce357fcd414c8 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Wed, 5 Oct 2022 09:56:05 +0200
Subject: [PATCH] Make libmGen compatible with latest changes in HOL4

---
 libmGen/Holmakefile                           |   2 -
 libmGen/README.md                             |  25 +
 libmGen/atnDeg3Script.sml                     |  27 +
 libmGen/expDeg4Script.sml                     |  29 +
 libmGen/expExampleScript.sml                  |  29 +
 libmGen/libmLib.sml                           |   2 +-
 libmGen/logAddDeg3Script.sml                  |  26 +
 tools/dandelion/README.md                     | 137 +++++
 tools/dandelion/bitArithLib.sml               | 125 ----
 tools/dandelion/bitArithScript.sml            | 546 ------------------
 tools/dandelion/certificate_DopplerScript.sml |  45 --
 tools/dandelion/cosDeg5Script.sml             |  27 -
 tools/dandelion/euclidDivScript.sml           |  17 +-
 tools/dandelion/mcLaurinApproxScript.sml      |   4 +-
 tools/dandelion/moreRealScript.sml            |   3 +-
 tools/dandelion/readmePrefix                  |  43 ++
 tools/dandelion/realDeepScript.sml            |  23 -
 tools/dandelion/sinDeg3Script.sml             |   2 +-
 tools/dandelion/sturmScript.sml               |   4 +-
 19 files changed, 336 insertions(+), 780 deletions(-)
 create mode 100644 libmGen/README.md
 create mode 100644 libmGen/atnDeg3Script.sml
 create mode 100644 libmGen/expDeg4Script.sml
 create mode 100644 libmGen/expExampleScript.sml
 create mode 100644 libmGen/logAddDeg3Script.sml
 create mode 100644 tools/dandelion/README.md
 delete mode 100644 tools/dandelion/bitArithLib.sml
 delete mode 100644 tools/dandelion/bitArithScript.sml
 delete mode 100644 tools/dandelion/certificate_DopplerScript.sml
 delete mode 100644 tools/dandelion/cosDeg5Script.sml
 create mode 100644 tools/dandelion/readmePrefix
 delete mode 100644 tools/dandelion/realDeepScript.sml

diff --git a/libmGen/Holmakefile b/libmGen/Holmakefile
index 8cb102f872..590c3ae526 100644
--- a/libmGen/Holmakefile
+++ b/libmGen/Holmakefile
@@ -2,8 +2,6 @@ INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\
            $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
 	   $(CAKEMLDIR)/unverified/sexpr-bootstrap\
 	   $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\
-	   $(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/inference\
-	   $(CAKEMLDIR)/compiler/backend/proofs\
 	   $(CAKEMLDIR)/icing\
 	   $(CAKEMLDIR)/tools/flover\
 	   $(CAKEMLDIR)/tools/dandelion
diff --git a/libmGen/README.md b/libmGen/README.md
new file mode 100644
index 0000000000..6f2799dd3b
--- /dev/null
+++ b/libmGen/README.md
@@ -0,0 +1,25 @@
+A libm-generator for CakeML that uses Dandelion and FloVer from `tools`
+to prove a specification that relates CakeML code to the real-valued elementary
+function.
+
+[FloVerToCakeMLProofsScript.sml](FloVerToCakeMLProofsScript.sml):
+Main connection theorem relating FloVer's roundoff error bound
+to CakeML floating-point kernel executions
+
+[FloVerToCakeMLScript.sml](FloVerToCakeMLScript.sml):
+Translation from CakeML floating-point kernels to FloVer input
+
+[cosExampleScript.sml](cosExampleScript.sml):
+Example libm function generated from cosine certificate of Dandelion
+
+[expExampleScript.sml](expExampleScript.sml):
+Example libm function generated from cosine certificate of Dandelion
+
+[libmLib.sml](libmLib.sml):
+Implementation of automatic generation of libm functions
+
+[libmScript.sml](libmScript.sml):
+Supporting proofs for automation
+
+[sinExampleScript.sml](sinExampleScript.sml):
+Example libm function generated from sine certificate of Dandelion
diff --git a/libmGen/atnDeg3Script.sml b/libmGen/atnDeg3Script.sml
new file mode 100644
index 0000000000..ce8b311460
--- /dev/null
+++ b/libmGen/atnDeg3Script.sml
@@ -0,0 +1,27 @@
+open realZeroLib bitArithLib libmLib preambleDandelion;
+
+val _ = new_theory "atnDeg3";
+
+val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.createMetiTarskiQuery := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+  transc := Fun Atn (Var "x");
+  poly := [
+     -6809284315197713  * inv ( 2 pow  84 );
+     8979859070570549  * inv ( 2 pow  53 );
+     2502429001398681  * inv ( 2 pow  78 );
+     -2531269759855903  * inv ( 2 pow  53 );
+    ];
+  eps :=  77569196655847480248172279652945299732867702355  * inv (2 pow 167 );
+  iv := [ ("x",
+    ( -1  * inv (2 pow 1 ),
+      1  * inv (2 pow 1 )))];
+|>
+End
+
+Theorem atn_cml_code_corr = implement cos_example_def "atn"
+
+val _ = export_theory();
diff --git a/libmGen/expDeg4Script.sml b/libmGen/expDeg4Script.sml
new file mode 100644
index 0000000000..252fb2ef66
--- /dev/null
+++ b/libmGen/expDeg4Script.sml
@@ -0,0 +1,29 @@
+open realZeroLib bitArithLib preambleDandelion;
+
+val _ = new_theory "expDeg4";
+
+
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "x");
+    poly := [
+        2251860978014963  * inv ( 2 pow  51 );
+        2248839599087155  * inv ( 2 pow  51 );
+        1148731941443245  * inv ( 2 pow  51 );
+        2516578118969257  * inv ( 2 pow  54 );
+        5022738147898817  * inv ( 2 pow  56 );
+      ];
+    eps :=  61174722613  * inv (2 pow 51 );
+    iv := [
+        ("x",
+         ( 0 * inv (2 pow 0 ),
+           1 * inv (2 pow 0 )))
+      ];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def “16:num”;
+
+val _ = export_theory();
diff --git a/libmGen/expExampleScript.sml b/libmGen/expExampleScript.sml
new file mode 100644
index 0000000000..fc0d6ca317
--- /dev/null
+++ b/libmGen/expExampleScript.sml
@@ -0,0 +1,29 @@
+(*
+  Example libm function generated from cosine certificate of Dandelion
+*)
+open libmLib;
+
+val _ = new_theory "expExample";
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Bop Add (Fun Exp (Bop Mul (Var "x") (Cst (1/2:real)))) (Fun Cos (Bop Mul (Var "x") (Cst (1/2:real))));
+poly := [
+     9007199045267507  * inv ( 2 pow  52 );
+     4503607326537297  * inv ( 2 pow  53 );
+     -3241616109733325  * inv ( 2 pow  69 );
+     375588665660545  * inv ( 2 pow  54 );
+     5979080956143783  * inv ( 2 pow  60 );
+     5038332231908613  * inv ( 2 pow  64 );
+    ];
+  eps :=  27896958177787588423236394485375286824270176601341  * inv (2 pow 192 );
+  iv := [ ("x",
+    ( 37414441915671114706014331717536845303191873100185  * inv (2 pow 168 ),
+      1  * inv (2 pow 0 )))];
+  |>
+End
+
+Theorem cos_cml_code_corr = implement exp_example_def "exp_add_cos"
+
+val _ = export_theory();
diff --git a/libmGen/libmLib.sml b/libmGen/libmLib.sml
index 786bb75d78..dd9da2c60b 100644
--- a/libmGen/libmLib.sml
+++ b/libmGen/libmLib.sml
@@ -17,7 +17,7 @@ struct
 
   exception libmGenException of string;
 
-  val approxSteps = “20:num”; (** TODO: make this a parameter ? **)
+  val approxSteps = “16:num”; (** TODO: make this a parameter ? **)
 
   val zero_eq = GSYM $ Q.SPEC ‘1’ REAL_DIV_LZERO
 
diff --git a/libmGen/logAddDeg3Script.sml b/libmGen/logAddDeg3Script.sml
new file mode 100644
index 0000000000..a980d1cf92
--- /dev/null
+++ b/libmGen/logAddDeg3Script.sml
@@ -0,0 +1,26 @@
+open realZeroLib bitArithLib libmLib preambleDandelion;
+
+val _ = new_theory "logAddDeg3";
+
+
+
+Definition log_example_def:
+  log_example =
+  <|
+    transc := Fun Log (Bop Add (Var "x") (Cst (1/10))) ;
+  poly := [
+     -1550808607  * inv ( 2 pow  30 );
+     641406787  * inv ( 2 pow  28 );
+     -573949725  * inv ( 2 pow  29 );
+     3766713447  * inv ( 2 pow  34 );
+    ];
+  eps :=  10535917144680386079769337698113777809575837070019  * inv (2 pow 186 );
+  iv := [ ("x",
+    ( 23407410223491741137950216280783988842809415608303  * inv (2 pow 164 ),
+      12861214408511945680192426527903290572972206378189  * inv (2 pow 163 )))];
+|>
+End
+
+Theorem log_cml_code_corr = implement log_example_def "log"
+
+val _ = export_theory();
diff --git a/tools/dandelion/README.md b/tools/dandelion/README.md
new file mode 100644
index 0000000000..f2f013256c
--- /dev/null
+++ b/tools/dandelion/README.md
@@ -0,0 +1,137 @@
+# Dandelion
+
+A certificate checker for approximations of elementary functions.
+
+## Key theorems and definitions relating to the original ITP'22 paper
+
+The first phase is defined across the files `transcApproxSemScript.sml` and
+`approxPolyScript.sml`. The first file defines the overall approximation
+function `approxAsPoly` and gives its soundness proof, and
+`approxPolyScript.sml` defines the low-level approximation function for
+approximating a single elementary function with a single polynomial and proves
+soundness of this function.
+
+Theorem 4 (First Phase Soundness) from section 3 is proven in file
+`transcApproxSemScript.sml` as `approxTransc_sound`.
+Variants of Theorem 5 are proven for the supported elementary function in file
+`mcLaurinApproxScript.sml` if they are not provided by HOL4.
+Variants of Theorem 6 are proven for the supported elementary functions in file
+`approxPolyScript.sml`.
+
+The second phase is implemented and proven sound in the file
+`checkerScript.sml`.
+It relies on the implementation of computable Sturm sequences in
+`sturmComputeScript.sml` and computable polynomial division in
+`euclidDivScript.sml`.
+
+Theorem 7 (Second Phase Soundness) from section 4 is proven in file
+`checkerScript.sml` as the combination of `numZeros_sound`,
+`validBounds_is_valid`, and `validateZerosLeqErr_sound`.
+
+Theorem 8 was ported from Harrison's HOL-Light proofs in file `drangScript.sml`
+and is called `BOUND_THEOREM_INEXACT`.
+
+Theorem 9 (Dandelion soundness) is called `checker_soundness` in file
+`checkerScript.sml`.
+
+The extracted binary is created in the directory `binary`.
+File `translateScript.sml` sets up the CakeML translation of the definitions of
+Dandelion, file `certParserScript.sml` defines our (unverified) parser and
+lexer, file `sturmMainCakeScript.sml` proves the CakeML specification for the
+binary, and file `sturmMainCakeCompileScript.sml` compiles the binary for the
+second phase by running the CakeML compiler in-logic on the translated
+definitions.
+
+[approxCompErrScript.sml](approxCompErrScript.sml):
+Theorems about how to compose errors from truncated Taylor series
+for each supported elementary function
+
+[approxPolyScript.sml](approxPolyScript.sml):
+Function that computes a polynomial approximation for a single elementary
+function on a fixed interval, and its soundness proof.
+Function approxPoly is reused in transcApproxSemScript.sml to build the overall
+function implementing the first phase of Dandelion
+
+[checkerDefsScript.sml](checkerDefsScript.sml):
+Basic definitions used by Dandelion
+
+[checkerScript.sml](checkerScript.sml):
+Define high-level functions used by Dandelion and prove their
+soundness by composing soundness proofs from the included files
+
+[cosDeg3Script.sml](cosDeg3Script.sml):
+Simple cosine of degree 3
+
+[drangScript.sml](drangScript.sml):
+Proofs ported about extrema of real-valued, univariate functions,
+ported from the work by Harrison
+
+[euclidDivScript.sml](euclidDivScript.sml):
+Computable version of polynomial division and a correctness proof.
+Inspired by the implementation in Isabelle/HOL
+isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html
+used to implement a computable version of Sturm sequences
+
+[floverConnScript.sml](floverConnScript.sml):
+Connection to FloVer roundoff error analyzer, currently unused
+
+[mcLaurinApproxScript.sml](mcLaurinApproxScript.sml):
+Proofs of McLaurin series for the supported elementary functions
+described in transcLang file
+
+[moreRealScript.sml](moreRealScript.sml):
+small theorems extending HOL4's realTheory
+used throughout the development
+
+[pointCheckerProofsScript.sml](pointCheckerProofsScript.sml):
+Soundness theorem of the point-wise equivalence checker
+Currently unused
+
+[pointCheckerScript.sml](pointCheckerScript.sml):
+A simple checker for polynomial evaluation
+Part one of the soundness proof requires showing that the approximated
+polynomial agrees with what Remez thought the trancendental function behaves
+like on the set of points Ω
+
+[realPolyProofsScript.sml](realPolyProofsScript.sml):
+Some simple properties of polynomials on reals
+
+[realPolyScript.sml](realPolyScript.sml):
+Definition of datatype for real-valued polynomials
+
+[realZeroLib.sml](realZeroLib.sml):
+Library automating Dandelion's certificate validation
+
+[renameScript.sml](renameScript.sml):
+renaming theory to unify naming of theorems
+
+[sinDeg3Script.sml](sinDeg3Script.sml):
+Simple approximation of sine of degree 3
+
+[sturmComputeScript.sml](sturmComputeScript.sml):
+Define a computable version of the sturm sequence and
+prove its equivalence with the non-computable version
+of John Harrison
+
+[sturmScript.sml](sturmScript.sml):
+Proof of Sturm's theorem, ported from Harrison material
+
+[transcApproxSemScript.sml](transcApproxSemScript.sml):
+Define an "approximating" semantics on the elementary functions
+of Dandelion. The function approxTransc corresponds to the
+function "approxAsPoly" in the paper
+
+[transcIntvSemScript.sml](transcIntvSemScript.sml):
+Define an interval semantics on the elementary functions
+of Dandelion. The function borrows the definitions and soundness
+proof of basic arithmetic from FloVer
+
+[transcLangScript.sml](transcLangScript.sml):
+Define a simple "language" for describing elementary
+functions. For now we only allow combinations, i.e.
+exp (sin (cos ...) but no additional operators like +,-,*,/
+
+[transcReflectScript.sml](transcReflectScript.sml):
+Simple reflection function translating elements of the deeply
+embedded transc datatype into the polynomials defined in
+realPolyScript.sml
diff --git a/tools/dandelion/bitArithLib.sml b/tools/dandelion/bitArithLib.sml
deleted file mode 100644
index 164b7d4540..0000000000
--- a/tools/dandelion/bitArithLib.sml
+++ /dev/null
@@ -1,125 +0,0 @@
-(**
-  Library implementing Karatsuba multiplication for the HOL4 evaluator
-  based on the theorems in bitArithScript.sml
-**)
-structure bitArithLib =
-struct
-  open HolKernel Parse Theory arithmeticTheory realTheory
-        boolLib bossLib; (* HOL4 dependencies *)
-  open bitArithTheory; (* Theory dependencies *)
-
-  (** A simple karatsuba conversion **)
-  val karatsuba_lim = ref $ Arbnum.fromInt 200
-
-  val mk_frac_thm = DB.find_all "mk_frac_thm" |> hd |> snd |> #1
-  val id_thm = DB.find_all "id_thm" |> hd |> snd |> #1
-  val mul_frac_thm = DB.find_all "mul_frac_thm" |> hd |> snd |> #1
-
-  local
-    val subst_let_conv = (REWR_CONV LET_THM THENC BETA_CONV)
-    fun eval_let_conv c = RAND_CONV c THENC subst_let_conv
-    fun rhs_fun_conv c = RIGHT_CONV_RULE $ RAND_CONV c
-    fun karatsuba_rec_conv tm = let
-      val bs1 = rand $ rator $ rand tm
-      val bs2 = rand $ rand tm
-      val len_bs1 = numSyntax.dest_numeral $ rhs o concl $ EVAL “LENGTH ^bs1”
-      val len_bs2 = numSyntax.dest_numeral $ rhs o concl $ EVAL “LENGTH ^bs2”
-      in
-        if Arbnum.<(len_bs1,!karatsuba_lim) orelse Arbnum.<(len_bs2,!karatsuba_lim)
-        then  (RAND_CONV EVAL) tm
-        else let
-      val _ = print "."
-      val th = SPECL [bs1, bs2] karatsuba_bit
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let d = ... *)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let x1 = ... *)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let x0 = ... *)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let y1 = ... *)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let y0 = ... *)
-      (** Ugly: Get rid of lets for mults **)
-      val z0 = th |> rhs o concl |> rand |> rand
-      val th = th |> rhs_fun_conv subst_let_conv (* inline z0 *)
-      val z2 = th |> rhs o concl |> rand |> rand
-      val th = th |> rhs_fun_conv subst_let_conv (* inline z2 *)
-      (** Continue eval **)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let z1a = ... *)
-      val th = th |> rhs_fun_conv (eval_let_conv EVAL) (* let z1b = ... *)
-      (** Ugly: More inlining **)
-      val z1Mul = th |> rhs o concl |> rand |> rand
-      val th = th |> rhs_fun_conv subst_let_conv (* inline z1Mul *)
-      val th = th |> rhs_fun_conv subst_let_conv (* inline z1Sub *)
-      (** Now evaluate the terms we inlined **)
-      val z0Eval = karatsuba_rec_conv “bleval ^z0” (* z0 *)
-      val z2Eval = karatsuba_rec_conv “bleval ^z2” (* z2 *)
-      val z1MulEval = karatsuba_rec_conv “bleval ^z1Mul” (* z1Mul **)
-      (** Now first get down to ‘bleval (mul _ _)’ terms **)
-      (** TODO: Prove a single rewriting theorem for this part in the needed shape and apply it with REWR_CONV **)
-      val th2 = th |> REWRITE_RULE [add_thm, mulpow2_thm, sub_thm]
-      val th3 = th2 |> REWRITE_RULE [z0Eval, z2Eval, z1MulEval]
-  (** TODO: Use a single use theorem here too *)
-      val th4 = th3 |> REWRITE_RULE [GSYM add_thm, GSYM mulpow2_thm, GSYM sub_thm]
-      in
-        th4 |> rhs_fun_conv EVAL
-      end end;
-  in
-    fun karatsuba_conv tm =
-        let val (arg1, arg2) = numSyntax.dest_mult tm
-          val arg1_bval = ONCE_REWRITE_CONV [GSYM tobl_correct] arg1 |> RIGHT_CONV_RULE $ RAND_CONV EVAL
-          val arg2_bval = ONCE_REWRITE_CONV [GSYM tobl_correct] arg2 |> RIGHT_CONV_RULE $ RAND_CONV EVAL
-          val th = REWRITE_CONV [arg1_bval, arg2_bval] tm |> REWRITE_RULE [GSYM mul_thm]
-          val karat = th |> RIGHT_CONV_RULE $ karatsuba_rec_conv
-        in
-          karat |> REWRITE_RULE [GSYM fromBL_correct] |> RIGHT_CONV_RULE EVAL
-      end
-  end;
-
-  (** Now turn this into a conversion on reals **)
-  local
-    (* Apply conversion c to term tm if tm is not a negation,
-       otherwise use its rand with RAND_CONV **)
-    fun real_neg_app_conv c tm =
-      if realSyntax.is_negated tm then RAND_CONV c tm else c tm
-    fun app_karatsuba_conv tm =
-      if not $ numSyntax.is_mult tm then REFL tm
-      else karatsuba_conv tm
-  in
-  fun real_mul_conv tm =
-    if not $ realSyntax.is_mult tm then raise UNCHANGED else
-    let
-      val _ = print "rmc ";
-      val (lhsTm, rhsTm) = realSyntax.dest_mult tm
-      val ((lnom, lden), rw_lhs_thm) =
-        if realSyntax.is_div lhsTm
-        then (realSyntax.dest_div lhsTm, SPEC lhsTm id_thm)
-        else ((lhsTm, “1”), SPEC lhsTm mk_frac_thm)
-      val ((rnom, rden), rw_rhs_thm) =
-        if realSyntax.is_div rhsTm
-        then (realSyntax.dest_div rhsTm, SPEC rhsTm id_thm)
-        else ((rhsTm, “1”), SPEC rhsTm mk_frac_thm)
-      val th = tm |> ONCE_REWRITE_CONV [rw_lhs_thm, rw_rhs_thm]
-                |> RIGHT_CONV_RULE $ ONCE_REWRITE_CONV [mul_frac_thm]
-      (* Before multiplying, simplify *)
-      val th = th |> RIGHT_CONV_RULE $ REWRITE_CONV [mult_ints, MULT_CLAUSES]
-      val thKaratsuba_nom = th
-        |> RIGHT_CONV_RULE $ RATOR_CONV $ RAND_CONV $ real_neg_app_conv $
-              RAND_CONV app_karatsuba_conv
-      val thKaratsuba_denom = thKaratsuba_nom
-        |> RIGHT_CONV_RULE $ RAND_CONV $ real_neg_app_conv $ RAND_CONV app_karatsuba_conv
-    in
-      thKaratsuba_denom
-    end
-  end;
-
-  val _ =
-    (* record the library as a dependency for future theories *)
-    (Theory.add_ML_dependency "bitArithLib";
-      (*Theory.adjoin_to_theory
-        {sig_ps = NONE,
-          struct_ps =
-            SOME(fn _ => PP.add_string "val _ = bitArithLib.use_karatsuba();")}; *)
-      (* Remove old definitions of multiplication for reals and nums *)
-      computeLib.del_consts [“($*):real->real->real”, “($*):num->num->num”];
-      (* Add karatsuba multiplication as conversion for reals and nums *)
-      computeLib.add_convs [(“($*):real->real->real”,2, real_mul_conv),
-                            (“($*):num->num->num”, 2, karatsuba_conv)])
-
-end
diff --git a/tools/dandelion/bitArithScript.sml b/tools/dandelion/bitArithScript.sml
deleted file mode 100644
index b8dc6dfc55..0000000000
--- a/tools/dandelion/bitArithScript.sml
+++ /dev/null
@@ -1,546 +0,0 @@
-(**
-  Translation from HOL4 numbers to bit strings
-
-  Used in inital attempt to speed up computations, used by evaluation of the
-  first phase
-**)
-open HolKernel Parse BasicProvers listTheory arithmeticTheory;
-open realTheory;
-open boolLib bossLib;
-
-val _ = new_theory "bitArith";
-
-val _ = numLib.prefer_num();
-
-(** Code from Michael Norrish for translating to boolean vectors **)
-val tobl_def = new_specification(
-  "tobl_def", ["tobl"],
-  numeralTheory.bit_initiality
-    |> INST_TYPE [alpha |-> “:bool -> bool list”]
-    |> SPECL [“λb:bool. if b then [] else [T]”,
-              “λ(n:num) r b. b::(r b : bool list)”,
-              “λ(n:num) r b. ~b::r F”]
-    |> SIMP_RULE bool_ss [FUN_EQ_THM])
-
-val _ = computeLib.add_persistent_funs ["tobl_def"]
-
-Theorem tobl_NUMERAL[compute]: tobl (NUMERAL x) = tobl x
-Proof
-  simp[arithmeticTheory.NUMERAL_DEF]
-QED
-
-Theorem tobl0[compute]: tobl 0 b = tobl ZERO b
-Proof
-  simp[arithmeticTheory.ALT_ZERO]
-QED
-
-Definition bleval_def:
-  bleval [] = 0 ∧
-  bleval (T::rest) = 2 * bleval rest + 1 ∧
-  bleval (F::rest) = 2 * bleval rest
-End
-
-Theorem bleval_APPEND:
-  bleval (xs ++ ys) = bleval ys * 2 EXP (LENGTH xs) + bleval xs
-Proof
-  Induct_on ‘xs’ >> simp[FORALL_BOOL, bleval_def] >>
-  simp[arithmeticTheory.EXP]
-QED
-
-Theorem EVERYF_bleval0:
-  bleval bs = 0 ⇔ EVERY ((=) F) bs
-Proof
-  Induct_on ‘bs’ >> simp[bleval_def, FORALL_BOOL]
-QED
-
-Theorem EVERYF_suffix_bleval:
-  EVERY ((=) F) s ⇒ bleval (p ++ s) = bleval p
-Proof
-  simp[bleval_APPEND, EVERYF_bleval0]
-QED
-
-Theorem LASTbl_nonzero:
-  LAST (x::xs) ⇒ 0 < bleval (x::xs)
-Proof
-  qid_spec_tac ‘x’ >> Induct_on ‘xs’ >> simp[bleval_def] >> rpt gen_tac >>
-  rename [‘bleval (a::b::xs)’] >> Cases_on ‘a’ >> simp[bleval_def]
-QED
-
-Theorem tobl_correct:
-  bleval (tobl n T) = n ∧
-  bleval (tobl n F) = n + 1
-Proof
-  Induct_on ‘n’ using numeralTheory.bit_induction >>
-  simp[tobl_def, bleval_def] >> rpt strip_tac
-  >- simp[arithmeticTheory.ALT_ZERO]
-  >- simp[arithmeticTheory.ALT_ZERO] >>
-  simp[SimpRHS, Once arithmeticTheory.BIT1] >>
-  simp[SimpRHS, Once arithmeticTheory.BIT2]
-QED
-
-Definition frombl_def:
-  frombl addedp [] = 0 ∧
-  frombl T [T] = ZERO ∧
-  frombl F [T] = BIT1 ZERO ∧
-  frombl T (F::rest) = BIT1 (frombl T rest) ∧
-  frombl F (F::rest) = BIT2 (frombl T rest) ∧
-  frombl T (T::rest) = BIT2 (frombl T rest) ∧
-  frombl F (T::rest) = BIT1 (frombl F rest)
-End
-
-Theorem frombl_correct:
-  bl ≠ [] ∧ LAST bl ⇒
-  frombl F bl = bleval bl ∧
-  frombl T bl = bleval bl - 1
-Proof
-  Induct_on ‘bl’ >> simp[] >> Cases_on ‘bl’ >> gs[] >>
-  simp[frombl_def, bleval_def]
-  >- (simp[Once arithmeticTheory.BIT1, SimpLHS] >>
-      simp[arithmeticTheory.ALT_ZERO]) >>
-  rpt strip_tac >> gs[] >> rename [‘frombl _ (x::y::xs)’] >>
-  Cases_on ‘x’ >> simp[frombl_def, bleval_def]
-  >- simp[Once arithmeticTheory.BIT1, SimpLHS]
-  >- (simp[Once arithmeticTheory.BIT2, SimpLHS] >>
-      ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
-      simp[LASTbl_nonzero])
-  >- (simp[Once arithmeticTheory.BIT2, SimpLHS] >>
-      ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
-      simp[LASTbl_nonzero]) >>
-  simp[Once arithmeticTheory.BIT1, SimpLHS] >>
-  ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
-  simp[LASTbl_nonzero]
-QED
-
-Definition fromBL_def:
-  fromBL bs =
-  if bs = [] then 0
-  else
-    let bs1 = REV bs []
-    in
-      case HD bs1 of
-        T => NUMERAL (frombl F bs)
-      | F =>
-          let
-            bs2 = dropWhile ((=) F) bs1 ;
-            bs3 = REV bs2 [] ;
-          in
-            if bs3 = [] then 0 else NUMERAL (frombl F bs3)
-End
-
-Theorem fromBL_correct:
-  fromBL bs = bleval bs
-Proof
-  rw[fromBL_def, bleval_def] >> gs[GSYM listTheory.REVERSE_REV]
-  >- (Cases_on ‘bs’ using listTheory.SNOC_CASES >>
-      gvs[listTheory.REVERSE_SNOC] >>
-      simp[arithmeticTheory.NUMERAL_DEF] >> irule (cj 1 frombl_correct) >>
-      simp[])
-  >- gs[listTheory.dropWhile_eq_nil, EVERYF_bleval0] >>
-  gs[listTheory.dropWhile_eq_nil, listTheory.EXISTS_MEM,
-     arithmeticTheory.NUMERAL_DEF] >>
-  pop_assum mp_tac >>
-  simp[Once listTheory.MEM_SPLIT_APPEND_last] >> rw[] >>
-  simp[listTheory.REVERSE_APPEND] >>
-  ‘EVERY ((=) F) (REVERSE sfx)’ by simp[listTheory.EVERY_MEM] >>
-  simp[listTheory.dropWhile_APPEND_EVERY, frombl_correct] >>
-  gs[EVERYF_suffix_bleval]
-QED
-
-(** Now use the code to develop bit list arithmetic and implement karatsuba
-    multiplication. The original idea is due to Magnus Myreen **)
-Definition add_aux_def:
-  add_aux [] bs F = bs ∧
-  add_aux [] [] T = [T] ∧
-  add_aux [] (F :: bs) T = T :: bs ∧
-  add_aux [] (T :: bs) T = F :: (add_aux [] bs T) ∧
-  add_aux bs [] F = bs ∧
-  add_aux (F :: bs) [] T = T :: bs ∧
-  add_aux (T :: bs) [] T = F :: (add_aux [] bs T) ∧
-  add_aux (F :: bs1) (F :: bs2) T = T ::(add_aux bs1 bs2 F) ∧
-  add_aux (F :: bs1) (F :: bs2) F = F :: (add_aux bs1 bs2 F) /\
-  add_aux (T :: bs1) (F :: bs2) F = T ::(add_aux bs1 bs2 F) /\
-  add_aux (T :: bs1) (F :: bs2) T = F :: (add_aux bs1 bs2 T) /\
-  add_aux (F :: bs1) (T :: bs2) T = F :: (add_aux bs1 bs2 T) /\
-  add_aux (F :: bs1) (T :: bs2) F = T ::(add_aux bs1 bs2 F) /\
-  add_aux (T :: bs1) (T :: bs2) T = T ::(add_aux bs1 bs2 T) /\
-  add_aux (T :: bs1) (T :: bs2) F = F :: (add_aux bs1 bs2 T)
-End
-
-Definition add_def:
-  add bs1 bs2 = add_aux bs1 bs2 F
-End
-
-Theorem add_aux_thm:
-  ∀m n b.
-    bleval (add_aux m n b) = bleval m + bleval n + if b then 1 else 0
-Proof
-  ho_match_mp_tac add_aux_ind \\ fs [add_aux_def,bleval_def]
-QED
-
-Theorem add_thm:
-  bleval (add m n) = bleval m + bleval n
-Proof
-  fs [add_def,add_aux_thm]
-QED
-
-Definition divpow2_def:
-  divpow2 ([]:bool list) k = [] ∧
-  divpow2 bs 0 = bs ∧
-  divpow2 (b::bs) (SUC k) = divpow2 bs k
-End
-
-Theorem DIV_POW2:
-  ∀ x y. 0 < y ⇒ 2 * x DIV (2 * y) = x DIV y
-Proof
-  rpt strip_tac >> gs[GSYM DIV_DIV_DIV_MULT]
-  >> ‘2 * x = x * 2’ by gs[]
-  >> pop_assum $ rewrite_tac o single
-  >> gs[MULT_DIV]
-QED
-
-Theorem divpow2_thm:
-  ∀ x k. bleval (divpow2 x k) = bleval x DIV (2 ** k)
-Proof
-  ho_match_mp_tac divpow2_ind >> gs[divpow2_def, bleval_def, ZERO_DIV]
-  >> rpt strip_tac
-  >> reverse $ Cases_on ‘b’ >> gs[bleval_def]
-  >- (
-    ‘2 ** SUC k = 2 * 2 ** k’ by gs[EXP]
-    >> ‘2 * bleval x = bleval x * 2’ by gs[]
-    >> pop_assum $ rewrite_tac o single
-    >> gs[MULT_DIV, DIV_POW2])
-  >> ‘2 ** SUC k = 2 * 2 ** k’ by gs[EXP]
-  >> ‘2 * bleval x = bleval x * 2’ by gs[]
-  >> gs[GSYM DIV_DIV_DIV_MULT]
-  >> ‘2 * bleval x = bleval x * 2’ by gs[]
-  >> pop_assum $ rewrite_tac o single
-  >> gs[DIV_MULT]
-QED
-
-(** TODO: Try a tail recursive version that drops leading 0s **)
-Definition modpow2_def:
-  modpow2 ([]:bool list) k = [] ∧
-  modpow2 bs 0 = [] ∧
-  modpow2 (b::bs) (SUC k) = b :: (modpow2 bs k)
-End
-
-Theorem bleval_less:
-  ∀ bs. bleval bs < 2 ** (LENGTH bs)
-Proof
-  ho_match_mp_tac bleval_ind >> gs[bleval_def] >> rw[]
-  >> irule LESS_LESS_EQ_TRANS >> qexists_tac ‘2 * 2 ** LENGTH bs’
-  >> conj_tac >> gs[EXP]
-QED
-
-Theorem bleval_less_large:
-  LENGTH bs ≤ k ⇒ bleval bs < 2 ** k
-Proof
-  rpt strip_tac >> irule LESS_LESS_EQ_TRANS
-  >> qexists_tac ‘2 ** LENGTH bs’ >> gs[bleval_less]
-QED
-
-Theorem modpow2_thm:
-  ∀ x k. bleval (modpow2 x k) = bleval x MOD (2 ** k)
-Proof
-  ho_match_mp_tac modpow2_ind >> gs[modpow2_def, bleval_def, ZERO_MOD]
-  >> rpt strip_tac >> reverse $ Cases_on ‘b’ >> gs[bleval_def]
-  >- (
-    Cases_on ‘LENGTH x < k’ >> gs[NOT_LESS]
-    >- (
-      ‘bleval x MOD 2 ** k = bleval x’ by gs[LESS_MOD, bleval_less_large]
-      >> pop_assum $ rewrite_tac o single
-      >> ‘2 * bleval x = bleval (F :: x)’ by gs[bleval_def]
-      >> pop_assum $ rewrite_tac o single
-      >> ‘bleval (F::x) MOD 2 ** SUC k = bleval (F::x)’
-        by gs[LESS_MOD, bleval_less_large]
-      >> pop_assum $ rewrite_tac o single)
-    >> gs[quantHeuristicsTheory.LENGTH_LE_NUM, bleval_APPEND]
-    >> ‘bleval l1 MOD 2 ** k = bleval l1’
-        by (gs[LESS_MOD] >> rpt VAR_EQ_TAC >> gs[bleval_less])
-    >> first_assum $ once_rewrite_tac o single
-    >> gs[LEFT_ADD_DISTRIB]
-    >> ‘2 * (bleval l2 * 2 ** k) = bleval l2 * 2 ** SUC k’ by gs[EXP]
-    >> pop_assum $ once_rewrite_tac o single
-    >> gs[]
-    >> ‘2 * bleval l1 = bleval (F :: l1)’ by gs[bleval_def]
-    >> pop_assum $ rewrite_tac o single
-    >> gs[bleval_less_large])
-  >> Cases_on ‘LENGTH x < k’ >> gs[NOT_LESS]
-  >- (
-    ‘bleval x MOD 2 ** k = bleval x’ by gs[LESS_MOD, bleval_less_large]
-    >> pop_assum $ rewrite_tac o single
-    >> ‘2 * bleval x + 1 = bleval (T :: x)’ by gs[bleval_def]
-    >> pop_assum $ rewrite_tac o single
-    >> ‘bleval (T::x) MOD 2 ** SUC k = bleval (T::x)’
-        by gs[LESS_MOD, bleval_less_large]
-    >> pop_assum $ rewrite_tac o single)
-  >> gs[quantHeuristicsTheory.LENGTH_LE_NUM, bleval_APPEND]
-  >> ‘bleval l1 MOD 2 ** k = bleval l1’
-      by (gs[LESS_MOD] >> rpt VAR_EQ_TAC >> gs[bleval_less])
-  >> first_assum $ once_rewrite_tac o single
-  >> gs[LEFT_ADD_DISTRIB]
-  >> ‘2 * (bleval l2 * 2 ** k) = bleval l2 * 2 ** SUC k’ by gs[EXP]
-  >> pop_assum $ once_rewrite_tac o single
-  >> gs[]
-  >> ‘2 * bleval l1 + 1 = bleval (T :: l1)’ by gs[bleval_def]
-  >> pop_assum $ rewrite_tac o single
-  >> gs[bleval_less_large]
-QED
-
-Definition mul_def:
-  mul [] _ = [] ∧
-  mul (T::bs) bs2 = add bs2 (mul bs (F::bs2)) ∧
-  mul (F::bs) bs2 = mul bs (F::bs2)
-End
-
-Theorem mul_thm:
-  ∀ x y. bleval (mul x y) = bleval x * bleval y
-Proof
-  ho_match_mp_tac mul_ind >> gs[mul_def, bleval_def, add_thm]
-QED
-
-Definition mulpow2_def:
-  mulpow2 [] _ = [] ∧
-  mulpow2 bs 0 = bs ∧
-  mulpow2 bs (SUC k) = F::(mulpow2 bs k)
-End
-
-Theorem mulpow2_thm:
-  ∀ bs k. bleval (mulpow2 bs k) =  bleval bs * 2 ** k
-Proof
-  ho_match_mp_tac mulpow2_ind >> gs[mulpow2_def, bleval_def, EXP]
-QED
-
-Definition lte_aux_def:
-  lte_aux [] [] = T ∧
-  lte_aux (F::bs1) (T::bs2) = T ∧
-  lte_aux (T::bs1) (F::bs2) = F ∧
-  lte_aux (T::bs1) (T::bs2) = lte_aux bs1 bs2 ∧
-  lte_aux (F::bs1) (F::bs2) = lte_aux bs1 bs2 ∧
-  lte_aux _ _ = F
-End
-
-Theorem lte_aux_thm:
-  ∀ bs1 bs2.
-    LENGTH bs1 = LENGTH bs2 ⇒
-    (lte_aux bs1 bs2 ⇔ bleval (REVERSE bs1) ≤ bleval (REVERSE bs2))
-Proof
-  ho_match_mp_tac lte_aux_ind >> rpt strip_tac
-  >> gs[lte_aux_def, bleval_def, bleval_APPEND]
-  >- (
-    ‘bleval (REVERSE bs1) ≤ 2 ** LENGTH (REVERSE bs1)’
-    by gs[LESS_OR_EQ, bleval_less]
-    >> ‘LENGTH (REVERSE bs1) = LENGTH bs2’ by gs[LENGTH_REVERSE]
-    >> irule LESS_EQ_TRANS
-    >> qexists_tac ‘2 ** LENGTH bs2’ >> gs[])
-  >> gs[NOT_LEQ]
-  >> ‘bleval (REVERSE bs2) < 2 ** LENGTH (REVERSE bs2)’
-    by gs[bleval_less]
-  >> ‘LENGTH (REVERSE bs2) = LENGTH bs2’ by gs[LENGTH_REVERSE]
-  >> ‘SUC (bleval (REVERSE bs2)) ≤ 2 ** LENGTH (REVERSE bs2)’
-    by gs[]
-  >> irule LESS_EQ_TRANS
-  >> qexists_tac ‘2 ** LENGTH bs2’ >> gs[]
-QED
-
-Definition zeroPad_def:
-  zeroPad [] [] = ([], []) ∧
-  zeroPad (b::bs1) [] =
-    (let (bs1pad, bs2pad) = zeroPad bs1 [] in
-      (b::bs1pad, F::bs2pad)) ∧
-  zeroPad [] (b::bs2) =
-    (let (bs1pad, bs2pad) = zeroPad [] bs2 in
-       (F::bs1pad, b::bs2pad)) ∧
-  zeroPad (b1::bs1) (b2::bs2) =
-    (let (bs1pad, bs2pad) = zeroPad bs1 bs2 in
-       (b1::bs1pad, b2::bs2pad))
-End
-
-Theorem zeroPad_thm:
-  ∀ bs1 bs2 bs1pad bs2pad.
-    zeroPad bs1 bs2 = (bs1pad, bs2pad) ⇒
-    bleval bs1 = bleval bs1pad ∧ bleval bs2 = bleval bs2pad ∧
-    LENGTH bs1pad = LENGTH bs2pad
-Proof
-  ho_match_mp_tac zeroPad_ind >> rpt strip_tac
-  >> gs[zeroPad_def, bleval_def, CaseEq"prod"]
-  >- (
-    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
-    >> Cases_on ‘b’ >> gs[bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[])
-  >- (
-    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
-    >> Cases_on ‘b’ >> gs[bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
-    >> Cases_on ‘b’ >> gs[bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[])
-  >- (
-    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
-    >> Cases_on ‘b1’ >> gs[bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
-    >> Cases_on ‘b2’ >> gs[bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[bleval_def])
-  >- (
-    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
-    >> rpt VAR_EQ_TAC >> gs[])
-QED
-
-Definition lte_def:
-  lte bs1 bs2 =
-  let (bs1pad, bs2pad) = zeroPad bs1 bs2 in
-    lte_aux (REV bs1pad []) (REV bs2pad [])
-End
-
-Theorem lte_thm:
-  ∀ bs1 bs2. lte bs1 bs2 ⇔ bleval bs1 ≤ bleval bs2
-Proof
-  rpt strip_tac >> gs[lte_def]
-  >> Cases_on ‘zeroPad bs1 bs2’ >> imp_res_tac zeroPad_thm
-  >> ‘LENGTH (REVERSE q) = LENGTH (REVERSE r)’ by gs[LENGTH_REVERSE]
-  >> first_assum $ mp_then Any mp_tac lte_aux_thm
-  >> gs[GSYM REVERSE_REV, REVERSE_REVERSE]
-QED
-
-Definition sub_aux_def:
-  sub_aux [] _ _ = [] ∧
-  sub_aux (F :: bs1) [] T = T :: (sub_aux bs1 [] T) ∧
-  sub_aux (T :: bs1) [] T = F :: bs1 ∧
-  sub_aux (F :: bs1) [] F = F :: bs1 ∧
-  sub_aux (T :: bs1) [] F = T :: bs1 ∧
-  sub_aux (F :: bs1) (F :: bs2) T = T :: (sub_aux bs1 bs2 T) ∧
-  sub_aux (F :: bs1) (F :: bs2) F = F :: (sub_aux bs1 bs2 F) ∧
-  sub_aux (F :: bs1) (T :: bs2) T = F :: (sub_aux bs1 bs2 T) ∧
-  sub_aux (F :: bs1) (T :: bs2) F = T :: (sub_aux bs1 bs2 T) ∧
-  sub_aux (T :: bs1) (F :: bs2) T = F :: (sub_aux bs1 bs2 F) ∧
-  sub_aux (T :: bs1) (F :: bs2) F = T :: (sub_aux bs1 bs2 F) ∧
-  sub_aux (T :: bs1) (T :: bs2) T = T :: (sub_aux bs1 bs2 T) ∧
-  sub_aux (T :: bs1) (T :: bs2) F = F :: (sub_aux bs1 bs2 F)
-End
-
-Definition sub_def:
-  sub bs1 bs2 = if lte bs2 bs1 then sub_aux bs1 bs2 F else []
-End
-
-Theorem sub_aux_thm:
-  ∀ bs1 bs2 b.
-    (bleval bs2 + if b then 1 else 0) ≤ bleval bs1 ⇒
-    bleval (sub_aux bs1 bs2 b) = bleval bs1 - (bleval bs2 + if b then 1 else 0)
-Proof
-  ho_match_mp_tac sub_aux_ind >> rpt conj_tac >> rpt strip_tac
-  >> gs[sub_aux_def, bleval_def, LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
-  >- (
-    TOP_CASE_TAC >> gs[]
-    >> ‘bleval bs1 = 1’ by (Cases_on ‘bleval bs1’ >> gs[])
-    >> gs[])
-  >- (
-    COND_CASES_TAC >> gs[]
-    >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
-    >> pop_assum $ once_rewrite_tac o single >> gs[])
-  >- (
-    COND_CASES_TAC >> gs[]
-    >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
-    >> pop_assum $ once_rewrite_tac o single >> gs[])
-  >- (
-    COND_CASES_TAC >> gs[]
-    >> ‘bleval bs2 ≤ bleval bs1’ by gs[]
-    >> ‘bleval bs2 = bleval bs1’ by gs[]
-    >> pop_assum $ once_rewrite_tac o single >> gs[])
-  >> COND_CASES_TAC >> gs[]
-  >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
-  >> pop_assum $ once_rewrite_tac o single >> gs[]
-QED
-
-Theorem sub_thm:
-  ∀ m n. bleval (sub m n) = bleval m - bleval n
-Proof
-  rw[sub_def, lte_thm, sub_aux_thm, bleval_def, SUB_EQ_0, NOT_LEQ]
-QED
-
-Theorem karatsuba_num:
-  ∀d x y.
-    0 < d ⇒
-    x * y =
-      let x1 = x DIV d in
-      let x0 = x MOD d in
-      let y1 = y DIV d in
-      let y0 = y MOD d in
-      let z0 = x0 * y0 in
-      let z2 = x1 * y1 in
-      let z1a = x1 + x0 in
-      let z1b = y1 + y0 in
-      let z1 = z1a * z1b in
-      let z1 = z1 - z2 - z0 in
-        (z2 * d + z1) * d + z0
-Proof
-  rpt strip_tac
-  \\ irule EQ_TRANS
-  \\ qexists_tac ‘(x DIV d * d + x MOD d) * (y DIV d * d + y MOD d)’
-  \\ conj_tac THEN1 metis_tac [DIVISION]
-  \\ fs [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB]
-QED
-
-Theorem karatsuba_bit:
-  ∀ x y.
-  bleval (mul x y) = bleval (
-    let d = (fromBL
-            (divpow2
-             (add (divpow2 (tobl (LENGTH x) F) 1)
-              (divpow2 (tobl (LENGTH y) F) 1)) 1)) + 1 in
-      let x1 = divpow2 x d in
-      let x0 = modpow2 x d in
-      let y1 = divpow2 y d in
-      let y0 = modpow2 y d in
-      let z0 = mul x0 y0 in
-      let z2 = mul x1 y1 in
-      let z1a = add x1 x0 in
-      let z1b = add y1 y0 in
-      let z1Mul = mul z1a z1b in
-      let z1 = sub (sub z1Mul z2) z0 in
-        add (mulpow2 (add (mulpow2 z2 d) z1) d) z0)
-Proof
-  rpt strip_tac >> rewrite_tac [mul_thm]
-  >> qmatch_goalsub_abbrev_tac ‘fromBL dVal’
-  >> qspecl_then [‘2 ** (fromBL dVal + 1)’, ‘bleval x’, ‘bleval y’] mp_tac karatsuba_num
-  >> impl_tac
-  >- (unabbrev_all_tac >> gs[fromBL_correct, divpow2_thm, add_thm])
-  >> disch_then $ rewrite_tac o single
-  >> unabbrev_all_tac
-  >> gs[divpow2_thm, modpow2_thm, add_thm, mul_thm, mulpow2_thm, sub_thm, fromBL_correct]
-QED
-
-(** Infrastructural Theorems for lib implementation **)
-Theorem mk_frac_thm[unlisted]:
-  !(x:real). x = x / 1
-Proof
-  gs[]
-QED
-
-Theorem id_thm[unlisted]:
-  ! (x:real). x = x
-Proof
-  gs[]
-QED
-
-Theorem mul_frac_thm[unlisted]:
-  ! a b c (d:real). (a / b) * (c / d) = (a * c) / (b * d)
-Proof
-  rpt gen_tac >> rewrite_tac [real_div, GSYM REAL_MUL_ASSOC]
-  >> ‘inv b * (c * inv d) = c * (inv b * inv d)’ by (gs[REAL_MUL_ASSOC] >> gs[REAL_MUL_COMM])
-  >> pop_assum $ once_rewrite_tac o single
-  >> gs[REAL_INV_MUL']
-QED
-
-val _ = export_theory();
diff --git a/tools/dandelion/certificate_DopplerScript.sml b/tools/dandelion/certificate_DopplerScript.sml
deleted file mode 100644
index 88ef069ea2..0000000000
--- a/tools/dandelion/certificate_DopplerScript.sml
+++ /dev/null
@@ -1,45 +0,0 @@
-open  FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
-open simpLib realTheory realLib RealArith;
-
-val _ = new_theory "certificate_Doppler";
-
-
-val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
-val C34_def = Define `C34:(real expr) = Const M64 ((3)/(5))`;
-val T2_def = Define `T2:(real expr) = Var 2`;
-val MultC34T2 = Define `MultC34T2:(real expr) = Binop Mult C34 T2`;;
-val PlusC12MultC34T2 = Define `PlusC12MultC34T2:(real expr) = Binop Plus C12 MultC34T2`;;
-val CastM32PlusC12MultC34T2 = Define `CastM32PlusC12MultC34T2 : real expr = Downcast M32 PlusC12MultC34T2`;;
-val t15_def = Define `t15:(real expr) = Var 5`;
-val UMint15 = Define `UMint15:(real expr) = Unop Neg t15`;
-val v1_def = Define `v1:(real expr) = Var 1`;
-val MultUMint15v1 = Define `MultUMint15v1:(real expr) = Binop Mult UMint15 v1`;;
-val u0_def = Define `u0:(real expr) = Var 0`;
-val Plust15u0 = Define `Plust15u0:(real expr) = Binop Plus t15 u0`;;
-val MultPlust15u0Plust15u0 = Define `MultPlust15u0Plust15u0:(real expr) = Binop Mult Plust15u0 Plust15u0`;;
-val DivMultUMint15v1MultPlust15u0Plust15u0 = Define `DivMultUMint15v1MultPlust15u0Plust15u0:(real expr) = Binop Div MultUMint15v1 MultPlust15u0Plust15u0`;;
-val RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `RetDivMultUMint15v1MultPlust15u0Plust15u0 = Ret DivMultUMint15v1MultPlust15u0Plust15u0`;
-val Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 = Let M32 5 CastM32PlusC12MultC34T2 RetDivMultUMint15v1MultPlust15u0Plust15u0`;
-
-
-val defVars_doppler_def = Define `
- defVars_doppler : typeMap = 
-(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_insert (Var 1) (M32) (FloverMapTree_insert (Var 5) (M32) (FloverMapTree_insert (Var 2) (M64) (FloverMapTree_empty)))))`;
-
-
-val thePrecondition_doppler_def = Define ` 
- thePreconditiondoppler (n:num):interval = 
-if n = 0 then ( (-100)/(1), (100)/(1)) else if n = 1 then ( (20)/(1), (20000)/(1)) else if n = 2 then ( (-30)/(1), (50)/(1)) else (0,1)`;
-
-val absenv_doppler_def = RIGHT_CONV_RULE EVAL (Define `
-  absenv_doppler:analysisResult = 
-FloverMapTree_insert (Var 5) (( (1567)/(5), (1807)/(5)) , (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert DivMultUMint15v1MultPlust15u0Plust15u0 (( (-180700000)/(1138489), (-156700)/(5322249)), (3128798615377558964734587413815260935766775940003133188505004688351541231456980597512692494850911181122476079460422247077079176104347591604229243224768895229048954292495195716430601972291603510900358841802949847973326821449585470105361794370971246392326730165769086503662250520953800794720080442853388469377023727444437325832874114769965213547362197536886857310450874114551302656316164631446184855133337791662127325138346785397490340980930573694307935576641198224172023812349312175410753884375)/(32036808664321353711103483032138488273658359037549607658529725639211828966830820254532621633000657987120666498279218129796043154742555162761269493533793888535784577584907972014998498622632370186488026019213317308445273559994196553084922725810710211676061848042954653773443813684285036579995330627524678538042961243278389567362111169788921619483881120057899533645621131479344403647093086239019570741449266701692934633407390503406115529744843066088021266694728367150101865392734271463782370359902208)) (FloverMapTree_insert MultPlust15u0Plust15u0 (( (1138489)/(25), (5322249)/(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)/(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert MultUMint15v1 (( (-7228000)/(1), (-6268)/(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)/(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMapTree_insert v1 (( (20)/(1), (20000)/(1)), (625)/(524288)) (FloverMapTree_insert UMint15 (( (-1807)/(5), (-1567)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert CastM32PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert MultC34T2 (( (-18)/(1), (30)/(1)), (3650833728657301081634471694827535)/(365375409332725729550921208179070754913983135744)) (FloverMapTree_insert T2 (( (-30)/(1), (50)/(1)), (25)/(4503599627370496)) (FloverMapTree_insert C34 (( (3)/(5), (3)/(5)), (3)/(45035996273704960)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))))))))))))))))))`);
-
-val _ = store_thm ("ErrorBound_doppler_Sound",
-``?Gamma. CertificateCheckerCmd
-Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0
-absenv_doppler thePreconditiondoppler defVars_doppler = SOME Gamma``,
- flover_eval_tac \\ fs[REAL_INV_1OVER]);
-
-
- val _ = export_theory();
diff --git a/tools/dandelion/cosDeg5Script.sml b/tools/dandelion/cosDeg5Script.sml
deleted file mode 100644
index 3e642dc70c..0000000000
--- a/tools/dandelion/cosDeg5Script.sml
+++ /dev/null
@@ -1,27 +0,0 @@
-open realLib realZeroLib bitArithLib;
-open preambleDandelion;
-
-val _ = new_theory "cosDeg5";
-
-Definition cos_example_def:
-  cos_example =
-<|
-  transc := Fun Cos (Var "x");
-  poly := [
-     2147500729  * inv ( 2 pow  31 );
-     -1335232053  * inv ( 2 pow  43 );
-     -4286087759  * inv ( 2 pow  33 );
-     -1814406069  * inv ( 2 pow  39 );
-     3231673215  * inv ( 2 pow  36 );
-     -2371596027  * inv ( 2 pow  39 );
-    ];
-  eps :=  30519469678010330798002460719449001203933634455913  * inv (2 pow 186 );
-  iv := [ ("x",
-    ( 37414441915671114706014331717536845303191873100185  * inv (2 pow 168 ),
-      1  * inv (2 pow 0 )))];
-|>
-End
-
-Theorem checkerSucceeds = validateCert cos_example_def “16:num”;
-
-val _ = export_theory();
diff --git a/tools/dandelion/euclidDivScript.sml b/tools/dandelion/euclidDivScript.sml
index 30c7c7283f..ee1c290d8b 100644
--- a/tools/dandelion/euclidDivScript.sml
+++ b/tools/dandelion/euclidDivScript.sml
@@ -1,8 +1,9 @@
 (**
   Computable version of polynomial division and a correctness proof.
   Inspired by the implementation in Isabelle/HOL
-  https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html
-  used to implement a computable version of Sturm sequences **)
+  isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html
+  used to implement a computable version of Sturm sequences
+**)
 open pred_setTheory listTheory bossLib RealArith realTheory polyTheory;
 open realPolyTheory sturmTheory realPolyProofsTheory;
 open renameTheory;
@@ -79,7 +80,8 @@ Proof
     by (
        VAR_EQ_TAC >> gs[Abbr‘rrr’, Abbr‘b’]
        >> irule LESS_EQ_TRANS
-       >> qexists_tac ‘if zerop (monom n [qq]) ∨ zerop d then 0 else deg (monom n [qq]) + deg d’
+       >> qexists_tac ‘if zerop (monom n [qq]) ∨ zerop d then 0
+                       else deg (monom n [qq]) + deg d’
        >> gs[deg_mul_poly]
        >> cond_cases_tac >> gs[]
        >> Cases_on ‘qq = 0’ >> gs[]
@@ -97,7 +99,8 @@ Proof
          >> conj_tac
          >- irule deg_sub_poly
          >> gs[])
-  >> first_x_assum $ qspecl_then [‘lc’, ‘qqq’, ‘rrr’, ‘d’, ‘dr - 1’, ‘q'’, ‘r'’] mp_tac
+  >> first_x_assum $
+       qspecl_then [‘lc’, ‘qqq’, ‘rrr’, ‘d’, ‘dr - 1’, ‘q'’, ‘r'’] mp_tac
   >> impl_tac
   >- (
     gs[] >> reverse $ Cases_on ‘dr’ >- gs[]
@@ -115,11 +118,13 @@ Proof
   >> gs[FUN_EQ_THM, eval_simps]
   >> rpt gen_tac
   >> qmatch_goalsub_abbrev_tac ‘_ = lc pow _ * ( _ * (_ * _ + mnm) + _)’
-  >> ‘evalPoly d x * (lc * evalPoly q x + mnm) = lc * (evalPoly d x * evalPoly q x) + evalPoly d x * mnm’
+  >> ‘evalPoly d x * (lc * evalPoly q x + mnm) =
+      lc * (evalPoly d x * evalPoly q x) + evalPoly d x * mnm’
      by real_tac
   >> pop_assum $ rewrite_tac o single
   >> rewrite_tac [GSYM REAL_ADD_ASSOC]
-  >> ‘evalPoly d x * mnm + (lc * evalPoly r x - evalPoly d x * mnm) = lc * evalPoly r x’ by real_tac
+  >> ‘evalPoly d x * mnm + (lc * evalPoly r x - evalPoly d x * mnm) =
+      lc * evalPoly r x’ by real_tac
   >> pop_assum $ rewrite_tac o single
   >> rewrite_tac [GSYM REAL_LDISTRIB]
   >> rewrite_tac [REAL_MUL_ASSOC]
diff --git a/tools/dandelion/mcLaurinApproxScript.sml b/tools/dandelion/mcLaurinApproxScript.sml
index 2af4dc4714..bea01bb11d 100644
--- a/tools/dandelion/mcLaurinApproxScript.sml
+++ b/tools/dandelion/mcLaurinApproxScript.sml
@@ -1,6 +1,7 @@
 (***
   Proofs of McLaurin series for the supported elementary functions
-  described in transcLang file **)
+  described in transcLang file
+**)
 
 open moreRealTheory realPolyTheory realPolyProofsTheory;
 open preambleDandelion;
@@ -364,6 +365,7 @@ Proof
       >> pop_assum $ rewrite_tac o single
       >> gs[REAL_LDISTRIB]
     )
+  >> pop_assum $ once_rewrite_tac o single
   >> gs[]
 QED
 
diff --git a/tools/dandelion/moreRealScript.sml b/tools/dandelion/moreRealScript.sml
index 42b4222156..10648eb9ec 100644
--- a/tools/dandelion/moreRealScript.sml
+++ b/tools/dandelion/moreRealScript.sml
@@ -283,7 +283,8 @@ Theorem cos_pi2_pi_le:
     pi / 2 ≤ x ∧ x ≤ pi ⇒
     cos x ≤ 0
 Proof
-  rpt strip_tac >> Cases_on ‘x = pi/2’ >- gs[COS_PI2]
+  rpt strip_tac >> Cases_on ‘x = pi/2’
+  >- (VAR_EQ_TAC >> gs[COS_PI2])
   >> ‘pi/2 < x’ by real_tac
   >> qspecl_then [‘cos’, ‘λ x. - sin x’, ‘pi/2’, ‘x’] mp_tac MVT_ALT
   >> impl_tac
diff --git a/tools/dandelion/readmePrefix b/tools/dandelion/readmePrefix
new file mode 100644
index 0000000000..34a61bacf3
--- /dev/null
+++ b/tools/dandelion/readmePrefix
@@ -0,0 +1,43 @@
+# Dandelion
+
+A certificate checker for approximations of elementary functions.
+
+## Key theorems and definitions relating to the original ITP'22 paper
+
+The first phase is defined across the files `transcApproxSemScript.sml` and
+`approxPolyScript.sml`. The first file defines the overall approximation
+function `approxAsPoly` and gives its soundness proof, and
+`approxPolyScript.sml` defines the low-level approximation function for
+approximating a single elementary function with a single polynomial and proves
+soundness of this function.
+
+Theorem 4 (First Phase Soundness) from section 3 is proven in file
+`transcApproxSemScript.sml` as `approxTransc_sound`.
+Variants of Theorem 5 are proven for the supported elementary function in file
+`mcLaurinApproxScript.sml` if they are not provided by HOL4.
+Variants of Theorem 6 are proven for the supported elementary functions in file
+`approxPolyScript.sml`.
+
+The second phase is implemented and proven sound in the file
+`checkerScript.sml`.
+It relies on the implementation of computable Sturm sequences in
+`sturmComputeScript.sml` and computable polynomial division in
+`euclidDivScript.sml`.
+
+Theorem 7 (Second Phase Soundness) from section 4 is proven in file
+`checkerScript.sml` as the combination of `numZeros_sound`,
+`validBounds_is_valid`, and `validateZerosLeqErr_sound`.
+
+Theorem 8 was ported from Harrison's HOL-Light proofs in file `drangScript.sml`
+and is called `BOUND_THEOREM_INEXACT`.
+
+Theorem 9 (Dandelion soundness) is called `checker_soundness` in file
+`checkerScript.sml`.
+
+The extracted binary is created in the directory `binary`.
+File `translateScript.sml` sets up the CakeML translation of the definitions of
+Dandelion, file `certParserScript.sml` defines our (unverified) parser and
+lexer, file `sturmMainCakeScript.sml` proves the CakeML specification for the
+binary, and file `sturmMainCakeCompileScript.sml` compiles the binary for the
+second phase by running the CakeML compiler in-logic on the translated
+definitions.
\ No newline at end of file
diff --git a/tools/dandelion/realDeepScript.sml b/tools/dandelion/realDeepScript.sml
deleted file mode 100644
index 69a9838d9e..0000000000
--- a/tools/dandelion/realDeepScript.sml
+++ /dev/null
@@ -1,23 +0,0 @@
-(** A deep embedding of real-number arithmetic,
-    needed to do automatic differentiation **)
-open preambleDandelion;
-
-val _ = new_theory "realDeep";
-
-Datatype:
-  rUop = Inv | Neg
-End
-
-Datatype:
-  rBop = Add | Sub | Mul | Div
-End
-
-Datatype:
-  deepReal =
-    Cst int num
-    | Var string
-    | Uop rUop deepReal
-    | Bop rBop deepReal deepReal
-End
-
-val _ = export_theory();
diff --git a/tools/dandelion/sinDeg3Script.sml b/tools/dandelion/sinDeg3Script.sml
index 5f36b7fd24..aa2b39e800 100644
--- a/tools/dandelion/sinDeg3Script.sml
+++ b/tools/dandelion/sinDeg3Script.sml
@@ -25,6 +25,6 @@ Definition sin_example_def:
   |>
 End
 
-Theorem checkerSucceeds = validateCert sin_example_def “16:num”;
+Theorem checkerSucceeds = validateCert sin_example_def “8:num”;
 
 val _ = export_theory();
diff --git a/tools/dandelion/sturmScript.sml b/tools/dandelion/sturmScript.sml
index 2b2087a04d..b725cf275b 100644
--- a/tools/dandelion/sturmScript.sml
+++ b/tools/dandelion/sturmScript.sml
@@ -1209,7 +1209,7 @@ Proof
 QED
 
 Theorem lemma4[local]:
-  (!k. (i:num->real) k < i(SUC k)) ==> !k n. ~((i k + i (SUC k)) / &2 = i n)
+  (!k. (i:num->real) k < i(SUC k)) ==> !k n. ~((i k + i (SUC k)) = 2 * i n)
 Proof
   DISCH_TAC >> REPEAT GEN_TAC
   >> ONCE_REWRITE_TAC[GSYM REAL_LE_ANTISYM] >> STRIP_TAC
@@ -1338,7 +1338,7 @@ Proof
     >> ‘k= SUC(PRE k)’ by gs[]
     >> ‘i k = i (SUC (PRE k))’ by metis_tac[]
     >> pop_assum $ rewrite_tac o single
-    >> irule lemma4 >> metis_tac[]
+    >> irule (SIMP_RULE (simpLib.mk_simpset [realSimps.RMULRELNORM_ss]) [] lemma4) >> metis_tac[]
   )
   >> GEN_TAC >> gs[]
   >> ASM_CASES_TAC “k:num =0” >> ASM_REWRITE_TAC[]