diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lemScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lemScript.sml | 284 |
1 files changed, 284 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lemScript.sml b/snapshots/hol4/lem/hol-lib/lemScript.sml new file mode 100644 index 00000000..d6bb1bc8 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/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() |