Add snapshots of theorem prover definitions

31 files changed, 6781 insertions, 0 deletions

diff --git a/prover_snapshots/hol4/lib/lem/Holmakefile b/prover_snapshots/hol4/lib/lem/Holmakefile
new file mode 100644
index 0000000..0d07567
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/Holmakefile
@@ -0,0 +1,14 @@
+ifdef POLY
+HOLHEAP_NAME = lemheap
+EXTRA_CLEANS = $(HOLHEAP_NAME) $(HOLHEAP_NAME).o 
+
+BARE_DEPS = lemLib lemTheory lem_pervasivesTheory lem_pervasives_extraTheory lem_stringTheory lem_wordTheory
+DEPS = $(patsubst %,%.uo,$(BARE_DEPS))
+
+.PHONY: all
+all: $(HOLHEAP_NAME) 
+
+$(HOLHEAP_NAME): $(DEPS)
+	rm -f $(HOLHEAP_NAME)
+	$(protect $(HOLDIR)/bin/buildheap) -o $@ $(BARE_DEPS)
+endif
diff --git a/prover_snapshots/hol4/lib/lem/lemLib.sml b/prover_snapshots/hol4/lib/lem/lemLib.sml
new file mode 100644
index 0000000..93d06dc
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lemLib.sml
@@ -0,0 +1,105 @@
+(*========================================================================*)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(*========================================================================*)
+
+
+structure lemLib =
+struct
+
+open HolKernel Parse boolLib bossLib;
+open lemTheory intReduce wordsLib;
+
+val run_interactive = ref false
+val lem_conv_eval = computeLib.EVAL_CONV
+val lem_conv_simp = SIMP_CONV (srw_ss()++permLib.PERM_ss) [] 
+
+
+val lem_convs = [lem_conv_eval, lem_conv_simp];
+
+
+datatype test_result =
+    Success
+  | Fail
+  | Unknown of term
+
+
+fun lem_run_single_test (t:term) conv = 
+case total conv t of
+    NONE => NONE
+  | SOME thm => 
+      if (can EQT_ELIM thm) then SOME Success else
+      if (can EQF_ELIM thm) then SOME Fail else
+      NONE
+;
+
+fun lem_run_test t = 
+  case Lib.get_first (lem_run_single_test t) lem_convs of
+      NONE => Unknown (rhs (concl (EVAL t)))
+    | SOME r => r
+
+
+fun lem_assertion s t =
+let
+    open PPBackEnd Parse;
+    fun terminal_print sty s = (if !run_interactive then print_with_style sty s else
+      Lib.with_flag (Parse.current_backend, PPBackEnd.vt100_terminal) (print_with_style sty) s);
+    val _ = print "Testing ";
+    val _ = terminal_print [FG LightBlue] s;
+    val _ = print ": ``";
+    val _ = print_term t;
+    val _ = print ("`` ");
+    val result = lem_run_test t;
+    val _ = case result of
+                Success => terminal_print [FG Green] "OK\n"
+              | Fail => (terminal_print [FG OrangeRed] "FAILED\n";
+                         if (not (!run_interactive)) then Process.exit Process.failure else ())
+              | Unknown t => (terminal_print [FG Yellow] "evaluation failed\n")
+(*                            print_term t;
+                              print "\n\n"*) 
+in
+    ()
+end;
+
+end
diff --git a/prover_snapshots/hol4/lib/lem/lemScript.sml b/prover_snapshots/hol4/lib/lem/lemScript.sml
new file mode 100644
index 0000000..d6bb1bc
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lemScript.sml
@@ -0,0 +1,284 @@
+(*========================================================================*)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(*========================================================================*)
+
+open finite_mapTheory finite_mapLib
+open HolKernel Parse boolLib bossLib;
+open pred_setSimps pred_setTheory
+open finite_mapTheory
+open set_relationTheory
+open integerTheory intReduce quantHeuristicsLib;
+open wordsTheory
+
+val _ = numLib.prefer_num();
+
+(* From BasicProvers, for compatibility with older versions of HOL *)
+fun subgoal q = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC
+
+val _ = new_theory "lem"
+
+val failwith_def = Define `failwith (s:'a) = (ARB:'b)`;
+
+val set_CASE_def = zDefine `
+  set_CASE s c_emp c_sing c_else =
+    (if s = {} then c_emp else (
+     if (FINITE s /\ (CARD s = 1)) then c_sing (CHOICE s) else
+     c_else))`
+
+val set_CASE_emp = prove ( 
+``!c_emp c_sing c_else. set_CASE {} c_emp c_sing c_else = c_emp``,
+  SIMP_TAC std_ss [set_CASE_def])
+
+
+
+val set_CASE_sing = prove (
+``!x c_emp c_sing c_else. set_CASE {x} c_emp c_sing c_else = c_sing x``,
+  SIMP_TAC (std_ss++PRED_SET_ss) [set_CASE_def])
+
+
+val set_CASE_infinite = prove (``~(FINITE s) ==> (set_CASE s c_emp c_sing c_else = c_else)``,
+REPEAT STRIP_TAC THEN
+`~ (s = {})` by METIS_TAC [FINITE_EMPTY] THEN
+ASM_SIMP_TAC (std_ss++PRED_SET_ss) [set_CASE_def])
+
+val set_CASE_else_two_elems = store_thm ("set_CASE_else_two_elems",
+``(x1 IN s /\ x2 IN s /\ ~(x1 = x2)) ==>
+  (set_CASE s c_emp c_sing c_else = c_else)``,
+
+REPEAT STRIP_TAC THEN
+Tactical.REVERSE (Cases_on `FINITE s`) THEN1 (
+  ASM_SIMP_TAC std_ss [set_CASE_infinite]
+) THEN
+
+`~(s = {})` by (PROVE_TAC [MEMBER_NOT_EMPTY]) THEN
+
+subgoal `2 <= CARD s` THEN1 (
+  `CARD {x1; x2} = 2` by ASM_SIMP_TAC (std_ss++PRED_SET_ss) [] THEN
+  `{x1; x2} SUBSET s` by ASM_SIMP_TAC (std_ss++PRED_SET_ss) [] THEN
+  PROVE_TAC [CARD_SUBSET]
+) THEN
+
+ASM_SIMP_TAC arith_ss [set_CASE_def]);
+
+
+val set_CASE_else_1 = prove (``~(x1 = x2) ==> (set_CASE (x1 INSERT (x2 INSERT s)) c_emp c_sing c_else = c_else)``,
+REPEAT STRIP_TAC THEN
+MATCH_MP_TAC set_CASE_else_two_elems THEN
+ASM_SIMP_TAC (std_ss++PRED_SET_ss) [])
+
+
+val set_CASE_else_2 = prove (``(x1 = x2) ==> (set_CASE (x1 INSERT (x2 INSERT s)) c_emp c_sing c_else = set_CASE (x2 INSERT s) c_emp c_sing c_else)``,
+SIMP_TAC (std_ss++PRED_SET_ss) [])
+
+
+val set_CASE_REWRITES = save_thm ("set_CASE_REWRITES",
+  LIST_CONJ (map GEN_ALL [set_CASE_emp, set_CASE_sing, set_CASE_else_1, set_CASE_else_2, set_CASE_infinite]));
+
+val _ = export_rewrites ["set_CASE_REWRITES"]
+
+
+val set_CASE_compute = store_thm ("set_CASE_compute", ``
+   (!c_sing c_emp c_else. set_CASE {} c_emp c_sing c_else = c_emp) /\
+   (!x c_sing c_emp c_else.
+      set_CASE {x} c_emp c_sing c_else = c_sing x) /\
+   (!x2 x1 s c_sing c_emp c_else.
+      x1 <> x2 ==>
+      (set_CASE (x1 INSERT x2 INSERT s) c_emp c_sing c_else =
+       c_else)) /\
+   (!x2 x1 s c_sing c_emp c_else.
+      (set_CASE (x1 INSERT x2 INSERT s) c_emp c_sing c_else =
+       if (x1 = x2) then set_CASE (x2 INSERT s) c_emp c_sing c_else else c_else))``,
+METIS_TAC[set_CASE_REWRITES]);
+
+
+val SET_FILTER_def = zDefine `
+ (SET_FILTER P s = ({e | e | (e IN s) /\ P e}))`;
+
+val SET_FILTER_REWRITES = store_thm ("SET_FILTER_REWRITES",``
+  (!P. (SET_FILTER P {} = {})) /\
+  (!P x s. P x ==> (SET_FILTER P (x INSERT s) = x INSERT (SET_FILTER P s))) /\
+  (!P x s. (~(P x) ==> (SET_FILTER P (x INSERT s) = SET_FILTER P s)))``,
+
+SIMP_TAC (std_ss++PRED_SET_ss) [SET_FILTER_def, EXTENSION] THEN
+METIS_TAC[])
+
+val _ = export_rewrites ["SET_FILTER_REWRITES"]
+
+
+val SET_FILTER_compute = store_thm ("SET_FILTER_compute",``
+  (!P. (SET_FILTER P {} = {})) /\
+  (!P x s. (SET_FILTER P (x INSERT s) = if P x then 
+        x INSERT (SET_FILTER P s) else (SET_FILTER P s)))``,
+METIS_TAC [SET_FILTER_REWRITES])
+
+
+val _ = computeLib.add_persistent_funs ["set_CASE_compute", "SET_FILTER_compute"]
+
+
+val SET_SIGMA_def = zDefine 
+  `SET_SIGMA P Q = { (x, y) | x IN P /\ y IN Q x }`;
+
+val SET_SIGMA_EMPTY = store_thm(
+  "SET_SIGMA_EMPTY",
+  ``!Q. SET_SIGMA {} Q = {}``,
+  SIMP_TAC (std_ss++PRED_SET_ss) [SET_SIGMA_def, EXTENSION]);
+val _ = export_rewrites ["SET_SIGMA_EMPTY"]
+val _ = computeLib.add_persistent_funs ["SET_SIGMA_EMPTY"]
+
+val SET_SIGMA_INSERT_LEFT = store_thm(
+  "SET_SIGMA_INSERT_LEFT",
+  ``!P Q x. SET_SIGMA (x INSERT P) Q = 
+     (IMAGE (\y. (x, y)) (Q x)) UNION (SET_SIGMA P Q)``,
+  SIMP_TAC (std_ss++PRED_SET_ss) [SET_SIGMA_def, EXTENSION] THEN
+  METIS_TAC[])
+val _ = export_rewrites ["SET_SIGMA_INSERT_LEFT"]
+val _ = computeLib.add_persistent_funs ["SET_SIGMA_INSERT_LEFT"]
+
+
+val _ = computeLib.add_persistent_funs ["list.LIST_TO_SET"]
+
+
+val FMAP_TO_SET_def = zDefine 
+  `FMAP_TO_SET m = IMAGE (\k. (k, FAPPLY m k)) (FDOM m)`;
+
+val FMAP_TO_SET_FEMPTY = store_thm ("FMAP_TO_SET_FEMPTY",
+  ``FMAP_TO_SET FEMPTY = {}``,
+SIMP_TAC std_ss [FMAP_TO_SET_def, FDOM_FEMPTY, IMAGE_EMPTY]);
+val _ = export_rewrites ["FMAP_TO_SET_FEMPTY"]
+val _ = computeLib.add_persistent_funs ["FMAP_TO_SET_FEMPTY"]
+
+val FMAP_TO_SET_FUPDATE = store_thm ("FMAP_TO_SET_FUPDATE",
+  ``FMAP_TO_SET (FUPDATE m (k, v)) = (k, v) INSERT (FMAP_TO_SET (m \\ k))``,
+SIMP_TAC (std_ss ++ PRED_SET_ss) [FMAP_TO_SET_def, FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION,
+  FDOM_DOMSUB, DOMSUB_FAPPLY_THM] THEN
+METIS_TAC[]);
+val _ = export_rewrites ["FMAP_TO_SET_FUPDATE"]
+val _ = computeLib.add_persistent_funs ["FMAP_TO_SET_FUPDATE"]
+
+
+val IN_FMAP_TO_SET = store_thm ("IN_FMAP_TO_SET",
+  ``(k, v) IN FMAP_TO_SET m = (FLOOKUP m k = SOME v)``,
+SIMP_TAC (std_ss++PRED_SET_ss) [FMAP_TO_SET_def, FLOOKUP_DEF] THEN
+METIS_TAC[optionTheory.option_CLAUSES])
+
+val FUPDATE_NEQ_FEMPTY = store_thm ("FUPDATE_NEQ_FEMPTY", ``(FUPDATE m (k, v) = FEMPTY) = F``,
+  SIMP_TAC (std_ss++PRED_SET_ss) [fmap_EXT, FDOM_FUPDATE, FDOM_FEMPTY])
+val _ = export_rewrites ["FUPDATE_NEQ_FEMPTY"]
+val _ = computeLib.add_persistent_funs ["FUPDATE_NEQ_FEMPTY"]
+
+val FUPDATE_EQ_FUPDATE = store_thm ("FUPDATE_EQ_FUPDATE", 
+  ``(FUPDATE m (k, v) = FUPDATE m' (k', v')) = 
+    (k IN FDOM (FUPDATE m' (k', v')) /\
+     (FUPDATE m' (k', v') ' k = v) /\
+     (m \\ k = (FUPDATE m' (k', v') \\ k))) ``,
+
+  EQ_TAC THEN STRIP_TAC THEN1 (
+     POP_ASSUM (ASSUME_TAC o GSYM) THEN
+     ASM_REWRITE_TAC [] THEN
+     SIMP_TAC std_ss [FDOM_FUPDATE, IN_INSERT, FAPPLY_FUPDATE, DOMSUB_FUPDATE]
+  ) THEN
+  FULL_SIMP_TAC std_ss [fmap_EXT, EXTENSION, FDOM_DOMSUB, IN_DELETE, FDOM_FUPDATE, IN_INSERT,
+     DOMSUB_FAPPLY_THM, FAPPLY_FUPDATE_THM] THEN
+  METIS_TAC[]
+)
+
+val _ = export_rewrites ["FUPDATE_EQ_FUPDATE"]
+val _ = computeLib.add_persistent_funs ["FUPDATE_EQ_FUPDATE"]
+
+
+val FEVERY_FUPDATE_DOMSUB = store_thm ("FEVERY_FUPDATE_DOMSUB",
+  ``(FEVERY P (FUPDATE m (k, v))) = (P (k, v) /\ FEVERY P (m \\ k))``,
+SIMP_TAC std_ss [FEVERY_FUPDATE, fmap_domsub]);
+
+val _ = computeLib.add_persistent_funs ["finite_map.FRANGE_FEMPTY", "finite_map.FRANGE_FUPDATE_DOMSUB", 
+  "finite_map.FEVERY_FEMPTY", "FEVERY_FUPDATE_DOMSUB"]
+
+val _ = computeLib.add_persistent_funs ["finite_map.o_f_FUPDATE", "finite_map.o_f_FEMPTY", 
+   "finite_map.FCARD_FEMPTY", "finite_map.FCARD_FUPDATE"]
+
+
+
+
+
+val rcomp_empty_1 = store_thm ("rcomp_empty_1",
+  ``({} OO r) = {}``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [rcomp_def, EXTENSION])
+
+val rcomp_empty_2 = store_thm ("rcomp_empty_2",
+  ``(r OO {}) = {}``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [rcomp_def, EXTENSION])
+
+val rcomp_insert_compute = store_thm ("rcomp_insert_compute",
+  ``(r1 OO ((x, y) INSERT r2)) = ((r1 OO r2) UNION (IMAGE (\ xy'. (FST xy', y)) (SET_FILTER (\ xy'. SND xy' = x) r1)))``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss++quantHeuristicsLib.QUANT_INST_ss [std_qp]) [rcomp_def, EXTENSION, SET_FILTER_def] THEN
+METIS_TAC[])
+
+val _ = computeLib.add_persistent_funs ["rcomp_insert_compute", "rcomp_empty_1", "rcomp_empty_2"]
+
+
+val rrestrict_eval = store_thm ("rrestrict_eval",
+  ``rrestrict r s = SET_FILTER (\ (x, y). x IN s /\ y IN s) r``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss++quantHeuristicsLib.QUANT_INST_ss [std_qp]) [rrestrict_def, EXTENSION, SET_FILTER_def])
+
+val domain_eval = store_thm ("domain_eval",
+  ``domain r = IMAGE FST r``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss++QUANT_INST_ss [std_qp]) [domain_def, EXTENSION])
+
+val range_eval = store_thm ("range_eval",
+  ``range r = IMAGE SND r``,
+SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss++QUANT_INST_ss [std_qp]) [range_def, EXTENSION])
+
+val _ = computeLib.add_persistent_funs ["rrestrict_eval", "domain_eval", "range_eval"]
+
+val w2int_def = Define `w2int (w : 'a word) = 
+  let i1 = (w2n w) in
+  let i2 = (INT_MAX (:'a)) in
+  if i1 > i2 then (int_of_num i1 - (int_of_num (UINT_MAX (:'a)))) - 1 else int_of_num i1`
+
+val w2ui_def = Define `w2ui (w : 'a word) = int_of_num (w2n w)`
+
+val _ = Define `MAP_TO_LIST m = SET_TO_LIST (\(x, y). FAPPLY m x = y)`
+
+val _ = export_theory()
diff --git a/prover_snapshots/hol4/lib/lem/lem_assert_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_assert_extraScript.sml
new file mode 100644
index 0000000..79d5eda
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_assert_extraScript.sml
@@ -0,0 +1,46 @@
+(*Generated by Lem from assert_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open stringTheory lemTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_assert_extra"
+
+
+(*open import {ocaml} `Xstring`*)
+(*open import {hol} `stringTheory` `lemTheory`*)
+(*open import {coq} `Coq.Strings.Ascii` `Coq.Strings.String`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+
+(* ------------------------------------ *)
+(* failing with a proper error message  *)
+(* ------------------------------------ *)
+
+(*val failwith: forall 'a. string -> 'a*)
+
+(* ------------------------------------ *)
+(* failing without an error message     *)
+(* ------------------------------------ *)
+
+(*val fail : forall 'a. 'a*)
+val _ = Define `
+ ((fail:'a)=  (failwith "fail"))`;
+
+
+(* ------------------------------------- *)
+(* assertions                            *)
+(* ------------------------------------- *)
+
+(*val ensure : bool -> string -> unit*)
+val _ = Define `
+ ((ensure:bool -> string -> unit) test msg=
+   (if test then
+    () 
+  else
+    failwith msg))`;
+
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml b/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml
new file mode 100644
index 0000000..4788ee1
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml
@@ -0,0 +1,503 @@
+(*Generated by Lem from basic_classes.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory ternaryComparisonsTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_basic_classes"
+
+(******************************************************************************)
+(* Basic Type Classes                                                         *)
+(******************************************************************************)
+
+(*open import Bool*) 
+
+(*open import {coq} `Coq.Strings.Ascii`*)
+(*open import {hol} `ternaryComparisonsTheory`*)
+
+(* ========================================================================== *)
+(* Equality                                                                   *)
+(* ========================================================================== *)
+
+(* Lem`s default equality (=) is defined by the following type-class Eq.
+   This typeclass should define equality on an abstract datatype 'a. It should
+   always coincide with the default equality of Coq, HOL and Isabelle.
+   For OCaml, it might be different, since abstract datatypes like sets
+   might have fancy equalities. *)
+
+(*class ( Eq 'a ) 
+  val = [isEqual] : 'a -> 'a -> bool
+  val <> [isInequal] : 'a -> 'a -> bool
+end*)
+
+
+(* (=) should for all instances be an equivalence relation 
+   The isEquivalence predicate of relations could be used here.
+   However, this would lead to a cyclic dependency. *)
+
+(* TODO: add later, once lemmata can be assigned to classes 
+lemma eq_equiv: ((forall x. (x = x)) &&
+                 (forall x y. (x = y) <-> (y = x)) &&
+                 (forall x y z. ((x = y) && (y = z)) --> (x = z)))
+*)
+
+(* Structural equality *)
+
+(* Sometimes, it is also handy to be able to use structural equality.
+   This equality is mapped to the build-in equality of backends. This equality
+   differs significantly for each backend. For example, OCaml can`t check equality
+   of function types, whereas HOL can.  When using structural equality, one should 
+   know what one is doing. The only guarentee is that is behaves like 
+   the native backend equality.
+
+   A lengthy name for structural equality is used to discourage its direct use.
+   It also ensures that users realise it is unsafe (e.g. OCaml can`t check two functions
+   for equality *)
+(*val unsafe_structural_equality : forall 'a. 'a -> 'a -> bool*)
+
+(*val unsafe_structural_inequality : forall 'a. 'a -> 'a -> bool*)
+(*let unsafe_structural_inequality x y=  not (unsafe_structural_equality x y)*)
+
+
+(* ========================================================================== *)
+(* Orderings                                                                  *)
+(* ========================================================================== *)
+
+(* The type-class Ord represents total orders (also called linear orders) *)
+(*type ordering = LT | EQ | GT*)
+
+val _ = Define `
+ ((orderingIsLess:ordering -> bool) LESS=        T)
+/\ ((orderingIsLess:ordering -> bool) _=        F)`;
+
+val _ = Define `
+ ((orderingIsGreater:ordering -> bool) GREATER=     T)
+/\ ((orderingIsGreater:ordering -> bool) _=     F)`;
+
+val _ = Define `
+ ((orderingIsEqual:ordering -> bool) EQUAL=       T)
+/\ ((orderingIsEqual:ordering -> bool) _=       F)`;
+
+
+val _ = Define `
+ ((ordering_cases:ordering -> 'a -> 'a -> 'a -> 'a) r lt eq gt=
+   (if orderingIsLess r then lt else
+  if orderingIsEqual r then eq else gt))`;
+
+
+
+(*val orderingEqual : ordering -> ordering -> bool*)
+
+val _ = Hol_datatype `
+(*  'a *) Ord_class= <| 
+  compare_method                 : 'a -> 'a -> ordering;
+  isLess_method         : 'a -> 'a -> bool;
+  isLessEqual_method    : 'a -> 'a -> bool;
+  isGreater_method      : 'a -> 'a -> bool;
+  isGreaterEqual_method : 'a -> 'a -> bool 
+|>`;
+
+
+
+(* Ocaml provides default, polymorphic compare functions. Let's use them
+   as the default. However, because used perhaps in a typeclass they must be 
+   defined for all targets. So, explicitly declare them as undefined for
+   all other targets. If explictly declare undefined, the type-checker won't complain and
+   an error will only be raised when trying to actually output the function for a certain
+   target. *)
+(*val defaultCompare   : forall 'a. 'a -> 'a -> ordering*)
+(*val defaultLess      : forall 'a. 'a -> 'a -> bool*)
+(*val defaultLessEq    : forall 'a. 'a -> 'a -> bool*)
+(*val defaultGreater   : forall 'a. 'a -> 'a -> bool*)
+(*val defaultGreaterEq : forall 'a. 'a -> 'a -> bool*) 
+
+
+val _ = Define `
+ ((genericCompare:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a -> 'a -> ordering) (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a)=
+   (if less x y then
+    LESS
+  else if equal x y then
+    EQUAL
+  else
+    GREATER))`;
+
+
+
+(*
+(* compare should really be a total order *)
+lemma ord_OK_1: (
+  (forall x y. (compare x y = EQ) <-> (compare y x = EQ)) &&
+  (forall x y. (compare x y = LT) <-> (compare y x = GT)))
+
+lemma ord_OK_2: (
+  (forall x y z. (x <= y) && (y <= z) --> (x <= z)) &&
+  (forall x y. (x <= y) || (y <= x))
+)
+*)
+
+(* let's derive a compare function from the Ord type-class *)
+(*val ordCompare : forall 'a. Eq 'a, Ord 'a => 'a -> 'a -> ordering*)
+val _ = Define `
+ ((ordCompare:'a Ord_class -> 'a -> 'a -> ordering)dict_Basic_classes_Ord_a x y=
+   (if ( dict_Basic_classes_Ord_a.isLess_method x y) then LESS else
+  if (x = y) then EQUAL else GREATER))`;
+
+
+val _ = Hol_datatype `
+(*  'a *) OrdMaxMin_class= <| 
+  max_method : 'a -> 'a -> 'a;
+  min_method : 'a -> 'a -> 'a
+|>`;
+
+
+(*val minByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*)
+val _ = Define `
+ ((minByLessEqual:('a -> 'a -> bool) -> 'a -> 'a -> 'a) le x y=  (if (le x y) then x else y))`;
+
+
+(*val maxByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*)
+val _ = Define `
+ ((maxByLessEqual:('a -> 'a -> bool) -> 'a -> 'a -> 'a) le x y=  (if (le y x) then x else y))`;
+
+
+(*val defaultMax : forall 'a. Ord 'a => 'a -> 'a -> 'a*)
+
+(*val defaultMin : forall 'a. Ord 'a => 'a -> 'a -> 'a*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_var_dict:'a Ord_class -> 'a OrdMaxMin_class)dict_Basic_classes_Ord_a= (<|
+
+  max_method := (maxByLessEqual  
+  dict_Basic_classes_Ord_a.isLessEqual_method);
+
+  min_method := (minByLessEqual  
+  dict_Basic_classes_Ord_a.isLessEqual_method)|>))`;
+
+
+
+(* ========================================================================== *)
+(* SetTypes                                                                   *)
+(* ========================================================================== *)
+
+(* Set implementations use often an order on the elements. This allows the OCaml implementation
+   to use trees for implementing them. At least, one needs to be able to check equality on sets.
+   One could use the Ord type-class for sets. However, defining a special typeclass is cleaner
+   and allows more flexibility. One can make e.g. sure, that this type-class is ignored for
+   backends like HOL or Isabelle, which don't need it. Moreover, one is not forced to also instantiate
+   the functions "<", "<=" ... *)
+
+(*class ( SetType 'a ) 
+  val {ocaml;coq} setElemCompare : 'a -> 'a -> ordering
+end*)
+
+val _ = Define `
+ ((boolCompare:bool -> bool -> ordering) T T=  EQUAL)
+/\ ((boolCompare:bool -> bool -> ordering) T F=  GREATER)
+/\ ((boolCompare:bool -> bool -> ordering) F T=  LESS)
+/\ ((boolCompare:bool -> bool -> ordering) F F=  EQUAL)`;
+
+
+(* strings *)
+
+(*val charEqual : char -> char -> bool*)
+
+(*val stringEquality : string -> string -> bool*)
+
+(* pairs *)
+
+(*val pairEqual : forall 'a 'b. Eq 'a, Eq 'b => ('a * 'b) -> ('a * 'b) -> bool*)
+(*let pairEqual (a1, b1) (a2, b2)=  (a1 = a2) && (b1 = b2)*)
+
+(*val pairEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b) -> ('a * 'b) -> bool*)
+
+(*val pairCompare : forall 'a 'b. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('a * 'b) -> ('a * 'b) -> ordering*)
+val _ = Define `
+ ((pairCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) -> 'a#'b -> 'a#'b -> ordering) cmpa cmpb (a1, b1) (a2, b2)=
+   ((case cmpa a1 a2 of
+      LESS => LESS
+    | GREATER => GREATER
+    | EQUAL => cmpb b1 b2
+  )))`;
+
+
+val _ = Define `
+ ((pairLess:'a Ord_class -> 'b Ord_class -> 'b#'a -> 'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2)=  (( 
+  dict_Basic_classes_Ord_b.isLess_method x1 y1) \/ (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) /\ ( dict_Basic_classes_Ord_a.isLess_method x2 y2))))`;
+
+val _ = Define `
+ ((pairLessEq:'a Ord_class -> 'b Ord_class -> 'b#'a -> 'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2)=  (( 
+  dict_Basic_classes_Ord_b.isLess_method x1 y1) \/ (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) /\ ( dict_Basic_classes_Ord_a.isLessEqual_method x2 y2))))`;
+
+
+val _ = Define `
+ ((pairGreater:'a Ord_class -> 'b Ord_class -> 'a#'b -> 'a#'b -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12=  (pairLess 
+  dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12))`;
+
+val _ = Define `
+ ((pairGreaterEq:'a Ord_class -> 'b Ord_class -> 'a#'b -> 'a#'b -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12=  (pairLessEq 
+  dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_tup2_dict:'a Ord_class -> 'b Ord_class ->('a#'b)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b= (<|
+
+  compare_method := (pairCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method);
+
+  isLess_method := 
+  (pairLess dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isLessEqual_method := 
+  (pairLessEq dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isGreater_method := 
+  (pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b);
+
+  isGreaterEqual_method := 
+  (pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b)|>))`;
+
+
+
+(* triples *)
+
+(*val tripleEqual : forall 'a 'b 'c. Eq 'a, Eq 'b, Eq 'c => ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool*)
+(*let tripleEqual (x1, x2, x3) (y1, y2, y3)=  ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, x3)) (y1, (y2, y3)))*)
+
+(*val tripleCompare : forall 'a 'b 'c. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> ordering*)
+val _ = Define `
+ ((tripleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) -> 'a#'b#'c -> 'a#'b#'c -> ordering) cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2)=
+   (pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))))`;
+
+
+val _ = Define `
+ ((tripleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'a#'b#'c -> 'a#'b#'c -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3)=  (pairLess 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))))`;
+
+val _ = Define `
+ ((tripleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'a#'b#'c -> 'a#'b#'c -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3)=  (pairLessEq 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))))`;
+
+
+val _ = Define `
+ ((tripleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'c#'b#'a -> 'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123=  (tripleLess 
+  dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123))`;
+
+val _ = Define `
+ ((tripleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'c#'b#'a -> 'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123=  (tripleLessEq 
+  dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_tup3_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class ->('a#'b#'c)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c= (<|
+
+  compare_method := (tripleCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method  dict_Basic_classes_Ord_c.compare_method);
+
+  isLess_method := 
+  (tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c);
+
+  isLessEqual_method := 
+  (tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c);
+
+  isGreater_method := 
+  (tripleGreater dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a);
+
+  isGreaterEqual_method := 
+  (tripleGreaterEq dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a)|>))`;
+
+
+(* quadruples *)
+
+(*val quadrupleEqual : forall 'a 'b 'c 'd. Eq 'a, Eq 'b, Eq 'c, Eq 'd => ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> bool*)
+(*let quadrupleEqual (x1, x2, x3, x4) (y1, y2, y3, y4)=  ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4))))*)
+
+(*val quadrupleCompare : forall 'a 'b 'c 'd. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) ->
+                                              ('d -> 'd -> ordering) -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> ordering*)
+val _ = Define `
+ ((quadrupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> ordering) cmpa cmpb cmpc cmpd (a1, b1, c1, d1) (a2, b2, c2, d2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc cmpd)) (a1, (b1, (c1, d1))) (a2, (b2, (c2, d2)))))`;
+
+
+val _ = Define `
+ ((quadrupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d (x1, x2, x3, x4) (y1, y2, y3, y4)=  (pairLess 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        dict_Basic_classes_Ord_d)) dict_Basic_classes_Ord_a (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4)))))`;
+
+val _ = Define `
+ ((quadrupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d (x1, x2, x3, x4) (y1, y2, y3, y4)=  (pairLessEq 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        dict_Basic_classes_Ord_d)) dict_Basic_classes_Ord_a (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4)))))`;
+
+
+val _ = Define `
+ ((quadrupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'd#'c#'b#'a -> 'd#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d x1234 y1234=  (quadrupleLess 
+  dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y1234 x1234))`;
+
+val _ = Define `
+ ((quadrupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'd#'c#'b#'a -> 'd#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d x1234 y1234=  (quadrupleLessEq 
+  dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y1234 x1234))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_tup4_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class ->('a#'b#'c#'d)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d= (<|
+
+  compare_method := (quadrupleCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method  dict_Basic_classes_Ord_c.compare_method  dict_Basic_classes_Ord_d.compare_method);
+
+  isLess_method := 
+  (quadrupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d);
+
+  isLessEqual_method := 
+  (quadrupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d);
+
+  isGreater_method := 
+  (quadrupleGreater dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c
+     dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isGreaterEqual_method := 
+  (quadrupleGreaterEq dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c
+     dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a)|>))`;
+
+
+(* quintuples *)
+
+(*val quintupleEqual : forall 'a 'b 'c 'd 'e. Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e => ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> bool*)
+(*let quintupleEqual (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)=  ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5)))))*)
+
+(*val quintupleCompare : forall 'a 'b 'c 'd 'e. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) ->
+                                              ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> ordering*)
+val _ = Define `
+ ((quintupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> ordering) cmpa cmpb cmpc cmpd cmpe (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd cmpe))) (a1, (b1, (c1, (d1, e1)))) (a2, (b2, (c2, (d2, e2))))))`;
+
+
+val _ = Define `
+ ((quintupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)=  (pairLess 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d
+           dict_Basic_classes_Ord_e))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5))))))`;
+
+val _ = Define `
+ ((quintupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)=  (pairLessEq 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d
+           dict_Basic_classes_Ord_e))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5))))))`;
+
+
+val _ = Define `
+ ((quintupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'e#'d#'c#'b#'a -> 'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e x12345 y12345=  (quintupleLess 
+  dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12345 x12345))`;
+
+val _ = Define `
+ ((quintupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'e#'d#'c#'b#'a -> 'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e x12345 y12345=  (quintupleLessEq 
+  dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12345 x12345))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_tup5_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class ->('a#'b#'c#'d#'e)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e= (<|
+
+  compare_method := (quintupleCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method  dict_Basic_classes_Ord_c.compare_method  dict_Basic_classes_Ord_d.compare_method  dict_Basic_classes_Ord_e.compare_method);
+
+  isLess_method := 
+  (quintupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_e);
+
+  isLessEqual_method := 
+  (quintupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_e);
+
+  isGreater_method := 
+  (quintupleGreater dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a);
+
+  isGreaterEqual_method := 
+  (quintupleGreaterEq dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a)|>))`;
+
+
+(* sextuples *)
+
+(*val sextupleEqual : forall 'a 'b 'c 'd 'e 'f. Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f => ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> bool*)
+(*let sextupleEqual (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)=  ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6))))))*)
+
+(*val sextupleCompare : forall 'a 'b 'c 'd 'e 'f. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) ->
+                                              ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('f -> 'f -> ordering) ->
+                                              ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> ordering*)
+val _ = Define `
+ ((sextupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) ->('f -> 'f -> ordering) -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> ordering) cmpa cmpb cmpc cmpd cmpe cmpf (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd (pairCompare cmpe cmpf)))) (a1, (b1, (c1, (d1, (e1, f1))))) (a2, (b2, (c2, (d2, (e2, f2)))))))`;
+
+
+val _ = Define `
+ ((sextupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)=  (pairLess 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d
+           (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_e
+              dict_Basic_classes_Ord_f)))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6)))))))`;
+
+val _ = Define `
+ ((sextupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)=  (pairLessEq 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c
+        (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d
+           (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_e
+              dict_Basic_classes_Ord_f)))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6)))))))`;
+
+
+val _ = Define `
+ ((sextupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'f#'e#'d#'c#'b#'a -> 'f#'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f x123456 y123456=  (sextupleLess 
+  dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123456 x123456))`;
+
+val _ = Define `
+ ((sextupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'f#'e#'d#'c#'b#'a -> 'f#'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f x123456 y123456=  (sextupleLessEq 
+  dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123456 x123456))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_tup6_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class ->('a#'b#'c#'d#'e#'f)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f= (<|
+
+  compare_method := (sextupleCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method  dict_Basic_classes_Ord_c.compare_method  dict_Basic_classes_Ord_d.compare_method  dict_Basic_classes_Ord_e.compare_method  dict_Basic_classes_Ord_f.compare_method);
+
+  isLess_method := 
+  (sextupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f);
+
+  isLessEqual_method := 
+  (sextupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d
+     dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f);
+
+  isGreater_method := 
+  (sextupleGreater dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e
+     dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c
+     dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isGreaterEqual_method := 
+  (sextupleGreaterEq dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e
+     dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c
+     dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a)|>))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_boolScript.sml b/prover_snapshots/hol4/lib/lem/lem_boolScript.sml
new file mode 100644
index 0000000..5e6aa09
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_boolScript.sml
@@ -0,0 +1,75 @@
+(*Generated by Lem from bool.lem.*)
+open HolKernel Parse boolLib bossLib;
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_bool"
+
+ 
+
+(* The type bool is hard-coded, so are true and false *)
+
+(* ----------------------- *)
+(* not                     *)
+(* ----------------------- *)
+
+(*val not : bool -> bool*)
+(*let not b=  match b with
+  | true -> false
+  | false -> true
+end*)
+
+(* ----------------------- *)
+(* and                     *)
+(* ----------------------- *)
+
+(*val && [and] : bool -> bool -> bool*)
+(*let && b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* or                      *)
+(* ----------------------- *)
+
+(*val || [or] : bool -> bool -> bool*)
+(*let || b1 b2=  match (b1, b2) with
+  | (false, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* implication             *)
+(* ----------------------- *)
+
+(*val --> [imp] : bool -> bool -> bool*)
+(*let --> b1 b2=  match (b1, b2) with
+  | (true, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* equivalence             *)
+(* ----------------------- *)
+
+(*val <-> [equiv] : bool -> bool -> bool*)
+(*let <-> b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | (false, false) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* xor                     *)
+(* ----------------------- *)
+
+(*val xor : bool -> bool -> bool*)
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml b/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml
new file mode 100644
index 0000000..cad5388
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml
@@ -0,0 +1,83 @@
+(*Generated by Lem from either.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_listTheory lem_tupleTheory sumTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_either"
+
+ 
+
+(*open import Bool Basic_classes List Tuple*)
+(*open import {hol} `sumTheory`*)
+(*open import {ocaml} `Either`*)
+
+(*type either 'a 'b
+  = Left  of 'a
+  | Right of 'b*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Equality.                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val eitherEqual : forall 'a 'b. Eq 'a, Eq 'b => (either 'a 'b) -> (either 'a 'b) -> bool*)
+(*val eitherEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> (either 'a 'b) -> (either 'a 'b) -> bool*)
+
+val _ = Define `
+ ((eitherEqualBy:('a -> 'a -> bool) ->('b -> 'b -> bool) ->('a,'b)sum ->('a,'b)sum -> bool) eql eqr (left: ('a, 'b) sum) (right: ('a, 'b) sum)=
+   ((case (left, right) of
+      (INL l, INL l') => eql l l'
+    | (INR r, INR r') => eqr r r'
+    | _ => F
+  )))`;
+
+(*let eitherEqual=  eitherEqualBy (=) (=)*)
+
+val _ = Define `
+ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL x') (INL y')=  (cmpa x' y'))
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR x') (INR y')=  (cmpb x' y'))
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL _) (INR _)=  LESS)
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR _) (INL _)=  GREATER)`;
+
+                           
+
+(* -------------------------------------------------------------------------- *)
+(* Utility functions.                                                         *)
+(* -------------------------------------------------------------------------- *)
+
+(*val isLeft : forall 'a 'b. either 'a 'b -> bool*)
+
+(*val isRight : forall 'a 'b. either 'a 'b -> bool*)
+
+
+(*val either : forall 'a 'b 'c. ('a -> 'c) -> ('b -> 'c) -> either 'a 'b -> 'c*)
+(*let either fa fb x=  match x with
+  | Left a -> fa a
+  | Right b -> fb b
+end*)
+
+
+(*val partitionEither : forall 'a 'b. list (either 'a 'b) -> (list 'a * list 'b)*)
+ val _ = Define `
+ ((SUM_PARTITION:(('a,'b)sum)list -> 'a list#'b list) ([])=  ([], []))
+/\ ((SUM_PARTITION:(('a,'b)sum)list -> 'a list#'b list) (x :: xs)=  ((
+      let (ll, rl) = (SUM_PARTITION xs) in
+      (case x of 
+          INL l => ((l::ll), rl)
+        | INR r => (ll, (r::rl))
+      )
+    )))`;
+
+
+
+(*val lefts : forall 'a 'b. list (either 'a 'b) -> list 'a*)
+
+
+(*val rights : forall 'a 'b. list (either 'a 'b) -> list 'b*)
+
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_functionScript.sml b/prover_snapshots/hol4/lib/lem/lem_functionScript.sml
new file mode 100644
index 0000000..2f6f52b
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_functionScript.sml
@@ -0,0 +1,72 @@
+(*Generated by Lem from function.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_function"
+
+(******************************************************************************)
+(* A library for common operations on functions                               *)
+(******************************************************************************)
+
+(*open import Bool Basic_classes*)
+
+(*open import {coq} `Program.Basics`*)
+
+(* ----------------------- *)
+(* identity function       *)
+(* ----------------------- *)
+
+(*val id : forall 'a. 'a -> 'a*)
+(*let id x=  x*)
+
+
+(* ----------------------- *)
+(* constant function       *)
+(* ----------------------- *)
+
+(*val const : forall 'a 'b. 'a -> 'b -> 'a*)
+
+
+(* ----------------------- *)
+(* function composition    *)
+(* ----------------------- *)
+
+(*val comb : forall 'a 'b 'c. ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)*)
+(*let comb f g=  (fun x -> f (g x))*)
+
+
+(* ----------------------- *)
+(* function application    *)
+(* ----------------------- *)
+
+(*val $ [apply] : forall 'a 'b. ('a -> 'b) -> ('a -> 'b)*)
+(*let $ f=  (fun x -> f x)*)
+
+(*val $> [rev_apply] : forall 'a 'b. 'a -> ('a -> 'b) -> 'b*)
+(*let $> x f=  f x*)
+
+(* ----------------------- *)
+(* flipping argument order *)
+(* ----------------------- *)
+
+(*val flip : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)*)
+(*let flip f=  (fun x y -> f y x)*)
+
+
+(* currying / uncurrying *)
+
+(*val curry : forall 'a 'b 'c. (('a * 'b) -> 'c) -> 'a -> 'b -> 'c*)
+val _ = Define `
+ ((curry:('a#'b -> 'c) -> 'a -> 'b -> 'c) f=  (\ a b .  f (a, b)))`;
+
+
+(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)
+val _ = Define `
+ ((uncurry:('a -> 'b -> 'c) -> 'a#'b -> 'c) f (a,b)=  (f a b))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_function_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_function_extraScript.sml
new file mode 100644
index 0000000..c77c977
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_function_extraScript.sml
@@ -0,0 +1,25 @@
+(*Generated by Lem from function_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_maybeTheory lem_boolTheory lem_basic_classesTheory lem_numTheory lem_functionTheory lemTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_function_extra"
+
+
+
+(*open import Maybe Bool Basic_classes Num Function*)
+
+(*open import {hol} `lemTheory`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+
+(* ----------------------- *)
+(* getting a unique value  *)
+(* ----------------------- *)
+
+(*val THE : forall 'a. ('a -> bool) -> maybe 'a*)
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_listScript.sml b/prover_snapshots/hol4/lib/lem/lem_listScript.sml
new file mode 100644
index 0000000..1b8f25f
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_listScript.sml
@@ -0,0 +1,776 @@
+(*Generated by Lem from list.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_maybeTheory lem_basic_classesTheory lem_functionTheory lem_tupleTheory lem_numTheory lemTheory listTheory rich_listTheory sortingTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_list"
+
+ 
+
+(*open import Bool Maybe Basic_classes Function Tuple Num*)
+
+(*open import {coq} `Coq.Lists.List`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+(*open import {hol} `lemTheory` `listTheory` `rich_listTheory` `sortingTheory`*)
+
+(* ========================================================================== *)
+(* Basic list functions                                                       *)
+(* ========================================================================== *)
+
+(* The type of lists as well as list literals like [], [1;2], ... are hardcoded. 
+   Thus, we can directly dive into derived definitions. *)
+
+
+(* ----------------------- *)
+(* cons                    *)
+(* ----------------------- *)
+
+(*val :: : forall 'a. 'a -> list 'a -> list 'a*)
+
+
+(* ----------------------- *)
+(* Emptyness check         *)
+(* ----------------------- *)
+
+(*val null : forall 'a. list 'a -> bool*)
+(*let null l=  match l with [] -> true | _ -> false end*)
+
+(* ----------------------- *)
+(* Length                  *)
+(* ----------------------- *)
+
+(*val length : forall 'a. list 'a -> nat*)
+(*let rec length l=
+   match l with
+    | [] -> 0
+    | x :: xs -> (Instance_Num_NumAdd_nat.+) (length xs) 1
+  end*)
+
+(* ----------------------- *)
+(* Equality                *)
+(* ----------------------- *)
+
+(*val listEqual : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*val listEqualBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+
+ val _ = Define `
+ ((listEqualBy:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq ([]) ([])=  T)
+/\ ((listEqualBy:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq ([]) (_::_)=  F)
+/\ ((listEqualBy:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq (_::_) ([])=  F)
+/\ ((listEqualBy:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq (x::xs) (y :: ys)=  (eq x y /\ listEqualBy eq xs ys))`;
+
+
+
+(* ----------------------- *)
+(* compare                 *)
+(* ----------------------- *)
+
+(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> ordering*)
+(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> ordering*)
+
+ val _ = Define `
+ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp ([]) ([])=  EQUAL)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp ([]) (_::_)=  LESS)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp (_::_) ([])=  GREATER)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp (x::xs) (y::ys)=  ((
+      (case cmp x y of 
+          LESS => LESS
+        | GREATER => GREATER
+        | EQUAL => lexicographic_compare cmp xs ys
+      )
+    )))`;
+
+
+(*val lexicographicLess : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+ val _ = Define `
+ ((lexicographic_less:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq ([]) ([])=  F)
+/\ ((lexicographic_less:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq ([]) (_::_)=  T)
+/\ ((lexicographic_less:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq (_::_) ([])=  F)
+/\ ((lexicographic_less:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq (x::xs) (y::ys)=  ((less x y) \/ ((less_eq x y) /\ (lexicographic_less less less_eq xs ys))))`;
+
+
+(*val lexicographicLessEq : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessEqBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+ val _ = Define `
+ ((lexicographic_less_eq:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq ([]) ([])=  T)
+/\ ((lexicographic_less_eq:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq ([]) (_::_)=  T)
+/\ ((lexicographic_less_eq:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq (_::_) ([])=  F)
+/\ ((lexicographic_less_eq:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a list -> 'a list -> bool) less less_eq (x::xs) (y::ys)=  (less x y \/ (less_eq x y /\ lexicographic_less_eq less less_eq xs ys)))`;
+
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_list_dict:'a Ord_class ->('a list)Ord_class)dict_Basic_classes_Ord_a= (<|
+
+  compare_method := (lexicographic_compare  
+  dict_Basic_classes_Ord_a.compare_method);
+
+  isLess_method := (lexicographic_less  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method);
+
+  isLessEqual_method := (lexicographic_less_eq  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method);
+
+  isGreater_method := (\ x y. (lexicographic_less  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method y x));
+
+  isGreaterEqual_method := (\ x y. (lexicographic_less_eq  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method y x))|>))`;
+
+
+
+(* ----------------------- *)
+(* Append                  *)
+(* ----------------------- *)
+
+(*val ++ : forall 'a. list 'a -> list 'a -> list 'a*) (* originally append *)
+(*let rec ++ xs ys=  match xs with
+                     | [] -> ys
+                     | x :: xs' -> x :: (xs' ++ ys)
+                   end*)
+
+(* ----------------------- *)
+(* snoc                    *)
+(* ----------------------- *)
+
+(*val snoc : forall 'a. 'a -> list 'a -> list 'a*)
+(*let snoc e l=  l ++ [e]*)
+
+
+(* ----------------------- *)
+(* Reverse                 *)
+(* ----------------------- *)
+
+(* First lets define the function [reverse_append], which is
+   closely related to reverse. [reverse_append l1 l2] appends the list [l2] to the reverse of [l1].
+   This can be implemented more efficienctly than appending and is
+   used to implement reverse. *)
+
+(*val reverseAppend : forall 'a. list 'a -> list 'a -> list 'a*) (* originally named rev_append *)
+(*let rec reverseAppend l1 l2=  match l1 with 
+                                | [] -> l2
+                                | x :: xs -> reverseAppend xs (x :: l2)
+                               end*)
+
+(* Reversing a list *)
+(*val reverse : forall 'a. list 'a -> list 'a*) (* originally named rev *)
+(*let reverse l=  reverseAppend l []*)
+
+(* ----------------------- *)
+(* Map                     *)
+(* ----------------------- *)
+
+(*val map_tr : forall 'a 'b. list 'b -> ('a -> 'b) -> list 'a -> list 'b*)
+ val map_tr_defn = Defn.Hol_multi_defns `
+ ((map_tr:'b list ->('a -> 'b) -> 'a list -> 'b list) rev_acc f ([])=  (REVERSE rev_acc))
+/\ ((map_tr:'b list ->('a -> 'b) -> 'a list -> 'b list) rev_acc f (x :: xs)=  (map_tr ((f x) :: rev_acc) f xs))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) map_tr_defn;
+
+(* taken from: https://blogs.janestreet.com/optimizing-list-map/ *)
+(*val count_map : forall 'a 'b. ('a -> 'b) -> list 'a -> nat -> list 'b*)
+ val count_map_defn = Defn.Hol_multi_defns `
+ ((count_map:('a -> 'b) -> 'a list -> num -> 'b list) f ([]) ctr=  ([]))
+/\ ((count_map:('a -> 'b) -> 'a list -> num -> 'b list) f (hd :: tl) ctr=  (f hd :: 
+    (if ctr <( 5000 : num) then count_map f tl (ctr +( 1 : num)) 
+    else map_tr [] f tl)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) count_map_defn;
+ 
+(*val map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+(*let map f l=  count_map f l 0*)
+
+(* ----------------------- *)
+(* Reverse Map             *)
+(* ----------------------- *)
+
+(*val reverseMap : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+
+
+(* ========================================================================== *)
+(* Folding                                                                    *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* fold left               *)
+(* ----------------------- *)
+
+(*val foldl : forall 'a 'b. ('a -> 'b -> 'a) -> 'a -> list 'b -> 'a*) (* originally foldl *)
+
+(*let rec foldl f b l=  match l with
+  | []      -> b
+  | x :: xs -> foldl f (f b x) xs
+end*)
+
+
+(* ----------------------- *)
+(* fold right              *)
+(* ----------------------- *)
+
+(*val foldr : forall 'a 'b. ('a -> 'b -> 'b) -> 'b -> list 'a -> 'b*) (* originally foldr with different argument order *)
+(*let rec foldr f b l=  match l with
+  | []      -> b
+  | x :: xs -> f x (foldr f b xs)
+end*)
+
+
+(* ----------------------- *)
+(* concatenating lists     *)
+(* ----------------------- *)
+
+(*val concat : forall 'a. list (list 'a) -> list 'a*) (* before also called "flatten" *)
+(*let concat=  foldr (++) []*)
+
+
+(* -------------------------- *)
+(* concatenating with mapping *)
+(* -------------------------- *)
+
+(*val concatMap : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*)
+
+
+(* ------------------------- *)
+(* universal qualification   *)
+(* ------------------------- *)
+
+(*val all : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally for_all *)
+(*let all P l=  foldl (fun r e -> P e && r) true l*)
+
+
+
+(* ------------------------- *)
+(* existential qualification *)
+(* ------------------------- *)
+
+(*val any : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally exist *)
+(*let any P l=  foldl (fun r e -> P e || r) false l*)
+
+
+(* ------------------------- *)
+(* dest_init                 *)
+(* ------------------------- *)
+
+(* get the initial part and the last element of the list in a safe way *)
+
+(*val dest_init : forall 'a. list 'a -> maybe (list 'a * 'a)*) 
+
+ val _ = Define `
+ ((dest_init_aux:'a list -> 'a -> 'a list -> 'a list#'a) rev_init last_elem_seen ([])=  (REVERSE rev_init, last_elem_seen))
+/\ ((dest_init_aux:'a list -> 'a -> 'a list -> 'a list#'a) rev_init last_elem_seen (x::xs)=  (dest_init_aux (last_elem_seen::rev_init) x xs))`;
+
+
+val _ = Define `
+ ((dest_init:'a list ->('a list#'a)option) ([])=  NONE)
+/\ ((dest_init:'a list ->('a list#'a)option) (x::xs)=  (SOME (dest_init_aux [] x xs)))`;
+
+
+
+(* ========================================================================== *)
+(* Indexing lists                                                             *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* index / nth with maybe   *)
+(* ------------------------- *)
+
+(*val index : forall 'a. list 'a -> nat -> maybe 'a*)
+
+ val _ = Define `
+ ((list_index:'a list -> num -> 'a option) ([]) n=  NONE)
+/\ ((list_index:'a list -> num -> 'a option) (x :: xs) n=  (if n =( 0 : num) then SOME x else list_index xs (n -( 1 : num))))`;
+
+
+(* ------------------------- *)
+(* findIndices               *)
+(* ------------------------- *)
+
+(* [findIndices P l] returns the indices of all elements of list [l] that satisfy predicate [P]. 
+   Counting starts with 0, the result list is sorted ascendingly *)
+(*val findIndices : forall 'a. ('a -> bool) -> list 'a -> list nat*)
+
+ val _ = Define `
+ ((find_indices_aux:num ->('a -> bool) -> 'a list ->(num)list) (i:num) P ([])=  ([]))
+/\ ((find_indices_aux:num ->('a -> bool) -> 'a list ->(num)list) (i:num) P (x :: xs)=  (if P x then i :: find_indices_aux (i +( 1 : num)) P xs else find_indices_aux (i +( 1 : num)) P xs))`;
+
+val _ = Define `
+ ((find_indices:('a -> bool) -> 'a list ->(num)list) P l=  (find_indices_aux(( 0 : num)) P l))`;
+
+
+
+
+(* ------------------------- *)
+(* findIndex                 *)
+(* ------------------------- *)
+
+(* findIndex returns the first index of a list that satisfies a given predicate. *)
+(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> maybe nat*)
+val _ = Define `
+ ((find_index:('a -> bool) -> 'a list ->(num)option) P l=  ((case find_indices P l of
+    [] => NONE
+  | x :: _ => SOME x
+)))`;
+
+
+(* ------------------------- *)
+(* elemIndices               *)
+(* ------------------------- *)
+
+(*val elemIndices : forall 'a. Eq 'a => 'a -> list 'a -> list nat*)
+
+(* ------------------------- *)
+(* elemIndex                 *)
+(* ------------------------- *)
+
+(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> maybe nat*)
+
+
+(* ========================================================================== *)
+(* Creating lists                                                             *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* genlist                   *)
+(* ------------------------- *)
+
+(* [genlist f n] generates the list [f 0; f 1; ... (f (n-1))] *)
+(*val genlist : forall 'a. (nat -> 'a) -> nat -> list 'a*)
+
+
+(*let rec genlist f n=
+   match n with
+    | 0 -> []
+    | n' + 1 -> snoc (f n') (genlist f n')
+  end*)
+
+
+(* ------------------------- *)
+(* replicate                 *)
+(* ------------------------- *)
+
+(*val replicate : forall 'a. nat -> 'a -> list 'a*)
+(*let rec replicate n x=
+   match n with
+    | 0 -> []
+    | n' + 1 -> x :: replicate n' x
+  end*)
+
+
+(* ========================================================================== *)
+(* Sublists                                                                   *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* splitAt                   *)
+(* ------------------------- *)
+
+(* [splitAt n xs] returns a tuple (xs1, xs2), with "append xs1 xs2 = xs" and 
+   "length xs1 = n". If there are not enough elements 
+   in [xs], the original list and the empty one are returned. *)
+(*val splitAtAcc : forall 'a. list 'a -> nat -> list 'a -> (list 'a * list 'a)*)
+ val splitAtAcc_defn = Hol_defn "splitAtAcc" `
+ ((splitAtAcc:'a list -> num -> 'a list -> 'a list#'a list) revAcc n l= 
+   ((case l of
+      []    => (REVERSE revAcc, [])
+    | x::xs => if n <=( 0 : num) then (REVERSE revAcc, l) else splitAtAcc (x::revAcc) (n -( 1 : num)) xs
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn splitAtAcc_defn;
+
+(*val splitAt : forall 'a. nat -> list 'a -> (list 'a * list 'a)*)
+(*let rec splitAt n l= 
+    splitAtAcc [] n l*)
+
+
+(* ------------------------- *)
+(* take                      *)
+(* ------------------------- *)
+
+(* take n xs returns the prefix of xs of length n, or xs itself if n > length xs *)
+(*val take : forall 'a. nat -> list 'a -> list 'a*)
+(*let take n l=  fst (splitAt n l)*)
+
+(* ------------------------- *)
+(* drop                      *)
+(* ------------------------- *)
+
+(* [drop n xs] drops the first [n] elements of [xs]. It returns the empty list, if [n] > [length xs]. *)
+(*val drop : forall 'a. nat -> list 'a -> list 'a*)
+(*let drop n l=  snd (splitAt n l)*)
+
+(* ------------------------------------ *)
+(* splitWhile, takeWhile, and dropWhile *)
+(* ------------------------------------ *)
+
+(*val splitWhile_tr : forall 'a. ('a -> bool) -> list 'a -> list 'a -> (list 'a * list 'a)*)
+ val _ = Define `
+ ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p ([]) acc=
+     (REVERSE acc, []))
+/\ ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p (x::xs) acc=
+     (if p x then
+      splitWhile_tr p xs (x::acc)
+    else
+      (REVERSE acc, (x::xs))))`;
+
+
+(*val splitWhile : forall 'a. ('a -> bool) -> list 'a -> (list 'a * list 'a)*)
+val _ = Define `
+ ((splitWhile:('a -> bool) -> 'a list -> 'a list#'a list) p xs=  (splitWhile_tr p xs []))`;
+
+
+(* [takeWhile p xs] takes the first elements of [xs] that satisfy [p]. *)
+(*val takeWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+val _ = Define `
+ ((takeWhile:('a -> bool) -> 'a list -> 'a list) p l=  (FST (splitWhile p l)))`;
+
+
+(* [dropWhile p xs] drops the first elements of [xs] that satisfy [p]. *)
+(*val dropWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+val _ = Define `
+ ((dropWhile:('a -> bool) -> 'a list -> 'a list) p l=  (SND (splitWhile p l)))`;
+
+
+(* ------------------------- *)
+(* isPrefixOf                *)
+(* ------------------------- *)
+
+(*val isPrefixOf : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*let rec isPrefixOf l1 l2=  match (l1, l2) with
+  | ([], _) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> (x = y) && isPrefixOf xs ys
+end*)
+
+(* ------------------------- *)
+(* update                    *)
+(* ------------------------- *)
+(*val update : forall 'a. list 'a -> nat -> 'a -> list 'a*)
+(*let rec update l n e= 
+   match l with
+    | []      -> []
+    | x :: xs -> if (Instance_Basic_classes_Eq_nat.=) n 0 then e :: xs else x :: (update xs ((Instance_Num_NumMinus_nat.-) n 1) e)
+end*)
+
+
+
+(* ========================================================================== *)
+(* Searching lists                                                            *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* Membership test           *)
+(* ------------------------- *)
+
+(* The membership test, one of the basic list functions, is actually tricky for
+   Lem, because it is tricky, which equality to use. From Lem`s point of 
+   perspective, we want to use the equality provided by the equality type - class.
+   This allows for example to check whether a set is in a list of sets.
+
+   However, in order to use the equality type class, elem essentially becomes
+   existential quantification over lists. For types, which implement semantic
+   equality (=) with syntactic equality, this is overly complicated. In
+   our theorem prover backend, we would end up with overly complicated, harder
+   to read definitions and some of the automation would be harder to apply.
+   Moreover, nearly all the old Lem generated code would change and require 
+   (hopefully minor) adaptions of proofs.
+
+   For now, we ignore this problem and just demand, that all instances of
+   the equality type class do the right thing for the theorem prover backends.   
+*)
+
+(*val elem : forall 'a. Eq 'a => 'a -> list 'a -> bool*)
+(*val elemBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> bool*)
+
+val _ = Define `
+ ((elemBy:('a -> 'a -> bool) -> 'a -> 'a list -> bool) eq e l=  (EXISTS (eq e) l))`;
+
+(*let elem=  elemBy (=)*)
+
+(* ------------------------- *)
+(* Find                      *)
+(* ------------------------- *)
+(*val find : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) (* previously not of maybe type *)
+ val _ = Define `
+ ((list_find_opt:('a -> bool) -> 'a list -> 'a option) P ([])=  NONE)
+/\ ((list_find_opt:('a -> bool) -> 'a list -> 'a option) P (x :: xs)=  (if P x then SOME x else list_find_opt P xs))`;
+
+
+
+(* ----------------------------- *)
+(* Lookup in an associative list *)
+(* ----------------------------- *)
+(*val lookup   : forall 'a 'b. Eq 'a              => 'a -> list ('a * 'b) -> maybe 'b*)
+(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> maybe 'b*)
+
+(* DPM: eta-expansion for Coq backend type-inference. *)
+val _ = Define `
+ ((lookupBy:('a -> 'a -> bool) -> 'a ->('a#'b)list -> 'b option) eq k m=  (OPTION_MAP (\ x .  SND x) (list_find_opt (\p .  
+  (case (p ) of ( (k', _) ) => eq k k' )) m)))`;
+
+
+(* ------------------------- *)
+(* filter                    *)
+(* ------------------------- *)
+(*val filter : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+(*let rec filter P l=  match l with
+                       | [] -> []
+                       | x :: xs -> if (P x) then x :: (filter P xs) else filter P xs
+                     end*)
+
+
+(* ------------------------- *)
+(* partition                 *)
+(* ------------------------- *)
+(*val partition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+(*let partition P l=  (filter P l, filter (fun x -> not (P x)) l)*)
+
+(*val reversePartition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+(*let reversePartition P l=  partition P (reverse l)*)
+
+
+(* ------------------------- *)
+(* delete first element      *)
+(* with certain property     *)
+(* ------------------------- *)
+
+(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> maybe (list 'a)*) 
+ val _ = Define `
+ ((list_delete_first:('a -> bool) -> 'a list ->('a list)option) P ([])=  NONE)
+/\ ((list_delete_first:('a -> bool) -> 'a list ->('a list)option) P (x :: xs)=  (if (P x) then SOME xs else OPTION_MAP (\ xs' .  x :: xs') (list_delete_first P xs)))`;
+
+
+
+(*val delete : forall 'a. Eq 'a => 'a -> list 'a -> list 'a*)
+(*val deleteBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
+
+val _ = Define `
+ ((list_delete:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list) eq x l=  (option_CASE (list_delete_first (eq x) l) l I))`;
+
+
+
+(* ========================================================================== *)
+(* Zipping and unzipping lists                                                *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* zip                       *)
+(* ------------------------- *)
+
+(* zip takes two lists and returns a list of corresponding pairs. If one input list is short, excess elements of the longer list are discarded. *)
+(*val zip : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) (* before combine *)
+ val _ = Define `
+ ((list_combine:'a list -> 'b list ->('a#'b)list) l1 l2=  ((case (l1, l2) of
+    (x :: xs, y :: ys) => (x, y) :: list_combine xs ys
+  | _ => []
+)))`;
+
+
+(* ------------------------- *)
+(* unzip                     *)
+(* ------------------------- *)
+
+(*val unzip: forall 'a 'b. list ('a * 'b) -> (list 'a * list 'b)*)
+(*let rec unzip l=  match l with
+  | [] -> ([], [])
+  | (x, y) :: xys -> let (xs, ys) = unzip xys in (x :: xs, y :: ys)
+end*)
+
+(* ------------------------- *)
+(* distinct elements         *)
+(* ------------------------- *)
+
+(*val allDistinct : forall 'a. Eq 'a => list 'a -> bool*)
+(*let rec allDistinct l= 
+   match l with
+    | [] -> true
+    | (x::l') -> not (elem x l') && allDistinct l'
+  end*)
+
+(* some more useful functions *)
+(*val mapMaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*)
+ val mapMaybe_defn = Defn.Hol_multi_defns `
+ ((mapMaybe:('a -> 'b option) -> 'a list -> 'b list) f ([])=  ([]))
+/\ ((mapMaybe:('a -> 'b option) -> 'a list -> 'b list) f (x::xs)=
+       ((case f x of
+        NONE => mapMaybe f xs
+      | SOME y => y :: (mapMaybe f xs)
+      )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) mapMaybe_defn;
+
+(*val mapi : forall 'a 'b. (nat -> 'a -> 'b) -> list 'a -> list 'b*)
+ val mapiAux_defn = Defn.Hol_multi_defns `
+ ((mapiAux:(num -> 'b -> 'a) -> num -> 'b list -> 'a list) f (n : num) ([])=  ([]))
+/\ ((mapiAux:(num -> 'b -> 'a) -> num -> 'b list -> 'a list) f (n : num) (x :: xs)=  ((f n x) :: mapiAux f (n +( 1 : num)) xs))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) mapiAux_defn;
+val _ = Define `
+ ((mapi:(num -> 'a -> 'b) -> 'a list -> 'b list) f l=  (mapiAux f(( 0 : num)) l))`;
+
+
+(*val deletes: forall 'a. Eq 'a => list 'a -> list 'a -> list 'a*)
+val _ = Define `
+ ((deletes:'a list -> 'a list -> 'a list) xs ys=
+   (FOLDL (combin$C (list_delete (=))) xs ys))`;
+
+
+(* ========================================================================== *)
+(* Comments (not clean yet, please ignore the rest of the file)               *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* skipped from Haskell Lib*)
+(* ----------------------- 
+
+intersperse :: a -> [a] -> [a]
+intercalate :: [a] -> [[a]] -> [a]
+transpose :: [[a]] -> [[a]]
+subsequences :: [a] -> [[a]]
+permutations :: [a] -> [[a]]
+foldl` :: (a -> b -> a) -> a -> [b] -> aSource
+foldl1` :: (a -> a -> a) -> [a] -> aSource
+
+and
+or
+sum
+product
+maximum
+minimum
+scanl
+scanr
+scanl1
+scanr1
+Accumulating maps
+
+mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+
+iterate :: (a -> a) -> a -> [a]
+repeat :: a -> [a]
+cycle :: [a] -> [a]
+unfoldr
+
+
+takeWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhileEnd :: (a -> Bool) -> [a] -> [a]Source
+span :: (a -> Bool) -> [a] -> ([a], [a])Source
+break :: (a -> Bool) -> [a] -> ([a], [a])Source
+break p is equivalent to span (not . p).
+stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]Source
+group :: Eq a => [a] -> [[a]]Source
+inits :: [a] -> [[a]]Source
+tails :: [a] -> [[a]]Source
+
+
+isPrefixOf :: Eq a => [a] -> [a] -> BoolSource
+isSuffixOf :: Eq a => [a] -> [a] -> BoolSource
+isInfixOf :: Eq a => [a] -> [a] -> BoolSource
+
+
+
+notElem :: Eq a => a -> [a] -> BoolSource
+
+zip3 :: [a] -> [b] -> [c] -> [(a, b, c)]Source
+zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]Source
+zip5 :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]Source
+zip6 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [(a, b, c, d, e, f)]Source
+zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]Source
+
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]Source
+zipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]Source
+zipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]Source
+zipWith5 :: (a -> b -> c -> d -> e -> f) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f]Source
+zipWith6 :: (a -> b -> c -> d -> e -> f -> g) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]Source
+zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]Source
+
+
+unzip3 :: [(a, b, c)] -> ([a], [b], [c])Source
+unzip4 :: [(a, b, c, d)] -> ([a], [b], [c], [d])Source
+unzip5 :: [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])Source
+unzip6 :: [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])Source
+unzip7 :: [(a, b, c, d, e, f, g)] -> ([a], [b], [c], [d], [e], [f], [g])Source
+
+
+lines :: String -> [String]Source
+words :: String -> [String]Source
+unlines :: [String] -> StringSource
+unwords :: [String] -> StringSource
+nub :: Eq a => [a] -> [a]Source
+delete :: Eq a => a -> [a] -> [a]Source
+
+(\\) :: Eq a => [a] -> [a] -> [a]Source
+union :: Eq a => [a] -> [a] -> [a]Source
+intersect :: Eq a => [a] -> [a] -> [a]Source
+sort :: Ord a => [a] -> [a]Source
+insert :: Ord a => a -> [a] -> [a]Source
+
+
+nubBy :: (a -> a -> Bool) -> [a] -> [a]Source
+deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]Source
+deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+groupBy :: (a -> a -> Bool) -> [a] -> [[a]]Source
+sortBy :: (a -> a -> Ordering) -> [a] -> [a]Source
+insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]Source
+maximumBy :: (a -> a -> Ordering) -> [a] -> aSource
+minimumBy :: (a -> a -> Ordering) -> [a] -> aSource
+genericLength :: Num i => [b] -> iSource
+genericTake :: Integral i => i -> [a] -> [a]Source
+genericDrop :: Integral i => i -> [a] -> [a]Source
+genericSplitAt :: Integral i => i -> [b] -> ([b], [b])Source
+genericIndex :: Integral a => [b] -> a -> bSource
+genericReplicate :: Integral i => i -> a -> [a]Source
+
+
+*)
+
+
+(* ----------------------- *)
+(* skipped from Lem Lib    *)
+(* ----------------------- 
+
+
+val for_all2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val exists2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c 
+val rev_map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c
+val fold_left2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'a) -> 'a -> list 'b -> list 'c -> 'a
+val fold_right2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'c) -> list 'a -> list 'b -> 'c -> 'c
+
+
+(* now maybe result and called lookup *)
+val assoc : forall 'a 'b. 'a -> list ('a * 'b) -> 'b
+let inline {ocaml} assoc = Ocaml.List.assoc
+
+
+val mem_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> bool
+val remove_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> list ('a * 'b)
+
+
+
+val stable_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+val fast_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+
+val merge : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a -> list 'a
+val intersect : forall 'a. list 'a -> list 'a -> list 'a
+
+
+*)
+
+(*val     catMaybes : forall 'a. list (maybe 'a) -> list 'a*)
+ val catMaybes_defn = Defn.Hol_multi_defns `
+ ((catMaybes:('a option)list -> 'a list) ([])=
+         ([]))
+/\ ((catMaybes:('a option)list -> 'a list) (NONE :: xs')=
+         (catMaybes xs'))
+/\ ((catMaybes:('a option)list -> 'a list) (SOME x :: xs')=
+         (x :: catMaybes xs'))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) catMaybes_defn;
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_list_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_list_extraScript.sml
new file mode 100644
index 0000000..123d8a7
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_list_extraScript.sml
@@ -0,0 +1,110 @@
+(*Generated by Lem from list_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_maybeTheory lem_basic_classesTheory lem_tupleTheory lem_numTheory lem_listTheory lem_assert_extraTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_list_extra"
+
+
+
+(*open import Bool Maybe Basic_classes Tuple Num List Assert_extra*)
+
+(* ------------------------- *)
+(* head of non-empty list    *)
+(* ------------------------- *)
+(*val head : forall 'a. list 'a -> 'a*)
+(*let head l=  match l with | x::xs -> x | [] -> failwith "List_extra.head of empty list" end*)
+
+
+(* ------------------------- *)
+(* tail of non-empty list    *)
+(* ------------------------- *)
+(*val tail : forall 'a. list 'a -> list 'a*)
+(*let tail l=  match l with | x::xs -> xs | [] -> failwith "List_extra.tail of empty list" end*)
+
+
+(* ------------------------- *)
+(* last                      *)
+(* ------------------------- *)
+(*val last : forall 'a. list 'a -> 'a*)
+(*let rec last l=  match l with | [x] -> x | x1::x2::xs -> last (x2 :: xs) | [] -> failwith "List_extra.last of empty list" end*)
+
+
+(* ------------------------- *)
+(* init                      *)
+(* ------------------------- *)
+
+(* All elements of a non-empty list except the last one. *)
+(*val init : forall 'a. list 'a -> list 'a*)
+(*let rec init l=  match l with | [x] -> [] | x1::x2::xs -> x1::(init (x2::xs)) | [] -> failwith "List_extra.init of empty list" end*)
+
+
+(* ------------------------- *)
+(* foldl1 / foldr1           *)
+(* ------------------------- *)
+
+(* folding functions for non-empty lists,
+    which don`t take the base case *)
+(*val foldl1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*)
+val _ = Define `
+ ((foldl1:('a -> 'a -> 'a) -> 'a list -> 'a) f (x :: xs)=  (FOLDL f x xs))
+/\ ((foldl1:('a -> 'a -> 'a) -> 'a list -> 'a) f ([])=  (failwith "List_extra.foldl1 of empty list"))`;
+
+
+(*val foldr1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*)
+val _ = Define `
+ ((foldr1:('a -> 'a -> 'a) -> 'a list -> 'a) f (x :: xs)=  (FOLDR f x xs))
+/\ ((foldr1:('a -> 'a -> 'a) -> 'a list -> 'a) f ([])=  (failwith "List_extra.foldr1 of empty list"))`;
+
+
+  
+(* ------------------------- *)
+(* nth element               *)
+(* ------------------------- *)
+
+(* get the nth element of a list *)
+(*val nth : forall 'a. list 'a -> nat -> 'a*)
+(*let nth l n=  match index l n with Just e -> e | Nothing -> failwith "List_extra.nth" end*)
+
+
+(* ------------------------- *)
+(* Find_non_pure             *)
+(* ------------------------- *)
+(*val findNonPure : forall 'a. ('a -> bool) -> list 'a -> 'a*) 
+val _ = Define `
+ ((findNonPure:('a -> bool) -> 'a list -> 'a) P l=  ((case (list_find_opt P l) of 
+    SOME e      => e
+  | NONE     => failwith "List_extra.findNonPure"
+)))`;
+
+
+
+(* ------------------------- *)
+(* zip same length           *)
+(* ------------------------- *)
+
+(*val zipSameLength : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) 
+(*let rec zipSameLength l1 l2=  match (l1, l2) with
+  | (x :: xs, y :: ys) -> (x, y) :: zipSameLength xs ys
+  | ([], []) -> []
+  | _ -> failwith "List_extra.zipSameLength of different length lists"
+
+end*)
+
+(*val     unfoldr: forall 'a 'b. ('a -> maybe ('b * 'a)) -> 'a -> list 'b*)
+ val unfoldr_defn = Hol_defn "unfoldr" `
+ ((unfoldr:('a ->('b#'a)option) -> 'a -> 'b list) f x=
+   ((case f x of
+      SOME (y, x') =>
+        y :: unfoldr f x'
+    | NONE =>
+        []
+  )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn unfoldr_defn;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_machine_wordScript.sml b/prover_snapshots/hol4/lib/lem/lem_machine_wordScript.sml
new file mode 100644
index 0000000..40bbef3
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_machine_wordScript.sml
@@ -0,0 +1,433 @@
+(*Generated by Lem from machine_word.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_numTheory lem_basic_classesTheory lem_showTheory lem_functionTheory wordsTheory wordsLib bitstringTheory integer_wordTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_machine_word"
+
+
+
+(*open import Bool Num Basic_classes Show Function*)
+
+(*open import {isabelle} `HOL-Word.Word`*)
+(*open import {hol} `wordsTheory` `wordsLib` `bitstringTheory` `integer_wordTheory`*)
+
+(*type mword 'a*)
+
+(*class (Size 'a)
+  val size : nat
+end*)
+
+(*val native_size : forall 'a. nat*)
+
+(*val ocaml_inject : forall 'a. nat * natural -> mword 'a*)
+
+(* A singleton type family that can be used to carry a size as the type parameter *)
+
+(*type itself 'a*)
+
+(*val the_value : forall 'a. itself 'a*)
+
+(*val size_itself : forall 'a. Size 'a => itself 'a -> nat*)
+val _ = Define `
+ ((size_itself:'a itself -> num) x=  (dimindex (the_value : 'a itself)))`;
+
+
+(*******************************************************************)
+(* Fixed bitwidths extracted from Anthony's models.                *)
+(*                                                                 *)
+(* If you need a size N that is not included here, put the lines   *)
+(*                                                                 *)
+(* type tyN                                                        *)
+(* instance (Size tyN) let size = N end                            *)
+(* declare isabelle target_rep type tyN = `N`                      *)
+(* declare hol target_rep type tyN = `N`                           *)
+(*                                                                 *)
+(* in your project, replacing N in each line.                      *)
+(*******************************************************************)
+
+(*type ty1*)
+(*type ty2*)
+(*type ty3*)
+(*type ty4*)
+(*type ty5*)
+(*type ty6*)
+(*type ty7*)
+(*type ty8*)
+(*type ty9*)
+(*type ty10*)
+(*type ty11*)
+(*type ty12*)
+(*type ty13*)
+(*type ty14*)
+(*type ty15*)
+(*type ty16*)
+(*type ty17*)
+(*type ty18*)
+(*type ty19*)
+(*type ty20*)
+(*type ty21*)
+(*type ty22*)
+(*type ty23*)
+(*type ty24*)
+(*type ty25*)
+(*type ty26*)
+(*type ty27*)
+(*type ty28*)
+(*type ty29*)
+(*type ty30*)
+(*type ty31*)
+(*type ty32*)
+(*type ty33*)
+(*type ty34*)
+(*type ty35*)
+(*type ty36*)
+(*type ty37*)
+(*type ty38*)
+(*type ty39*)
+(*type ty40*)
+(*type ty41*)
+(*type ty42*)
+(*type ty43*)
+(*type ty44*)
+(*type ty45*)
+(*type ty46*)
+(*type ty47*)
+(*type ty48*)
+(*type ty49*)
+(*type ty50*)
+(*type ty51*)
+(*type ty52*)
+(*type ty53*)
+(*type ty54*)
+(*type ty55*)
+(*type ty56*)
+(*type ty57*)
+(*type ty58*)
+(*type ty59*)
+(*type ty60*)
+(*type ty61*)
+(*type ty62*)
+(*type ty63*)
+(*type ty64*)
+(*type ty65*)
+(*type ty66*)
+(*type ty67*)
+(*type ty68*)
+(*type ty69*)
+(*type ty70*)
+(*type ty71*)
+(*type ty72*)
+(*type ty73*)
+(*type ty74*)
+(*type ty75*)
+(*type ty76*)
+(*type ty77*)
+(*type ty78*)
+(*type ty79*)
+(*type ty80*)
+(*type ty81*)
+(*type ty82*)
+(*type ty83*)
+(*type ty84*)
+(*type ty85*)
+(*type ty86*)
+(*type ty87*)
+(*type ty88*)
+(*type ty89*)
+(*type ty90*)
+(*type ty91*)
+(*type ty92*)
+(*type ty93*)
+(*type ty94*)
+(*type ty95*)
+(*type ty96*)
+(*type ty97*)
+(*type ty98*)
+(*type ty99*)
+(*type ty100*)
+(*type ty101*)
+(*type ty102*)
+(*type ty103*)
+(*type ty104*)
+(*type ty105*)
+(*type ty106*)
+(*type ty107*)
+(*type ty108*)
+(*type ty109*)
+(*type ty110*)
+(*type ty111*)
+(*type ty112*)
+(*type ty113*)
+(*type ty114*)
+(*type ty115*)
+(*type ty116*)
+(*type ty117*)
+(*type ty118*)
+(*type ty119*)
+(*type ty120*)
+(*type ty121*)
+(*type ty122*)
+(*type ty123*)
+(*type ty124*)
+(*type ty125*)
+(*type ty126*)
+(*type ty127*)
+(*type ty128*)
+(*type ty129*)
+(*type ty130*)
+(*type ty131*)
+(*type ty132*)
+(*type ty133*)
+(*type ty134*)
+(*type ty135*)
+(*type ty136*)
+(*type ty137*)
+(*type ty138*)
+(*type ty139*)
+(*type ty140*)
+(*type ty141*)
+(*type ty142*)
+(*type ty143*)
+(*type ty144*)
+(*type ty145*)
+(*type ty146*)
+(*type ty147*)
+(*type ty148*)
+(*type ty149*)
+(*type ty150*)
+(*type ty151*)
+(*type ty152*)
+(*type ty153*)
+(*type ty154*)
+(*type ty155*)
+(*type ty156*)
+(*type ty157*)
+(*type ty158*)
+(*type ty159*)
+(*type ty160*)
+(*type ty161*)
+(*type ty162*)
+(*type ty163*)
+(*type ty164*)
+(*type ty165*)
+(*type ty166*)
+(*type ty167*)
+(*type ty168*)
+(*type ty169*)
+(*type ty170*)
+(*type ty171*)
+(*type ty172*)
+(*type ty173*)
+(*type ty174*)
+(*type ty175*)
+(*type ty176*)
+(*type ty177*)
+(*type ty178*)
+(*type ty179*)
+(*type ty180*)
+(*type ty181*)
+(*type ty182*)
+(*type ty183*)
+(*type ty184*)
+(*type ty185*)
+(*type ty186*)
+(*type ty187*)
+(*type ty188*)
+(*type ty189*)
+(*type ty190*)
+(*type ty191*)
+(*type ty192*)
+(*type ty193*)
+(*type ty194*)
+(*type ty195*)
+(*type ty196*)
+(*type ty197*)
+(*type ty198*)
+(*type ty199*)
+(*type ty200*)
+(*type ty201*)
+(*type ty202*)
+(*type ty203*)
+(*type ty204*)
+(*type ty205*)
+(*type ty206*)
+(*type ty207*)
+(*type ty208*)
+(*type ty209*)
+(*type ty210*)
+(*type ty211*)
+(*type ty212*)
+(*type ty213*)
+(*type ty214*)
+(*type ty215*)
+(*type ty216*)
+(*type ty217*)
+(*type ty218*)
+(*type ty219*)
+(*type ty220*)
+(*type ty221*)
+(*type ty222*)
+(*type ty223*)
+(*type ty224*)
+(*type ty225*)
+(*type ty226*)
+(*type ty227*)
+(*type ty228*)
+(*type ty229*)
+(*type ty230*)
+(*type ty231*)
+(*type ty232*)
+(*type ty233*)
+(*type ty234*)
+(*type ty235*)
+(*type ty236*)
+(*type ty237*)
+(*type ty238*)
+(*type ty239*)
+(*type ty240*)
+(*type ty241*)
+(*type ty242*)
+(*type ty243*)
+(*type ty244*)
+(*type ty245*)
+(*type ty246*)
+(*type ty247*)
+(*type ty248*)
+(*type ty249*)
+(*type ty250*)
+(*type ty251*)
+(*type ty252*)
+(*type ty253*)
+(*type ty254*)
+(*type ty255*)
+(*type ty256*)
+(*type ty257*)
+
+(*val word_length : forall 'a. mword 'a -> nat*)
+
+(******************************************************************)
+(* Conversions                                                    *)
+(******************************************************************)
+
+(*val signedIntegerFromWord : forall 'a. mword 'a -> integer*)
+
+(*val unsignedIntegerFromWord : forall 'a. mword 'a -> integer*)
+
+(* Version without typeclass constraint so that we can derive operations
+   in Lem for one of the theorem provers without requiring it. *)
+(*val proverWordFromInteger : forall 'a. integer -> mword 'a*)
+
+(*val wordFromInteger : forall 'a. Size 'a => integer -> mword 'a*)
+(* The OCaml version is defined after the arithmetic operations, below. *)
+
+(*val naturalFromWord : forall 'a. mword 'a -> natural*)
+
+(*val wordFromNatural : forall 'a. Size 'a => natural -> mword 'a*)
+
+(*val wordToHex : forall 'a. mword 'a -> string*)
+
+val _ = Define `
+((instance_Show_Show_Machine_word_mword_dict:('a words$word)Show_class)= (<|
+
+  show_method := words$word_to_hex_string|>))`;
+
+
+(*val wordFromBitlist : forall 'a. Size 'a => list bool -> mword 'a*)
+
+(*val bitlistFromWord : forall 'a. mword 'a -> list bool*)
+
+
+(*val size_test_fn : forall 'a. Size 'a => mword 'a -> nat*)
+val _ = Define `
+ ((size_test_fn:'a words$word -> num) _=  (dimindex (the_value : 'a itself)))`;
+
+
+(******************************************************************)
+(* Comparisons                                                    *)
+(******************************************************************)
+
+(*val mwordEq : forall 'a. mword 'a -> mword 'a -> bool*)
+
+(*val signedLess : forall 'a. mword 'a -> mword 'a -> bool*)
+
+(*val signedLessEq : forall 'a. mword 'a -> mword 'a -> bool*)
+
+(*val unsignedLess : forall 'a. mword 'a -> mword 'a -> bool*)
+
+(*val unsignedLessEq : forall 'a. mword 'a -> mword 'a -> bool*)
+
+(* Comparison tests are below, after the definition of wordFromInteger *)
+
+(******************************************************************)
+(* Appending, splitting and probing words                         *)
+(******************************************************************)
+
+(*val word_concat : forall 'a 'b 'c. mword 'a -> mword 'b -> mword 'c*)
+
+(* Note that we assume the result type has the correct size, especially
+   for Isabelle. *)
+(*val word_extract : forall 'a 'b. nat -> nat -> mword 'a -> mword 'b*)
+
+(*  Needs to be in the prover because we'd end up with unknown sizes in the
+   types in Lem.
+*)
+(*val word_update : forall 'a 'b. mword 'a -> nat -> nat -> mword 'b -> mword 'a*)
+
+(*val setBit : forall 'a. mword 'a -> nat -> bool -> mword 'a*)
+
+(*val getBit : forall 'a. mword 'a -> nat -> bool*)
+
+(*val msb : forall 'a. mword 'a -> bool*)
+
+(*val lsb : forall 'a. mword 'a -> bool*)
+
+(******************************************************************)
+(* Bitwise operations, shifts, etc.                               *)
+(******************************************************************)
+
+(*val shiftLeft  : forall 'a. mword 'a -> nat -> mword 'a*)
+
+(*val shiftRight : forall 'a. mword 'a -> nat -> mword 'a*)
+
+(*val arithShiftRight : forall 'a. mword 'a -> nat -> mword 'a*)
+
+(*val lAnd       : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val lOr        : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val lXor       : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val lNot       : forall 'a. mword 'a -> mword 'a*)
+
+(*val rotateRight : forall 'a. nat -> mword 'a -> mword 'a*)
+
+(*val rotateLeft : forall 'a. nat -> mword 'a -> mword 'a*)
+
+(*val zeroExtend : forall 'a 'b. Size 'b => mword 'a -> mword 'b*)
+
+(*val signExtend : forall 'a 'b. Size 'b => mword 'a -> mword 'b*)
+
+(* Sign extension tests are below, after the definition of wordFromInteger *)
+
+(*****************************************************************)
+(* Arithmetic                                                    *)
+(*****************************************************************)
+
+(*val plus   : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val minus  : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val uminus : forall 'a. mword 'a -> mword 'a*)
+
+(*val times : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val unsignedDivide : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+(*val signedDivide : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+
+(*val modulo : forall 'a. mword 'a -> mword 'a -> mword 'a*)
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_mapScript.sml b/prover_snapshots/hol4/lib/lem/lem_mapScript.sml
new file mode 100644
index 0000000..e05af7f
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_mapScript.sml
@@ -0,0 +1,153 @@
+(*Generated by Lem from map.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_functionTheory lem_maybeTheory lem_listTheory lem_tupleTheory lem_setTheory lem_numTheory finite_mapTheory finite_mapLib;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_map"
+
+
+
+(*open import Bool Basic_classes Function Maybe List Tuple Set Num*)
+(*open import {hol} `finite_mapTheory` `finite_mapLib`*)
+
+(*type map 'k 'v*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* Map equality.                                                              *)
+(* -------------------------------------------------------------------------- *)
+
+(*val mapEqual : forall 'k 'v. Eq 'k, Eq 'v => map 'k 'v -> map 'k 'v -> bool*)
+(*val mapEqualBy : forall 'k 'v. ('k -> 'k -> bool) -> ('v -> 'v -> bool) -> map 'k 'v -> map 'k 'v -> bool*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Map type class                                                             *)
+(* -------------------------------------------------------------------------- *)
+
+(*class ( MapKeyType 'a )
+  val {ocaml;coq} mapKeyCompare : 'a -> 'a -> ordering
+end*)
+
+(* -------------------------------------------------------------------------- *)
+(* Empty maps                                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+(*val empty : forall 'k 'v. MapKeyType 'k => map 'k 'v*)
+(*val emptyBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Insertion                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val insert    : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Singleton                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val singleton : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* Emptyness check                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+(*val null  : forall 'k 'v. MapKeyType 'k, Eq 'k, Eq 'v => map 'k 'v -> bool*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* lookup                                                                     *)
+(* -------------------------------------------------------------------------- *)
+
+(*val lookupBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> maybe 'v*)
+
+(*val lookup          : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> maybe 'v*)
+
+(* -------------------------------------------------------------------------- *)
+(* findWithDefault                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+(*val findWithDefault : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> 'v*)
+
+(* -------------------------------------------------------------------------- *)
+(* from lists                                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+(*val fromList  : forall 'k 'v. MapKeyType 'k => list ('k * 'v) -> map 'k 'v*)
+(*let fromList l=  foldl (fun m (k,v) -> insert k v m) empty l*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* to sets / domain / range                                                   *)
+(* -------------------------------------------------------------------------- *)
+
+(*val toSet : forall 'k 'v. MapKeyType 'k, SetType 'k, SetType 'v => map 'k 'v -> set ('k * 'v)*) 
+(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> ordering) -> map 'k 'v -> set ('k * 'v)*)
+
+
+(*val domainBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v -> set 'k*)
+(*val domain : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> set 'k*)
+
+
+(*val range : forall 'k 'v. MapKeyType 'k, SetType 'v => map 'k 'v -> set 'v*)
+(*val rangeBy : forall 'k 'v. ('v -> 'v -> ordering) -> map 'k 'v -> set 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* member                                                                     *)
+(* -------------------------------------------------------------------------- *)
+
+(*val member          : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)
+
+(*val notMember       : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)
+
+(* -------------------------------------------------------------------------- *)
+(* Quantification                                                             *)
+(* -------------------------------------------------------------------------- *)
+
+(*val any : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 
+(*val all : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 
+
+(*let all P m=  (forall k v. (P k v && ((Instance_Basic_classes_Eq_Maybe_maybe.=) (lookup k m) (Just v))))*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Set-like operations.                                                       *)
+(* -------------------------------------------------------------------------- *)
+(*val deleteBy         : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> map 'k 'v*)
+(*val delete           : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> map 'k 'v*)
+(*val deleteSwap      : forall 'k 'v. MapKeyType 'k => map 'k 'v -> 'k -> map 'k 'v*)
+
+(*val union          : forall 'k 'v. MapKeyType 'k => map 'k 'v -> map 'k 'v -> map 'k 'v*)
+
+(*val unions           : forall 'k 'v. MapKeyType 'k => list (map 'k 'v) -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Maps (in the functor sense).                                               *)
+(* -------------------------------------------------------------------------- *)
+
+(*val map             : forall 'k 'v 'w. MapKeyType 'k => ('v -> 'w) -> map 'k 'v -> map 'k 'w*)
+
+(*val mapi : forall 'k 'v 'w. MapKeyType 'k => ('k -> 'v -> 'w) -> map 'k 'v -> map 'k 'w*)
+
+(* -------------------------------------------------------------------------- *)
+(* Cardinality                                                                *)
+(* -------------------------------------------------------------------------- *)
+(*val size  : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> nat*)
+
+(* instance of SetType *)
+val _ = Define `
+ ((map_setElemCompare:(('d#'c)set ->('b#'a)set -> 'e) ->('d,'c)fmap ->('b,'a)fmap -> 'e) cmp x y=
+   (cmp (FMAP_TO_SET x) (FMAP_TO_SET y)))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_map_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_map_extraScript.sml
new file mode 100644
index 0000000..7e32efb
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_map_extraScript.sml
@@ -0,0 +1,72 @@
+(*Generated by Lem from map_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_functionTheory lem_assert_extraTheory lem_maybeTheory lem_listTheory lem_numTheory lem_setTheory lem_mapTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_map_extra"
+
+
+
+(*open import Bool Basic_classes Function Assert_extra Maybe List Num Set Map*)
+
+(* -------------------------------------------------------------------------- *)
+(* find                                                                       *)
+(* -------------------------------------------------------------------------- *)
+
+(*val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v*)
+(*let find k m=  match (lookup k m) with Just x -> x | Nothing -> failwith "Map_extra.find" end*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* from sets / domain / range                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+
+(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v*)
+(*let fromSet f s=  Set_helpers.fold (fun k m -> Map.insert k (f k) m) s Map.empty*)
+
+(*
+assert fromSet_0: (fromSet succ (Set.empty : set nat) = Map.empty)
+assert fromSet_1: (fromSet succ {(2:nat); 3; 4}) = Map.fromList [(2,3); (3, 4); (4, 5)]
+*)
+
+(* -------------------------------------------------------------------------- *)
+(* fold                                                                       *)
+(* -------------------------------------------------------------------------- *)
+
+(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r*)
+val _ = Define `
+ ((fold:('k -> 'v -> 'r -> 'r) ->('k,'v)fmap -> 'r -> 'r) f m v=  (ITSET (\ (k, v) r .  f k v r) (FMAP_TO_SET m) v))`;
+
+
+(*
+assert fold_1: (fold (fun k v a -> (a+k)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 9)
+assert fold_2: (fold (fun k v a -> (a+v)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 12)
+*)
+
+(*val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)*)
+(* declare compile_message toList = "Map_extra.toList is only defined for the ocaml, isabelle and coq backend" *)
+
+(* more 'map' functions *)
+
+(* TODO: this function is in map_extra rather than map just for implementation reasons *)
+(*val mapMaybe : forall 'a 'b 'c. MapKeyType 'a => ('a -> 'b -> maybe 'c) -> map 'a 'b -> map 'a 'c*)
+(* OLD: TODO: mapMaybe depends on toList that is not defined for hol and isabelle *)
+val _ = Define `
+ ((option_map:('a -> 'b -> 'c option) ->('a,'b)fmap ->('a,'c)fmap) f m=
+   (FOLDL
+    (\ m' (k, v) . 
+      (case f k v of
+          NONE => m'
+        | SOME v' =>m' |+ (k, v')
+      ))
+    FEMPTY
+    (MAP_TO_LIST m)))`;
+
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_maybeScript.sml b/prover_snapshots/hol4/lib/lem/lem_maybeScript.sml
new file mode 100644
index 0000000..bcf4348
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_maybeScript.sml
@@ -0,0 +1,112 @@
+(*Generated by Lem from maybe.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_functionTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_maybe"
+
+ 
+
+(*open import Bool Basic_classes Function*)
+
+(* ========================================================================== *)
+(* Basic stuff                                                                *)
+(* ========================================================================== *)
+
+(*type maybe 'a = 
+  | Nothing
+  | Just of 'a*)
+
+
+(*val maybeEqual : forall 'a. Eq 'a => maybe 'a -> maybe 'a -> bool*)
+(*val maybeEqualBy : forall 'a. ('a -> 'a -> bool) -> maybe 'a -> maybe 'a -> bool*)
+
+val _ = Define `
+ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq NONE NONE=  T)
+/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq NONE (SOME _)=  F)
+/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq (SOME _) NONE=  F)
+/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq (SOME x') (SOME y')=  (eq x' y'))`;
+  
+
+
+val _ = Define `
+ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE NONE=  EQUAL)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE (SOME _)=  LESS)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME _) NONE=  GREATER)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME x') (SOME y')=  (cmp x' y'))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_Maybe_maybe_dict:'a Ord_class ->('a option)Ord_class)dict_Basic_classes_Ord_a= (<|
+
+  compare_method := (maybeCompare  
+  dict_Basic_classes_Ord_a.compare_method);
+
+  isLess_method := (\ m1 .  (\ m2 .  maybeCompare  
+  dict_Basic_classes_Ord_a.compare_method m1 m2 = LESS));
+
+  isLessEqual_method := (\ m1 .  (\ m2 .  (let r = (maybeCompare  
+  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = LESS) \/ (r = EQUAL))));
+
+  isGreater_method := (\ m1 .  (\ m2 .  maybeCompare  
+  dict_Basic_classes_Ord_a.compare_method m1 m2 = GREATER));
+
+  isGreaterEqual_method := (\ m1 .  (\ m2 .  (let r = (maybeCompare  
+  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = GREATER) \/ (r = EQUAL))))|>))`;
+
+
+(* ----------------------- *)
+(* maybe                   *)
+(* ----------------------- *)
+
+(*val maybe : forall 'a 'b. 'b -> ('a -> 'b) -> maybe 'a -> 'b*)
+(*let maybe d f mb=  match mb with 
+  | Just a -> f a
+  | Nothing -> d
+end*)
+
+(* ----------------------- *)
+(* isJust / isNothing      *)
+(* ----------------------- *)
+
+(*val isJust : forall 'a. maybe 'a -> bool*)
+(*let isJust mb=  match mb with 
+  | Just _ -> true
+  | Nothing -> false
+end*)
+
+(*val isNothing : forall 'a. maybe 'a -> bool*)
+(*let isNothing mb=  match mb with 
+  | Just _ -> false
+  | Nothing -> true
+end*)
+
+(* ----------------------- *)
+(* fromMaybe               *)
+(* ----------------------- *)
+
+(*val fromMaybe : forall 'a. 'a -> maybe 'a -> 'a*)
+(*let fromMaybe d mb=  match mb with
+   | Just v  -> v
+   | Nothing -> d
+end*)
+
+(* ----------------------- *)
+(* map                     *)
+(* ----------------------- *)
+
+(*val map : forall 'a 'b. ('a -> 'b) -> maybe 'a -> maybe 'b*) 
+(*let map f=  maybe Nothing (fun v -> Just (f v))*)
+
+
+(* ----------------------- *)
+(* bind                    *)
+(* ----------------------- *)
+
+(*val bind : forall 'a 'b. maybe 'a -> ('a -> maybe 'b) -> maybe 'b*) 
+(*let bind mb f=  maybe Nothing f mb*)
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_maybe_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_maybe_extraScript.sml
new file mode 100644
index 0000000..22d7e06
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_maybe_extraScript.sml
@@ -0,0 +1,23 @@
+(*Generated by Lem from maybe_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_basic_classesTheory lem_maybeTheory lem_assert_extraTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_maybe_extra"
+
+ 
+
+(*open import Basic_classes Maybe Assert_extra*)
+
+(* ----------------------- *)
+(* fromJust                *)
+(* ----------------------- *)
+
+(*val fromJust : forall 'a. maybe 'a -> 'a*)
+(*let fromJust op=  match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_numScript.sml b/prover_snapshots/hol4/lib/lem/lem_numScript.sml
new file mode 100644
index 0000000..d891079
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_numScript.sml
@@ -0,0 +1,1329 @@
+(*Generated by Lem from num.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory integerTheory intReduce wordsTheory wordsLib ratTheory realTheory intrealTheory transcTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_num"
+
+
+
+(*open import Bool Basic_classes*)
+(*open import {isabelle} `HOL-Word.Word` `Complex_Main`*)
+(*open import {hol} `integerTheory` `intReduce` `wordsTheory` `wordsLib` `ratTheory` `realTheory` `intrealTheory` `transcTheory`*)
+(*open import {coq} `Coq.Numbers.BinNums` `Coq.ZArith.BinInt` `Coq.ZArith.Zpower` `Coq.ZArith.Zdiv` `Coq.ZArith.Zmax` `Coq.Reals.Rsqrt_def` `Coq.Numbers.Natural.Peano.NPeano` `Coq.QArith.Qabs` `Coq.QArith.Qminmax` `Coq.QArith.Qround` `Coq.Reals.ROrderedType` `Coq.Reals.Rbase` `Coq.Reals.Rfunctions`*) 
+
+(*class inline ( Numeral 'a ) 
+  val fromNumeral : numeral -> 'a 
+end*)
+
+(* ========================================================================== *)
+(* Syntactic type-classes for common operations                               *)
+(* ========================================================================== *)
+
+(* Typeclasses can be used as a mean to overload constants like "+", "-", etc *)
+
+val _ = Hol_datatype `
+(*  'a *) NumNegate_class= <| 
+  numNegate_method : 'a -> 'a 
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumAbs_class= <| 
+  abs_method : 'a -> 'a 
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumAdd_class= <| 
+  numAdd_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumMinus_class= <| 
+  numMinus_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumMult_class= <| 
+  numMult_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumPow_class= <| 
+  numPow_method : 'a -> num -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumDivision_class= <| 
+  numDivision_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumIntegerDivision_class= <| 
+  div_method : 'a -> 'a -> 'a
+|>`;
+
+
+
+val _ = Hol_datatype `
+(*  'a *) NumRemainder_class= <| 
+  mod_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumSucc_class= <| 
+  succ_method : 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) NumPred_class= <| 
+  pred_method : 'a -> 'a
+|>`;
+ 
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(* unbounded size natural numbers *)
+(*type natural*)
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(* bounded size integers with uncertain length *)
+
+(*type int*)
+
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(* unbounded size integers *)
+
+(*type integer*)
+
+(* ----------------------- *)
+(* bint                    *)
+(* ----------------------- *)
+
+(* TODO the bounded ints are only partially implemented, use with care. *)
+
+(* 32 bit integers *)
+(*type int32*) 
+
+(* 64 bit integers *)
+(*type int64*) 
+
+
+(* ----------------------- *)
+(* rational                *)
+(* ----------------------- *)
+
+(* unbounded size and precision rational numbers *)
+
+(*type rational*) (* ???: better type for this in HOL? *)
+
+
+(* ----------------------- *)
+(* real                    *)
+(* ----------------------- *)
+
+(* real numbers *)
+(* Note that for OCaml, this is mapped to floats with 64 bits. *)
+
+(*type real*) (* ???: better type for this in HOL? *)
+
+
+(* ----------------------- *)
+(* double                  *)
+(* ----------------------- *)
+
+(* double precision floating point (64 bits) *)
+
+(*type float64*) (* ???: better type for this in HOL? *)
+
+(*type float32*) (* ???: better type for this in HOL? *)
+
+
+(* ========================================================================== *)
+(* Binding the standard operations for the number types                       *)
+(* ========================================================================== *)
+
+
+(* ----------------------- *)
+(* nat                     *)
+(* ----------------------- *)
+
+(*val natFromNumeral : numeral -> nat*)
+
+(*val natEq : nat -> nat -> bool*)
+
+(*val natLess : nat -> nat -> bool*)
+(*val natLessEqual : nat -> nat -> bool*)
+(*val natGreater : nat -> nat -> bool*)
+(*val natGreaterEqual : nat -> nat -> bool*)
+
+(*val natCompare : nat -> nat -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_nat_dict:(num)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val natAdd : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumAdd_nat_dict:(num)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val natMinus : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumMinus_nat_dict:(num)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val natSucc : nat -> nat*)
+(*let natSucc n=  (Instance_Num_NumAdd_nat.+) n 1*)
+val _ = Define `
+((instance_Num_NumSucc_nat_dict:(num)NumSucc_class)= (<|
+
+  succ_method := SUC|>))`;
+
+
+(*val natPred : nat -> nat*)
+val _ = Define `
+((instance_Num_NumPred_nat_dict:(num)NumPred_class)= (<|
+
+  pred_method := PRE|>))`;
+
+
+(*val natMult : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumMult_nat_dict:(num)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+(*val natDiv : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_nat_dict:(num)NumIntegerDivision_class)= (<|
+
+  div_method := (DIV)|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_nat_dict:(num)NumDivision_class)= (<|
+
+  numDivision_method := (DIV)|>))`;
+
+
+(*val natMod : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumRemainder_nat_dict:(num)NumRemainder_class)= (<|
+
+  mod_method := (MOD)|>))`;
+
+
+
+(*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*)
+ val _ = Define `
+ ((gen_pow_aux:('a -> 'a -> 'a) -> 'a -> 'a -> num -> 'a) (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : num)=
+    ((case e of
+       0 => a (* cannot happen, call discipline guarentees e >= 1 *)
+     | (SUC 0) => mul a b
+     | (  (SUC(SUC e'))) => let e'' = (e DIV( 2 : num)) in
+                   let a' = (if (e MOD( 2 : num)) =( 0 : num) then a else mul a b) in
+                   gen_pow_aux mul a' (mul b b) e''
+   )))`;
+
+       
+val _ = Define `
+ ((gen_pow:'a ->('a -> 'a -> 'a) -> 'a -> num -> 'a) (one1 : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : num) : 'a= 
+   (if e <( 0 : num) then one1 else 
+  if (e =( 0 : num)) then one1 else gen_pow_aux mul one1 b e))`;
+
+
+(*val natPow : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Num_NumPow_nat_dict:(num)NumPow_class)= (<|
+
+  numPow_method := ( ** )|>))`;
+
+
+(*val natMin : nat -> nat -> nat*)
+
+(*val natMax : nat -> nat -> nat*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_nat_dict:(num)OrdMaxMin_class)= (<|
+
+  max_method := MAX;
+
+  min_method := MIN|>))`;
+
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(*val naturalFromNumeral : numeral -> natural*)
+
+(*val naturalEq : natural -> natural -> bool*)
+
+(*val naturalLess : natural -> natural -> bool*)
+(*val naturalLessEqual : natural -> natural -> bool*)
+(*val naturalGreater : natural -> natural -> bool*)
+(*val naturalGreaterEqual : natural -> natural -> bool*)
+
+(*val naturalCompare : natural -> natural -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_natural_dict:(num)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val naturalAdd : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_natural_dict:(num)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val naturalMinus : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_natural_dict:(num)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val naturalSucc : natural -> natural*)
+(*let naturalSucc n=  (Instance_Num_NumAdd_Num_natural.+) n 1*)
+val _ = Define `
+((instance_Num_NumSucc_Num_natural_dict:(num)NumSucc_class)= (<|
+
+  succ_method := SUC|>))`;
+
+
+(*val naturalPred : natural -> natural*)
+val _ = Define `
+((instance_Num_NumPred_Num_natural_dict:(num)NumPred_class)= (<|
+
+  pred_method := PRE|>))`;
+
+
+(*val naturalMult : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_natural_dict:(num)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+
+(*val naturalPow : natural -> nat -> natural*)
+
+val _ = Define `
+((instance_Num_NumPow_Num_natural_dict:(num)NumPow_class)= (<|
+
+  numPow_method := ( ** )|>))`;
+
+
+(*val naturalDiv : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Num_natural_dict:(num)NumIntegerDivision_class)= (<|
+
+  div_method := (DIV)|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Num_natural_dict:(num)NumDivision_class)= (<|
+
+  numDivision_method := (DIV)|>))`;
+
+
+(*val naturalMod : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Num_NumRemainder_Num_natural_dict:(num)NumRemainder_class)= (<|
+
+  mod_method := (MOD)|>))`;
+
+
+(*val naturalMin : natural -> natural -> natural*)
+
+(*val naturalMax : natural -> natural -> natural*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_natural_dict:(num)OrdMaxMin_class)= (<|
+
+  max_method := MAX;
+
+  min_method := MIN|>))`;
+
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(*val intFromNumeral : numeral -> int*)
+
+(*val intEq : int -> int -> bool*)
+
+(*val intLess : int -> int -> bool*)
+(*val intLessEqual : int -> int -> bool*)
+(*val intGreater : int -> int -> bool*)
+(*val intGreaterEqual : int -> int -> bool*)
+
+(*val intCompare : int -> int -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_int_dict:(int)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val intNegate : int -> int*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_int_dict:(int)NumNegate_class)= (<|
+
+  numNegate_method := (\ i. ~ i)|>))`;
+
+
+(*val intAbs : int -> int*) (* TODO: check *)
+
+val _ = Define `
+((instance_Num_NumAbs_Num_int_dict:(int)NumAbs_class)= (<|
+
+  abs_method := ABS|>))`;
+
+
+(*val intAdd : int -> int -> int*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_int_dict:(int)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val intMinus : int -> int -> int*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_int_dict:(int)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val intSucc : int -> int*)
+val _ = Define `
+((instance_Num_NumSucc_Num_int_dict:(int)NumSucc_class)= (<|
+
+  succ_method := (\ n. n +( 1 : int))|>))`;
+
+
+(*val intPred : int -> int*)
+val _ = Define `
+((instance_Num_NumPred_Num_int_dict:(int)NumPred_class)= (<|
+
+  pred_method := (\ n. n -( 1 : int))|>))`;
+
+
+(*val intMult : int -> int -> int*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_int_dict:(int)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+
+(*val intPow : int -> nat -> int*)
+
+val _ = Define `
+((instance_Num_NumPow_Num_int_dict:(int)NumPow_class)= (<|
+
+  numPow_method := ( ** )|>))`;
+
+
+(*val intDiv : int -> int -> int*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Num_int_dict:(int)NumIntegerDivision_class)= (<|
+
+  div_method := (/)|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Num_int_dict:(int)NumDivision_class)= (<|
+
+  numDivision_method := (/)|>))`;
+
+
+(*val intMod : int -> int -> int*)
+
+val _ = Define `
+((instance_Num_NumRemainder_Num_int_dict:(int)NumRemainder_class)= (<|
+
+  mod_method := (%)|>))`;
+
+
+(*val intMin : int -> int -> int*)
+
+(*val intMax : int -> int -> int*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_int_dict:(int)OrdMaxMin_class)= (<|
+
+  max_method := int_max;
+
+  min_method := int_min|>))`;
+
+
+(* ----------------------- *)
+(* int32                   *)
+(* ----------------------- *)
+(*val int32FromNumeral : numeral -> int32*)
+
+(*val int32Eq : int32 -> int32 -> bool*)
+
+(*val int32Less : int32 -> int32 -> bool*)
+(*val int32LessEqual : int32 -> int32 -> bool*)
+(*val int32Greater : int32 -> int32 -> bool*)
+(*val int32GreaterEqual : int32 -> int32 -> bool*)
+
+(*val int32Compare : int32 -> int32 -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_int32_dict:(word32)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val int32Negate : int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_int32_dict:(word32)NumNegate_class)= (<|
+
+  numNegate_method := (\ i. ((- i) : word32))|>))`;
+
+
+(*val int32Abs : int32 -> int32*)
+val _ = Define `
+ ((int32Abs:word32 -> word32) i=  (if((n2w 0) : word32) <= i then i else ((- i) : word32)))`;
+
+
+val _ = Define `
+((instance_Num_NumAbs_Num_int32_dict:(word32)NumAbs_class)= (<|
+
+  abs_method := int32Abs|>))`;
+
+
+
+(*val int32Add : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_int32_dict:(word32)NumAdd_class)= (<|
+
+  numAdd_method := (\ i1 i2. ((word_add i1 i2) : word32))|>))`;
+
+
+(*val int32Minus : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_int32_dict:(word32)NumMinus_class)= (<|
+
+  numMinus_method := (\ i1 i2. ((word_sub i1 i2) : word32))|>))`;
+
+
+(*val int32Succ : int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumSucc_Num_int32_dict:(word32)NumSucc_class)= (<|
+
+  succ_method := (\ n.  ((word_add n (((n2w 1) : word32))) : word32))|>))`;
+
+
+(*val int32Pred : int32 -> int32*)
+val _ = Define `
+((instance_Num_NumPred_Num_int32_dict:(word32)NumPred_class)= (<|
+
+  pred_method := (\ n.  ((word_sub n (((n2w 1) : word32))) : word32))|>))`;
+
+
+(*val int32Mult : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_int32_dict:(word32)NumMult_class)= (<|
+
+  numMult_method := (\ i1 i2. ((word_mul i1 i2) : word32))|>))`;
+
+
+
+(*val int32Pow : int32 -> nat -> int32*)
+val _ = Define `
+ ((int32Pow:word32 -> num -> word32)=  (gen_pow(((n2w 1) : word32)) (\ i1 i2. ((word_mul i1 i2) : word32))))`;
+
+
+val _ = Define `
+((instance_Num_NumPow_Num_int32_dict:(word32)NumPow_class)= (<|
+
+  numPow_method := int32Pow|>))`;
+
+
+(*val int32Div : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Num_int32_dict:(word32)NumIntegerDivision_class)= (<|
+
+  div_method := (\ i1 i2. ((word_div i1 i2) : word32))|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Num_int32_dict:(word32)NumDivision_class)= (<|
+
+  numDivision_method := (\ i1 i2. ((word_div i1 i2) : word32))|>))`;
+
+
+(*val int32Mod : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Num_NumRemainder_Num_int32_dict:(word32)NumRemainder_class)= (<|
+
+  mod_method := (\ i1 i2. ((word_mod i1 i2) : word32))|>))`;
+
+
+(*val int32Min : int32 -> int32 -> int32*)
+
+(*val int32Max : int32 -> int32 -> int32*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_int32_dict:(word32)OrdMaxMin_class)= (<|
+
+  max_method := word_smax;
+
+  min_method := word_smin|>))`;
+
+
+
+
+(* ----------------------- *)
+(* int64                   *)
+(* ----------------------- *)
+(*val int64FromNumeral : numeral -> int64*)
+
+(*val int64Eq : int64 -> int64 -> bool*)
+
+(*val int64Less : int64 -> int64 -> bool*)
+(*val int64LessEqual : int64 -> int64 -> bool*)
+(*val int64Greater : int64 -> int64 -> bool*)
+(*val int64GreaterEqual : int64 -> int64 -> bool*)
+
+(*val int64Compare : int64 -> int64 -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_int64_dict:(word64)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val int64Negate : int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_int64_dict:(word64)NumNegate_class)= (<|
+
+  numNegate_method := (\ i. ((- i) : word64))|>))`;
+
+
+(*val int64Abs : int64 -> int64*)
+val _ = Define `
+ ((int64Abs:word64 -> word64) i=  (if((n2w 0) : word64) <= i then i else ((- i) : word64)))`;
+
+
+val _ = Define `
+((instance_Num_NumAbs_Num_int64_dict:(word64)NumAbs_class)= (<|
+
+  abs_method := int64Abs|>))`;
+
+
+
+(*val int64Add : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_int64_dict:(word64)NumAdd_class)= (<|
+
+  numAdd_method := (\ i1 i2. ((word_add i1 i2) : word64))|>))`;
+
+
+(*val int64Minus : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_int64_dict:(word64)NumMinus_class)= (<|
+
+  numMinus_method := (\ i1 i2. ((word_sub i1 i2) : word64))|>))`;
+
+
+(*val int64Succ : int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumSucc_Num_int64_dict:(word64)NumSucc_class)= (<|
+
+  succ_method := (\ n.  ((word_add n (((n2w 1) : word64))) : word64))|>))`;
+
+
+(*val int64Pred : int64 -> int64*)
+val _ = Define `
+((instance_Num_NumPred_Num_int64_dict:(word64)NumPred_class)= (<|
+
+  pred_method := (\ n.  ((word_sub n (((n2w 1) : word64))) : word64))|>))`;
+
+
+(*val int64Mult : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_int64_dict:(word64)NumMult_class)= (<|
+
+  numMult_method := (\ i1 i2. ((word_mul i1 i2) : word64))|>))`;
+
+
+
+(*val int64Pow : int64 -> nat -> int64*)
+val _ = Define `
+ ((int64Pow:word64 -> num -> word64)=  (gen_pow(((n2w 1) : word64)) (\ i1 i2. ((word_mul i1 i2) : word64))))`;
+
+
+val _ = Define `
+((instance_Num_NumPow_Num_int64_dict:(word64)NumPow_class)= (<|
+
+  numPow_method := int64Pow|>))`;
+
+
+(*val int64Div : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Num_int64_dict:(word64)NumIntegerDivision_class)= (<|
+
+  div_method := (\ i1 i2. ((word_div i1 i2) : word64))|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Num_int64_dict:(word64)NumDivision_class)= (<|
+
+  numDivision_method := (\ i1 i2. ((word_div i1 i2) : word64))|>))`;
+
+
+(*val int64Mod : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Num_NumRemainder_Num_int64_dict:(word64)NumRemainder_class)= (<|
+
+  mod_method := (\ i1 i2. ((word_mod i1 i2) : word64))|>))`;
+
+
+(*val int64Min : int64 -> int64 -> int64*)
+
+(*val int64Max : int64 -> int64 -> int64*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_int64_dict:(word64)OrdMaxMin_class)= (<|
+
+  max_method := word_smax;
+
+  min_method := word_smin|>))`;
+
+
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(*val integerFromNumeral : numeral -> integer*)
+
+(*val integerFromNat : nat -> integer*) (* TODO: check *)
+
+(*val integerEq : integer -> integer -> bool*)
+
+(*val integerLess : integer -> integer -> bool*)
+(*val integerLessEqual : integer -> integer -> bool*)
+(*val integerGreater : integer -> integer -> bool*)
+(*val integerGreaterEqual : integer -> integer -> bool*)
+
+(*val integerCompare : integer -> integer -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_integer_dict:(int)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val integerNegate : integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_integer_dict:(int)NumNegate_class)= (<|
+
+  numNegate_method := (\ i. ~ i)|>))`;
+
+
+(*val integerAbs : integer -> integer*) (* TODO: check *)
+
+val _ = Define `
+((instance_Num_NumAbs_Num_integer_dict:(int)NumAbs_class)= (<|
+
+  abs_method := ABS|>))`;
+
+
+(*val integerAdd : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_integer_dict:(int)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val integerMinus : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_integer_dict:(int)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val integerSucc : integer -> integer*)
+val _ = Define `
+((instance_Num_NumSucc_Num_integer_dict:(int)NumSucc_class)= (<|
+
+  succ_method := (\ n. n +( 1 : int))|>))`;
+
+
+(*val integerPred : integer -> integer*)
+val _ = Define `
+((instance_Num_NumPred_Num_integer_dict:(int)NumPred_class)= (<|
+
+  pred_method := (\ n. n -( 1 : int))|>))`;
+
+
+(*val integerMult : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_integer_dict:(int)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+
+(*val integerPow : integer -> nat -> integer*)
+
+val _ = Define `
+((instance_Num_NumPow_Num_integer_dict:(int)NumPow_class)= (<|
+
+  numPow_method := ( ** )|>))`;
+
+
+(*val integerDiv : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Num_integer_dict:(int)NumIntegerDivision_class)= (<|
+
+  div_method := (/)|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Num_integer_dict:(int)NumDivision_class)= (<|
+
+  numDivision_method := (/)|>))`;
+
+
+(*val integerMod : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Num_NumRemainder_Num_integer_dict:(int)NumRemainder_class)= (<|
+
+  mod_method := (%)|>))`;
+
+
+(*val integerMin : integer -> integer -> integer*)
+
+(*val integerMax : integer -> integer -> integer*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_integer_dict:(int)OrdMaxMin_class)= (<|
+
+  max_method := int_max;
+
+  min_method := int_min|>))`;
+
+
+
+
+(* ----------------------- *)
+(* rational                *)
+(* ----------------------- *)
+
+(*val rationalFromNumeral : numeral -> rational*)
+
+(*val rationalFromInt : int -> rational*)
+
+(*val rationalFromInteger : integer -> rational*)
+
+(*val rationalEq : rational -> rational -> bool*)
+
+(*val rationalLess : rational -> rational -> bool*)
+(*val rationalLessEqual : rational -> rational -> bool*)
+(*val rationalGreater : rational -> rational -> bool*)
+(*val rationalGreaterEqual : rational -> rational -> bool*)
+
+(*val rationalCompare : rational -> rational -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_rational_dict:(rat)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val rationalAdd : rational -> rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_rational_dict:(rat)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val rationalMinus : rational -> rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_rational_dict:(rat)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val rationalNegate : rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_rational_dict:(rat)NumNegate_class)= (<|
+
+  numNegate_method := (\ n. ( 0 : rat) - n)|>))`;
+
+
+(*val rationalAbs : rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumAbs_Num_rational_dict:(rat)NumAbs_class)= (<|
+
+  abs_method := (\ n. (if n >( 0 : rat) then n else( 0 : rat) - n))|>))`;
+
+
+(*val rationalSucc : rational -> rational*)
+val _ = Define `
+((instance_Num_NumSucc_Num_rational_dict:(rat)NumSucc_class)= (<|
+
+  succ_method := (\ n. n +( 1 : rat))|>))`;
+
+
+(*val rationalPred : rational -> rational*)
+val _ = Define `
+((instance_Num_NumPred_Num_rational_dict:(rat)NumPred_class)= (<|
+
+  pred_method := (\ n. n -( 1 : rat))|>))`;
+
+
+(*val rationalMult : rational -> rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_rational_dict:(rat)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+(*val rationalDiv : rational -> rational -> rational*)
+
+val _ = Define `
+((instance_Num_NumDivision_Num_rational_dict:(rat)NumDivision_class)= (<|
+
+  numDivision_method := (/)|>))`;
+
+
+(*val rationalFromFrac : int -> int -> rational*)
+(*let rationalFromFrac n d=  (Instance_Num_NumDivision_Num_rational./) (rationalFromInt n) (rationalFromInt d)*)
+
+(*val rationalNumerator : rational -> integer*)  (* TODO: test *)
+
+(*val rationalDenominator : rational -> integer*)  (* TODO: test *)
+
+(*val rationalPowInteger : rational -> integer -> rational*)
+ val rationalPowInteger_defn = Hol_defn "rationalPowInteger" `
+ ((rationalPowInteger:rat -> int -> rat) b e=
+   (if e =( 0 : int) then( 1 : rat) else
+  if e >( 0 : int) then rationalPowInteger b (e -( 1 : int)) * b else
+  rationalPowInteger b (e +( 1 : int)) / b))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn rationalPowInteger_defn;
+
+(*val rationalPowNat : rational -> nat -> rational*)
+val _ = Define `
+ ((rationalPowNat:rat -> num -> rat) r e=  (rationalPowInteger r (int_of_num e)))`;
+
+
+val _ = Define `
+((instance_Num_NumPow_Num_rational_dict:(rat)NumPow_class)= (<|
+
+  numPow_method := rationalPowNat|>))`;
+
+
+(*val rationalMin : rational -> rational -> rational*)
+
+(*val rationalMax : rational -> rational -> rational*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_rational_dict:(rat)OrdMaxMin_class)= (<|
+
+  max_method := (maxByLessEqual (<=));
+
+  min_method := (minByLessEqual (<=))|>))`;
+
+
+
+
+(* ----------------------- *)
+(* real                    *)
+(* ----------------------- *)
+
+(*val realFromNumeral : numeral -> real*)
+
+(*val realFromInteger : integer -> real*)
+
+(*val realEq : real -> real -> bool*)
+
+(*val realLess : real -> real -> bool*)
+(*val realLessEqual : real -> real -> bool*)
+(*val realGreater : real -> real -> bool*)
+(*val realGreaterEqual : real -> real -> bool*)
+
+(*val realCompare : real -> real -> ordering*)
+
+val _ = Define `
+((instance_Basic_classes_Ord_Num_real_dict:(real)Ord_class)= (<|
+
+  compare_method := (genericCompare (<) (=));
+
+  isLess_method := (<);
+
+  isLessEqual_method := (<=);
+
+  isGreater_method := (>);
+
+  isGreaterEqual_method := (>=)|>))`;
+
+
+(*val realAdd : real -> real -> real*)
+
+val _ = Define `
+((instance_Num_NumAdd_Num_real_dict:(real)NumAdd_class)= (<|
+
+  numAdd_method := (+)|>))`;
+
+
+(*val realMinus : real -> real -> real*)
+
+val _ = Define `
+((instance_Num_NumMinus_Num_real_dict:(real)NumMinus_class)= (<|
+
+  numMinus_method := (-)|>))`;
+
+
+(*val realNegate : real -> real*)
+
+val _ = Define `
+((instance_Num_NumNegate_Num_real_dict:(real)NumNegate_class)= (<|
+
+  numNegate_method := (\ n. (real_of_num 0) - n)|>))`;
+
+
+(*val realAbs : real -> real*)
+
+val _ = Define `
+((instance_Num_NumAbs_Num_real_dict:(real)NumAbs_class)= (<|
+
+  abs_method := (\ n. (if n >(real_of_num 0) then n else(real_of_num 0) - n))|>))`;
+
+
+(*val realSucc : real -> real*)
+val _ = Define `
+((instance_Num_NumSucc_Num_real_dict:(real)NumSucc_class)= (<|
+
+  succ_method := (\ n. n +(real_of_num 1))|>))`;
+
+
+(*val realPred : real -> real*)
+val _ = Define `
+((instance_Num_NumPred_Num_real_dict:(real)NumPred_class)= (<|
+
+  pred_method := (\ n. n -(real_of_num 1))|>))`;
+
+
+(*val realMult : real -> real -> real*)
+
+val _ = Define `
+((instance_Num_NumMult_Num_real_dict:(real)NumMult_class)= (<|
+
+  numMult_method := ( * )|>))`;
+
+
+(*val realDiv : real -> real -> real*)
+
+val _ = Define `
+((instance_Num_NumDivision_Num_real_dict:(real)NumDivision_class)= (<|
+
+  numDivision_method := (/)|>))`;
+
+
+(*val realFromFrac : integer -> integer -> real*)
+val _ = Define `
+ ((realFromFrac:int -> int -> real) n d=  (((real_of_int n)) / ((real_of_int d))))`;
+
+
+(*val realPowInteger : real -> integer -> real*)
+ val realPowInteger_defn = Hol_defn "realPowInteger" `
+ ((realPowInteger:real -> int -> real) b e=
+   (if e =( 0 : int) then(real_of_num 1) else
+  if e >( 0 : int) then realPowInteger b (e -( 1 : int)) * b else
+  realPowInteger b (e +( 1 : int)) / b))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn realPowInteger_defn;
+
+(*val realPowNat : real -> nat -> real*)
+(*let realPowNat r e=  realPowInteger r (integerFromNat e)*)
+
+val _ = Define `
+((instance_Num_NumPow_Num_real_dict:(real)NumPow_class)= (<|
+
+  numPow_method := (pow)|>))`;
+
+
+(*val realSqrt : real -> real*)
+
+(*val realMin : real -> real -> real*)
+
+(*val realMax : real -> real -> real*)
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Num_real_dict:(real)OrdMaxMin_class)= (<|
+
+  max_method := max;
+
+  min_method := min|>))`;
+
+
+(*val realCeiling : real -> integer*)
+
+(*val realFloor : real -> integer*)
+
+
+(*val integerSqrt : integer -> integer*)
+val _ = Define `
+ ((integerSqrt:int -> int) i=  (flr (sqrt ((real_of_int i)))))`;
+
+
+(* ========================================================================== *)
+(* Translation between number types                                           *)
+(* ========================================================================== *)
+
+(******************)
+(* integerFrom... *)
+(******************)
+
+(*val integerFromInt : int -> integer*)
+
+(*val integerFromNatural : natural -> integer*)
+
+
+(*val integerFromInt32 : int32 -> integer*)
+
+
+(*val integerFromInt64 : int64 -> integer*)
+
+
+(******************)
+(* naturalFrom... *)
+(******************)
+
+(*val naturalFromNat : nat -> natural*)
+
+(*val naturalFromInteger : integer -> natural*)
+
+
+(******************)
+(* intFrom ...    *)
+(******************)
+
+(*val intFromInteger : integer -> int*)
+
+(*val intFromNat : nat -> int*)
+
+
+(******************)
+(* natFrom ...    *)
+(******************)
+
+(*val natFromNatural : natural -> nat*)
+
+(*val natFromInt : int -> nat*)
+
+
+(******************)
+(* int32From ...  *)
+(******************)
+
+(*val int32FromNat : nat -> int32*)
+
+(*val int32FromNatural : natural -> int32*)
+
+(*val int32FromInteger : integer -> int32*)
+val _ = Define `
+ ((int32FromInteger:int -> word32) i=  (
+  let abs_int32 = (((n2w (Num (ABS i))) : word32)) in
+  if (i <( 0 : int)) then (((- abs_int32) : word32)) else abs_int32 
+))`;
+
+
+(*val int32FromInt : int -> int32*)
+val _ = Define `
+ ((int32FromInt:int -> word32) i=  (int32FromInteger ( i)))`;
+
+
+
+(*val int32FromInt64 : int64 -> int32*)
+(*let int32FromInt64 i=  int32FromInteger (integerFromInt64 i)*)
+
+
+
+
+(******************)
+(* int64From ...  *)
+(******************)
+
+(*val int64FromNat : nat -> int64*)
+
+(*val int64FromNatural : natural -> int64*)
+
+(*val int64FromInteger : integer -> int64*)
+val _ = Define `
+ ((int64FromInteger:int -> word64) i=  (
+  let abs_int64 = (((n2w (Num (ABS i))) : word64)) in
+  if (i <( 0 : int)) then (((- abs_int64) : word64)) else abs_int64 
+))`;
+
+
+(*val int64FromInt : int -> int64*)
+val _ = Define `
+ ((int64FromInt:int -> word64) i=  (int64FromInteger ( i)))`;
+
+
+
+(*val int64FromInt32 : int32 -> int64*)
+(*let int64FromInt32 i=  int64FromInteger (integerFromInt32 i)*)
+
+
+(******************)
+(* what's missing *)
+(******************)
+
+(*val naturalFromInt : int -> natural*)
+(*val naturalFromInt32 : int32 -> natural*)
+(*val naturalFromInt64 : int64 -> natural*)
+
+
+(*val intFromNatural : natural -> int*)
+(*val intFromInt32 : int32 -> int*)
+(*val intFromInt64 : int64 -> int*)
+
+(*val natFromInteger : integer -> nat*)
+(*val natFromInt32 : int32 -> nat*)
+(*val natFromInt64 : int64 -> nat*)
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_num_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_num_extraScript.sml
new file mode 100644
index 0000000..eb97041
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_num_extraScript.sml
@@ -0,0 +1,73 @@
+(*Generated by Lem from num_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_numTheory lem_basic_classesTheory lem_assert_extraTheory lem_stringTheory ASCIInumbersTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_num_extra"
+
+(* **************************************************** *)
+(*                                                      *)
+(* A library of additional functions on numbers         *)
+(*                                                      *)
+(* **************************************************** *)
+
+(*open import Basic_classes*)
+(*open import Num*)
+(*open import String*)
+(*open import Assert_extra*)
+
+(*open import {hol} `ASCIInumbersTheory`*)
+
+(*val naturalOfString : string -> natural*)
+
+(*val integerOfString : string -> integer*)
+
+(*val integerOfChar : char -> integer*)
+
+val _ = Define `
+ ((integerOfChar:char -> int)= 
+  (\x .  (case x of
+               #"0" =>( 0 : int)
+           | #"1" =>( 1 : int)
+           | #"2" =>( 2 : int)
+           | #"3" =>( 3 : int)
+           | #"4" =>( 4 : int)
+           | #"5" =>( 5 : int)
+           | #"6" =>( 6 : int)
+           | #"7" =>( 7 : int)
+           | #"8" =>( 8 : int)
+           | #"9" =>( 9 : int)
+           | _ => failwith "integerOfChar: unexpected character"
+         )))`;
+
+
+(*val integerOfStringHelper : list char -> integer*)
+
+ val integerOfStringHelper_defn = Defn.Hol_multi_defns `
+ ((integerOfStringHelper:(char)list -> int) (d :: ds)=  (integerOfChar d + (( 10 : int) * integerOfStringHelper ds)))
+/\ ((integerOfStringHelper:(char)list -> int) ([])= (( 0 : int)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) integerOfStringHelper_defn;
+
+val _ = Define `
+ ((integerOfString:string -> int) s= 
+  (list_CASE s (int_of_num (toNum s))
+     (\c s0. (case(c,s0) of
+                 ( #"-",_) => ~ (int_of_num (toNum s0))
+               | (_,_) => int_of_num (toNum s)
+             ))))`;
+
+
+(* Truncation integer division (round toward zero) *)
+(*val integerDiv_t: integer -> integer -> integer*)
+
+(* Truncation modulo *)
+(*val integerRem_t: integer -> integer -> integer*)
+
+(* Flooring modulo *)
+(*val integerRem_f: integer -> integer -> integer*)
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_pervasivesScript.sml b/prover_snapshots/hol4/lib/lem/lem_pervasivesScript.sml
new file mode 100644
index 0000000..34c8b4a
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_pervasivesScript.sml
@@ -0,0 +1,18 @@
+(*Generated by Lem from pervasives.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_basic_classesTheory lem_boolTheory lem_tupleTheory lem_maybeTheory lem_eitherTheory lem_functionTheory lem_numTheory lem_mapTheory lem_setTheory lem_listTheory lem_stringTheory lem_wordTheory lem_showTheory lem_sortingTheory lem_relationTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_pervasives"
+
+ 
+
+(*include import Basic_classes Bool Tuple Maybe Either Function Num Map Set List String Word Show*)
+
+(*import Sorting Relation*)
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_pervasives_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_pervasives_extraScript.sml
new file mode 100644
index 0000000..33ccd62
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_pervasives_extraScript.sml
@@ -0,0 +1,16 @@
+(*Generated by Lem from pervasives_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasivesTheory lem_function_extraTheory lem_maybe_extraTheory lem_map_extraTheory lem_num_extraTheory lem_set_extraTheory lem_set_helpersTheory lem_list_extraTheory lem_string_extraTheory lem_assert_extraTheory lem_show_extraTheory lem_machine_wordTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_pervasives_extra"
+
+ 
+
+(*include import Pervasives*) 
+(*include import Function_extra Maybe_extra Map_extra Num_extra Set_extra Set_helpers List_extra String_extra Assert_extra Show_extra Machine_word*)
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_relationScript.sml b/prover_snapshots/hol4/lib/lem/lem_relationScript.sml
new file mode 100644
index 0000000..7d019b2
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_relationScript.sml
@@ -0,0 +1,448 @@
+(*Generated by Lem from relation.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_tupleTheory lem_setTheory lem_numTheory set_relationTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_relation"
+
+
+
+(*open import Bool Basic_classes Tuple Set Num*)
+(*open import {hol} `set_relationTheory`*)
+
+(* ========================================================================== *)
+(* The type of relations                                                      *)
+(* ========================================================================== *)
+
+val _ = type_abbrev((* ( 'a, 'b) *) "rel_pred" , ``: 'a -> 'b -> bool``);
+val _ = type_abbrev((* ( 'a, 'b) *) "rel_set" , ``: ('a # 'b) set``);
+
+(* Binary relations are usually represented as either
+   sets of pairs (rel_set) or as curried functions (rel_pred). 
+   
+   The choice depends on taste and the backend. Lem should not take a 
+   decision, but supports both representations. There is an abstract type
+   pred, which can be converted to both representations. The representation
+   of pred itself then depends on the backend. However, for the time beeing,
+   let's implement relations as sets to get them working more quickly. *)
+
+val _ = type_abbrev((* ( 'a, 'b) *) "rel" , ``: ('a, 'b) rel_set``);
+
+(*val relToSet : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel_set 'a 'b*)
+(*val relFromSet : forall 'a 'b. SetType 'a, SetType 'b => rel_set 'a 'b -> rel 'a 'b*)
+
+(*val relEq : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+val _ = Define `
+ ((relEq:('a#'b)set ->('a#'b)set -> bool) r1 r2=  (r1 = r2))`;
+
+
+(*val relToPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel_pred 'a 'b*)
+(*val relFromPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => set 'a -> set 'b -> rel_pred 'a 'b -> rel 'a 'b*)
+
+(*let relToPred r=  (fun x y -> (x, y) IN relToSet r)*)
+val _ = Define `
+ ((relFromPred:'a set -> 'b set ->('a -> 'b -> bool) ->('a#'b)set) xs ys p=  (SET_FILTER (\ (x,y) .  p x y) (xs CROSS ys)))`;
+
+
+ 
+(* ========================================================================== *)
+(* Basic Operations                                                           *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* membership test         *)
+(* ----------------------- *)
+
+(*val inRel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => 'a -> 'b -> rel 'a 'b -> bool*)
+
+
+(* ----------------------- *)
+(* empty relation          *)
+(* ----------------------- *)
+
+(*val relEmpty : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b*)
+
+(* ----------------------- *)
+(* Insertion               *)
+(* ----------------------- *)
+
+(*val relAdd : forall 'a 'b. SetType 'a, SetType 'b => 'a -> 'b -> rel 'a 'b -> rel 'a 'b*)
+
+
+(* ----------------------- *)
+(* Identity relation       *)
+(* ----------------------- *)
+
+(*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*)
+val _ = Define `
+ ((relIdOn:'a set ->('a#'a)set) s=  (relFromPred s s (=)))`;
+
+
+(*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*)
+val _ = Define `
+ ((relId:('a#'a)set)=  ({(x, x) |  x | T}))`;
+
+
+(* ----------------------- *)
+(* relation union          *)
+(* ----------------------- *)
+
+(*val relUnion : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* relation intersection   *)
+(* ----------------------- *)
+
+(*val relIntersection : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* Relation Composition    *)
+(* ----------------------- *)
+
+(*val relComp : forall 'a 'b 'c. SetType 'a, SetType 'b, SetType 'c, Eq 'a, Eq 'b => rel 'a 'b -> rel 'b 'c -> rel 'a 'c*)
+(*let relComp r1 r2=  relFromSet {(e1, e3) | forall ((e1,e2) IN (relToSet r1)) ((e2',e3) IN (relToSet r2)) | e2 = e2'}*)
+
+(* ----------------------- *)
+(* restrict                *)
+(* ----------------------- *)
+
+(*val relRestrict : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+(*let relRestrict r s=  relFromSet ({ (a, b) | forall (a IN s) (b IN s) | inRel a b r })*)
+
+
+(* ----------------------- *)
+(* Converse                *)
+(* ----------------------- *)
+
+(*val relConverse : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'b 'a*)
+val _ = Define `
+ ((lem_converse:('a#'b)set ->('b#'a)set) r=  (IMAGE SWAP (r)))`;
+
+
+
+(* ----------------------- *)
+(* domain                  *)
+(* ----------------------- *)
+
+(*val relDomain : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'a*)
+(*let relDomain r=  Set.map (fun x -> fst x) (relToSet r)*)
+
+(* ----------------------- *)
+(* range                   *)
+(* ----------------------- *)
+
+(*val relRange : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'b*)
+(*let relRange r=  Set.map (fun x -> snd x) (relToSet r)*)
+
+
+(* ----------------------- *)
+(* field / definedOn       *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relDefinedOn : forall 'a. SetType 'a => rel 'a 'a -> set 'a*)
+
+(* ----------------------- *)
+(* relOver                 *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relOver : forall 'a. SetType 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((rel_over:('a#'a)set -> 'a set -> bool) r s=  ((((domain r) UNION (range r))) SUBSET s))`;
+
+
+
+(* ----------------------- *)
+(* apply a relation        *)
+(* ----------------------- *)
+
+(* Given a relation r and a set s, relApply r s applies s to r, i.e.
+   it returns the set of all value reachable via r from a value in s.
+   This operation can be seen as a generalisation of function application. *)
+   
+(*val relApply : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a => rel 'a 'b -> set 'a -> set 'b*)
+val _ = Define `
+ ((rapply:('a#'b)set -> 'a set -> 'b set) r s= 
+  ({ y | x, y | ((x, y) IN (r)) /\ (x IN s) }))`;
+
+
+
+(* ========================================================================== *)
+(* Properties                                                                 *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* subrel                  *)
+(* ----------------------- *)
+
+(*val isSubrel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+
+(* ----------------------- *)
+(* reflexivity             *)
+(* ----------------------- *)
+
+(*val isReflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_reflexive_on:('a#'a)set -> 'a set -> bool) r s=  (! (e :: s). (e, e) IN r))`;
+
+
+(*val isReflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_reflexive:('a#'a)set -> bool) r=  (! e. (e, e) IN r))`;
+
+
+
+(* ----------------------- *)
+(* irreflexivity           *)
+(* ----------------------- *)
+
+(*val isIrreflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+(*let isIrreflexiveOn r s=  (forall (e IN s). not (inRel e e r))*)
+
+(*val isIrreflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_irreflexive:('a#'a)set -> bool) r=  (! ((e1, e2) :: (r)). ~ (e1 = e2)))`;
+
+
+
+(* ----------------------- *)
+(* symmetry                *)
+(* ----------------------- *)
+
+(*val isSymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_symmetric_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) ==> ((e2, e1) IN r)))`;
+
+
+(*val isSymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_symmetric:('a#'a)set -> bool) r=  (! ((e1, e2) :: r). (e2, e1) IN r))`;
+
+
+
+(* ----------------------- *)
+(* antisymmetry            *)
+(* ----------------------- *)
+
+(*val isAntisymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_antisymmetric_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) ==> (((e2, e1) IN r) ==> (e1 = e2))))`;
+
+
+(*val isAntisymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let isAntisymmetric r=  (forall ((e1, e2) IN relToSet r). (inRel e2 e1 r) --> (e1 = e2))*)
+
+
+(* ----------------------- *)
+(* transitivity            *)
+(* ----------------------- *)
+
+(*val isTransitiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_transitive_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s) (e3 :: s). ((e1, e2) IN r) ==> (((e2, e3) IN r) ==> ((e1, e3) IN r))))`;
+
+
+(*val isTransitive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let isTransitive r=  (forall ((e1, e2) IN relToSet r) (e3 IN relApply r {e2}). inRel e1 e3 r)*)
+
+(* ----------------------- *)
+(* total                   *)
+(* ----------------------- *)
+
+(*val isTotalOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) \/ ((e2, e1) IN r)))`;
+
+
+
+(*val isTotal : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_total:('a#'a)set -> bool) r=  (! e1 e2. ((e1, e2) IN r) \/ ((e2, e1) IN r)))`;
+
+
+(*val isTrichotomousOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_trichotomous_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) \/ ((e1 = e2) \/ ((e2, e1) IN r))))`;
+
+
+(*val isTrichotomous : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_trichotomous:('a#'a)set -> bool) r=  (! e1 e2. ((e1, e2) IN r) \/ ((e1 = e2) \/ ((e2, e1) IN r))))`;
+
+
+
+(* ----------------------- *)
+(* is_single_valued        *)
+(* ----------------------- *)
+
+(*val isSingleValued : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> bool*)
+val _ = Define `
+ ((lem_is_single_valued:('a#'b)set -> bool) r=  (! ((e1, e2a) :: r) (e2b :: rapply r {e1}). e2a = e2b))`;
+
+
+
+(* ----------------------- *)
+(* equivalence relation    *)
+(* ----------------------- *)
+
+(*val isEquivalenceOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_equivalence_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_is_symmetric_on r s /\ lem_transitive_on r s))`;
+
+
+
+(*val isEquivalence : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_equivalence:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ lem_is_symmetric r /\ transitive r))`;
+
+
+
+(* ----------------------- *)
+(* well founded            *)
+(* ----------------------- *)
+
+(*val isWellFounded : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let ~{ocaml;coq} isWellFounded r=  (forall P. (forall x. (forall y. inRel y x r --> P x) --> P x) --> (forall x. P x))*)
+
+
+(* ========================================================================== *)
+(* Orders                                                                     *)
+(* ========================================================================== *)
+
+
+(* ----------------------- *)
+(* pre- or quasiorders     *)
+(* ----------------------- *)
+
+(*val isPreorderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_preorder_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_transitive_on r s))`;
+
+
+(*val isPreorder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_preorder:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ transitive r))`;
+
+
+
+(* ----------------------- *)
+(* partial orders          *)
+(* ----------------------- *)
+
+(*val isPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_partial_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_transitive_on r s /\ lem_is_antisymmetric_on r s))`;
+
+
+
+(*val isStrictPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_partial_order_on:('a#'a)set -> 'a set -> bool) r s=  (irreflexive r s /\ lem_transitive_on r s))`;
+
+
+
+(*val isStrictPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_partial_order:('a#'a)set -> bool) r=  (lem_is_irreflexive r /\ transitive r))`;
+
+
+(*val isPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_partial_order:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ transitive r /\ antisym r))`;
+
+
+(* ----------------------- *)
+(* total / linear orders   *)
+(* ----------------------- *)
+
+(*val isTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_partial_order_on r s /\ lem_is_total_on r s))`;
+
+
+(*val isStrictTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_total_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_strict_partial_order_on r s /\ lem_is_trichotomous_on r s))`;
+
+
+(*val isTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_order:('a#'a)set -> bool) r=  (lem_is_partial_order r /\ lem_is_total r))`;
+
+
+(*val isStrictTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_total_order:('a#'a)set -> bool) r=  (lem_is_strict_partial_order r /\ lem_is_trichotomous r))`;
+
+
+
+
+(* ========================================================================== *)
+(* closures                                                                   *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* transitive closure      *)
+(* ----------------------- *)
+
+(*val transitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByEq  : forall 'a. ('a -> 'a -> bool) -> rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> ordering) -> rel 'a 'a -> rel 'a 'a*)
+
+
+(* ----------------------- *)
+(* transitive closure step *)
+(* ----------------------- *)
+
+(*val transitiveClosureAdd : forall 'a. SetType 'a, Eq 'a => 'a -> 'a -> rel 'a 'a -> rel 'a 'a*)
+
+val _ = Define `
+ ((tc_insert:'a -> 'a ->('a#'a)set ->('a#'a)set) x y r= 
+   ((((((x,y) INSERT (r)))) UNION ((((({(x, z) | z | 
+  (z IN range r) /\ ((y, z) IN r)})) UNION (({(z, y) | z | 
+  (z IN domain r) /\ ((z, x) IN r)}))))))))`;
+
+
+
+(* ========================================================================== *)
+(* reflexive closure                                                          *)
+(* ========================================================================== *)
+
+(*val reflexiveTransitiveClosureOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+val _ = Define `
+ ((reflexive_transitive_closure_on:('a#'a)set -> 'a set ->('a#'a)set) r s=  (tc (((r) UNION ((relIdOn s))))))`;
+
+
+
+(*val reflexiveTransitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+val _ = Define `
+ ((reflexiveTransitiveClosure:('a#'a)set ->('a#'a)set) r=  (tc (((r) UNION (relId)))))`;
+
+
+
+
+(* ========================================================================== *)
+(* inverse of closures                                                        *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* without transitve edges *)
+(* ----------------------- *)
+
+(*val withoutTransitiveEdges: forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+val _ = Define `
+ ((withoutTransitiveEdges:('a#'a)set ->('a#'a)set) r=
+   (let tc1 = (tc r) in
+  {(a, c) | a, c 
+  | ((a, c) IN r) /\
+   (! (b :: range r).
+      ((a <> b) /\ (b <> c)) ==> ~ (((a, b) IN tc1) /\ ((b, c) IN tc1)))}))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_setScript.sml b/prover_snapshots/hol4/lib/lem/lem_setScript.sml
new file mode 100644
index 0000000..c03aec5
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_setScript.sml
@@ -0,0 +1,317 @@
+(*Generated by Lem from set.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_functionTheory lem_numTheory lem_listTheory lem_set_helpersTheory lemTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_set"
+
+(******************************************************************************)
+(* A library for sets                                                         *)
+(*                                                                            *)
+(* It mainly follows the Haskell Set-library                                  *)
+(******************************************************************************)
+
+(* Sets in Lem are a bit tricky. On the one hand, we want efficiently executable sets.
+   OCaml and Haskell both represent sets by some kind of balancing trees. This means
+   that sets are finite and an order on the element type is required. 
+   Such sets are constructed by simple, executable operations like inserting or
+   deleting elements, union, intersection, filtering etc.
+
+   On the other hand, we want to use sets for specifications. This leads often
+   infinite sets, which are specificied in complicated, perhaps even undecidable
+   ways.
+
+   The set library in this file, chooses the first approach. It describes 
+   *finite* sets with an underlying order. Infinite sets should in the medium
+   run be represented by a separate type. Since this would require some significant
+   changes to Lem, for the moment also infinite sets are represented using this
+   class. However, a run-time exception might occour when using these sets. 
+   This problem needs adressing in the future. *)
+   
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+(*open import Bool Basic_classes Maybe Function Num List Set_helpers*)
+
+(* DPM: sets currently implemented as lists due to mismatch between Coq type
+ * class hierarchy and the hierarchy implemented in Lem.
+ *)
+(*open import {coq} `Coq.Lists.List`*)
+(*open import {hol} `lemTheory`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+
+(* ----------------------- *)
+(* Equality check          *)
+(* ----------------------- *)
+
+(*val setEqualBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+
+(*val setEqual : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+
+(* ----------------------- *)
+(* Empty set               *)
+(* ----------------------- *)
+
+(*val empty : forall 'a. SetType 'a => set 'a*) 
+(*val emptyBy : forall 'a. ('a -> 'a -> ordering) -> set 'a*)
+
+(* ----------------------- *)
+(* any / all               *)
+(* ----------------------- *)
+
+(*val any : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*)
+
+(*val all : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*)
+
+
+(* ----------------------- *)
+(* (IN)                    *)
+(* ----------------------- *)
+
+(*val IN [member] : forall 'a. SetType 'a => 'a -> set 'a -> bool*) 
+(*val memberBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a -> bool*)
+
+(* ----------------------- *)
+(* not (IN)                *)
+(* ----------------------- *)
+
+(*val NIN [notMember] : forall 'a. SetType 'a => 'a -> set 'a -> bool*)
+
+
+
+(* ----------------------- *)
+(* Emptyness check         *)
+(* ----------------------- *)
+
+(*val null : forall 'a. SetType 'a => set 'a -> bool*)
+
+
+(* ------------------------ *)
+(* singleton                *)
+(* ------------------------ *)
+
+(*val singletonBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a*)
+(*val singleton : forall 'a. SetType 'a => 'a -> set 'a*)
+
+
+(* ----------------------- *)
+(* size                    *)
+(* ----------------------- *)
+
+(*val size : forall 'a. SetType 'a => set 'a -> nat*)
+
+
+(* ----------------------------*)
+(* setting up pattern matching *)
+(* --------------------------- *)
+
+(*val set_case : forall 'a 'b. SetType 'a => set 'a -> 'b -> ('a -> 'b) -> 'b -> 'b*)
+
+
+(* ------------------------ *)
+(* union                    *)
+(* ------------------------ *)
+
+(*val unionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+(*val union : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+
+(* ----------------------- *)
+(* insert                  *)
+(* ----------------------- *)
+
+(*val insert : forall 'a. SetType 'a => 'a -> set 'a -> set 'a*)
+
+(* ----------------------- *)
+(* filter                  *)
+(* ----------------------- *)
+
+(*val filter : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a*) 
+(*let filter P s=  {e | forall (e IN s) | P e}*)
+
+
+(* ----------------------- *)
+(* partition               *)
+(* ----------------------- *)
+
+(*val partition : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a * set 'a*)
+val _ = Define `
+ ((SET_PARTITION:('a -> bool) -> 'a set -> 'a set#'a set) P s=  (SET_FILTER P s, SET_FILTER (\ e .  ~ (P e)) s))`;
+
+
+
+(* ----------------------- *)
+(* split                   *)
+(* ----------------------- *)
+
+(*val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a*)
+val _ = Define `
+ ((SET_SPLIT:'a Ord_class -> 'a -> 'a set -> 'a set#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
+  dict_Basic_classes_Ord_a.isGreater_method p) s, SET_FILTER (dict_Basic_classes_Ord_a.isLess_method p) s))`;
+
+
+(*val splitMember : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * bool * set 'a*)
+val _ = Define `
+ ((splitMember:'a Ord_class -> 'a -> 'a set -> 'a set#bool#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
+  dict_Basic_classes_Ord_a.isLess_method p) s, (p IN s), SET_FILTER (
+  dict_Basic_classes_Ord_a.isGreater_method p) s))`;
+
+
+(* ------------------------ *)
+(* subset and proper subset *)
+(* ------------------------ *)
+
+(*val isSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+(*val isProperSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+
+(*val isSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+(*val isProperSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+
+
+(* ------------------------ *)
+(* delete                   *)
+(* ------------------------ *)
+
+(*val delete : forall 'a. SetType 'a, Eq 'a => 'a -> set 'a -> set 'a*)
+(*val deleteBy : forall 'a. SetType 'a => ('a -> 'a -> bool) -> 'a -> set 'a -> set 'a*)
+
+
+(* ------------------------ *)
+(* bigunion                 *)
+(* ------------------------ *)
+
+(*val bigunion : forall 'a. SetType 'a => set (set 'a) -> set 'a*)
+(*val bigunionBy : forall 'a. ('a -> 'a -> ordering) -> set (set 'a) -> set 'a*)
+
+(*let bigunion bs=  {x | forall (s IN bs) (x IN s) | true}*)
+
+(* ------------------------ *)
+(* big intersection         *)
+(* ------------------------ *)
+
+(* Shaked's addition, for which he is now forever responsible as a de facto
+ * Lem maintainer...
+ *)
+(*val bigintersection : forall 'a. SetType 'a => set (set 'a) -> set 'a*)
+val _ = Define `
+ ((bigintersection:('a set)set -> 'a set) bs= 
+  ({x | x | (x IN (BIGUNION bs)) /\ (! (s :: bs). x IN s)}))`;
+
+
+(* ------------------------ *)
+(* difference               *)
+(* ------------------------ *)
+
+(*val differenceBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+(*val difference : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+
+(* ------------------------ *)
+(* intersection             *)
+(* ------------------------ *)
+
+(*val intersection : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+(*val intersectionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+
+
+(* ------------------------ *)
+(* map                      *)
+(* ------------------------ *)
+
+(*val map : forall 'a 'b. SetType 'a, SetType 'b => ('a -> 'b) -> set 'a -> set 'b*) (* before image *)
+(*let map f s=  { f e | forall (e IN s) | true }*)
+
+(*val mapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> 'b) -> set 'a -> set 'b*) 
+
+
+(* ------------------------ *)
+(* bigunionMap              *)
+(* ------------------------ *)
+
+(* In order to avoid providing an comparison function for sets of sets,
+   it might be better to combine bigunion and map sometimes into a single operation. *)
+
+(*val bigunionMap : forall 'a 'b. SetType 'a, SetType 'b => ('a -> set 'b) -> set 'a -> set 'b*)
+(*val bigunionMapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> set 'b) -> set 'a -> set 'b*)
+
+(* ------------------------ *)
+(* mapMaybe and fromMaybe   *)
+(* ------------------------ *)
+
+(* If the mapping function returns Just x, x is added to the result
+   set. If it returns Nothing, no element is added. *)
+
+(*val mapMaybe : forall 'a 'b. SetType 'a, SetType 'b => ('a -> maybe 'b) -> set 'a -> set 'b*)
+val _ = Define `
+ ((setMapMaybe:('a -> 'b option) -> 'a set -> 'b set) f s= 
+   (BIGUNION (IMAGE (\ x .  (case f x of 
+                          SOME y  => {y} 
+                        | NONE => EMPTY
+                        )) s)))`;
+
+
+(*val removeMaybe : forall 'a. SetType 'a => set (maybe 'a) -> set 'a*)
+val _ = Define `
+ ((removeMaybe:('a option)set -> 'a set) s=  (setMapMaybe (\ x .  x) s))`;
+
+
+(* ------------------------ *)
+(* min and max              *)
+(* ------------------------ *)
+
+(*val findMin : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*) 
+(*val findMax : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*)
+
+(* ------------------------ *)
+(* fromList                 *)
+(* ------------------------ *)
+
+(*val fromList : forall 'a.  SetType 'a => list 'a -> set 'a*) (* before from_list *)
+(*val fromListBy : forall 'a.  ('a -> 'a -> ordering) -> list 'a -> set 'a*) 
+
+
+(* ------------------------ *)
+(* Sigma                    *)
+(* ------------------------ *)
+
+(*val sigma : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
+(*val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
+
+(*let sigma sa sb=  { (a, b) | forall (a IN sa) (b IN sb a) | true }*)
+
+
+(* ------------------------ *)
+(* cross product            *)
+(* ------------------------ *)
+
+(*val cross : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> set 'b -> set ('a * 'b)*)
+(*val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> set 'b -> set ('a * 'b)*)
+
+(*let cross s1 s2=  { (e1, e2) | forall (e1 IN s1) (e2 IN s2) | true }*)
+
+
+(* ------------------------ *)
+(* finite                   *)
+(* ------------------------ *)
+
+(*val finite : forall 'a. SetType 'a => set 'a -> bool*)
+
+
+(* ----------------------------*)
+(* fixed point                 *)
+(* --------------------------- *)
+
+(*val leastFixedPoint : forall 'a. SetType 'a 
+  => nat -> (set 'a -> set 'a) -> set 'a -> set 'a*)
+ val leastFixedPoint_defn = Defn.Hol_multi_defns `
+ ((leastFixedPoint:num ->('a set -> 'a set) -> 'a set -> 'a set) 0 f x=  x)
+/\ ((leastFixedPoint:num ->('a set -> 'a set) -> 'a set -> 'a set) ((SUC bound')) f x=  (let fx = (f x) in
+                  if fx SUBSET x then x
+                  else leastFixedPoint bound' f (fx UNION x)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) leastFixedPoint_defn; 
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_set_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_set_extraScript.sml
new file mode 100644
index 0000000..1e51c14
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_set_extraScript.sml
@@ -0,0 +1,118 @@
+(*Generated by Lem from set_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_functionTheory lem_numTheory lem_listTheory lem_sortingTheory lem_setTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_set_extra"
+
+(******************************************************************************)
+(* A library for sets                                                         *)
+(*                                                                            *)
+(* It mainly follows the Haskell Set-library                                  *)
+(******************************************************************************)
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+(*open import Bool Basic_classes Maybe Function Num List Sorting Set*)
+
+
+(* ----------------------------*)
+(* set choose (be careful !)   *)
+(* --------------------------- *)
+
+(*val choose : forall 'a. SetType 'a => set 'a -> 'a*)
+
+(* ------------------------ *)
+(* chooseAndSplit           *)
+(* ------------------------ *)
+(* The idea here is to provide a simple primitive that Lem code can use
+ * to perform its own custom searches within the set -- likely using a
+ * search criterion related to the element ordering, but not necessarily).
+ * For example, sometimes we don't necessarily want to search for a specific
+ * element, but want to search for elements greater than or less than some other.
+ * Someties we'd like to use "split" but don't know a good value to "split" at.
+ * This function lets the set implementation decide that value.
+ *
+ * The contract of chooseAndSplit is simply to select an element nondeterministically
+ * and return that element, together with the subsets of elements less than and
+ * greater than it. In this way, we can recursively traverse the set with any
+ * search criterion, and we avoid baking in the tree representation (although that
+ * is the obvious choice).
+ *)
+(*val chooseAndSplit : forall 'a. SetType 'a, Ord 'a => set 'a -> maybe (set 'a * 'a * set 'a)*)
+val _ = Define `
+ ((chooseAndSplit:'a Ord_class -> 'a set ->('a set#'a#'a set)option)dict_Basic_classes_Ord_a s=
+   (if s = EMPTY then
+    NONE
+  else
+    let element1  = (CHOICE s) in
+    let (lt, gt) = (lem_set$SET_SPLIT 
+  dict_Basic_classes_Ord_a element1 s) in
+      SOME (lt, element1, gt)))`;
+
+
+(* ----------------------------*)
+(* universal set               *)
+(* --------------------------- *)
+
+(*val universal : forall 'a. SetType 'a => set 'a*)
+
+
+(* ----------------------------*)
+(* toList                      *)
+(* --------------------------- *)
+
+(*val toList        : forall 'a. SetType 'a => set 'a -> list 'a*)
+
+
+(* ----------------------------*)
+(* toOrderedList               *)
+(* --------------------------- *)
+
+(* "toOrderedList" returns a sorted list. Therefore the result is (given a suitable order) deterministic.
+   Therefore, it is much preferred to "toList". However, it still is only defined for finite sets. So, please
+   use carefully and consider using set-operations instead of translating sets to lists, performing list manipulations
+   and then transforming back to sets. *)
+
+(*val toOrderedListBy : forall 'a. ('a -> 'a -> bool) -> set 'a -> list 'a*)
+
+(*val toOrderedList : forall 'a. SetType 'a, Ord 'a => set 'a -> list 'a*)
+
+(* ----------------------- *)
+(* compare                 *)
+(* ----------------------- *)
+
+(*val setCompareBy: forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> ordering*)
+val _ = Define `
+ ((setCompareBy:('a -> 'a -> ordering) -> 'a set -> 'a set -> ordering) cmp ss ts=
+   (let ss' = (ARB (\ x y .  cmp x y = LESS) ss) in
+  let ts' = (ARB (\ x y .  cmp x y = LESS) ts) in
+    lexicographic_compare cmp ss' ts'))`;
+
+
+(*val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> ordering*)
+val _ = Define `
+ ((setCompare:'a Ord_class -> 'a set -> 'a set -> ordering)dict_Basic_classes_Ord_a=  (setCompareBy  
+  dict_Basic_classes_Ord_a.compare_method))`;
+
+
+(* ----------------------------*)
+(* unbounded fixed point       *)
+(* --------------------------- *)
+
+(* Is NOT supported by the coq backend! *)
+(*val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a*)
+ val leastFixedPointUnbounded_defn = Hol_defn "leastFixedPointUnbounded" `
+ ((leastFixedPointUnbounded:('a set -> 'a set) -> 'a set -> 'a set) f x=
+    (let fx = (f x) in
+   if fx SUBSET x then x
+   else leastFixedPointUnbounded f (fx UNION x)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn leastFixedPointUnbounded_defn;
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_set_helpersScript.sml b/prover_snapshots/hol4/lib/lem/lem_set_helpersScript.sml
new file mode 100644
index 0000000..5ce9f93
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_set_helpersScript.sml
@@ -0,0 +1,47 @@
+(*Generated by Lem from set_helpers.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_functionTheory lem_numTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_set_helpers"
+
+(******************************************************************************)
+(* Helper functions for sets                                                  *)
+(******************************************************************************)
+
+(* Usually there is a something.lem file containing the main definitions and a 
+   something_extra.lem one containing functions that might cause problems for
+   some backends or are just seldomly used.
+
+   For sets the situation is different. folding is not well defined, since it
+   is only sensibly defined for finite sets and the traversal 
+   order is underspecified. *) 
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+(*open import Bool Basic_classes Maybe Function Num*) 
+
+(*open import {coq} `Coq.Lists.List`*)
+
+(* ------------------------ *)
+(* fold                     *)
+(* ------------------------ *)
+
+(* fold is suspicious, because if given a function, for which
+   the order, in which the arguments are given, matters, its
+   results are undefined. On the other hand, it is very handy to
+   define other - non suspicious functions. 
+
+   Moreover, fold is central for OCaml, since it is used to
+   compile set comprehensions *)
+
+(*val fold : forall 'a 'b. ('a -> 'b -> 'b) -> set 'a -> 'b -> 'b*)
+
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_showScript.sml b/prover_snapshots/hol4/lib/lem/lem_showScript.sml
new file mode 100644
index 0000000..eef2c93
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_showScript.sml
@@ -0,0 +1,85 @@
+(*Generated by Lem from show.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_stringTheory lem_maybeTheory lem_numTheory lem_basic_classesTheory lemTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_show"
+
+
+
+(*open import String Maybe Num Basic_classes*)
+
+(*open import {hol} `lemTheory`*)
+
+val _ = Hol_datatype `
+(*  'a *) Show_class= <|
+  show_method: 'a -> string
+|>`;
+
+
+val _ = Define `
+((instance_Show_Show_string_dict:(string)Show_class)= (<|
+
+  show_method := (\ s.  STRCAT"\""  (STRCAT s "\""))|>))`;
+
+
+(*val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string*)
+val _ = Define `
+ ((stringFromMaybe:('a -> string) -> 'a option -> string) showX (SOME x)=   (STRCAT"Just ("  (STRCAT(showX x) ")")))
+/\ ((stringFromMaybe:('a -> string) -> 'a option -> string) showX NONE=  "Nothing")`;
+
+
+val _ = Define `
+((instance_Show_Show_Maybe_maybe_dict:'a Show_class ->('a option)Show_class)dict_Show_Show_a= (<|
+
+  show_method := (\ x_opt. stringFromMaybe  
+  dict_Show_Show_a.show_method x_opt)|>))`;
+
+
+(*val stringFromListAux : forall 'a. ('a -> string) -> list 'a -> string*)
+ val stringFromListAux_defn = Defn.Hol_multi_defns `
+ ((stringFromListAux:('a -> string) -> 'a list -> string) showX ([])=  "")
+/\ ((stringFromListAux:('a -> string) -> 'a list -> string) showX (x::xs')=
+       ((case xs' of
+        [] => showX x
+      | _ =>  STRCAT(showX x)  (STRCAT"; " (stringFromListAux showX xs'))
+      )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) stringFromListAux_defn;
+
+(*val stringFromList : forall 'a. ('a -> string) -> list 'a -> string*)
+val _ = Define `
+ ((stringFromList:('a -> string) -> 'a list -> string) showX xs= 
+   (STRCAT"["  (STRCAT(stringFromListAux showX xs) "]")))`;
+
+
+val _ = Define `
+((instance_Show_Show_list_dict:'a Show_class ->('a list)Show_class)dict_Show_Show_a= (<|
+
+  show_method := (\ xs. stringFromList  
+  dict_Show_Show_a.show_method xs)|>))`;
+
+
+(*val stringFromPair : forall 'a 'b. ('a -> string) -> ('b -> string) -> ('a * 'b) -> string*)
+val _ = Define `
+ ((stringFromPair:('a -> string) ->('b -> string) -> 'a#'b -> string) showX showY (x,y)= 
+   (STRCAT"("  (STRCAT(showX x)  (STRCAT", "  (STRCAT(showY y) ")")))))`;
+
+
+val _ = Define `
+((instance_Show_Show_tup2_dict:'a Show_class -> 'b Show_class ->('a#'b)Show_class)dict_Show_Show_a dict_Show_Show_b= (<|
+
+  show_method := (stringFromPair  
+  dict_Show_Show_a.show_method  dict_Show_Show_b.show_method)|>))`;
+
+
+val _ = Define `
+((instance_Show_Show_bool_dict:(bool)Show_class)= (<|
+
+  show_method := (\ b. if b then "true" else "false")|>))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_show_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_show_extraScript.sml
new file mode 100644
index 0000000..6be9427
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_show_extraScript.sml
@@ -0,0 +1,67 @@
+(*Generated by Lem from show_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_stringTheory lem_maybeTheory lem_numTheory lem_basic_classesTheory lem_setTheory lem_relationTheory lem_showTheory lem_set_extraTheory lem_string_extraTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_show_extra"
+
+
+
+(*open import String Maybe Num Basic_classes Set Relation Show*) 
+(*import Set_extra String_extra*)
+
+val _ = Define `
+((instance_Show_Show_nat_dict:(num)Show_class)= (<|
+
+  show_method := num_to_dec_string|>))`;
+
+
+val _ = Define `
+((instance_Show_Show_Num_natural_dict:(num)Show_class)= (<|
+
+  show_method := num_to_dec_string|>))`;
+
+
+val _ = Define `
+((instance_Show_Show_Num_int_dict:(int)Show_class)= (<|
+
+  show_method := lem_string_extra$stringFromInt|>))`;
+
+
+val _ = Define `
+((instance_Show_Show_Num_integer_dict:(int)Show_class)= (<|
+
+  show_method := lem_string_extra$stringFromInteger|>))`;
+
+
+val _ = Define `
+ ((stringFromSet:('a -> string) -> 'a set -> string) showX xs= 
+   (STRCAT"{"  (STRCAT(lem_show$stringFromListAux showX (SET_TO_LIST xs)) "}")))`;
+
+
+(* Abbreviates the representation if the relation is transitive. *)
+val _ = Define `
+ ((stringFromRelation:('a#'a -> string) ->('a#'a)set -> string) showX rel=
+   (if transitive rel then
+    let pruned_rel = (withoutTransitiveEdges rel) in
+    if (! (e :: rel). (e IN pruned_rel)) then
+      (* The relations are the same (there are no transitive edges),
+         so we can just as well print the original one. *)
+      stringFromSet showX rel
+    else 
+      STRCAT"trancl of " (stringFromSet showX pruned_rel)
+  else
+    stringFromSet showX rel))`;
+
+
+val _ = Define `
+((instance_Show_Show_set_dict:'a Show_class ->('a set)Show_class)dict_Show_Show_a= (<|
+
+  show_method := (\ xs. stringFromSet  
+  dict_Show_Show_a.show_method xs)|>))`;
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_sortingScript.sml b/prover_snapshots/hol4/lib/lem/lem_sortingScript.sml
new file mode 100644
index 0000000..74d8496
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_sortingScript.sml
@@ -0,0 +1,107 @@
+(*Generated by Lem from sorting.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_listTheory lem_numTheory sortingTheory permLib;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_sorting"
+
+
+
+(*open import Bool Basic_classes Maybe List Num*)
+
+(*open import {isabelle} `HOL-Library.Permutation`*)
+(*open import {coq} `Coq.Lists.List`*)
+(*open import {hol} `sortingTheory` `permLib`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+
+(* ------------------------- *)
+(* permutations              *)
+(* ------------------------- *)
+
+(*val isPermutation : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*val isPermutationBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+
+ val _ = Define `
+ ((PERM_BY:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq ([]) l2=  (NULL l2))
+/\ ((PERM_BY:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq (x :: xs) l2=  ((
+      (case list_delete_first (eq x) l2 of
+          NONE => F
+        | SOME ys => PERM_BY eq xs ys
+      )
+    )))`;
+
+
+
+
+(* ------------------------- *)
+(* isSorted                  *)
+(* ------------------------- *)
+
+(* isSortedBy R l 
+   checks, whether the list l is sorted by ordering R. 
+   R should represent an order, i.e. it should be transitive.
+   Different backends defined "isSorted" slightly differently. However,
+   the definitions coincide for transitive R. Therefore there is the
+   following restriction:
+
+   WARNING: Use isSorted and isSortedBy only with transitive relations!
+*)
+
+(*val isSorted : forall 'a. Ord 'a => list 'a -> bool*)
+(*val isSortedBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> bool*)
+
+(* DPM: rejigged the definition with a nested match to get past Coq's termination checker. *)
+(*let rec isSortedBy cmp l=  match l with
+  | [] -> true
+  | x1 :: xs ->
+    match xs with
+      | [] -> true
+      | x2 :: _ -> (cmp x1 x2 && isSortedBy cmp xs)
+    end
+end*)
+
+
+(* ----------------------- *)
+(* insertion sort          *)
+(* ----------------------- *) 
+
+(*val insert : forall 'a. Ord 'a => 'a -> list 'a -> list 'a*)
+(*val insertBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
+
+(*val insertSort: forall 'a. Ord 'a => list 'a -> list 'a*)
+(*val insertSortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
+
+ val _ = Define `
+ ((INSERT_SORT_INSERT:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list) cmp e ([])=  ([e]))
+/\ ((INSERT_SORT_INSERT:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list) cmp e (x :: xs)=  (if cmp x e then x :: (INSERT_SORT_INSERT cmp e xs) else (e :: (x :: xs))))`;
+
+
+val _ = Define `
+ ((INSERT_SORT:('a -> 'a -> bool) -> 'a list -> 'a list) cmp l=  (FOLDL (\ l e .  INSERT_SORT_INSERT cmp e l) [] l))`;
+
+
+
+(* ----------------------- *)
+(* general sorting         *)
+(* ----------------------- *) 
+
+(*val sort: forall 'a. Ord 'a => list 'a -> list 'a*)
+(*val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
+(*val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*)
+
+(*val predicate_of_ord : forall 'a. ('a -> 'a -> ordering) -> 'a -> 'a -> bool*)
+val _ = Define `
+ ((predicate_of_ord:('a -> 'a -> ordering) -> 'a -> 'a -> bool) f x y=
+   ((case f x y of
+      LESS => T
+    | EQUAL => T
+    | GREATER => F
+  )))`;
+
+
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_stringScript.sml b/prover_snapshots/hol4/lib/lem/lem_stringScript.sml
new file mode 100644
index 0000000..f91a4cb
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_stringScript.sml
@@ -0,0 +1,74 @@
+(*Generated by Lem from string.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_listTheory lemTheory stringTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_string"
+
+
+
+(*open import Bool Basic_classes List*)
+(*open import {ocaml} `Xstring`*)
+(*open import {hol} `lemTheory` `stringTheory`*)
+(*open import {coq} `Coq.Strings.Ascii` `Coq.Strings.String`*)
+
+(* ------------------------------------------- *)
+(* translations between strings and char lists *)
+(* ------------------------------------------- *)
+
+(*val toCharList : string -> list char*)
+
+(*val toString : list char -> string*)
+
+
+(* ----------------------- *)
+(* generating strings      *)
+(* ----------------------- *)
+
+(*val makeString : nat -> char -> string*)
+(*let makeString len c=  toString (replicate len c)*)
+
+(* ----------------------- *)
+(* length                  *)
+(* ----------------------- *)
+
+(*val stringLength : string -> nat*)
+
+(* ----------------------- *)
+(* string concatenation    *)
+(* ----------------------- *)
+
+(*val ^ [stringAppend] : string -> string -> string*)
+
+
+(* ----------------------------*)
+(* setting up pattern matching *)
+(* --------------------------- *)
+
+(*val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a*)
+
+(*let string_case s c_empty c_cons=
+   match (toCharList s) with
+    | [] -> c_empty
+    | c :: cs -> c_cons c (toString cs)
+  end*)
+
+(*val empty_string : string*)
+
+(*val cons_string : char -> string -> string*)
+
+(*val concat : string -> list string -> string*)
+ val concat_defn = Defn.Hol_multi_defns `
+ ((concat:string ->(string)list -> string) sep ([])=  "")
+/\ ((concat:string ->(string)list -> string) sep (s :: ss')=
+       ((case ss' of
+        [] => s
+      | _ =>  STRCAT s  (STRCAT sep (concat sep ss'))
+      )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) concat_defn;
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_string_extraScript.sml b/prover_snapshots/hol4/lib/lem/lem_string_extraScript.sml
new file mode 100644
index 0000000..33f71ab
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_string_extraScript.sml
@@ -0,0 +1,124 @@
+(*Generated by Lem from string_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_numTheory lem_listTheory lem_basic_classesTheory lem_stringTheory lem_list_extraTheory ASCIInumbersTheory stringLib;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_string_extra"
+
+(******************************************************************************)
+(* String functions                                                           *)
+(******************************************************************************)
+
+(*open import Basic_classes*)
+(*open import Num*)
+(*open import List*)
+(*open import String*)
+(*open import List_extra*)
+(*open import {hol} `stringLib`*)
+(*open import {hol} `ASCIInumbersTheory`*)
+
+
+(******************************************************************************)
+(* Character's to numbers                                                     *)
+(******************************************************************************)
+
+(*val ord : char -> nat*)
+
+(*val chr : nat -> char*)
+
+(******************************************************************************)
+(* Converting to strings                                                      *)
+(******************************************************************************)
+
+(*val stringFromNatHelper : nat -> list char -> list char*)
+ val stringFromNatHelper_defn = Hol_defn "stringFromNatHelper" `
+ ((stringFromNatHelper:num ->(char)list ->(char)list) n acc=
+   (if n =( 0 : num) then
+    acc
+  else
+    stringFromNatHelper (n DIV( 10 : num)) (CHR ((n MOD( 10 : num)) +( 48 : num)) :: acc)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNatHelper_defn;
+
+(*val stringFromNat : nat -> string*)
+
+(*val stringFromNaturalHelper : natural -> list char -> list char*)
+ val stringFromNaturalHelper_defn = Hol_defn "stringFromNaturalHelper" `
+ ((stringFromNaturalHelper:num ->(char)list ->(char)list) n acc=
+   (if n =( 0:num) then
+    acc
+  else
+    stringFromNaturalHelper (n DIV( 10:num)) (CHR ((((n MOD( 10:num)) +( 48:num)):num)) :: acc)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNaturalHelper_defn;
+
+(*val stringFromNatural : natural -> string*)
+
+(*val stringFromInt : int -> string*)
+val _ = Define `
+ ((stringFromInt:int -> string) i= 
+   (if i <( 0 : int) then  
+    STRCAT"-" (num_to_dec_string (Num (ABS i)))
+  else
+    num_to_dec_string (Num (ABS i))))`;
+
+
+(*val stringFromInteger : integer -> string*)
+val _ = Define `
+ ((stringFromInteger:int -> string) i= 
+   (if i <( 0 : int) then  
+    STRCAT"-" (num_to_dec_string (Num (ABS i)))
+  else
+    num_to_dec_string (Num (ABS i))))`;
+
+
+
+(******************************************************************************)
+(* List-like operations                                                       *)
+(******************************************************************************)
+
+(*val nth : string -> nat -> char*)
+(*let nth s n=  List_extra.nth (toCharList s) n*)
+
+(*val stringConcat : list string -> string*)
+(*let stringConcat s=
+   List.foldr (^) "" s*)
+
+(******************************************************************************)
+(* String comparison                                                          *)
+(******************************************************************************)
+
+(*val stringCompare : string -> string -> ordering*)
+
+val _ = Define `
+ ((stringLess:string -> string -> bool) x y=  (orderingIsLess (EQUAL)))`;
+
+val _ = Define `
+ ((stringLessEq:string -> string -> bool) x y=  (~ (orderingIsGreater (EQUAL))))`;
+
+val _ = Define `
+ ((stringGreater:string -> string -> bool) x y=  (stringLess y x))`;
+
+val _ = Define `
+ ((stringGreaterEq:string -> string -> bool) x y=  (stringLessEq y x))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_string_dict:(string)Ord_class)= (<|
+
+  compare_method := (\ x y. EQUAL);
+
+  isLess_method := stringLess;
+
+  isLessEqual_method := stringLessEq;
+
+  isGreater_method := stringGreater;
+
+  isGreaterEqual_method := stringGreaterEq|>))`;
+
+ 
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_tupleScript.sml b/prover_snapshots/hol4/lib/lem/lem_tupleScript.sml
new file mode 100644
index 0000000..7ee21f6
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_tupleScript.sml
@@ -0,0 +1,51 @@
+(*Generated by Lem from tuple.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_tuple"
+
+ 
+
+(*open import Bool Basic_classes*)
+
+(* ----------------------- *)
+(* fst                     *)
+(* ----------------------- *)
+
+(*val fst : forall 'a 'b. 'a * 'b -> 'a*)
+(*let fst (v1, v2)=  v1*)
+
+(* ----------------------- *)
+(* snd                     *)
+(* ----------------------- *)
+
+(*val snd : forall 'a 'b. 'a * 'b -> 'b*)
+(*let snd (v1, v2)=  v2*)
+
+
+(* ----------------------- *)
+(* curry                   *)
+(* ----------------------- *)
+
+(*val curry : forall 'a 'b 'c. ('a * 'b -> 'c) -> ('a -> 'b -> 'c)*)
+
+(* ----------------------- *)
+(* uncurry                 *)
+(* ----------------------- *)
+
+(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)
+
+
+(* ----------------------- *)
+(* swap                    *)
+(* ----------------------- *)
+
+(*val swap : forall 'a 'b. ('a * 'b) -> ('b * 'a)*) 
+(*let swap (v1, v2)=  (v2, v1)*)
+
+val _ = export_theory()
+
diff --git a/prover_snapshots/hol4/lib/lem/lem_wordScript.sml b/prover_snapshots/hol4/lib/lem/lem_wordScript.sml
new file mode 100644
index 0000000..552f031
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_wordScript.sml
@@ -0,0 +1,1021 @@
+(*Generated by Lem from word.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_maybeTheory lem_numTheory lem_basic_classesTheory lem_listTheory wordsTheory wordsLib;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_word"
+
+
+
+(*open import Bool Maybe Num Basic_classes List*)
+
+(*open import {isabelle} `HOL-Word.Word`*)
+(*open import {hol} `wordsTheory` `wordsLib`*)
+
+
+(* ========================================================================== *)
+(* Define general purpose word, i.e. sequences of bits of arbitrary length    *)
+(* ========================================================================== *)
+
+val _ = Hol_datatype `
+ bitSequence = BitSeq of 
+    num option  => (* length of the sequence, Nothing means infinite length *)
+   bool => bool       (* sign of the word, used to fill up after concrete value is exhausted *)
+   list`;
+    (* the initial part of the sequence, least significant bit first *)
+
+(*val bitSeqEq : bitSequence -> bitSequence -> bool*)
+
+(*val boolListFrombitSeq : nat -> bitSequence -> list bool*)
+
+ val _ = Define `
+ ((boolListFrombitSeqAux:num -> 'a -> 'a list -> 'a list) n s bl=
+   (if n =( 0 : num) then [] else
+  (case bl of
+      []       => REPLICATE n s
+    | b :: bl' => b :: (boolListFrombitSeqAux (n -( 1 : num)) s bl')
+  )))`;
+
+
+val _ = Define `
+ ((boolListFrombitSeq:num -> bitSequence ->(bool)list) n (BitSeq _ s bl)=  (boolListFrombitSeqAux n s bl))`;
+
+
+
+(*val bitSeqFromBoolList : list bool -> maybe bitSequence*)
+val _ = Define `
+ ((bitSeqFromBoolList:(bool)list ->(bitSequence)option) bl=
+   ((case dest_init bl of
+      NONE => NONE
+    | SOME (bl', s) => SOME (BitSeq (SOME (LENGTH bl)) s bl')
+  )))`;
+
+
+
+(* cleans up the representation of a bitSequence without changing its semantics *)
+(*val cleanBitSeq : bitSequence -> bitSequence*)
+val _ = Define `
+ ((cleanBitSeq:bitSequence -> bitSequence) (BitSeq len s bl)=  ((case len of
+    NONE => (BitSeq len s (REVERSE (dropWhile ((<=>) s) (REVERSE bl))))
+  | SOME n  => (BitSeq len s (REVERSE (dropWhile ((<=>) s) (REVERSE (TAKE (n -( 1 : num)) bl)))))
+)))`;
+
+
+
+(*val bitSeqTestBit : bitSequence -> nat -> maybe bool*)
+val _ = Define `
+ ((bitSeqTestBit:bitSequence -> num ->(bool)option) (BitSeq NONE s bl) pos=  (if pos < LENGTH bl then list_index bl pos else SOME s))
+/\ ((bitSeqTestBit:bitSequence -> num ->(bool)option) (BitSeq(SOME l) s bl) pos=  (if (pos >= l) then NONE else
+                if ((pos = (l -( 1 : num))) \/ (pos >= LENGTH bl)) then SOME s else
+                list_index bl pos))`;
+
+
+(*val bitSeqSetBit : bitSequence -> nat -> bool -> bitSequence*)
+val _ = Define `
+ ((bitSeqSetBit:bitSequence -> num -> bool -> bitSequence) (BitSeq len s bl) pos v=
+   (let bl' = (if (pos < LENGTH bl) then bl else bl ++ REPLICATE pos s) in
+  let bl'' = (LUPDATE v pos bl') in
+  let bs' = (BitSeq len s bl'') in
+  cleanBitSeq bs'))`;
+
+
+
+(*val resizeBitSeq : maybe nat -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((resizeBitSeq:(num)option -> bitSequence -> bitSequence) new_len bs= 
+  ((case cleanBitSeq bs of
+       (BitSeq len s bl) =>
+   let shorten_opt = ((case (new_len, len) of
+                            (NONE, _) => NONE
+                        | (SOME l1, NONE) => SOME l1
+                        | (SOME l1, SOME l2) =>
+                      if (l1 < l2) then SOME l1 else NONE
+                      )) in
+   (case shorten_opt of
+         NONE => BitSeq new_len s bl
+     | SOME l1 => (
+                  let bl' = (TAKE l1 (bl ++ [s])) in
+                  (case dest_init bl' of
+                        NONE => (BitSeq len s bl) (* do nothing if size 0 is requested *)
+                    | SOME (bl'', s') => cleanBitSeq (BitSeq new_len s' bl'')
+                  ))
+   )
+   )))`;
+ 
+
+(*val bitSeqNot : bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqNot:bitSequence -> bitSequence) (BitSeq len s bl)=  (BitSeq len (~ s) (MAP (\ x. ~ x) bl)))`;
+
+
+(*val bitSeqBinop : (bool -> bool -> bool) -> bitSequence -> bitSequence -> bitSequence*)
+
+(*val bitSeqBinopAux : (bool -> bool -> bool) -> bool -> list bool -> bool -> list bool -> list bool*)
+ val _ = Define `
+ ((bitSeqBinopAux:(bool -> bool -> bool) -> bool ->(bool)list -> bool ->(bool)list ->(bool)list) binop s1 ([]) s2 ([])=  ([]))
+/\ ((bitSeqBinopAux:(bool -> bool -> bool) -> bool ->(bool)list -> bool ->(bool)list ->(bool)list) binop s1 (b1 :: bl1') s2 ([])=  ((binop b1 s2) :: bitSeqBinopAux binop s1 bl1' s2 []))
+/\ ((bitSeqBinopAux:(bool -> bool -> bool) -> bool ->(bool)list -> bool ->(bool)list ->(bool)list) binop s1 ([]) s2 (b2 :: bl2')=  ((binop s1 b2) :: bitSeqBinopAux binop s1 []   s2 bl2'))
+/\ ((bitSeqBinopAux:(bool -> bool -> bool) -> bool ->(bool)list -> bool ->(bool)list ->(bool)list) binop s1 (b1 :: bl1') s2 (b2 :: bl2')=  ((binop b1 b2) :: bitSeqBinopAux binop s1 bl1' s2 bl2'))`;
+
+
+val _ = Define `
+ ((bitSeqBinop:(bool -> bool -> bool) -> bitSequence -> bitSequence -> bitSequence) binop bs1 bs2=  ( 
+  (case cleanBitSeq bs1 of
+      (BitSeq len1 s1 bl1) =>
+  (case cleanBitSeq bs2 of
+      (BitSeq len2 s2 bl2) =>
+  let len = ((case (len1, len2) of
+                   (SOME l1, SOME l2) => SOME (MAX l1 l2)
+               | _ => NONE
+             )) in
+  let s = (binop s1 s2) in
+  let bl = (bitSeqBinopAux binop s1 bl1 s2 bl2) in
+  cleanBitSeq (BitSeq len s bl)
+  )
+  )
+))`;
+
+
+val _ = Define `
+ ((bitSeqAnd:bitSequence -> bitSequence -> bitSequence)=  (bitSeqBinop (/\)))`;
+
+val _ = Define `
+ ((bitSeqOr:bitSequence -> bitSequence -> bitSequence)=  (bitSeqBinop (\/)))`;
+
+val _ = Define `
+ ((bitSeqXor:bitSequence -> bitSequence -> bitSequence)=  (bitSeqBinop (\ b1 b2. ~ (b1 <=> b2))))`;
+
+
+(*val bitSeqShiftLeft : bitSequence -> nat -> bitSequence*)
+val _ = Define `
+ ((bitSeqShiftLeft:bitSequence -> num -> bitSequence) (BitSeq len s bl) n=  (cleanBitSeq (BitSeq len s (REPLICATE n F ++ bl))))`;
+
+
+(*val bitSeqArithmeticShiftRight : bitSequence -> nat -> bitSequence*)
+val _ = Define `
+ ((bitSeqArithmeticShiftRight:bitSequence -> num -> bitSequence) bs n= 
+  ((case cleanBitSeq bs of
+       (BitSeq len s bl) =>
+   cleanBitSeq (BitSeq len s (DROP n bl))
+   )))`;
+
+
+(*val bitSeqLogicalShiftRight : bitSequence -> nat -> bitSequence*)
+val _ = Define `
+ ((bitSeqLogicalShiftRight:bitSequence -> num -> bitSequence) bs n= 
+   (if (n =( 0 : num)) then cleanBitSeq bs else  
+  (case cleanBitSeq bs of
+      (BitSeq len s bl) =>
+  (case len of
+        NONE => cleanBitSeq (BitSeq len s (DROP n bl))
+    | SOME l => cleanBitSeq (BitSeq len F ((DROP n bl) ++ REPLICATE l s))
+  )
+  )))`;
+
+
+
+(* integerFromBoolList sign bl creates an integer from a list of bits
+   (least significant bit first) and an explicitly given sign bit.
+   It uses two's complement encoding. *)
+(*val integerFromBoolList : (bool * list bool) -> integer*)
+
+ val _ = Define `
+ ((integerFromBoolListAux:int ->(bool)list -> int) (acc : int) (([]) : bool list)=  acc)
+/\ ((integerFromBoolListAux:int ->(bool)list -> int) (acc : int) ((T :: bl') : bool list)=  (integerFromBoolListAux ((acc *( 2 : int)) +( 1 : int)) bl'))
+/\ ((integerFromBoolListAux:int ->(bool)list -> int) (acc : int) ((F :: bl') : bool list)=  (integerFromBoolListAux (acc *( 2 : int)) bl'))`;
+
+
+val _ = Define `
+ ((integerFromBoolList:bool#(bool)list -> int) (sign, bl)= 
+    (if sign then 
+     ~ (integerFromBoolListAux(( 0 : int)) (REVERSE (MAP (\ x. ~ x) bl)) +( 1 : int))
+   else integerFromBoolListAux(( 0 : int)) (REVERSE bl)))`;
+
+
+(* [boolListFromInteger i] creates a sign bit and a list of booleans from an integer. The len_opt tells it when to stop.*)
+(*val boolListFromInteger :    integer -> bool * list bool*)
+
+ val _ = Define `
+ ((boolListFromNatural:(bool)list -> num ->(bool)list) acc (remainder : num)=
+  (if (remainder >( 0:num)) then 
+   (boolListFromNatural (((remainder MOD( 2:num)) =( 1:num)) :: acc) 
+      (remainder DIV( 2:num)))
+ else
+   REVERSE acc))`;
+
+
+val _ = Define `
+ ((boolListFromInteger:int -> bool#(bool)list) (i : int)= 
+   (if (i <( 0 : int)) then
+    (T, MAP (\ x. ~ x) (boolListFromNatural [] (Num (ABS (~ (i +( 1 : int)))))))
+  else
+    (F, boolListFromNatural [] (Num (ABS i)))))`;
+
+
+
+(* [bitSeqFromInteger len_opt i] encodes [i] as a bitsequence with [len_opt] bits. If there are not enough
+   bits, truncation happens *)
+(*val bitSeqFromInteger : maybe nat -> integer -> bitSequence*)
+val _ = Define `
+ ((bitSeqFromInteger:(num)option -> int -> bitSequence) len_opt i=
+   (let (s, bl) = (boolListFromInteger i) in
+  resizeBitSeq len_opt (BitSeq NONE s bl)))`;
+
+
+
+(*val integerFromBitSeq : bitSequence -> integer*)
+val _ = Define `
+ ((integerFromBitSeq:bitSequence -> int) bs= 
+  ((case cleanBitSeq bs of (BitSeq len s bl) => integerFromBoolList (s, bl) )))`;
+
+
+
+(* Now we can via translation to integers map arithmetic operations to bitSequences *)
+
+(*val bitSeqArithUnaryOp : (integer -> integer) -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqArithUnaryOp:(int -> int) -> bitSequence -> bitSequence) uop bs= 
+  ((case bs of
+       (BitSeq len _ _) =>
+   bitSeqFromInteger len (uop (integerFromBitSeq bs))
+   )))`;
+
+
+(*val bitSeqArithBinOp : (integer -> integer -> integer) -> bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqArithBinOp:(int -> int -> int) -> bitSequence -> bitSequence -> bitSequence) binop bs1 bs2= 
+  ((case bs1 of
+       (BitSeq len1 _ _) =>
+   (case bs2 of
+       (BitSeq len2 _ _) =>
+   let len = ((case (len1, len2) of
+                    (SOME l1, SOME l2) => SOME (MAX l1 l2)
+                | _ => NONE
+              )) in
+   bitSeqFromInteger len
+     (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2))
+   )
+   )))`;
+
+
+(*val bitSeqArithBinTest : forall 'a. (integer -> integer -> 'a) -> bitSequence -> bitSequence -> 'a*)
+val _ = Define `
+ ((bitSeqArithBinTest:(int -> int -> 'a) -> bitSequence -> bitSequence -> 'a) binop bs1 bs2=  (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2)))`;
+
+
+
+(* now instantiate the number interface for bit-sequences *)
+
+(*val bitSeqFromNumeral : numeral -> bitSequence*)
+
+(*val bitSeqLess : bitSequence -> bitSequence -> bool*)
+val _ = Define `
+ ((bitSeqLess:bitSequence -> bitSequence -> bool) bs1 bs2=  (bitSeqArithBinTest (<) bs1 bs2))`;
+
+
+(*val bitSeqLessEqual : bitSequence -> bitSequence -> bool*)
+val _ = Define `
+ ((bitSeqLessEqual:bitSequence -> bitSequence -> bool) bs1 bs2=  (bitSeqArithBinTest (<=) bs1 bs2))`;
+
+
+(*val bitSeqGreater : bitSequence -> bitSequence -> bool*)
+val _ = Define `
+ ((bitSeqGreater:bitSequence -> bitSequence -> bool) bs1 bs2=  (bitSeqArithBinTest (>) bs1 bs2))`;
+
+
+(*val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool*)
+val _ = Define `
+ ((bitSeqGreaterEqual:bitSequence -> bitSequence -> bool) bs1 bs2=  (bitSeqArithBinTest (>=) bs1 bs2))`;
+
+
+(*val bitSeqCompare : bitSequence -> bitSequence -> ordering*)
+val _ = Define `
+ ((bitSeqCompare:bitSequence -> bitSequence -> ordering) bs1 bs2=  (bitSeqArithBinTest (genericCompare (<) (=)) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_Word_bitSequence_dict:(bitSequence)Ord_class)= (<|
+
+  compare_method := bitSeqCompare;
+
+  isLess_method := bitSeqLess;
+
+  isLessEqual_method := bitSeqLessEqual;
+
+  isGreater_method := bitSeqGreater;
+
+  isGreaterEqual_method := bitSeqGreaterEqual|>))`;
+
+
+(* arithmetic negation, don't mix up with bitwise negation *)
+(*val bitSeqNegate : bitSequence -> bitSequence*) 
+val _ = Define `
+ ((bitSeqNegate:bitSequence -> bitSequence) bs=  (bitSeqArithUnaryOp (\ i. ~ i) bs))`;
+
+
+val _ = Define `
+((instance_Num_NumNegate_Word_bitSequence_dict:(bitSequence)NumNegate_class)= (<|
+
+  numNegate_method := bitSeqNegate|>))`;
+
+
+
+(*val bitSeqAdd : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqAdd:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp (+) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Num_NumAdd_Word_bitSequence_dict:(bitSequence)NumAdd_class)= (<|
+
+  numAdd_method := bitSeqAdd|>))`;
+
+
+(*val bitSeqMinus : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqMinus:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp (-) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Num_NumMinus_Word_bitSequence_dict:(bitSequence)NumMinus_class)= (<|
+
+  numMinus_method := bitSeqMinus|>))`;
+
+
+(*val bitSeqSucc : bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqSucc:bitSequence -> bitSequence) bs=  (bitSeqArithUnaryOp (\ n. n +( 1 : int)) bs))`;
+
+
+val _ = Define `
+((instance_Num_NumSucc_Word_bitSequence_dict:(bitSequence)NumSucc_class)= (<|
+
+  succ_method := bitSeqSucc|>))`;
+
+
+(*val bitSeqPred : bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqPred:bitSequence -> bitSequence) bs=  (bitSeqArithUnaryOp (\ n. n -( 1 : int)) bs))`;
+
+
+val _ = Define `
+((instance_Num_NumPred_Word_bitSequence_dict:(bitSequence)NumPred_class)= (<|
+
+  pred_method := bitSeqPred|>))`;
+
+
+(*val bitSeqMult : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqMult:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp ( * ) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Num_NumMult_Word_bitSequence_dict:(bitSequence)NumMult_class)= (<|
+
+  numMult_method := bitSeqMult|>))`;
+
+
+
+(*val bitSeqPow : bitSequence -> nat -> bitSequence*)
+val _ = Define `
+ ((bitSeqPow:bitSequence -> num -> bitSequence) bs n=  (bitSeqArithUnaryOp (\ i .  i ** n) bs))`;
+
+
+val _ = Define `
+((instance_Num_NumPow_Word_bitSequence_dict:(bitSequence)NumPow_class)= (<|
+
+  numPow_method := bitSeqPow|>))`;
+
+
+(*val bitSeqDiv : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqDiv:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp (/) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Num_NumIntegerDivision_Word_bitSequence_dict:(bitSequence)NumIntegerDivision_class)= (<|
+
+  div_method := bitSeqDiv|>))`;
+
+
+val _ = Define `
+((instance_Num_NumDivision_Word_bitSequence_dict:(bitSequence)NumDivision_class)= (<|
+
+  numDivision_method := bitSeqDiv|>))`;
+
+
+(*val bitSeqMod : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqMod:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp (%) bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Num_NumRemainder_Word_bitSequence_dict:(bitSequence)NumRemainder_class)= (<|
+
+  mod_method := bitSeqMod|>))`;
+
+
+(*val bitSeqMin : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqMin:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp int_min bs1 bs2))`;
+
+
+(*val bitSeqMax : bitSequence -> bitSequence -> bitSequence*)
+val _ = Define `
+ ((bitSeqMax:bitSequence -> bitSequence -> bitSequence) bs1 bs2=  (bitSeqArithBinOp int_max bs1 bs2))`;
+
+
+val _ = Define `
+((instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict:(bitSequence)OrdMaxMin_class)= (<|
+
+  max_method := bitSeqMax;
+
+  min_method := bitSeqMin|>))`;
+
+
+
+
+
+(* ========================================================================== *)
+(* Interface for bitoperations                                                *)
+(* ========================================================================== *)
+
+val _ = Hol_datatype `
+(*  'a *) WordNot_class= <|
+  lnot_method : 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) WordAnd_class= <|
+  land_method  : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) WordOr_class= <|
+  lor_method : 'a -> 'a -> 'a
+|>`;
+
+
+
+val _ = Hol_datatype `
+(*  'a *) WordXor_class= <|
+  lxor_method : 'a -> 'a -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) WordLsl_class= <|
+  lsl_method : 'a -> num -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) WordLsr_class= <|
+  lsr_method : 'a -> num -> 'a
+|>`;
+
+
+val _ = Hol_datatype `
+(*  'a *) WordAsr_class= <|
+  asr_method : 'a -> num -> 'a
+|>`;
+
+
+(* ----------------------- *)
+(* bitSequence             *)
+(* ----------------------- *)
+
+val _ = Define `
+((instance_Word_WordNot_Word_bitSequence_dict:(bitSequence)WordNot_class)= (<|
+
+  lnot_method := bitSeqNot|>))`;
+
+
+val _ = Define `
+((instance_Word_WordAnd_Word_bitSequence_dict:(bitSequence)WordAnd_class)= (<|
+
+  land_method := bitSeqAnd|>))`;
+
+
+val _ = Define `
+((instance_Word_WordOr_Word_bitSequence_dict:(bitSequence)WordOr_class)= (<|
+
+  lor_method := bitSeqOr|>))`;
+
+
+val _ = Define `
+((instance_Word_WordXor_Word_bitSequence_dict:(bitSequence)WordXor_class)= (<|
+
+  lxor_method := bitSeqXor|>))`;
+
+
+val _ = Define `
+((instance_Word_WordLsl_Word_bitSequence_dict:(bitSequence)WordLsl_class)= (<|
+
+  lsl_method := bitSeqShiftLeft|>))`;
+
+
+val _ = Define `
+((instance_Word_WordLsr_Word_bitSequence_dict:(bitSequence)WordLsr_class)= (<|
+
+  lsr_method := bitSeqLogicalShiftRight|>))`;
+
+
+val _ = Define `
+((instance_Word_WordAsr_Word_bitSequence_dict:(bitSequence)WordAsr_class)= (<|
+
+  asr_method := bitSeqArithmeticShiftRight|>))`;
+
+
+
+(* ----------------------- *)
+(* int32                   *)
+(* ----------------------- *)
+
+(*val int32Lnot : int32 -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordNot_Num_int32_dict:(word32)WordNot_class)= (<|
+
+  lnot_method := (\ w. (~ w))|>))`;
+
+
+
+(*val int32Lor  : int32 -> int32 -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordOr_Num_int32_dict:(word32)WordOr_class)= (<|
+
+  lor_method := word_or|>))`;
+
+
+(*val int32Lxor : int32 -> int32 -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordXor_Num_int32_dict:(word32)WordXor_class)= (<|
+
+  lxor_method := word_xor|>))`;
+
+
+(*val int32Land : int32 -> int32 -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordAnd_Num_int32_dict:(word32)WordAnd_class)= (<|
+
+  land_method := word_and|>))`;
+
+
+(*val int32Lsl  : int32 -> nat -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordLsl_Num_int32_dict:(word32)WordLsl_class)= (<|
+
+  lsl_method := word_lsl|>))`;
+
+
+(*val int32Lsr  : int32 -> nat -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordLsr_Num_int32_dict:(word32)WordLsr_class)= (<|
+
+  lsr_method := word_lsr|>))`;
+
+
+
+(*val int32Asr  : int32 -> nat -> int32*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordAsr_Num_int32_dict:(word32)WordAsr_class)= (<|
+
+  asr_method := word_asr|>))`;
+
+
+
+(* ----------------------- *)
+(* int64                   *)
+(* ----------------------- *)
+
+(*val int64Lnot : int64 -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordNot_Num_int64_dict:(word64)WordNot_class)= (<|
+
+  lnot_method := (\ w. (~ w))|>))`;
+
+
+(*val int64Lor  : int64 -> int64 -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordOr_Num_int64_dict:(word64)WordOr_class)= (<|
+
+  lor_method := word_or|>))`;
+
+
+(*val int64Lxor : int64 -> int64 -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordXor_Num_int64_dict:(word64)WordXor_class)= (<|
+
+  lxor_method := word_xor|>))`;
+
+
+(*val int64Land : int64 -> int64 -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordAnd_Num_int64_dict:(word64)WordAnd_class)= (<|
+
+  land_method := word_and|>))`;
+
+
+(*val int64Lsl  : int64 -> nat -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordLsl_Num_int64_dict:(word64)WordLsl_class)= (<|
+
+  lsl_method := word_lsl|>))`;
+
+
+(*val int64Lsr  : int64 -> nat -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordLsr_Num_int64_dict:(word64)WordLsr_class)= (<|
+
+  lsr_method := word_lsr|>))`;
+
+
+(*val int64Asr  : int64 -> nat -> int64*) (* XXX: fix *)
+
+val _ = Define `
+((instance_Word_WordAsr_Num_int64_dict:(word64)WordAsr_class)= (<|
+
+  asr_method := word_asr|>))`;
+
+
+
+(* ----------------------- *)
+(* Words via bit sequences *)
+(* ----------------------- *)
+
+(*val defaultLnot : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a*) 
+val _ = Define `
+ ((defaultLnot:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> 'a) fromBitSeq toBitSeq x=  (fromBitSeq (bitSeqNegate (toBitSeq x))))`;
+
+
+(*val defaultLand : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+val _ = Define `
+ ((defaultLand:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> 'a -> 'a) fromBitSeq toBitSeq x1 x2=  (fromBitSeq (bitSeqAnd (toBitSeq x1) (toBitSeq x2))))`;
+
+
+(*val defaultLor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+val _ = Define `
+ ((defaultLor:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> 'a -> 'a) fromBitSeq toBitSeq x1 x2=  (fromBitSeq (bitSeqOr (toBitSeq x1) (toBitSeq x2))))`;
+
+
+(*val defaultLxor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+val _ = Define `
+ ((defaultLxor:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> 'a -> 'a) fromBitSeq toBitSeq x1 x2=  (fromBitSeq (bitSeqXor (toBitSeq x1) (toBitSeq x2))))`;
+
+
+(*val defaultLsl : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+val _ = Define `
+ ((defaultLsl:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> num -> 'a) fromBitSeq toBitSeq x n=  (fromBitSeq (bitSeqShiftLeft (toBitSeq x) n)))`;
+
+
+(*val defaultLsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+val _ = Define `
+ ((defaultLsr:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> num -> 'a) fromBitSeq toBitSeq x n=  (fromBitSeq (bitSeqLogicalShiftRight (toBitSeq x) n)))`;
+
+
+(*val defaultAsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+val _ = Define `
+ ((defaultAsr:(bitSequence -> 'a) ->('a -> bitSequence) -> 'a -> num -> 'a) fromBitSeq toBitSeq x n=  (fromBitSeq (bitSeqArithmeticShiftRight (toBitSeq x) n)))`;
+
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(*val integerLnot : integer -> integer*)
+val _ = Define `
+ ((integerLnot:int -> int) i=  (~ (i +( 1 : int))))`;
+
+
+val _ = Define `
+((instance_Word_WordNot_Num_integer_dict:(int)WordNot_class)= (<|
+
+  lnot_method := integerLnot|>))`;
+
+
+
+(*val integerLor  : integer -> integer -> integer*)
+val _ = Define `
+ ((integerLor:int -> int -> int) i1 i2=  (defaultLor integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordOr_Num_integer_dict:(int)WordOr_class)= (<|
+
+  lor_method := integerLor|>))`;
+
+
+(*val integerLxor : integer -> integer -> integer*)
+val _ = Define `
+ ((integerLxor:int -> int -> int) i1 i2=  (defaultLxor integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordXor_Num_integer_dict:(int)WordXor_class)= (<|
+
+  lxor_method := integerLxor|>))`;
+
+
+(*val integerLand : integer -> integer -> integer*)
+val _ = Define `
+ ((integerLand:int -> int -> int) i1 i2=  (defaultLand integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordAnd_Num_integer_dict:(int)WordAnd_class)= (<|
+
+  land_method := integerLand|>))`;
+
+
+(*val integerLsl  : integer -> nat -> integer*)
+val _ = Define `
+ ((integerLsl:int -> num -> int) i n=  (defaultLsl integerFromBitSeq (bitSeqFromInteger NONE) i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsl_Num_integer_dict:(int)WordLsl_class)= (<|
+
+  lsl_method := integerLsl|>))`;
+
+
+(*val integerAsr  : integer -> nat -> integer*)
+val _ = Define `
+ ((integerAsr:int -> num -> int) i n=  (defaultAsr integerFromBitSeq (bitSeqFromInteger NONE) i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsr_Num_integer_dict:(int)WordLsr_class)= (<|
+
+  lsr_method := integerAsr|>))`;
+
+
+val _ = Define `
+((instance_Word_WordAsr_Num_integer_dict:(int)WordAsr_class)= (<|
+
+  asr_method := integerAsr|>))`;
+
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(* sometimes it is convenient to be able to perform bit-operations on ints.
+   However, since int is not well-defined (it has different size on different systems),
+   it should be used very carefully and only for operations that don't depend on the
+   bitwidth of int *)
+
+(*val intFromBitSeq : bitSequence -> int*)
+val _ = Define `
+ ((intFromBitSeq:bitSequence -> int) bs=  (I (integerFromBitSeq (resizeBitSeq (SOME(( 31 : num))) bs))))`;
+
+
+
+(*val bitSeqFromInt : int -> bitSequence*) 
+val _ = Define `
+ ((bitSeqFromInt:int -> bitSequence) i=  (bitSeqFromInteger (SOME(( 31 : num))) ( i)))`;
+
+
+
+(*val intLnot : int -> int*)
+val _ = Define `
+ ((intLnot:int -> int) i=  (~ (i +( 1 : int))))`;
+
+
+val _ = Define `
+((instance_Word_WordNot_Num_int_dict:(int)WordNot_class)= (<|
+
+  lnot_method := intLnot|>))`;
+
+
+(*val intLor  : int -> int -> int*)
+val _ = Define `
+ ((intLor:int -> int -> int) i1 i2=  (defaultLor intFromBitSeq bitSeqFromInt i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordOr_Num_int_dict:(int)WordOr_class)= (<|
+
+  lor_method := intLor|>))`;
+
+
+(*val intLxor : int -> int -> int*)
+val _ = Define `
+ ((intLxor:int -> int -> int) i1 i2=  (defaultLxor intFromBitSeq bitSeqFromInt i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordXor_Num_int_dict:(int)WordXor_class)= (<|
+
+  lxor_method := intLxor|>))`;
+
+
+(*val intLand : int -> int -> int*)
+val _ = Define `
+ ((intLand:int -> int -> int) i1 i2=  (defaultLand intFromBitSeq bitSeqFromInt i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordAnd_Num_int_dict:(int)WordAnd_class)= (<|
+
+  land_method := intLand|>))`;
+
+
+(*val intLsl  : int -> nat -> int*)
+val _ = Define `
+ ((intLsl:int -> num -> int) i n=  (defaultLsl intFromBitSeq bitSeqFromInt i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsl_Num_int_dict:(int)WordLsl_class)= (<|
+
+  lsl_method := intLsl|>))`;
+
+
+(*val intAsr  : int -> nat -> int*)
+val _ = Define `
+ ((intAsr:int -> num -> int) i n=  (defaultAsr intFromBitSeq bitSeqFromInt i n))`;
+
+
+val _ = Define `
+((instance_Word_WordAsr_Num_int_dict:(int)WordAsr_class)= (<|
+
+  asr_method := intAsr|>))`;
+
+
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(* some operations work also on positive numbers *)
+
+(*val naturalFromBitSeq : bitSequence -> natural*)
+val _ = Define `
+ ((naturalFromBitSeq:bitSequence -> num) bs=  (Num (ABS (integerFromBitSeq bs))))`;
+
+
+(*val bitSeqFromNatural : maybe nat -> natural -> bitSequence*)
+val _ = Define `
+ ((bitSeqFromNatural:(num)option -> num -> bitSequence) len n=  (bitSeqFromInteger len (int_of_num n)))`;
+
+
+(*val naturalLor  : natural -> natural -> natural*)
+val _ = Define `
+ ((naturalLor:num -> num -> num) i1 i2=  (defaultLor naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordOr_Num_natural_dict:(num)WordOr_class)= (<|
+
+  lor_method := naturalLor|>))`;
+
+
+(*val naturalLxor : natural -> natural -> natural*)
+val _ = Define `
+ ((naturalLxor:num -> num -> num) i1 i2=  (defaultLxor naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordXor_Num_natural_dict:(num)WordXor_class)= (<|
+
+  lxor_method := naturalLxor|>))`;
+
+
+(*val naturalLand : natural -> natural -> natural*)
+val _ = Define `
+ ((naturalLand:num -> num -> num) i1 i2=  (defaultLand naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordAnd_Num_natural_dict:(num)WordAnd_class)= (<|
+
+  land_method := naturalLand|>))`;
+
+
+(*val naturalLsl  : natural -> nat -> natural*)
+val _ = Define `
+ ((naturalLsl:num -> num -> num) i n=  (defaultLsl naturalFromBitSeq (bitSeqFromNatural NONE) i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsl_Num_natural_dict:(num)WordLsl_class)= (<|
+
+  lsl_method := naturalLsl|>))`;
+
+
+(*val naturalAsr  : natural -> nat -> natural*)
+val _ = Define `
+ ((naturalAsr:num -> num -> num) i n=  (defaultAsr naturalFromBitSeq (bitSeqFromNatural NONE) i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsr_Num_natural_dict:(num)WordLsr_class)= (<|
+
+  lsr_method := naturalAsr|>))`;
+
+
+val _ = Define `
+((instance_Word_WordAsr_Num_natural_dict:(num)WordAsr_class)= (<|
+
+  asr_method := naturalAsr|>))`;
+
+
+
+(* ----------------------- *)
+(* nat                     *)
+(* ----------------------- *)
+
+(* sometimes it is convenient to be able to perform bit-operations on nats.
+   However, since nat is not well-defined (it has different size on different systems),
+   it should be used very carefully and only for operations that don't depend on the
+   bitwidth of nat *)
+
+(*val natFromBitSeq : bitSequence -> nat*)
+val _ = Define `
+ ((natFromBitSeq:bitSequence -> num) bs=  (((naturalFromBitSeq (resizeBitSeq (SOME(( 31 : num))) bs)):num)))`;
+
+
+
+(*val bitSeqFromNat : nat -> bitSequence*) 
+val _ = Define `
+ ((bitSeqFromNat:num -> bitSequence) i=  (bitSeqFromNatural (SOME(( 31 : num))) (( i:num))))`;
+
+
+
+(*val natLor  : nat -> nat -> nat*)
+val _ = Define `
+ ((natLor:num -> num -> num) i1 i2=  (defaultLor natFromBitSeq bitSeqFromNat i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordOr_nat_dict:(num)WordOr_class)= (<|
+
+  lor_method := natLor|>))`;
+
+
+(*val natLxor : nat -> nat -> nat*)
+val _ = Define `
+ ((natLxor:num -> num -> num) i1 i2=  (defaultLxor natFromBitSeq bitSeqFromNat i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordXor_nat_dict:(num)WordXor_class)= (<|
+
+  lxor_method := natLxor|>))`;
+
+
+(*val natLand : nat -> nat -> nat*)
+val _ = Define `
+ ((natLand:num -> num -> num) i1 i2=  (defaultLand natFromBitSeq bitSeqFromNat i1 i2))`;
+
+
+val _ = Define `
+((instance_Word_WordAnd_nat_dict:(num)WordAnd_class)= (<|
+
+  land_method := natLand|>))`;
+
+
+(*val natLsl  : nat -> nat -> nat*)
+val _ = Define `
+ ((natLsl:num -> num -> num) i n=  (defaultLsl natFromBitSeq bitSeqFromNat i n))`;
+
+
+val _ = Define `
+((instance_Word_WordLsl_nat_dict:(num)WordLsl_class)= (<|
+
+  lsl_method := natLsl|>))`;
+
+
+(*val natAsr  : nat -> nat -> nat*)
+val _ = Define `
+ ((natAsr:num -> num -> num) i n=  (defaultAsr natFromBitSeq bitSeqFromNat i n))`;
+
+
+val _ = Define `
+((instance_Word_WordAsr_nat_dict:(num)WordAsr_class)= (<|
+
+  asr_method := natAsr|>))`;
+
+
+val _ = export_theory()
+