diff options
Diffstat (limited to 'prover_snapshots/hol4/lib/lem')
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() + |