From adadda8dfc80d0b7e6a967ceeda98624198800c1 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 10 Jul 2018 14:05:36 +0100 Subject: Update HOL setup --- aarch64/mono/demo/mk.hol | 4 +- lib/hol/Holmakefile | 9 ++- lib/hol/Makefile | 31 +++---- lib/hol/prompt.lem | 18 ----- lib/hol/prompt_monad.lem | 49 ----------- lib/hol/sail2_prompt.lem | 19 +++++ lib/hol/sail2_prompt_monad.lem | 49 +++++++++++ lib/hol/sail2_stateAuxiliaryScript.sml | 61 ++++++++++++++ lib/hol/sail2_valuesAuxiliaryScript.sml | 139 ++++++++++++++++++++++++++++++++ lib/hol/sail_valuesAuxiliaryScript.sml | 139 -------------------------------- lib/hol/stateAuxiliaryScript.sml | 61 -------------- 11 files changed, 293 insertions(+), 286 deletions(-) delete mode 100644 lib/hol/prompt.lem delete mode 100644 lib/hol/prompt_monad.lem create mode 100644 lib/hol/sail2_prompt.lem create mode 100644 lib/hol/sail2_prompt_monad.lem create mode 100644 lib/hol/sail2_stateAuxiliaryScript.sml create mode 100644 lib/hol/sail2_valuesAuxiliaryScript.sml delete mode 100644 lib/hol/sail_valuesAuxiliaryScript.sml delete mode 100644 lib/hol/stateAuxiliaryScript.sml diff --git a/aarch64/mono/demo/mk.hol b/aarch64/mono/demo/mk.hol index cd9f84fc..3aa142a3 100755 --- a/aarch64/mono/demo/mk.hol +++ b/aarch64/mono/demo/mk.hol @@ -5,5 +5,7 @@ set -ex -no_lexp_bounds_check -memo_z3 -undefined_gen \ -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \ -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono -lem -hol -outdir . -lib ../../../lib/hol -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem +# Explicitly include replacement prompt files, as Lem's choice of file depends +# on some internal dependency ordering +lem -hol -outdir . -lib ../../../lib/hol ../../../lib/hol/sail2_prompt_monad.lem ../../../lib/hol/sail2_prompt.lem -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem Holmake diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile index eac4fec8..8e8403f3 100644 --- a/lib/hol/Holmakefile +++ b/lib/hol/Holmakefile @@ -1,11 +1,12 @@ -LEM_SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ - sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ - state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml +LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \ + sail2_stringScript.sml LEM_CLEANS = $(LEM_SCRIPTS) SCRIPTS = $(LEM_SCRIPTS) \ - sail_valuesAuxiliaryScript.sml stateAuxiliaryScript.sml + sail2_valuesAuxiliaryScript.sml sail2_stateAuxiliaryScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) diff --git a/lib/hol/Makefile b/lib/hol/Makefile index 065f887a..783ef23d 100644 --- a/lib/hol/Makefile +++ b/lib/hol/Makefile @@ -1,22 +1,25 @@ LEMSRC = \ - ../../src/lem_interp/sail_instr_kinds.lem \ - ../../src/gen_lib/sail_values.lem \ - ../../src/gen_lib/sail_operators.lem \ - ../../src/gen_lib/sail_operators_mwords.lem \ - ../../src/gen_lib/sail_operators_bitlists.lem \ - ../../src/gen_lib/state_monad.lem \ - ../../src/gen_lib/state.lem \ - prompt_monad.lem \ - prompt.lem + ../../src/lem_interp/sail2_instr_kinds.lem \ + ../../src/gen_lib/sail2_values.lem \ + ../../src/gen_lib/sail2_operators.lem \ + ../../src/gen_lib/sail2_operators_mwords.lem \ + ../../src/gen_lib/sail2_operators_bitlists.lem \ + ../../src/gen_lib/sail2_state_monad.lem \ + ../../src/gen_lib/sail2_state.lem \ + ../../src/gen_lib/sail2_string.lem \ + sail2_prompt_monad.lem \ + sail2_prompt.lem -SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ - sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ - state_monadScript.sml stateScript.sml \ - prompt_monadScript.sml promptScript.sml +SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml \ + sail2_prompt_monadScript.sml sail2_promptScript.sml \ + sail2_stringScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) all: sail-heap $(THYS) +all-scripts: $(SCRIPTS) $(SCRIPTS): $(LEMSRC) lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC) @@ -28,4 +31,4 @@ $(THYS) sail-heap: $(SCRIPTS) clean: Holmake cleanAll -.PHONY: all clean +.PHONY: all all-scripts clean diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem deleted file mode 100644 index 3597fa06..00000000 --- a/lib/hol/prompt.lem +++ /dev/null @@ -1,18 +0,0 @@ -open import Prompt_monad -open import State_monad -open import State - -let inline undefined_bool = undefined_boolS -let inline bool_of_bitU_nondet = bool_of_bitU_nondetS -let inline bool_of_bitU_fail = bool_of_bitU_fail -let inline bools_of_bits_nondet = bools_of_bits_nondetS -let inline of_bits_nondet = of_bits_nondetS -let inline of_bits_fail = of_bits_failS -let inline mword_nondet = mword_nondetS -let inline reg_deref = read_regS - -let inline foreachM = foreachS -let inline whileM = whileS -let inline untilM = untilS -let inline and_boolM = and_boolS -let inline or_boolM = or_boolS diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem deleted file mode 100644 index 8fcd645a..00000000 --- a/lib/hol/prompt_monad.lem +++ /dev/null @@ -1,49 +0,0 @@ -open import Pervasives_extra -open import Sail_instr_kinds -open import Sail_values -open import State_monad - -(* Fake interface of the prompt monad by redirecting to the state monad, since - the former is not currently supported by HOL4 *) - -type monad 'rv 'a 'e = monadS 'rv 'a 'e -type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r - -(* We need to use a target_rep for these because HOL doesn't handle unused - type parameters well. *) - -type base_monad 'regval 'regstate 'a 'e = monad 'regstate 'a 'e -declare hol target_rep type base_monad 'regval 'regstate 'a 'e = `monad` 'regstate 'a 'e -type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regstate 'a 'r 'e -declare hol target_rep type base_monadR 'regval 'regstate 'a 'r 'e = `monadR` 'regstate 'a 'r 'e - -let inline return = returnS -let inline bind = bindS -let inline (>>=) = (>>$=) -let inline (>>) = (>>$) - -let inline exit = exitS - -let inline throw = throwS -let inline try_catch = try_catchS - -let inline catch_early_return = catch_early_returnS -let inline early_return = early_returnS -let inline liftR = liftRS -let inline try_catchR = try_catchRS - -let inline maybe_fail = maybe_failS - -let inline read_mem_bytes = read_mem_bytesS -let inline read_reg = read_regS -let inline reg_deref = read_regS -let inline read_mem = read_memS -let inline read_tag = read_tagS -let inline excl_result = excl_resultS -let inline write_reg = write_regS -let inline write_tag = write_tagS -let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz) -let inline write_mem_val = write_mem_valS -let barrier _ = return () - -let inline assert_exp = assert_expS diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem new file mode 100644 index 00000000..674d4e34 --- /dev/null +++ b/lib/hol/sail2_prompt.lem @@ -0,0 +1,19 @@ +open import Sail2_prompt_monad +open import Sail2_state_monad +open import Sail2_state + +let inline undefined_bool = undefined_boolS +let inline bool_of_bitU_nondet = bool_of_bitU_nondetS +let inline bool_of_bitU_fail = bool_of_bitU_fail +let inline bools_of_bits_nondet = bools_of_bits_nondetS +let inline of_bits_nondet = of_bits_nondetS +let inline of_bits_fail = of_bits_failS +let inline mword_nondet = mword_nondetS +let inline reg_deref = read_regS +let inline internal_pick = internal_pickS + +let inline foreachM = foreachS +let inline whileM = whileS +let inline untilM = untilS +let inline and_boolM = and_boolS +let inline or_boolM = or_boolS diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem new file mode 100644 index 00000000..3af931a5 --- /dev/null +++ b/lib/hol/sail2_prompt_monad.lem @@ -0,0 +1,49 @@ +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_state_monad + +(* Fake interface of the prompt monad by redirecting to the state monad, since + the former is not currently supported by HOL4 *) + +type monad 'rv 'a 'e = monadS 'rv 'a 'e +type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r + +(* We need to use a target_rep for these because HOL doesn't handle unused + type parameters well. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regstate 'a 'e +declare hol target_rep type base_monad 'regval 'regstate 'a 'e = `monad` 'regstate 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regstate 'a 'r 'e +declare hol target_rep type base_monadR 'regval 'regstate 'a 'r 'e = `monadR` 'regstate 'a 'r 'e + +let inline return = returnS +let inline bind = bindS +let inline (>>=) = (>>$=) +let inline (>>) = (>>$) + +let inline exit = exitS + +let inline throw = throwS +let inline try_catch = try_catchS + +let inline catch_early_return = catch_early_returnS +let inline early_return = early_returnS +let inline liftR = liftRS +let inline try_catchR = try_catchRS + +let inline maybe_fail = maybe_failS + +let inline read_mem_bytes = read_mem_bytesS +let inline read_reg = read_regS +let inline reg_deref = read_regS +let inline read_mem = read_memS +let inline read_tag = read_tagS +let inline excl_result = excl_resultS +let inline write_reg = write_regS +let inline write_tag = write_tagS +let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz) +let inline write_mem_val = write_mem_valS +let barrier _ = return () + +let inline assert_exp = assert_expS diff --git a/lib/hol/sail2_stateAuxiliaryScript.sml b/lib/hol/sail2_stateAuxiliaryScript.sml new file mode 100644 index 00000000..4d70b033 --- /dev/null +++ b/lib/hol/sail2_stateAuxiliaryScript.sml @@ -0,0 +1,61 @@ +(*Generated by Lem from ../../src/gen_lib/state.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail2_valuesTheory sail2_state_monadTheory sail2_stateTheory; + +val _ = numLib.prefer_num(); + + + +open lemLib; +(* val _ = lemLib.run_interactive := true; *) +val _ = new_theory "sail2_stateAuxiliary" + + +(****************************************************) +(* *) +(* Termination Proofs *) +(* *) +(****************************************************) + +(* val gst = Defn.tgoal_no_defn (iterS_aux_def, iterS_aux_ind) *) +val (iterS_aux_rw, iterS_aux_ind_rw) = + Defn.tprove_no_defn ((iterS_aux_def, iterS_aux_ind), + WF_REL_TAC`measure (LENGTH o SND o SND)` \\ rw[] + ) +val iterS_aux_rw = save_thm ("iterS_aux_rw", iterS_aux_rw); +val iterS_aux_ind_rw = save_thm ("iterS_aux_ind_rw", iterS_aux_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (foreachS_def, foreachS_ind) *) +val (foreachS_rw, foreachS_ind_rw) = + Defn.tprove_no_defn ((foreachS_def, foreachS_ind), + WF_REL_TAC`measure (LENGTH o FST)` \\ rw[] + ) +val foreachS_rw = save_thm ("foreachS_rw", foreachS_rw); +val foreachS_ind_rw = save_thm ("foreachS_ind_rw", foreachS_ind_rw); + + +(* +These are unprovable. + +(* val gst = Defn.tgoal_no_defn (whileS_def, whileS_ind) *) +val (whileS_rw, whileS_ind_rw) = + Defn.tprove_no_defn ((whileS_def, whileS_ind), + cheat (* the termination proof *) + ) +val whileS_rw = save_thm ("whileS_rw", whileS_rw); +val whileS_ind_rw = save_thm ("whileS_ind_rw", whileS_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (untilS_def, untilS_ind) *) +val (untilS_rw, untilS_ind_rw) = + Defn.tprove_no_defn ((untilS_def, untilS_ind), + cheat (* the termination proof *) + ) +val untilS_rw = save_thm ("untilS_rw", untilS_rw); +val untilS_ind_rw = save_thm ("untilS_ind_rw", untilS_ind_rw); +*) + + +val _ = export_theory() + diff --git a/lib/hol/sail2_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml new file mode 100644 index 00000000..b475c5ea --- /dev/null +++ b/lib/hol/sail2_valuesAuxiliaryScript.sml @@ -0,0 +1,139 @@ +(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory sail2_valuesTheory; +open intLib; + +val _ = numLib.prefer_num(); + + + +open lemLib; +(* val _ = lemLib.run_interactive := true; *) +val _ = new_theory "sail2_valuesAuxiliary" + + +(****************************************************) +(* *) +(* Termination Proofs *) +(* *) +(****************************************************) + +(* val gst = Defn.tgoal_no_defn (shr_int_def, shr_int_ind) *) +val (shr_int_rw, shr_int_ind_rw) = + Defn.tprove_no_defn ((shr_int_def, shr_int_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val shr_int_rw = save_thm ("shr_int_rw", shr_int_rw); +val shr_int_ind_rw = save_thm ("shr_int_ind_rw", shr_int_ind_rw); +val () = computeLib.add_persistent_funs["shr_int_rw"]; + + +(* val gst = Defn.tgoal_no_defn (shl_int_def, shl_int_ind) *) +val (shl_int_rw, shl_int_ind_rw) = + Defn.tprove_no_defn ((shl_int_def, shl_int_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val shl_int_rw = save_thm ("shl_int_rw", shl_int_rw); +val shl_int_ind_rw = save_thm ("shl_int_ind_rw", shl_int_ind_rw); +val () = computeLib.add_persistent_funs["shl_int_rw"]; + + +(* val gst = Defn.tgoal_no_defn (repeat_def, repeat_ind) *) +val (repeat_rw, repeat_ind_rw) = + Defn.tprove_no_defn ((repeat_def, repeat_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val repeat_rw = save_thm ("repeat_rw", repeat_rw); +val repeat_ind_rw = save_thm ("repeat_ind_rw", repeat_ind_rw); +val () = computeLib.add_persistent_funs["repeat_rw"]; + + +(* val gst = Defn.tgoal_no_defn (bools_of_nat_aux_def, bools_of_nat_aux_ind) *) +val (bools_of_nat_aux_rw, bools_of_nat_aux_ind_rw) = + Defn.tprove_no_defn ((bools_of_nat_aux_def, bools_of_nat_aux_ind), + WF_REL_TAC`measure (Num o FST)` \\ COOPER_TAC + ) +val bools_of_nat_aux_rw = save_thm ("bools_of_nat_aux_rw", bools_of_nat_aux_rw); +val bools_of_nat_aux_ind_rw = save_thm ("bools_of_nat_aux_ind_rw", bools_of_nat_aux_ind_rw); +val () = computeLib.add_persistent_funs["bools_of_nat_aux_rw"]; + + +(* val gst = Defn.tgoal_no_defn (pad_list_def, pad_list_ind) *) +val (pad_list_rw, pad_list_ind_rw) = + Defn.tprove_no_defn ((pad_list_def, pad_list_ind), + WF_REL_TAC`measure (Num o SND o SND)` \\ COOPER_TAC + ) +val pad_list_rw = save_thm ("pad_list_rw", pad_list_rw); +val pad_list_ind_rw = save_thm ("pad_list_ind_rw", pad_list_ind_rw); +val () = computeLib.add_persistent_funs["pad_list_rw"]; + + +(* val gst = Defn.tgoal_no_defn (reverse_endianness_list_def, reverse_endianness_list_ind) *) +val (reverse_endianness_list_rw, reverse_endianness_list_ind_rw) = + Defn.tprove_no_defn ((reverse_endianness_list_def, reverse_endianness_list_ind), + WF_REL_TAC`measure LENGTH` \\ rw[drop_list_def,nat_of_int_def] + ) +val reverse_endianness_list_rw = save_thm ("reverse_endianness_list_rw", reverse_endianness_list_rw); +val reverse_endianness_list_ind_rw = save_thm ("reverse_endianness_list_ind_rw", reverse_endianness_list_ind_rw); +val () = computeLib.add_persistent_funs["reverse_endianness_list_rw"]; + + +(* val gst = Defn.tgoal_no_defn (index_list_def, index_list_ind) *) +val (index_list_rw, index_list_ind_rw) = + Defn.tprove_no_defn ((index_list_def, index_list_ind), + WF_REL_TAC`measure (λ(x,y,z). Num(1+(if z > 0 then int_max (-1) (y - x) else int_max (-1) (x - y))))` + \\ rw[integerTheory.INT_MAX] + \\ intLib.COOPER_TAC + ) +val index_list_rw = save_thm ("index_list_rw", index_list_rw); +val index_list_ind_rw = save_thm ("index_list_ind_rw", index_list_ind_rw); +val () = computeLib.add_persistent_funs["index_list_rw"]; + + +(* +(* val gst = Defn.tgoal_no_defn (while_def, while_ind) *) +val (while_rw, while_ind_rw) = + Defn.tprove_no_defn ((while_def, while_ind), + cheat (* the termination proof *) + ) +val while_rw = save_thm ("while_rw", while_rw); +val while_ind_rw = save_thm ("while_ind_rw", while_ind_rw); +*) + + +(* +(* val gst = Defn.tgoal_no_defn (until_def, until_ind) *) +val (until_rw, until_ind_rw) = + Defn.tprove_no_defn ((until_def, until_ind), + cheat (* the termination proof *) + ) +val until_rw = save_thm ("until_rw", until_rw); +val until_ind_rw = save_thm ("until_ind_rw", until_ind_rw); +*) + + +(****************************************************) +(* *) +(* Lemmata *) +(* *) +(****************************************************) + +val just_list_spec = store_thm("just_list_spec", +``((! xs. (just_list xs = NONE) <=> MEM NONE xs) /\ + (! xs es. (just_list xs = SOME es) <=> (xs = MAP SOME es)))``, + (* Theorem: just_list_spec*) + conj_tac + \\ ho_match_mp_tac just_list_ind + \\ Cases \\ rw[] + \\ rw[Once just_list_def] + >- ( CASE_TAC \\ fs[] \\ CASE_TAC ) + >- PROVE_TAC[] + \\ Cases_on`es` \\ fs[] + \\ CASE_TAC \\ fs[] + \\ CASE_TAC \\ fs[] +); + + + +val _ = export_theory() + diff --git a/lib/hol/sail_valuesAuxiliaryScript.sml b/lib/hol/sail_valuesAuxiliaryScript.sml deleted file mode 100644 index aa169979..00000000 --- a/lib/hol/sail_valuesAuxiliaryScript.sml +++ /dev/null @@ -1,139 +0,0 @@ -(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*) -open HolKernel Parse boolLib bossLib; -open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory; -open intLib; - -val _ = numLib.prefer_num(); - - - -open lemLib; -(* val _ = lemLib.run_interactive := true; *) -val _ = new_theory "sail_valuesAuxiliary" - - -(****************************************************) -(* *) -(* Termination Proofs *) -(* *) -(****************************************************) - -(* val gst = Defn.tgoal_no_defn (shr_int_def, shr_int_ind) *) -val (shr_int_rw, shr_int_ind_rw) = - Defn.tprove_no_defn ((shr_int_def, shr_int_ind), - WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC - ) -val shr_int_rw = save_thm ("shr_int_rw", shr_int_rw); -val shr_int_ind_rw = save_thm ("shr_int_ind_rw", shr_int_ind_rw); -val () = computeLib.add_persistent_funs["shr_int_rw"]; - - -(* val gst = Defn.tgoal_no_defn (shl_int_def, shl_int_ind) *) -val (shl_int_rw, shl_int_ind_rw) = - Defn.tprove_no_defn ((shl_int_def, shl_int_ind), - WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC - ) -val shl_int_rw = save_thm ("shl_int_rw", shl_int_rw); -val shl_int_ind_rw = save_thm ("shl_int_ind_rw", shl_int_ind_rw); -val () = computeLib.add_persistent_funs["shl_int_rw"]; - - -(* val gst = Defn.tgoal_no_defn (repeat_def, repeat_ind) *) -val (repeat_rw, repeat_ind_rw) = - Defn.tprove_no_defn ((repeat_def, repeat_ind), - WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC - ) -val repeat_rw = save_thm ("repeat_rw", repeat_rw); -val repeat_ind_rw = save_thm ("repeat_ind_rw", repeat_ind_rw); -val () = computeLib.add_persistent_funs["repeat_rw"]; - - -(* val gst = Defn.tgoal_no_defn (bools_of_nat_aux_def, bools_of_nat_aux_ind) *) -val (bools_of_nat_aux_rw, bools_of_nat_aux_ind_rw) = - Defn.tprove_no_defn ((bools_of_nat_aux_def, bools_of_nat_aux_ind), - WF_REL_TAC`measure (Num o FST)` \\ COOPER_TAC - ) -val bools_of_nat_aux_rw = save_thm ("bools_of_nat_aux_rw", bools_of_nat_aux_rw); -val bools_of_nat_aux_ind_rw = save_thm ("bools_of_nat_aux_ind_rw", bools_of_nat_aux_ind_rw); -val () = computeLib.add_persistent_funs["bools_of_nat_aux_rw"]; - - -(* val gst = Defn.tgoal_no_defn (pad_list_def, pad_list_ind) *) -val (pad_list_rw, pad_list_ind_rw) = - Defn.tprove_no_defn ((pad_list_def, pad_list_ind), - WF_REL_TAC`measure (Num o SND o SND)` \\ COOPER_TAC - ) -val pad_list_rw = save_thm ("pad_list_rw", pad_list_rw); -val pad_list_ind_rw = save_thm ("pad_list_ind_rw", pad_list_ind_rw); -val () = computeLib.add_persistent_funs["pad_list_rw"]; - - -(* val gst = Defn.tgoal_no_defn (reverse_endianness_list_def, reverse_endianness_list_ind) *) -val (reverse_endianness_list_rw, reverse_endianness_list_ind_rw) = - Defn.tprove_no_defn ((reverse_endianness_list_def, reverse_endianness_list_ind), - WF_REL_TAC`measure LENGTH` \\ rw[drop_list_def,nat_of_int_def] - ) -val reverse_endianness_list_rw = save_thm ("reverse_endianness_list_rw", reverse_endianness_list_rw); -val reverse_endianness_list_ind_rw = save_thm ("reverse_endianness_list_ind_rw", reverse_endianness_list_ind_rw); -val () = computeLib.add_persistent_funs["reverse_endianness_list_rw"]; - - -(* val gst = Defn.tgoal_no_defn (index_list_def, index_list_ind) *) -val (index_list_rw, index_list_ind_rw) = - Defn.tprove_no_defn ((index_list_def, index_list_ind), - WF_REL_TAC`measure (λ(x,y,z). Num(1+(if z > 0 then int_max (-1) (y - x) else int_max (-1) (x - y))))` - \\ rw[integerTheory.INT_MAX] - \\ intLib.COOPER_TAC - ) -val index_list_rw = save_thm ("index_list_rw", index_list_rw); -val index_list_ind_rw = save_thm ("index_list_ind_rw", index_list_ind_rw); -val () = computeLib.add_persistent_funs["index_list_rw"]; - - -(* -(* val gst = Defn.tgoal_no_defn (while_def, while_ind) *) -val (while_rw, while_ind_rw) = - Defn.tprove_no_defn ((while_def, while_ind), - cheat (* the termination proof *) - ) -val while_rw = save_thm ("while_rw", while_rw); -val while_ind_rw = save_thm ("while_ind_rw", while_ind_rw); -*) - - -(* -(* val gst = Defn.tgoal_no_defn (until_def, until_ind) *) -val (until_rw, until_ind_rw) = - Defn.tprove_no_defn ((until_def, until_ind), - cheat (* the termination proof *) - ) -val until_rw = save_thm ("until_rw", until_rw); -val until_ind_rw = save_thm ("until_ind_rw", until_ind_rw); -*) - - -(****************************************************) -(* *) -(* Lemmata *) -(* *) -(****************************************************) - -val just_list_spec = store_thm("just_list_spec", -``((! xs. (just_list xs = NONE) <=> MEM NONE xs) /\ - (! xs es. (just_list xs = SOME es) <=> (xs = MAP SOME es)))``, - (* Theorem: just_list_spec*) - conj_tac - \\ ho_match_mp_tac just_list_ind - \\ Cases \\ rw[] - \\ rw[Once just_list_def] - >- ( CASE_TAC \\ fs[] \\ CASE_TAC ) - >- PROVE_TAC[] - \\ Cases_on`es` \\ fs[] - \\ CASE_TAC \\ fs[] - \\ CASE_TAC \\ fs[] -); - - - -val _ = export_theory() - diff --git a/lib/hol/stateAuxiliaryScript.sml b/lib/hol/stateAuxiliaryScript.sml deleted file mode 100644 index c8269750..00000000 --- a/lib/hol/stateAuxiliaryScript.sml +++ /dev/null @@ -1,61 +0,0 @@ -(*Generated by Lem from ../../src/gen_lib/state.lem.*) -open HolKernel Parse boolLib bossLib; -open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory stateTheory; - -val _ = numLib.prefer_num(); - - - -open lemLib; -(* val _ = lemLib.run_interactive := true; *) -val _ = new_theory "stateAuxiliary" - - -(****************************************************) -(* *) -(* Termination Proofs *) -(* *) -(****************************************************) - -(* val gst = Defn.tgoal_no_defn (iterS_aux_def, iterS_aux_ind) *) -val (iterS_aux_rw, iterS_aux_ind_rw) = - Defn.tprove_no_defn ((iterS_aux_def, iterS_aux_ind), - WF_REL_TAC`measure (LENGTH o SND o SND)` \\ rw[] - ) -val iterS_aux_rw = save_thm ("iterS_aux_rw", iterS_aux_rw); -val iterS_aux_ind_rw = save_thm ("iterS_aux_ind_rw", iterS_aux_ind_rw); - - -(* val gst = Defn.tgoal_no_defn (foreachS_def, foreachS_ind) *) -val (foreachS_rw, foreachS_ind_rw) = - Defn.tprove_no_defn ((foreachS_def, foreachS_ind), - WF_REL_TAC`measure (LENGTH o FST)` \\ rw[] - ) -val foreachS_rw = save_thm ("foreachS_rw", foreachS_rw); -val foreachS_ind_rw = save_thm ("foreachS_ind_rw", foreachS_ind_rw); - - -(* -These are unprovable. - -(* val gst = Defn.tgoal_no_defn (whileS_def, whileS_ind) *) -val (whileS_rw, whileS_ind_rw) = - Defn.tprove_no_defn ((whileS_def, whileS_ind), - cheat (* the termination proof *) - ) -val whileS_rw = save_thm ("whileS_rw", whileS_rw); -val whileS_ind_rw = save_thm ("whileS_ind_rw", whileS_ind_rw); - - -(* val gst = Defn.tgoal_no_defn (untilS_def, untilS_ind) *) -val (untilS_rw, untilS_ind_rw) = - Defn.tprove_no_defn ((untilS_def, untilS_ind), - cheat (* the termination proof *) - ) -val untilS_rw = save_thm ("untilS_rw", untilS_rw); -val untilS_ind_rw = save_thm ("untilS_ind_rw", untilS_ind_rw); -*) - - -val _ = export_theory() - -- cgit v1.2.3