From 8f782f6b8ebd26b0c84d781bc1922f3b66149d7b Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Wed, 9 Oct 2024 21:44:38 +0200 Subject: [PATCH] Remove val ... = save_thm( automatically import os import re import sys def match_comment_parens(s, start_idx): if s[start_idx:start_idx + 2] == '(*': paren_count = 0 comment_content = "" for i, char in enumerate(s[start_idx:], start=start_idx): if char == '(' and s[i + 1] == '*': paren_count += 1 elif char == '*' and i + 1 < len(s) and s[i + 1] == ')': paren_count -= 1 comment_content += char if paren_count == 0: comment_content += ")" i += 1 while i + 1 < len(s) and s[i + 1].isspace(): i += 1 comment_content += s[i] return comment_content, i + 1 comment_content += char return None return "", start_idx def transform_definition(s): done_before = 0 pattern = re.compile(r"\nval[ \t]+(?:[a-zA-Z0-9][a-zA-Z0-9_']*|_)\s*=\s*save_thm\s*") match = pattern.search(s, done_before) while match: re_start, re_end = match.span() comment_parens, comment_end = match_comment_parens(s, re_end) if s[comment_end] == '(': paren_count = 0 paren_content = "" for i, char in enumerate(s[comment_end:]): if char == '(': paren_count += 1 elif char == ')': paren_count -= 1 paren_content += char if paren_count == 0: break paren_length = len(paren_content) paren_content = paren_content[1:paren_length-1] match2 = re.search(r"\"\s*(.*)\s*\",\s*(.*)\s*", paren_content, re.DOTALL) if comment_parens == "": replacement = f"\nTheorem {match2.group(1)} =\n {match2.group(2)}" else: replacement = f"\n{comment_parens}\nTheorem {match2.group(1)} =\n {match2.group(2)}" if comment_end + paren_length < len(s) and s[comment_end + paren_length] == ';': s = s[:re_start] + replacement + s[comment_end+paren_length+1:] else: s = s[:re_start] + replacement + s[comment_end+paren_length:] done_before = re_start + len(replacement) else: done_before = comment_end match = pattern.search(s, done_before) return s def process_sml_file(filepath): with open(filepath, 'r') as file: content = file.read() transformed_content = transform_definition(content) with open(filepath, 'w') as file: file.write(transformed_content) def find_and_transform_sml_files(directory): for root, _, files in os.walk(directory): for file in files: if (file.endswith("Script.sml")): filepath = os.path.join(root, file) print(f"Processing file: {filepath}") process_sml_file(filepath) if __name__ == "__main__": if len(sys.argv) != 2: print("Usage: python script.py ") sys.exit(1) directory_to_search = sys.argv[1] if not os.path.isdir(directory_to_search): print(f"Error: {directory_to_search} is not a valid directory.") sys.exit(1) find_and_transform_sml_files(directory_to_search) --- basis/IntProgScript.sml | 8 +- basis/ListProgScript.sml | 3 +- basis/basis_ffiScript.sml | 8 +- basis/pure/mlintScript.sml | 4 +- basis/pure/mllistScript.sml | 4 +- basis/pure/mlstringScript.sml | 6 +- basis/pure/mlvectorScript.sml | 9 +- .../ml_hol_kernel_funsProgScript.sml | 11 +- .../syntax/holSyntaxExtraScript.sml | 66 ++++----- candle/overloading/syntax/holSyntaxScript.sml | 6 +- candle/set-theory/jrhSetScript.sml | 4 +- candle/set-theory/setSpecScript.sml | 5 +- candle/set-theory/zfc/setSpecScript.sml | 5 +- .../ml_hol_kernel_funsProgScript.sml | 8 +- .../semantics/holSemanticsExtraScript.sml | 4 +- .../standard/syntax/holSyntaxExtraScript.sml | 70 +++++----- characteristic/cfDivScript.sml | 8 +- characteristic/cfLetAutoScript.sml | 4 +- characteristic/cfTacticsScript.sml | 8 +- compiler/backend/ag32/ag32_configScript.sml | 4 +- compiler/backend/ag32/ag32_memoryScript.sml | 4 +- .../backend/ag32/proofs/ag32_progScript.sml | 4 +- compiler/backend/arm7/arm7_configScript.sml | 4 +- compiler/backend/arm8/arm8_configScript.sml | 4 +- compiler/backend/backendScript.sml | 4 +- compiler/backend/bvi_tailrecScript.sml | 4 +- compiler/backend/bvl_handleScript.sml | 4 +- compiler/backend/bvl_to_bviScript.sml | 32 ++--- compiler/backend/data_to_wordScript.sml | 127 +++++++++--------- compiler/backend/exportScript.sml | 3 +- compiler/backend/flat_uncheck_ctorsScript.sml | 3 +- compiler/backend/gc/copying_gcScript.sml | 3 +- compiler/backend/gc/gc_sharedScript.sml | 15 ++- compiler/backend/gc/gen_gcScript.sml | 6 +- compiler/backend/gc/gen_gc_partialScript.sml | 12 +- compiler/backend/mips/mips_configScript.sml | 4 +- .../backend/proofs/bvi_letProofScript.sml | 4 +- .../backend/proofs/bvl_constProofScript.sml | 4 +- .../backend/proofs/bvl_handleProofScript.sml | 7 +- .../proofs/clos_annotateProofScript.sml | 8 +- .../backend/proofs/clos_fvsProofScript.sml | 5 +- .../backend/proofs/clos_knownProofScript.sml | 39 +++--- .../backend/proofs/clos_letopProofScript.sml | 5 +- .../backend/proofs/clos_mtiProofScript.sml | 5 +- .../backend/proofs/clos_ticksProofScript.sml | 5 +- .../proofs/data_to_wordProofScript.sml | 4 +- .../proofs/data_to_word_assignProofScript.sml | 9 +- .../proofs/data_to_word_bignumProofScript.sml | 4 +- .../proofs/data_to_word_gcProofScript.sml | 40 +++--- .../proofs/data_to_word_memoryProofScript.sml | 46 +++---- .../backend/proofs/flat_elimProofScript.sml | 4 +- .../proofs/lab_to_targetProofScript.sml | 4 +- .../backend/proofs/word_bignumProofScript.sml | 8 +- .../proofs/word_to_stackProofScript.sml | 4 +- .../backend/reg_alloc/linear_scanScript.sml | 15 ++- .../backend/reg_alloc/reg_allocScript.sml | 15 ++- compiler/backend/riscv/riscv_configScript.sml | 4 +- compiler/backend/semantics/bviPropsScript.sml | 3 +- compiler/backend/semantics/bvlPropsScript.sml | 16 ++- .../backend/semantics/closPropsScript.sml | 80 +++++------ compiler/backend/semantics/closSemScript.sml | 8 +- .../backend/semantics/flatPropsScript.sml | 4 +- compiler/backend/semantics/flatSemScript.sml | 9 +- compiler/backend/stackLangScript.sml | 8 +- compiler/backend/word_bignumScript.sml | 7 +- compiler/backend/x64/x64_configScript.sml | 4 +- .../bootstrap/translation/inferProgScript.sml | 11 +- .../translation/to_bvlProgScript.sml | 4 +- .../translation/to_word32ProgScript.sml | 6 +- .../translation/to_word64ProgScript.sml | 6 +- compiler/encoders/ag32/ag32_targetScript.sml | 6 +- compiler/encoders/arm7/arm7_targetScript.sml | 6 +- compiler/encoders/arm8/arm8_targetScript.sml | 6 +- compiler/encoders/asm/asmPropsScript.sml | 10 +- compiler/encoders/mips/mips_targetScript.sml | 10 +- .../monadic_enc/monadic_enc32Script.sml | 3 +- .../monadic_enc/monadic_enc64Script.sml | 3 +- .../encoders/riscv/riscv_targetScript.sml | 6 +- compiler/encoders/x64/x64_targetScript.sml | 6 +- compiler/inference/inferPropsScript.sml | 6 +- compiler/inference/unifyScript.sml | 6 +- compiler/parsing/cmlPEGScript.sml | 30 ++--- compiler/parsing/ocaml/camlPEGScript.sml | 10 +- .../bot/compile/x64/bot_x64CompileScript.sml | 3 +- examples/catProgScript.sml | 5 +- examples/diffProgScript.sml | 4 +- examples/divScript.sml | 3 +- examples/echoProgScript.sml | 4 +- examples/filterProgScript.sml | 7 +- examples/grepProgScript.sml | 7 +- examples/helloErrProgScript.sml | 4 +- examples/helloProgScript.sml | 4 +- .../compilation/readerIOCompileScript.sml | 4 +- .../opentheory/monadIO/readerIOProgScript.sml | 12 +- .../opentheory/reader_commonProgScript.sml | 4 +- examples/patchProgScript.sml | 8 +- misc/miscScript.sml | 48 ++++--- pancake/parser/panPEGScript.sml | 15 +-- pancake/semantics/crepSemScript.sml | 8 +- pancake/semantics/panSemScript.sml | 8 +- .../proofs/cmlPtreeConversionPropsScript.sml | 14 +- semantics/proofs/gramPropsScript.sml | 9 +- semantics/proofs/primSemEnvScript.sml | 4 +- .../proofs/semanticPrimitivesPropsScript.sml | 6 +- semantics/proofs/typeSysPropsScript.sml | 4 +- translator/ml_progScript.sml | 8 +- translator/ml_translatorScript.sml | 63 ++++----- translator/ml_translator_demoScript.sml | 8 +- .../monadic/examples/doubleArgProgScript.sml | 4 +- .../monadic/examples/helloProgScript.sml | 4 +- .../examples/poly_array_sortProgScript.sml | 3 +- translator/monadic/ml_monadStoreScript.sml | 11 +- .../monadic/ml_monad_translatorScript.sml | 16 +-- .../monadic/monad_base/ml_monadBaseScript.sml | 3 +- .../LazyPairingHeapScript.sml | 6 +- .../auxiliary/ninetyOneScript.sml | 6 +- .../auxiliary/regexpMatchScript.sml | 6 +- translator/std_preludeScript.sml | 3 +- tutorial/wordcountProgScript.sml | 4 +- 119 files changed, 702 insertions(+), 619 deletions(-) diff --git a/basis/IntProgScript.sml b/basis/IntProgScript.sml index 280877edff..81910b708c 100644 --- a/basis/IntProgScript.sml +++ b/basis/IntProgScript.sml @@ -78,8 +78,8 @@ val result = translate padLen_DEC_eq; val result = translate maxSmall_DEC_def; val _ = add_preferred_thy "-"; -val _ = save_thm("fromChars_unsafe_ind", - fromChars_unsafe_ind |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq]); +Theorem fromChars_unsafe_ind = + fromChars_unsafe_ind |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq] val result = translate (fromChars_unsafe_def |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq]); @@ -117,8 +117,8 @@ QED val result = translate fromChar_thm; val result = translate fromChars_range_def; -val _ = save_thm("fromChars_ind", - fromChars_ind |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq]); +Theorem fromChars_ind = + fromChars_ind |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq] val result = translate (fromChars_def |> REWRITE_RULE[maxSmall_DEC_def,padLen_DEC_eq]); diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml index a66e8ae5e0..6d32eee427 100644 --- a/basis/ListProgScript.sml +++ b/basis/ListProgScript.sml @@ -45,7 +45,8 @@ val res = translate flat_rev_def; (* New list-append translation *) val append_v_thm = trans "@" listSyntax.append_tm; -val _ = save_thm("append_v_thm[allow_rebind]",append_v_thm); +Theorem append_v_thm[allow_rebind] = + append_v_thm (* Old list-append translation *) (*val append_v_thm = translate APPEND;*) diff --git a/basis/basis_ffiScript.sml b/basis/basis_ffiScript.sml index f94132f740..449f985353 100644 --- a/basis/basis_ffiScript.sml +++ b/basis/basis_ffiScript.sml @@ -623,16 +623,16 @@ Proof \\ metis_tac[] QED -val basis_ffi_length_thms = save_thm("basis_ffi_length_thms", +Theorem basis_ffi_length_thms = LIST_CONJ [ffi_write_length,ffi_read_length,ffi_open_in_length,ffi_open_out_length, ffi_close_length, clFFITheory.ffi_get_arg_count_length, clFFITheory.ffi_get_arg_length_length, clFFITheory.ffi_get_arg_length, - ffi_exit_length]); + ffi_exit_length] -val basis_ffi_part_defs = save_thm("basis_ffi_part_defs", +Theorem basis_ffi_part_defs = LIST_CONJ - [fs_ffi_part_def,clFFITheory.cl_ffi_part_def,runtime_ffi_part_def]); + [fs_ffi_part_def,clFFITheory.cl_ffi_part_def,runtime_ffi_part_def] (* This is used to show to show one of the parts of parts_ok for the state after a spec *) Theorem oracle_parts: diff --git a/basis/pure/mlintScript.sml b/basis/pure/mlintScript.sml index bbb0a2960e..9c2da7a046 100644 --- a/basis/pure/mlintScript.sml +++ b/basis/pure/mlintScript.sml @@ -380,8 +380,8 @@ Proof \\ metis_tac[fromChars_range_lemma,EVERY_DEF] QED -val fromString_eq_unsafe = save_thm("fromString_eq_unsafe", - fromString_thm |> SIMP_RULE std_ss [GSYM fromString_unsafe_thm]); +Theorem fromString_eq_unsafe = + fromString_thm |> SIMP_RULE std_ss [GSYM fromString_unsafe_thm] Theorem fromString_toString_Num: 0 ≤ n ⇒ fromString (strlit (num_to_dec_string (Num n))) = SOME n diff --git a/basis/pure/mllistScript.sml b/basis/pure/mllistScript.sml index 87ddaf3ea1..873e784010 100644 --- a/basis/pure/mllistScript.sml +++ b/basis/pure/mllistScript.sml @@ -247,8 +247,8 @@ Theorem LENGTH_AUX_THM = Q.prove(` Induct THEN ASM_SIMP_TAC std_ss [LENGTH_AUX_def,LENGTH,ADD1,AC ADD_COMM ADD_ASSOC]) |> Q.SPECL [`xs`,`0`] |> GSYM |> SIMP_RULE std_ss []; -val _ = save_thm("list_compare_def", - ternaryComparisonsTheory.list_compare_def); +Theorem list_compare_def = + ternaryComparisonsTheory.list_compare_def (* tail-recursive MAP *) diff --git a/basis/pure/mlstringScript.sml b/basis/pure/mlstringScript.sml index f2006b28c1..e9539784f6 100644 --- a/basis/pure/mlstringScript.sml +++ b/basis/pure/mlstringScript.sml @@ -483,11 +483,11 @@ Theorem TOKENS_eq_tokens_sym \\ simp[MAP_MAP_o,INJ_DEF,explode_11,o_DEF,explode_implode,TOKENS_eq_tokens] *) -val TOKENS_eq_tokens_sym = save_thm("TOKENS_eq_tokens_sym", - TOKENS_eq_tokens +Theorem TOKENS_eq_tokens_sym = + TOKENS_eq_tokens |> SPEC_ALL |> Q.AP_TERM`MAP implode` - |> SIMP_RULE(srw_ss())[MAP_MAP_o,implode_explode,o_DEF]); + |> SIMP_RULE(srw_ss())[MAP_MAP_o,implode_explode,o_DEF] Theorem tokens_append: diff --git a/basis/pure/mlvectorScript.sml b/basis/pure/mlvectorScript.sml index 29a24e8ba6..0e9fba2e57 100644 --- a/basis/pure/mlvectorScript.sml +++ b/basis/pure/mlvectorScript.sml @@ -8,11 +8,14 @@ val _ = new_theory"mlvector" val _ = set_grammar_ancestry ["mllist", "regexp_compiler"] -val vector_nchotomy = save_thm("vector_nchotomy",regexp_compilerTheory.vector_nchotomy); +Theorem vector_nchotomy = + regexp_compilerTheory.vector_nchotomy -val sub_def = save_thm("sub_def",regexp_compilerTheory.sub_def); +Theorem sub_def = + regexp_compilerTheory.sub_def -val length_def = save_thm("length_def",regexp_compilerTheory.length_def); +Theorem length_def = + regexp_compilerTheory.length_def Definition tabulate_def: tabulate n f = Vector (GENLIST f n) diff --git a/candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml b/candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml index c7aed6ccfa..0ef9602761 100644 --- a/candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml +++ b/candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml @@ -347,8 +347,8 @@ val type_cmp_thm = Q.prove( |> CONJUNCT1; val _ = add_preferred_thy "-"; -val _ = save_thm("type_cmp_ind", - (fetch "-" "type_compare_ind") |> RW [GSYM type_cmp_thm]); +Theorem type_cmp_ind = + (fetch "-" "type_compare_ind") |> RW [GSYM type_cmp_thm] val res = translate (type_compare_def |> RW [GSYM type_cmp_thm]); Definition term_compare_def: @@ -401,8 +401,8 @@ Proof QED val _ = add_preferred_thy "-"; -val _ = save_thm("term_cmp_ind", - (fetch "-" "term_compare_ind") |> RW [GSYM term_cmp_thm]); +Theorem term_cmp_ind = + (fetch "-" "term_compare_ind") |> RW [GSYM term_cmp_thm] val res = translate (term_compare_def |> RW [GSYM term_cmp_thm]); val res = translate (check [‘ty’] holKernelPmatchTheory.codomain_def); @@ -458,7 +458,8 @@ val _ = ml_prog_update open_local_block; val fdM_def = new_definition("fdM_def",``fdM = first_dup``) val fdM_intro = SYM fdM_def -val fdM_ind = save_thm("fdM_ind",REWRITE_RULE[MEMBER_INTRO]first_dup_ind) +Theorem fdM_ind = + REWRITE_RULE[MEMBER_INTRO]first_dup_ind val fdM_eqs = REWRITE_RULE[MEMBER_INTRO,fdM_intro]first_dup_def val def = fdM_eqs |> translate val def = REWRITE_RULE[fdM_intro]add_constants_def |> m_translate diff --git a/candle/overloading/syntax/holSyntaxExtraScript.sml b/candle/overloading/syntax/holSyntaxExtraScript.sml index 3c07856c05..baf49697fb 100644 --- a/candle/overloading/syntax/holSyntaxExtraScript.sml +++ b/candle/overloading/syntax/holSyntaxExtraScript.sml @@ -701,15 +701,15 @@ End val _ = Parse.add_infix("subtype",401,Parse.NONASSOC) Overload subtype =``RTC subtype1`` -val subtype_Tyvar = save_thm("subtype_Tyvar", +Theorem subtype_Tyvar = ``ty subtype (Tyvar x)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subtype1_cases]) + [Once relationTheory.RTC_CASES2,subtype1_cases] val _ = export_rewrites["subtype_Tyvar"] -val subtype_Tyapp = save_thm("subtype_Tyapp", +Theorem subtype_Tyapp = ``ty subtype (Tyapp name args)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subtype1_cases]) + [Once relationTheory.RTC_CASES2,subtype1_cases] Theorem subtype_trans: !x y z. x subtype y /\ y subtype z ==> x subtype z @@ -869,25 +869,25 @@ End val _ = Parse.add_infix("subterm",401,Parse.NONASSOC) Overload subterm = ``RTC subterm1`` -val subterm_Var = save_thm("subterm_Var", +Theorem subterm_Var = ``tm subterm (Var x ty)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) -val subterm_Const = save_thm("subterm_Const", + [Once relationTheory.RTC_CASES2,subterm1_cases] +Theorem subterm_Const = ``tm subterm (Const x ty)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) + [Once relationTheory.RTC_CASES2,subterm1_cases] val _ = export_rewrites["subterm_Var","subterm_Const"] -val subterm_Comb = save_thm("subterm_Comb", +Theorem subterm_Comb = ``tm subterm (Comb t1 t2)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) -val subterm_Abs = save_thm("subterm_Abs", + [Once relationTheory.RTC_CASES2,subterm1_cases] +Theorem subterm_Abs = ``tm subterm (Abs v t)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) + [Once relationTheory.RTC_CASES2,subterm1_cases] -val subterm_welltyped = save_thm("subterm_welltyped", +Theorem subterm_welltyped = let val th = Q.prove(`∀tm ty. tm has_type ty ⇒ ∀t. t subterm tm ⇒ welltyped t`, ho_match_mp_tac has_type_strongind >> @@ -895,7 +895,7 @@ val subterm_welltyped = save_thm("subterm_welltyped", rw[] >> imp_res_tac WELLTYPED_LEMMA >> simp[]) in METIS_PROVE[th,welltyped_def] ``∀t tm. welltyped tm ∧ t subterm tm ⇒ welltyped t`` - end) + end (* term ordering *) @@ -1598,13 +1598,13 @@ Proof transitive_alpha_lt, antisymmetric_alpha_lt] QED -val hypset_ok_append = save_thm("hypset_ok_append", +Theorem hypset_ok_append = Q.ISPEC`alpha_lt` sortingTheory.SORTED_APPEND_GEN - |> REWRITE_RULE[GSYM hypset_ok_def]) + |> REWRITE_RULE[GSYM hypset_ok_def] -val hypset_ok_el_less = save_thm("hypset_ok_el_less", +Theorem hypset_ok_el_less = MATCH_MP sortingTheory.SORTED_EL_LESS transitive_alpha_lt - |> REWRITE_RULE[GSYM hypset_ok_def]) + |> REWRITE_RULE[GSYM hypset_ok_def] (* term_union lemmas *) @@ -3484,7 +3484,8 @@ End val variant_ind = fetch "-" "variant_ind" -val variant_vsubst_thm = save_thm("variant_vsubst_thm",prove( +Theorem variant_vsubst_thm = + prove( ``!xs v x name. (xs = [x]) /\ (v = (Var name ty)) ==> (variant xs (Var name ty) = @@ -3518,10 +3519,10 @@ val variant_vsubst_thm = save_thm("variant_vsubst_thm",prove( \\ `VARIANT_PRIMES x (STRCAT (explode name) "'") ty < n \/ n < VARIANT_PRIMES x (STRCAT (explode name) "'") ty` by DECIDE_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) - |> SIMP_RULE std_ss [] |> SPEC_ALL); + |> SIMP_RULE std_ss [] |> SPEC_ALL -val VSUBST_thm = save_thm("VSUBST_thm", - REWRITE_RULE[SYM variant_vsubst_thm] VSUBST_def) +Theorem VSUBST_thm = + REWRITE_RULE[SYM variant_vsubst_thm] VSUBST_def Definition subtract_def: subtract l1 l2 = FILTER (\t. ~(MEM t l2)) l1 @@ -3577,7 +3578,8 @@ Proof \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ METIS_TAC [] QED -val variant_inst_thm = save_thm("variant_inst_thm",prove( +Theorem variant_inst_thm = + prove( ``!xs v x name a. welltyped a ∧ (xs = frees a) /\ @@ -3624,7 +3626,7 @@ val variant_inst_thm = save_thm("variant_inst_thm",prove( \\ REPEAT STRIP_TAC \\ `k < n \/ n < k` by DECIDE_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) - |> SIMP_RULE std_ss [] |> SPEC_ALL); + |> SIMP_RULE std_ss [] |> SPEC_ALL Theorem INST_CORE_Abs_thm: ∀v t env tyin. welltyped (Abs v t) ⇒ @@ -3734,16 +3736,16 @@ QED (* some derived rules *) val assume = proves_rules |> CONJUNCTS |> el 2 -val deductAntisym_equation = save_thm("deductAntisym_equation", - proves_rules |> CONJUNCTS |> el 4) -val eqMp_equation = save_thm("eqMp_equation", +Theorem deductAntisym_equation = + proves_rules |> CONJUNCTS |> el 4 +Theorem eqMp_equation = proves_rules |> CONJUNCTS |> el 5 - |> REWRITE_RULE[GSYM AND_IMP_INTRO]) -val refl_equation = save_thm("refl_equation", - proves_rules |> CONJUNCTS |> el 9) -val appThm_equation = save_thm("appThm_equation", + |> REWRITE_RULE[GSYM AND_IMP_INTRO] +Theorem refl_equation = + proves_rules |> CONJUNCTS |> el 9 +Theorem appThm_equation = proves_rules |> CONJUNCTS |> el 8 - |> REWRITE_RULE[GSYM AND_IMP_INTRO]) + |> REWRITE_RULE[GSYM AND_IMP_INTRO] Theorem addAssum: ∀thy h c a. (thy,h) |- c ∧ term_ok (sigof thy) a ∧ (a has_type Bool) ⇒ diff --git a/candle/overloading/syntax/holSyntaxScript.sml b/candle/overloading/syntax/holSyntaxScript.sml index 6b13bfec14..811a0df7c5 100644 --- a/candle/overloading/syntax/holSyntaxScript.sml +++ b/candle/overloading/syntax/holSyntaxScript.sml @@ -36,8 +36,10 @@ Proof REPEAT STRIP_TAC \\ EVAL_TAC QED -val _ = save_thm("domain_raw[allow_rebind]",domain_raw); -val _ = save_thm("codomain_raw[allow_rebind]",codomain_raw); +Theorem domain_raw[allow_rebind] = + domain_raw +Theorem codomain_raw[allow_rebind] = + codomain_raw fun type_rec_tac proj = (WF_REL_TAC(`measure (type_size o `@[QUOTE proj]@`)`) >> simp[] >> diff --git a/candle/set-theory/jrhSetScript.sml b/candle/set-theory/jrhSetScript.sml index 1fc996e73d..f324da0a3a 100644 --- a/candle/set-theory/jrhSetScript.sml +++ b/candle/set-theory/jrhSetScript.sml @@ -764,7 +764,7 @@ Proof fs[inset_def] QED -val inset_ind = - save_thm("inset_ind",MATCH_MP WF_INDUCTION_THM WF_inset) +Theorem inset_ind = + MATCH_MP WF_INDUCTION_THM WF_inset val _ = export_theory() diff --git a/candle/set-theory/setSpecScript.sml b/candle/set-theory/setSpecScript.sml index f886ec8bcb..c1eea4aad9 100644 --- a/candle/set-theory/setSpecScript.sml +++ b/candle/set-theory/setSpecScript.sml @@ -446,7 +446,8 @@ Proof metis_tac[pair_inj] QED -val axiom_of_choice = save_thm("axiom_of_choice",UNDISCH(prove( +Theorem axiom_of_choice = + UNDISCH(prove( ``is_set_theory ^mem ⇒ ∀x. (∀a. mem a x ⇒ ∃b. mem b a) ⇒ ∃f. ∀a. mem a x ⇒ mem (f ' a) a``, @@ -460,7 +461,7 @@ val axiom_of_choice = save_thm("axiom_of_choice",UNDISCH(prove( match_mp_tac apply_abstract_matchable >> rw[mem_union] >> SELECT_ELIM_TAC >> rw[] >> - metis_tac[]))) + metis_tac[])) val indset = ``indset:'U`` val ch = ``ch:'U->'U`` diff --git a/candle/set-theory/zfc/setSpecScript.sml b/candle/set-theory/zfc/setSpecScript.sml index 72f0c5754d..f160515547 100644 --- a/candle/set-theory/zfc/setSpecScript.sml +++ b/candle/set-theory/zfc/setSpecScript.sml @@ -872,7 +872,8 @@ Proof rw[dep_prodspace_def,mem_sub] QED -val axiom_of_choice = save_thm("axiom_of_choice",UNDISCH(prove( +Theorem axiom_of_choice = + UNDISCH(prove( ``is_set_theory ^mem ⇒ ∀x. (∀a. mem a x ⇒ ∃b. mem b a) ⇒ ∃f. ∀a. mem a x ⇒ mem (f ' a) a``, @@ -886,7 +887,7 @@ val axiom_of_choice = save_thm("axiom_of_choice",UNDISCH(prove( match_mp_tac apply_abstract_matchable >> rw[mem_union] >> SELECT_ELIM_TAC >> rw[] >> - metis_tac[]))) + metis_tac[])) val indset = ``indset:'U`` val ch = ``ch:'U->'U`` diff --git a/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml b/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml index 4cecfc1fa9..e9099d0b4f 100644 --- a/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml +++ b/candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml @@ -302,8 +302,8 @@ val type_cmp_thm = Q.prove( |> CONJUNCT1; val _ = add_preferred_thy "-"; -val _ = save_thm("type_cmp_ind", - (fetch "-" "type_compare_ind") |> RW [GSYM type_cmp_thm]); +Theorem type_cmp_ind = + (fetch "-" "type_compare_ind") |> RW [GSYM type_cmp_thm] val res = translate (type_compare_def |> RW [GSYM type_cmp_thm]); Definition term_compare_def: @@ -356,8 +356,8 @@ Proof QED val _ = add_preferred_thy "-"; -val _ = save_thm("term_cmp_ind", - (fetch "-" "term_compare_ind") |> RW [GSYM term_cmp_thm]); +Theorem term_cmp_ind = + (fetch "-" "term_compare_ind") |> RW [GSYM term_cmp_thm] val res = translate (term_compare_def |> RW [GSYM term_cmp_thm]); val res = translate (check [‘ty’] holKernelPmatchTheory.codomain_def); diff --git a/candle/standard/semantics/holSemanticsExtraScript.sml b/candle/standard/semantics/holSemanticsExtraScript.sml index b01f45b5b0..4545ca67f1 100644 --- a/candle/standard/semantics/holSemanticsExtraScript.sml +++ b/candle/standard/semantics/holSemanticsExtraScript.sml @@ -775,9 +775,9 @@ QED (* special cases of interprets *) val rwt = MATCH_MP (PROVE[]``P x ⇒ ((∀x. P x ⇒ Q) ⇔ Q)``) is_type_valuation_exists -val interprets_nil = save_thm("interprets_nil", +Theorem interprets_nil = interprets_def |> SPEC_ALL |> Q.GEN`vs` |> Q.SPEC`[]` - |> SIMP_RULE (std_ss++listSimps.LIST_ss) [rwt] |> GEN_ALL) + |> SIMP_RULE (std_ss++listSimps.LIST_ss) [rwt] |> GEN_ALL Theorem interprets_one: i interprets name on [v] as f ⇔ diff --git a/candle/standard/syntax/holSyntaxExtraScript.sml b/candle/standard/syntax/holSyntaxExtraScript.sml index 9d520a16fc..b61b86b6cd 100644 --- a/candle/standard/syntax/holSyntaxExtraScript.sml +++ b/candle/standard/syntax/holSyntaxExtraScript.sml @@ -14,14 +14,14 @@ val _ = set_trace "BasicProvers.var_eq_old" 1 val cpn_distinct = TypeBase.distinct_of ``:ordering`` val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering`` -val type_ind = save_thm("type_ind", +Theorem type_ind = TypeBase.induction_of``:holSyntax$type`` |> Q.SPECL[`P`,`EVERY P`] |> SIMP_RULE std_ss [EVERY_DEF] |> UNDISCH_ALL |> CONJUNCT1 |> DISCH_ALL - |> Q.GEN`P`) + |> Q.GEN`P` Theorem type1_size_append: ∀l1 l2. type1_size (l1 ++ l2) = type1_size l1 + type1_size l2 @@ -265,15 +265,15 @@ End val _ = Parse.add_infix("subtype",401,Parse.NONASSOC) Overload subtype =``RTC subtype1`` -val subtype_Tyvar = save_thm("subtype_Tyvar", +Theorem subtype_Tyvar = ``ty subtype (Tyvar x)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subtype1_cases]) + [Once relationTheory.RTC_CASES2,subtype1_cases] val _ = export_rewrites["subtype_Tyvar"] -val subtype_Tyapp = save_thm("subtype_Tyapp", +Theorem subtype_Tyapp = ``ty subtype (Tyapp name args)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subtype1_cases]) + [Once relationTheory.RTC_CASES2,subtype1_cases] Theorem subtype_type_ok: ∀tysig ty1 ty2. type_ok tysig ty2 ∧ ty1 subtype ty2 ⇒ type_ok tysig ty1 @@ -302,25 +302,25 @@ End val _ = Parse.add_infix("subterm",401,Parse.NONASSOC) Overload subterm = ``RTC subterm1`` -val subterm_Var = save_thm("subterm_Var", +Theorem subterm_Var = ``tm subterm (Var x ty)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) -val subterm_Const = save_thm("subterm_Const", + [Once relationTheory.RTC_CASES2,subterm1_cases] +Theorem subterm_Const = ``tm subterm (Const x ty)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) + [Once relationTheory.RTC_CASES2,subterm1_cases] val _ = export_rewrites["subterm_Var","subterm_Const"] -val subterm_Comb = save_thm("subterm_Comb", +Theorem subterm_Comb = ``tm subterm (Comb t1 t2)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) -val subterm_Abs = save_thm("subterm_Abs", + [Once relationTheory.RTC_CASES2,subterm1_cases] +Theorem subterm_Abs = ``tm subterm (Abs v t)`` |> SIMP_CONV(srw_ss()++boolSimps.DNF_ss) - [Once relationTheory.RTC_CASES2,subterm1_cases]) + [Once relationTheory.RTC_CASES2,subterm1_cases] -val subterm_welltyped = save_thm("subterm_welltyped", +Theorem subterm_welltyped = let val th = Q.prove(`∀tm ty. tm has_type ty ⇒ ∀t. t subterm tm ⇒ welltyped t`, ho_match_mp_tac has_type_strongind >> @@ -328,7 +328,7 @@ val subterm_welltyped = save_thm("subterm_welltyped", rw[] >> imp_res_tac WELLTYPED_LEMMA >> simp[]) in METIS_PROVE[th,welltyped_def] ``∀t tm. welltyped tm ∧ t subterm tm ⇒ welltyped t`` - end) + end (* term ordering *) @@ -1031,13 +1031,13 @@ Proof transitive_alpha_lt, antisymmetric_alpha_lt] QED -val hypset_ok_append = save_thm("hypset_ok_append", +Theorem hypset_ok_append = Q.ISPEC`alpha_lt` sortingTheory.SORTED_APPEND_GEN - |> REWRITE_RULE[GSYM hypset_ok_def]) + |> REWRITE_RULE[GSYM hypset_ok_def] -val hypset_ok_el_less = save_thm("hypset_ok_el_less", +Theorem hypset_ok_el_less = MATCH_MP sortingTheory.SORTED_EL_LESS transitive_alpha_lt - |> REWRITE_RULE[GSYM hypset_ok_def]) + |> REWRITE_RULE[GSYM hypset_ok_def] (* term_union lemmas *) @@ -2874,7 +2874,8 @@ End val variant_ind = fetch "-" "variant_ind" -val variant_vsubst_thm = save_thm("variant_vsubst_thm",prove( +Theorem variant_vsubst_thm = + prove( ``!xs v x name. (xs = [x]) /\ (v = (Var name ty)) ==> (variant xs (Var name ty) = @@ -2908,10 +2909,10 @@ val variant_vsubst_thm = save_thm("variant_vsubst_thm",prove( \\ `VARIANT_PRIMES x (STRCAT (explode name) "'") ty < n \/ n < VARIANT_PRIMES x (STRCAT (explode name) "'") ty` by DECIDE_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) - |> SIMP_RULE std_ss [] |> SPEC_ALL); + |> SIMP_RULE std_ss [] |> SPEC_ALL -val VSUBST_thm = save_thm("VSUBST_thm", - REWRITE_RULE[SYM variant_vsubst_thm] VSUBST_def) +Theorem VSUBST_thm = + REWRITE_RULE[SYM variant_vsubst_thm] VSUBST_def Definition subtract_def: subtract l1 l2 = FILTER (\t. ~(MEM t l2)) l1 @@ -2967,7 +2968,8 @@ Proof \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ METIS_TAC [] QED -val variant_inst_thm = save_thm("variant_inst_thm",prove( +Theorem variant_inst_thm = + prove( ``!xs v x name a. welltyped a ∧ (xs = frees a) /\ @@ -3014,7 +3016,7 @@ val variant_inst_thm = save_thm("variant_inst_thm",prove( \\ REPEAT STRIP_TAC \\ `k < n \/ n < k` by DECIDE_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) - |> SIMP_RULE std_ss [] |> SPEC_ALL); + |> SIMP_RULE std_ss [] |> SPEC_ALL Theorem INST_CORE_Abs_thm: ∀v t env tyin. welltyped (Abs v t) ⇒ @@ -3124,16 +3126,16 @@ QED (* some derived rules *) val assume = proves_rules |> CONJUNCTS |> el 2 -val deductAntisym_equation = save_thm("deductAntisym_equation", - proves_rules |> CONJUNCTS |> el 4) -val eqMp_equation = save_thm("eqMp_equation", +Theorem deductAntisym_equation = + proves_rules |> CONJUNCTS |> el 4 +Theorem eqMp_equation = proves_rules |> CONJUNCTS |> el 5 - |> REWRITE_RULE[GSYM AND_IMP_INTRO]) -val refl_equation = save_thm("refl_equation", - proves_rules |> CONJUNCTS |> el 9) -val appThm_equation = save_thm("appThm_equation", + |> REWRITE_RULE[GSYM AND_IMP_INTRO] +Theorem refl_equation = + proves_rules |> CONJUNCTS |> el 9 +Theorem appThm_equation = proves_rules |> CONJUNCTS |> el 8 - |> REWRITE_RULE[GSYM AND_IMP_INTRO]) + |> REWRITE_RULE[GSYM AND_IMP_INTRO] Theorem addAssum: ∀thy h c a. (thy,h) |- c ∧ term_ok (sigof thy) a ∧ (a has_type Bool) ⇒ diff --git a/characteristic/cfDivScript.sml b/characteristic/cfDivScript.sml index 17632b6f6b..8cb4c479f2 100644 --- a/characteristic/cfDivScript.sml +++ b/characteristic/cfDivScript.sml @@ -367,8 +367,8 @@ Proof fs[] QED -val mk_single_app_F_unchanged = save_thm("mk_single_app_F_unchanged", - SIMP_RULE std_ss [] mk_single_app_F_unchanged_gen); +Theorem mk_single_app_F_unchanged = + SIMP_RULE std_ss [] mk_single_app_F_unchanged_gen Definition mk_inr_res_def: (mk_inr_res(Rval vs) = @@ -2540,8 +2540,8 @@ Proof fs[] QED -val make_single_app_F_unchanged = save_thm("make_single_app_F_unchanged", - SIMP_RULE std_ss [] make_single_app_F_unchanged_gen); +Theorem make_single_app_F_unchanged = + SIMP_RULE std_ss [] make_single_app_F_unchanged_gen Definition mk_tyerr_res_def: mk_tyerr_res (Rerr e) = Rerr e /\ diff --git a/characteristic/cfLetAutoScript.sml b/characteristic/cfLetAutoScript.sml index e71e73f1ed..6d93f77458 100644 --- a/characteristic/cfLetAutoScript.sml +++ b/characteristic/cfLetAutoScript.sml @@ -335,8 +335,8 @@ Proof EQ_TAC >-(rw[] >-(metis_tac[REPLICATE_APPEND_LEFT]) >-(metis_tac[REPLICATE_APPEND_RIGHT]) >> metis_tac [LENGTH_REPLICATE, LENGTH_APPEND]) >> metis_tac[REPLICATE_APPEND] QED -val REPLICATE_APPEND_DECOMPOSE_SYM = save_thm("REPLICATE_APPEND_DECOMPOSE_SYM", -CONV_RULE(PATH_CONV "lr" SYM_CONV) REPLICATE_APPEND_DECOMPOSE); +Theorem REPLICATE_APPEND_DECOMPOSE_SYM = + CONV_RULE(PATH_CONV "lr" SYM_CONV) REPLICATE_APPEND_DECOMPOSE Theorem REPLICATE_PLUS_ONE: REPLICATE (n + 1) x = x::REPLICATE n x diff --git a/characteristic/cfTacticsScript.sml b/characteristic/cfTacticsScript.sml index f9bf04e8b6..b0bec27489 100644 --- a/characteristic/cfTacticsScript.sml +++ b/characteristic/cfTacticsScript.sml @@ -149,10 +149,10 @@ Proof first_assum progress QED -val BOOL_T = save_thm("BOOL_T", - EVAL ``BOOL T (Conv (SOME (TypeStamp "True" 0)) [])``); +Theorem BOOL_T = + EVAL ``BOOL T (Conv (SOME (TypeStamp "True" 0)) [])`` -val BOOL_F = save_thm("BOOL_F", - EVAL ``BOOL F (Conv (SOME (TypeStamp "False" 0)) [])``); +Theorem BOOL_F = + EVAL ``BOOL F (Conv (SOME (TypeStamp "False" 0)) [])`` val _ = export_theory() diff --git a/compiler/backend/ag32/ag32_configScript.sml b/compiler/backend/ag32/ag32_configScript.sml index f8b33a4523..e867ffc94e 100644 --- a/compiler/backend/ag32/ag32_configScript.sml +++ b/compiler/backend/ag32/ag32_configScript.sml @@ -9,8 +9,8 @@ Definition ag32_names_def: ag32_names = LN:num num_map End -val ag32_names_def = save_thm("ag32_names_def[compute,allow_rebind]", - CONV_RULE (RAND_CONV EVAL) ag32_names_def); +Theorem ag32_names_def[compute,allow_rebind] = + CONV_RULE (RAND_CONV EVAL) ag32_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/backend/ag32/ag32_memoryScript.sml b/compiler/backend/ag32/ag32_memoryScript.sml index 7afa700856..a546cc1f2a 100644 --- a/compiler/backend/ag32/ag32_memoryScript.sml +++ b/compiler/backend/ag32/ag32_memoryScript.sml @@ -3683,8 +3683,8 @@ Definition startup_asm_code_def: JumpReg 1] End -val LENGTH_startup_asm_code = save_thm("LENGTH_startup_asm_code", - ``LENGTH (startup_asm_code n cl bl)`` |> EVAL); +Theorem LENGTH_startup_asm_code = + ``LENGTH (startup_asm_code n cl bl)`` |> EVAL Definition startup_code_def: startup_code ffi_len code_len data_len = diff --git a/compiler/backend/ag32/proofs/ag32_progScript.sml b/compiler/backend/ag32/proofs/ag32_progScript.sml index 7ed12be7d1..ed8e8ed715 100644 --- a/compiler/backend/ag32/proofs/ag32_progScript.sml +++ b/compiler/backend/ag32/proofs/ag32_progScript.sml @@ -297,10 +297,10 @@ Proof SRW_TAC [wordsLib.WORD_EXTRACT_ss] [] QED -val IMP_AG32_SPEC = save_thm("IMP_AG32_SPEC", +Theorem IMP_AG32_SPEC = (ONCE_REWRITE_RULE [STAR_COMM] o REWRITE_RULE [AG32_SPEC_CODE] o SPECL [``CODE_POOL ag32_instr c * p'``, - ``CODE_POOL ag32_instr c * q'``]) IMP_AG32_SPEC_LEMMA); + ``CODE_POOL ag32_instr c * q'``]) IMP_AG32_SPEC_LEMMA Definition mem_unchanged_def: mem_unchanged md m1 m2 = (!a. ~(a IN md) ==> m1 a = m2 a) diff --git a/compiler/backend/arm7/arm7_configScript.sml b/compiler/backend/arm7/arm7_configScript.sml index 783e27968b..2588752c0d 100644 --- a/compiler/backend/arm7/arm7_configScript.sml +++ b/compiler/backend/arm7/arm7_configScript.sml @@ -27,8 +27,8 @@ Definition arm7_names_def: insert 14 13) LN:num num_map End -val arm7_names_def = save_thm("arm7_names_def[allow_rebind]", - CONV_RULE (RAND_CONV EVAL) arm7_names_def); +Theorem arm7_names_def[allow_rebind] = + CONV_RULE (RAND_CONV EVAL) arm7_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/backend/arm8/arm8_configScript.sml b/compiler/backend/arm8/arm8_configScript.sml index 2a4910b994..a581c454bb 100644 --- a/compiler/backend/arm8/arm8_configScript.sml +++ b/compiler/backend/arm8/arm8_configScript.sml @@ -27,8 +27,8 @@ Definition arm8_names_def: insert 30 26) LN:num num_map End -val arm8_names_def = save_thm("arm8_names_def[compute,allow_rebind]", - CONV_RULE (RAND_CONV EVAL) arm8_names_def); +Theorem arm8_names_def[compute,allow_rebind] = + CONV_RULE (RAND_CONV EVAL) arm8_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/backend/backendScript.sml b/compiler/backend/backendScript.sml index ff643c8cc0..02c7b3fe08 100644 --- a/compiler/backend/backendScript.sml +++ b/compiler/backend/backendScript.sml @@ -209,8 +209,8 @@ Definition prim_config_def: FST (to_flat <| source_conf := empty_config |> (prim_types_program)) End -val prim_config_eq = save_thm("prim_config_eq", - EVAL ``prim_config`` |> SIMP_RULE std_ss [FUNION_FUPDATE_1,FUNION_FEMPTY_1]); +Theorem prim_config_eq = + EVAL ``prim_config`` |> SIMP_RULE std_ss [FUNION_FUPDATE_1,FUNION_FEMPTY_1] Definition from_lab_def: from_lab c names p bm = diff --git a/compiler/backend/bvi_tailrecScript.sml b/compiler/backend/bvi_tailrecScript.sml index ee64d1884b..8c3ef15d5c 100644 --- a/compiler/backend/bvi_tailrecScript.sml +++ b/compiler/backend/bvi_tailrecScript.sml @@ -108,11 +108,11 @@ Proof CONV_TAC (DEPTH_CONV PMATCH_ELIM_CONV) \\ Cases \\ rw [from_op_def] QED -val from_op_thm = save_thm("from_op_thm[simp]", +Theorem from_op_thm[simp] = map (fn tm => EVAL ``from_op ^tm``) (TypeBase.case_def_of ``:closLang$op`` |> CONJUNCTS |> map (el 1 o #2 o strip_comb o lhs o concl o SPEC_ALL)) - |> LIST_CONJ) + |> LIST_CONJ Definition op_eq_def: (op_eq Plus (Op op xs) <=> op = Add) /\ diff --git a/compiler/backend/bvl_handleScript.sml b/compiler/backend/bvl_handleScript.sml index ec784e8af5..04242a4b19 100644 --- a/compiler/backend/bvl_handleScript.sml +++ b/compiler/backend/bvl_handleScript.sml @@ -329,13 +329,13 @@ Proof \\ Cases_on `dx` \\ fs [LENGTH_NIL] QED -val compile_seqs_compute = save_thm("compile_seqs_compute", +Theorem compile_seqs_compute = LIST_CONJ [ compile_seqs_def |> Q.SPECL [`e`,`c`,`NONE`] |> SIMP_RULE std_ss [LET_THM], compile_seqs_def |> Q.SPECL [`e`,`c`,`SOME y`] - |> SIMP_RULE std_ss [LET_THM]]); + |> SIMP_RULE std_ss [LET_THM]] val _ = export_theory(); diff --git a/compiler/backend/bvl_to_bviScript.sml b/compiler/backend/bvl_to_bviScript.sml index 5a8596f436..ca19719419 100644 --- a/compiler/backend/bvl_to_bviScript.sml +++ b/compiler/backend/bvl_to_bviScript.sml @@ -130,22 +130,22 @@ Definition ConcatByte_location_def: ConcatByte_location = SumListLength_location+1 End -val AllocGlobal_location_eq = save_thm("AllocGlobal_location_eq", - ``AllocGlobal_location`` |> EVAL); -val CopyGlobals_location_eq = save_thm("CopyGlobals_location_eq", - ``CopyGlobals_location`` |> EVAL); -val InitGlobals_location_eq = save_thm("InitGlobals_location_eq", - ``InitGlobals_location`` |> EVAL); -val ListLength_location_eq = save_thm("ListLength_location_eq", - ``ListLength_location`` |> EVAL); -val FromListByte_location_eq = save_thm("FromListByte_location_eq", - ``FromListByte_location`` |> EVAL); -val ToListByte_location_eq = save_thm("ToListByte_location_eq", - ``ToListByte_location`` |> EVAL); -val SumListLength_location_eq = save_thm("SumListLength_location_eq", - ``SumListLength_location`` |> EVAL); -val ConcatByte_location_eq = save_thm("ConcatByte_location_eq", - ``ConcatByte_location`` |> EVAL); +Theorem AllocGlobal_location_eq = + ``AllocGlobal_location`` |> EVAL +Theorem CopyGlobals_location_eq = + ``CopyGlobals_location`` |> EVAL +Theorem InitGlobals_location_eq = + ``InitGlobals_location`` |> EVAL +Theorem ListLength_location_eq = + ``ListLength_location`` |> EVAL +Theorem FromListByte_location_eq = + ``FromListByte_location`` |> EVAL +Theorem ToListByte_location_eq = + ``ToListByte_location`` |> EVAL +Theorem SumListLength_location_eq = + ``SumListLength_location`` |> EVAL +Theorem ConcatByte_location_eq = + ``ConcatByte_location`` |> EVAL Definition AllocGlobal_code_def: AllocGlobal_code = (1:num, diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml index 13c8a4838e..dac6b65cc6 100644 --- a/compiler/backend/data_to_wordScript.sml +++ b/compiler/backend/data_to_wordScript.sml @@ -259,68 +259,68 @@ Definition Bignum_location_def: Bignum_location = AppendFastLoop_location+1 End -val FromList_location_eq = save_thm("FromList_location_eq", - ``FromList_location`` |> EVAL); -val FromList1_location_eq = save_thm("FromList1_location_eq", - ``FromList1_location`` |> EVAL); -val RefByte_location_eq = save_thm("RefByte_location_eq", - ``RefByte_location`` |> EVAL); -val RefArray_location_eq = save_thm("RefArray_location_eq", - ``RefArray_location`` |> EVAL); -val Replicate_location_eq = save_thm("Replicate_location_eq", - ``Replicate_location`` |> EVAL); -val AnyArith_location_eq = save_thm("AnyArith_location_eq", - ``AnyArith_location`` |> EVAL); -val Add_location_eq = save_thm("Add_location_eq", - ``Add_location`` |> EVAL); -val Sub_location_eq = save_thm("Sub_location_eq", - ``Sub_location`` |> EVAL); -val Mul_location_eq = save_thm("Mul_location_eq", - ``Mul_location`` |> EVAL); -val Div_location_eq = save_thm("Div_location_eq", - ``Div_location`` |> EVAL); -val Mod_location_eq = save_thm("Mod_location_eq", - ``Mod_location`` |> EVAL); -val Compare1_location_eq = save_thm("Compare1_location_eq", - ``Compare1_location`` |> EVAL); -val Compare_location_eq = save_thm("Compare_location_eq", - ``Compare_location`` |> EVAL); -val Equal1_location_eq = save_thm("Equal1_location_eq", - ``Equal1_location`` |> EVAL); -val Equal_location_eq = save_thm("Equal_location_eq", - ``Equal_location`` |> EVAL); -val LongDiv1_location_eq = save_thm("LongDiv1_location_eq", - ``LongDiv1_location`` |> EVAL); -val LongDiv_location_eq = save_thm("LongDiv_location_eq", - ``LongDiv_location`` |> EVAL); -val MemCopy_location_eq = save_thm("MemCopy_location_eq", - ``MemCopy_location`` |> EVAL); -val Bignum_location_eq = save_thm("Bignum_location_eq", - ``Bignum_location`` |> EVAL); -val ByteCopy_location_eq = save_thm("ByteCopy_location_eq", - ``ByteCopy_location`` |> EVAL); -val ByteCopyAdd_location_eq = save_thm("ByteCopyAdd_location_eq", - ``ByteCopyAdd_location`` |> EVAL); -val ByteCopySub_location_eq = save_thm("ByteCopySub_location_eq", - ``ByteCopySub_location`` |> EVAL); -val ByteCopyNew_location_eq = save_thm("ByteCopyNew_location_eq", - ``ByteCopyNew_location`` |> EVAL); -val Install_location_eq = save_thm("Install_location_eq", - ``Install_location`` |> EVAL); -val InstallCode_location_eq = save_thm("InstallCode_location_eq", - ``InstallCode_location`` |> EVAL); -val InstallData_location_eq = save_thm("InstallData_location_eq", - ``InstallData_location`` |> EVAL); -val Dummy_location_eq = save_thm("Dummy_location_eq", - ``Dummy_location`` |> EVAL); -val Append_location_eq = save_thm("Append_location_eq", - ``Append_location`` |> EVAL); -val AppendMainLoop_location_eq = save_thm("AppendMainLoop_location_eq", - ``AppendMainLoop_location`` |> EVAL); -val AppendLenLoop_location_eq = save_thm("AppendLenLoop_location_eq", - ``AppendLenLoop_location`` |> EVAL); -val AppendFastLoop_location_eq = save_thm("AppendFastLoop_location_eq", - ``AppendFastLoop_location`` |> EVAL); +Theorem FromList_location_eq = + ``FromList_location`` |> EVAL +Theorem FromList1_location_eq = + ``FromList1_location`` |> EVAL +Theorem RefByte_location_eq = + ``RefByte_location`` |> EVAL +Theorem RefArray_location_eq = + ``RefArray_location`` |> EVAL +Theorem Replicate_location_eq = + ``Replicate_location`` |> EVAL +Theorem AnyArith_location_eq = + ``AnyArith_location`` |> EVAL +Theorem Add_location_eq = + ``Add_location`` |> EVAL +Theorem Sub_location_eq = + ``Sub_location`` |> EVAL +Theorem Mul_location_eq = + ``Mul_location`` |> EVAL +Theorem Div_location_eq = + ``Div_location`` |> EVAL +Theorem Mod_location_eq = + ``Mod_location`` |> EVAL +Theorem Compare1_location_eq = + ``Compare1_location`` |> EVAL +Theorem Compare_location_eq = + ``Compare_location`` |> EVAL +Theorem Equal1_location_eq = + ``Equal1_location`` |> EVAL +Theorem Equal_location_eq = + ``Equal_location`` |> EVAL +Theorem LongDiv1_location_eq = + ``LongDiv1_location`` |> EVAL +Theorem LongDiv_location_eq = + ``LongDiv_location`` |> EVAL +Theorem MemCopy_location_eq = + ``MemCopy_location`` |> EVAL +Theorem Bignum_location_eq = + ``Bignum_location`` |> EVAL +Theorem ByteCopy_location_eq = + ``ByteCopy_location`` |> EVAL +Theorem ByteCopyAdd_location_eq = + ``ByteCopyAdd_location`` |> EVAL +Theorem ByteCopySub_location_eq = + ``ByteCopySub_location`` |> EVAL +Theorem ByteCopyNew_location_eq = + ``ByteCopyNew_location`` |> EVAL +Theorem Install_location_eq = + ``Install_location`` |> EVAL +Theorem InstallCode_location_eq = + ``InstallCode_location`` |> EVAL +Theorem InstallData_location_eq = + ``InstallData_location`` |> EVAL +Theorem Dummy_location_eq = + ``Dummy_location`` |> EVAL +Theorem Append_location_eq = + ``Append_location`` |> EVAL +Theorem AppendMainLoop_location_eq = + ``AppendMainLoop_location`` |> EVAL +Theorem AppendLenLoop_location_eq = + ``AppendLenLoop_location`` |> EVAL +Theorem AppendFastLoop_location_eq = + ``AppendFastLoop_location`` |> EVAL Definition SilentFFI_def: SilentFFI c n names = @@ -2265,7 +2265,8 @@ val def = assign_Define ` WriteWord64_on_32 c header dest 5 3],l))) : 'a wordLang$prog # num`; -val all_assign_defs = save_thm("all_assign_defs",LIST_CONJ (!assign_defs)); +Theorem all_assign_defs = + LIST_CONJ (!assign_defs) Definition assign_def: assign (c:data_to_word$config) (secn:num) (l:num) (dest:num) (op:closLang$op) diff --git a/compiler/backend/exportScript.sml b/compiler/backend/exportScript.sml index 8cf565c7ae..d839754f66 100644 --- a/compiler/backend/exportScript.sml +++ b/compiler/backend/exportScript.sml @@ -150,7 +150,8 @@ Definition all_bytes_def: all_bytes = Vector (GENLIST (\n. byte_to_string (n2w n)) 256) End -val all_bytes_eq = save_thm("all_bytes_eq",EVAL ``all_bytes``); +Theorem all_bytes_eq = + EVAL ``all_bytes`` Theorem byte_to_string_eq: !b. byte_to_string b = sub all_bytes (w2n b) diff --git a/compiler/backend/flat_uncheck_ctorsScript.sml b/compiler/backend/flat_uncheck_ctorsScript.sml index f5843d8a61..3e2d3b7d57 100644 --- a/compiler/backend/flat_uncheck_ctorsScript.sml +++ b/compiler/backend/flat_uncheck_ctorsScript.sml @@ -55,7 +55,8 @@ Proof \\ simp_tac(std_ss++listSimps.LIST_ss)[LENGTH_EQ_NUM_compute] QED -val compile_nil = save_thm ("compile_nil[simp]", EVAL ``compile []``); +Theorem compile_nil[simp] = + EVAL ``compile []`` Theorem compile_not_nil[simp]: compile [x] <> [] diff --git a/compiler/backend/gc/copying_gcScript.sml b/compiler/backend/gc/copying_gcScript.sml index 5dcd8643c6..784fb15c75 100644 --- a/compiler/backend/gc/copying_gcScript.sml +++ b/compiler/backend/gc/copying_gcScript.sml @@ -617,7 +617,8 @@ val lemma = prove(th |> concl |> dest_imp |> fst, val th = MP th lemma |> SIMP_RULE std_ss [] |> Q.SPECL [`h1`,`h2`,`a`,`n`,`heap`,`c`,`limit`,`h1'`,`a'`,`n'`,`heap'`] -val gc_move_loop_ok = save_thm("gc_move_loop_ok",th); +Theorem gc_move_loop_ok = + th Theorem gc_move_list_IMP_LENGTH: !l5 h a n heap c k xs ys a1 xs1 heap1 c1. diff --git a/compiler/backend/gc/gc_sharedScript.sml b/compiler/backend/gc/gc_sharedScript.sml index 669010e4e8..51cc3d671c 100644 --- a/compiler/backend/gc/gc_sharedScript.sml +++ b/compiler/backend/gc/gc_sharedScript.sml @@ -378,7 +378,8 @@ Definition ADDR_APPLY_def: (ADDR_APPLY f (Data y) = Data y) End -val heap_lookup_FLOOKUP = save_thm("heap_lookup_FLOOKUP",Q.prove( +Theorem heap_lookup_FLOOKUP = + Q.prove( `!heap n k. (heap_lookup n heap = SOME (ForwardPointer ptr u l)) ==> (FLOOKUP (heap_map k heap) (n+k) = SOME ptr)`, @@ -389,7 +390,7 @@ val heap_lookup_FLOOKUP = save_thm("heap_lookup_FLOOKUP",Q.prove( \\ full_simp_tac std_ss [] \\ Cases_on `h` \\ full_simp_tac std_ss [heap_map_def,el_length_def] \\ full_simp_tac (srw_ss()) [FLOOKUP_DEF,ADD_ASSOC,FAPPLY_FUPDATE_THM]) - |> Q.SPECL [`heap`,`n`,`0`] |> SIMP_RULE std_ss []); + |> Q.SPECL [`heap`,`n`,`0`] |> SIMP_RULE std_ss [] val _ = augment_srw_ss [rewrites [LIST_REL_def]]; @@ -408,7 +409,8 @@ Proof \\ full_simp_tac (srw_ss()) [heap_length_def,el_length_def] \\ decide_tac QED -val NOT_IN_heap_map = save_thm("NOT_IN_heap_map", Q.prove( +Theorem NOT_IN_heap_map = + Q.prove( `!ha n. ~(n + heap_length ha IN FDOM (heap_map n (ha ++ DataElement ys l d::hb)))`, Induct \\ full_simp_tac (srw_ss()) [heap_map_def,APPEND,heap_length_def] \\ rpt strip_tac \\ imp_res_tac IN_heap_map_IMP @@ -416,7 +418,7 @@ val NOT_IN_heap_map = save_thm("NOT_IN_heap_map", Q.prove( THEN1 (full_simp_tac std_ss [el_length_def] \\ decide_tac) \\ Cases_on `h` \\ full_simp_tac std_ss [heap_map_def] \\ res_tac \\ full_simp_tac (srw_ss()) [el_length_def,ADD_ASSOC] \\ res_tac - \\ decide_tac) |> Q.SPECL [`ha`,`0`] |> SIMP_RULE std_ss []) + \\ decide_tac) |> Q.SPECL [`ha`,`0`] |> SIMP_RULE std_ss [] Theorem isSomeDataOrForward_lemma: !ha ptr. @@ -486,13 +488,14 @@ Proof \\ full_simp_tac std_ss [FUNION_FUPDATE_1,el_length_def,ADD_ASSOC] QED -val FDOM_heap_map = save_thm("FDOM_heap_map", Q.prove( +Theorem FDOM_heap_map = + Q.prove( `!xs n. ~(n + heap_length xs IN FDOM (heap_map n xs))`, Induct \\ TRY (Cases_on `h`) \\ full_simp_tac (srw_ss()) [heap_map_def,heap_length_def,ADD_ASSOC] \\ rpt strip_tac \\ full_simp_tac std_ss [el_length_def,ADD_ASSOC] \\ TRY decide_tac \\ metis_tac []) - |> Q.SPECL [`xs`,`0`] |> SIMP_RULE std_ss []); + |> Q.SPECL [`xs`,`0`] |> SIMP_RULE std_ss [] Theorem heap_addresses_APPEND: !xs ys n. heap_addresses n (xs ++ ys) = diff --git a/compiler/backend/gc/gen_gcScript.sml b/compiler/backend/gc/gen_gcScript.sml index aed3532dcb..c10080fc26 100644 --- a/compiler/backend/gc/gen_gcScript.sml +++ b/compiler/backend/gc/gen_gcScript.sml @@ -1568,11 +1568,11 @@ Proof \\ full_simp_tac std_ss [] QED -val heap_lookup_IMP_heap_addresses = save_thm("heap_lookup_IMP_heap_addresses", - heap_lookup_IMP_heap_addresses_GEN +Theorem heap_lookup_IMP_heap_addresses = + heap_lookup_IMP_heap_addresses_GEN |> Q.SPECL [`xs`,`0`] |> SIMP_RULE std_ss [] - |> GEN_ALL); + |> GEN_ALL val heap_lookup_AND_APPEND_IMP = prove( ``!xs n ys d d1. diff --git a/compiler/backend/gc/gen_gc_partialScript.sml b/compiler/backend/gc/gen_gc_partialScript.sml index 33c84e02f6..5c84384e29 100644 --- a/compiler/backend/gc/gen_gc_partialScript.sml +++ b/compiler/backend/gc/gen_gc_partialScript.sml @@ -1267,8 +1267,8 @@ Proof \\ imp_res_tac heap_lookup_LESS QED -val f_old_ptrs_finite_open = save_thm("f_old_ptrs_finite_open[simp]", - f_old_ptrs_finite |> SIMP_RULE std_ss [f_old_ptrs_def]); +Theorem f_old_ptrs_finite_open[simp] = + f_old_ptrs_finite |> SIMP_RULE std_ss [f_old_ptrs_def] Definition new_f_def: new_f f conf heap = @@ -1318,8 +1318,8 @@ Proof \\ fs [isSomeDataElement_def]) QED -val isSomeDataElement_to_gen_heap_element = save_thm("isSomeDataElement_to_gen_heap_element", - isSomeDataElement_to_gen_heap_list |> SIMP_RULE std_ss [to_gen_heap_list_def]); +Theorem isSomeDataElement_to_gen_heap_element = + isSomeDataElement_to_gen_heap_list |> SIMP_RULE std_ss [to_gen_heap_list_def] val MEM_refs_to_roots_IMP_MEM = prove( ``!heap_refs. @@ -1403,8 +1403,8 @@ val roots_ok_simulation = prove( \\ fs [] \\ simp [isSomeDataElement_to_gen_heap_element]); -val heap_length_to_gen_heap_element = save_thm("heap_length_to_gen_heap_element[simp]", - heap_length_to_gen_heap_list |> SIMP_RULE std_ss [to_gen_heap_list_def]); +Theorem heap_length_to_gen_heap_element[simp] = + heap_length_to_gen_heap_list |> SIMP_RULE std_ss [to_gen_heap_list_def] val MEM_to_gen_heap_IMP_MEM = prove( ``!heap_current xs l d ptr u. diff --git a/compiler/backend/mips/mips_configScript.sml b/compiler/backend/mips/mips_configScript.sml index 4aa63337a8..7cdc0b2c1d 100644 --- a/compiler/backend/mips/mips_configScript.sml +++ b/compiler/backend/mips/mips_configScript.sml @@ -30,8 +30,8 @@ Definition mips_names_def: insert 31 1) LN:num num_map End -val mips_names_def = save_thm("mips_names_def[compute,allow_rebind]", - CONV_RULE (RAND_CONV EVAL) mips_names_def); +Theorem mips_names_def[compute,allow_rebind] = + CONV_RULE (RAND_CONV EVAL) mips_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/backend/proofs/bvi_letProofScript.sml b/compiler/backend/proofs/bvi_letProofScript.sml index 2ba664a47b..e2cb7e1fd3 100644 --- a/compiler/backend/proofs/bvi_letProofScript.sml +++ b/compiler/backend/proofs/bvi_letProofScript.sml @@ -302,10 +302,10 @@ Proof \\ asm_exists_tac \\ fs [] QED -val compile_thm = save_thm("compile_thm", +Theorem compile_thm = evaluate_env_rel |> Q.SPECL [`xs`,`env`,`s1`,`[]`,`env`,`res`,`s2`,`ys`,`0`] |> GEN_ALL - |> SIMP_RULE (srw_ss()) [env_rel_def]) + |> SIMP_RULE (srw_ss()) [env_rel_def] Theorem evaluate_compile_exp: evaluate ([d],env,s) = (r,t) /\ diff --git a/compiler/backend/proofs/bvl_constProofScript.sml b/compiler/backend/proofs/bvl_constProofScript.sml index a877dceacb..f4d05ba9fb 100644 --- a/compiler/backend/proofs/bvl_constProofScript.sml +++ b/compiler/backend/proofs/bvl_constProofScript.sml @@ -295,10 +295,10 @@ Proof \\ res_tac \\ fs [] \\ rw [] \\ fs [] \\ rw [] \\ fs [] QED -val compile_thm = save_thm("compile_thm", +Theorem compile_thm = evaluate_env_rel |> Q.SPECL [`xs`,`env`,`s1`,`[]`,`env`] |> GEN_ALL - |> SIMP_RULE std_ss [env_rel_def]) + |> SIMP_RULE std_ss [env_rel_def] Theorem evaluate_compile_exp: evaluate ([d],env,s) = (r,t) /\ diff --git a/compiler/backend/proofs/bvl_handleProofScript.sml b/compiler/backend/proofs/bvl_handleProofScript.sml index 58400c8966..edccc65f5e 100644 --- a/compiler/backend/proofs/bvl_handleProofScript.sml +++ b/compiler/backend/proofs/bvl_handleProofScript.sml @@ -186,10 +186,10 @@ Termination \\ SRW_TAC [] [bvlTheory.exp_size_def] \\ DECIDE_TAC End -val evaluate_GENLIST = save_thm("evaluate_GENLIST", +Theorem evaluate_GENLIST = evaluate_genlist_vars |> Q.SPECL[`0`,`env ++ ys`,`LENGTH (env:bvlSem$v list)`,`s`] - |> SIMP_RULE(srw_ss()++ETA_ss)[TAKE_APPEND1]); + |> SIMP_RULE(srw_ss()++ETA_ss)[TAKE_APPEND1] Definition env_rel_def: env_rel l env env1 = @@ -458,7 +458,8 @@ Theorem compile_correct = Q.prove(` |> Q.SPECL [`xs`,`env`,`s1`,`ys`,`env`,`res`,`s2`,`[]`] |> SIMP_RULE std_ss [APPEND_NIL,env_rel_refl]; -val _ = save_thm("compile_correct[allow_rebind]",compile_correct); +Theorem compile_correct[allow_rebind] = + compile_correct Theorem compile_correct[allow_rebind]: (evaluate ([x],env,s1) = (res,s2)) /\ res <> Rerr(Rabort Rtype_error) /\ diff --git a/compiler/backend/proofs/clos_annotateProofScript.sml b/compiler/backend/proofs/clos_annotateProofScript.sml index a50938a948..f4120541f4 100644 --- a/compiler/backend/proofs/clos_annotateProofScript.sml +++ b/compiler/backend/proofs/clos_annotateProofScript.sml @@ -78,7 +78,9 @@ QED Definition alt_fv1_def: alt_fv1 v e = alt_fv v [e] End -val alt_fv1_intro = save_thm("alt_fv1_intro[simp]",GSYM alt_fv1_def) + +Theorem alt_fv1_intro[simp] = + GSYM alt_fv1_def Theorem alt_fv1_thm = alt_fv |> SIMP_RULE (srw_ss())[] @@ -1243,10 +1245,10 @@ Proof full_simp_tac(srw_ss())[SUBSET_DEF,IN_DEF,env_ok_def] QED -val annotate_correct = save_thm("annotate_correct", +Theorem annotate_correct = shift_correct |> CONJUNCT1 |> SPEC_ALL |> Q.INST [`m`|->`0`,`l`|->`0`,`i`|->`LN`,`env`|->`[]`] - |> REWRITE_RULE [GSYM annotate_def,env_set_default,LENGTH,ADD_0]); + |> REWRITE_RULE [GSYM annotate_def,env_set_default,LENGTH,ADD_0] (* more correctness properties *) diff --git a/compiler/backend/proofs/clos_fvsProofScript.sml b/compiler/backend/proofs/clos_fvsProofScript.sml index fad88d4646..49de20ac67 100644 --- a/compiler/backend/proofs/clos_fvsProofScript.sml +++ b/compiler/backend/proofs/clos_fvsProofScript.sml @@ -77,7 +77,8 @@ Inductive v_rel: v_rel (Recclosure loc args1 env1 funs1 k) (Recclosure loc args2 env2 funs2 k)) End -val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ +Theorem v_rel_simps[simp] = + LIST_CONJ [ SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Number n) x``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Block n p) x``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Word64 p) x``, @@ -88,7 +89,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ prove(``v_rel (Boolv b) x <=> x = Boolv b``, Cases_on `b` \\ fs [Boolv_def,Once v_rel_cases]), prove(``v_rel Unit x <=> x = Unit``, - fs [closSemTheory.Unit_def,Once v_rel_cases])]) + fs [closSemTheory.Unit_def,Once v_rel_cases])] (* state relation *) diff --git a/compiler/backend/proofs/clos_knownProofScript.sml b/compiler/backend/proofs/clos_knownProofScript.sml index b72e256fcc..7b2a516645 100644 --- a/compiler/backend/proofs/clos_knownProofScript.sml +++ b/compiler/backend/proofs/clos_knownProofScript.sml @@ -270,9 +270,8 @@ Termination WF_REL_TAC `measure val_approx_size` End -val val_approx_sgc_free_def = save_thm( - "val_approx_sgc_free_def[simp,allow_rebind]", - val_approx_sgc_free_def |> SIMP_RULE (srw_ss() ++ ETA_ss) []); +Theorem val_approx_sgc_free_def[simp,allow_rebind] = + val_approx_sgc_free_def |> SIMP_RULE (srw_ss() ++ ETA_ss) [] Theorem val_approx_sgc_free_merge: !a1 a2. val_approx_sgc_free a1 /\ val_approx_sgc_free a2 ==> @@ -308,14 +307,15 @@ Inductive val_approx_val: (!m n b s env. val_approx_val (Clos m n b s) (Closure (SOME m) [] env n b)) End -val val_approx_val_simps = save_thm("val_approx_val_simps[simp]",LIST_CONJ [ +Theorem val_approx_val_simps[simp] = + LIST_CONJ [ SIMP_CONV (srw_ss()) [val_approx_val_cases] ``val_approx_val Other v``, SIMP_CONV (srw_ss()) [val_approx_val_cases] ``val_approx_val (Int i) v``, SIMP_CONV (srw_ss()) [val_approx_val_cases] ``val_approx_val (Tuple tg vas) v``, SIMP_CONV (srw_ss()) [val_approx_val_cases] ``val_approx_val (ClosNoInline m n) v``, SIMP_CONV (srw_ss()) [val_approx_val_cases] ``val_approx_val (Clos m n b1 s) v``, prove(``val_approx_val Impossible v <=> F``, simp [val_approx_val_cases]) -]); +] Theorem val_approx_val_merge_I_lemma: !a1 v. val_approx_val a1 v ==> !a2. val_approx_val (merge a1 a2) v @@ -1154,13 +1154,11 @@ Proof \\ qexists_tac `n` \\ fs []) QED -val evaluate_changed_globals = save_thm( - "evaluate_changed_globals", - CONJUNCT1 evaluate_changed_globals_0); +Theorem evaluate_changed_globals = + CONJUNCT1 evaluate_changed_globals_0 -val evaluate_app_changed_globals = save_thm( - "evaluate_app_changed_globals", - CONJUNCT2 evaluate_changed_globals_0); +Theorem evaluate_app_changed_globals = + CONJUNCT2 evaluate_changed_globals_0 Theorem mk_Ticks_set_globals[simp]: !t tc n exp. set_globals (mk_Ticks t tc n exp) = set_globals exp @@ -2461,8 +2459,8 @@ Termination \\ rpt strip_tac \\ imp_res_tac v_size_lemma \\ simp [] End -val v_rel_def = save_thm("v_rel_def[simp,compute,allow_rebind]", - v_rel_def |> SIMP_RULE (bool_ss ++ ETA_ss) []); +Theorem v_rel_def[simp,compute,allow_rebind] = + v_rel_def |> SIMP_RULE (bool_ss ++ ETA_ss) [] val v_rel_ind = theorem "v_rel_ind"; @@ -2593,9 +2591,10 @@ Inductive ref_rel: ref_rel c g (ValueArray xs) (ValueArray ys)) End -val ref_rel_simps = save_thm("ref_rel_simps[simp]",LIST_CONJ [ +Theorem ref_rel_simps[simp] = + LIST_CONJ [ SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ValueArray vs) x``, - SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ByteArray bs) x``]) + SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ByteArray bs) x``] Theorem ref_rel_upd_inline_factor: ref_rel (c with inline_factor := k) = ref_rel c @@ -2801,15 +2800,13 @@ val opt_caseT = case_eq_thms |> CONJUNCTS |> Q.INST [`v'` |-> `T`] |> SIMP_RULE (srw_ss()) [] -val loptrel_arg1_SOME = save_thm( - "loptrel_arg1_SOME", +Theorem loptrel_arg1_SOME = loptrel_def |> SPEC_ALL |> Q.INST [`lopt1` |-> `SOME loc1`] - |> SIMP_RULE (srw_ss()) [opt_caseT, v_caseT]) + |> SIMP_RULE (srw_ss()) [opt_caseT, v_caseT] -val loptrel_arg1_NONE = save_thm( - "loptrel_arg1_NONE", +Theorem loptrel_arg1_NONE = loptrel_def |> SPEC_ALL |> Q.INST [`lopt1` |-> `NONE`] - |> SIMP_RULE (srw_ss()) [opt_caseT, v_caseT]) + |> SIMP_RULE (srw_ss()) [opt_caseT, v_caseT] Theorem dest_closure_SOME_IMP: dest_closure max_app loc_opt f2 xs = SOME x ==> diff --git a/compiler/backend/proofs/clos_letopProofScript.sml b/compiler/backend/proofs/clos_letopProofScript.sml index 9238ee1a91..e8b7943743 100644 --- a/compiler/backend/proofs/clos_letopProofScript.sml +++ b/compiler/backend/proofs/clos_letopProofScript.sml @@ -72,7 +72,8 @@ Inductive v_rel: v_rel (Recclosure loc args1 env1 funs1 k) (Recclosure loc args2 env2 funs2 k)) End -val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ +Theorem v_rel_simps[simp] = + LIST_CONJ [ SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Number n) x``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Block n p) x``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel (Word64 p) x``, @@ -83,7 +84,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ prove(``v_rel (Boolv b) x <=> x = Boolv b``, Cases_on `b` \\ fs [Boolv_def,Once v_rel_cases]), prove(``v_rel Unit x <=> x = Unit``, - fs [closSemTheory.Unit_def,Once v_rel_cases])]) + fs [closSemTheory.Unit_def,Once v_rel_cases])] (* state relation *) diff --git a/compiler/backend/proofs/clos_mtiProofScript.sml b/compiler/backend/proofs/clos_mtiProofScript.sml index 58e553f5b3..d56a2b3076 100644 --- a/compiler/backend/proofs/clos_mtiProofScript.sml +++ b/compiler/backend/proofs/clos_mtiProofScript.sml @@ -444,7 +444,8 @@ val LIST_REL_f_rel_IMP = prove( \\ res_tac \\ fs [] \\ Cases_on `x` \\ Cases_on `h` \\ fs [f_rel_def]); -val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ ([ +Theorem v_rel_simps[simp] = + LIST_CONJ ([ SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel max_app x (Number n)``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel max_app x (Block n p)``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel max_app x (Word64 p)``, @@ -456,7 +457,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ ([ Cases_on `b` \\ fs [Boolv_def,Once v_rel_cases]), prove(``v_rel max_app x Unit <=> x = Unit``, fs [closSemTheory.Unit_def,Once v_rel_cases])] - |> map GEN_ALL)) + |> map GEN_ALL) val v_rel_opt_thm = prove( ``v_rel_opt m = OPTREL (v_rel m)``, diff --git a/compiler/backend/proofs/clos_ticksProofScript.sml b/compiler/backend/proofs/clos_ticksProofScript.sml index af6451d96a..ad57f18a2a 100644 --- a/compiler/backend/proofs/clos_ticksProofScript.sml +++ b/compiler/backend/proofs/clos_ticksProofScript.sml @@ -90,7 +90,8 @@ Inductive v_rel: v_rel (Recclosure loc args1 env1 funs1 k) (Recclosure loc args2 env2 funs2 k)) End -val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ +Theorem v_rel_simps[simp] = + LIST_CONJ [ SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel x (Number n)``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel x (Block n p)``, SIMP_CONV (srw_ss()) [v_rel_cases] ``v_rel x (Word64 p)``, @@ -101,7 +102,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [ prove(``v_rel x (Boolv b) <=> x = Boolv b``, Cases_on `b` \\ fs [Boolv_def,Once v_rel_cases]), prove(``v_rel x Unit <=> x = Unit``, - fs [closSemTheory.Unit_def,Once v_rel_cases])]) + fs [closSemTheory.Unit_def,Once v_rel_cases])] (* state relation *) diff --git a/compiler/backend/proofs/data_to_wordProofScript.sml b/compiler/backend/proofs/data_to_wordProofScript.sml index 4b5ae5964a..c16a8bb1fa 100644 --- a/compiler/backend/proofs/data_to_wordProofScript.sml +++ b/compiler/backend/proofs/data_to_wordProofScript.sml @@ -2620,8 +2620,8 @@ Definition stubs_fst_def: stubs_fst = ^(rconc th) End -val stubs_fst_eq = - save_thm("stubs_fst_eq",th |> REWRITE_RULE [GSYM stubs_fst_def]) +Theorem stubs_fst_eq = + th |> REWRITE_RULE [GSYM stubs_fst_def] (* The incremental version ONLY does data_to_word TODO: MAP FST stubs is independent of the data conf, diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml index f738c09bcf..5a4d711648 100644 --- a/compiler/backend/proofs/data_to_word_assignProofScript.sml +++ b/compiler/backend/proofs/data_to_word_assignProofScript.sml @@ -60,7 +60,8 @@ val eval_tac = fs [wordSemTheory.evaluate_def, wordLangTheory.word_op_def, wordLangTheory.word_sh_def] (* This list must list all auxiliary definitions used in assign_def *) -val assign_def_extras = save_thm("assign_def_extras",LIST_CONJ +Theorem assign_def_extras = + LIST_CONJ [LoadWord64_def,WriteWord64_def,BignumHalt_def,LoadBignum_def, AnyArith_code_def,Add_code_def,Sub_code_def,Mul_code_def, Div_code_def,Mod_code_def, Compare1_code_def, Compare_code_def, @@ -68,7 +69,7 @@ val assign_def_extras = save_thm("assign_def_extras",LIST_CONJ ShiftVar_def, generated_bignum_stubs_eq, DivCode_def, AddNumSize_def, AnyHeader_def, WriteWord64_on_32_def, WriteWord32_on_32_def, AllocVar_def, SilentFFI_def, - WordOp64_on_32_def, WordShift64_on_32_def, Make_ptr_bits_code_def]); + WordOp64_on_32_def, WordShift64_on_32_def, Make_ptr_bits_code_def] Theorem get_vars_SING: dataSem$get_vars args s = SOME [w] ==> ?y. args = [y] @@ -12009,9 +12010,9 @@ Proof \\ fs[] QED -val assign_ConsExtend = save_thm("assign_ConsExtend", +Theorem assign_ConsExtend = ``assign c n l dest (ConsExtend tag) args names_opt`` - |> SIMP_CONV (srw_ss()) [assign_def]) + |> SIMP_CONV (srw_ss()) [assign_def] Theorem get_vars_IMP_domain: !xs s y. diff --git a/compiler/backend/proofs/data_to_word_bignumProofScript.sml b/compiler/backend/proofs/data_to_word_bignumProofScript.sml index 510260e375..8f3e551a2f 100644 --- a/compiler/backend/proofs/data_to_word_bignumProofScript.sml +++ b/compiler/backend/proofs/data_to_word_bignumProofScript.sml @@ -41,7 +41,7 @@ val eval_tac = fs [wordSemTheory.evaluate_def, wordSemTheory.mem_load_def,wordLangTheory.word_op_def, wordLangTheory.word_sh_def] -val eq_eval = save_thm("eq_eval", +Theorem eq_eval = LIST_CONJ [wordSemTheory.evaluate_def,wordSemTheory.get_var_def, lookup_insert,wordSemTheory.get_var_imm_def,asmTheory.word_cmp_def, wordSemTheory.word_exp_def,wordSemTheory.set_var_def, @@ -49,7 +49,7 @@ val eq_eval = save_thm("eq_eval", wordSemTheory.bad_dest_args_def,wordSemTheory.get_vars_def, wordSemTheory.find_code_def,wordSemTheory.add_ret_loc_def, list_insert_def,wordSemTheory.dec_clock_def,wordSemTheory.the_words_def, - wordLangTheory.word_op_def]); + wordLangTheory.word_op_def] Theorem word_list_IMP_store_list: !xs a frame m dm. diff --git a/compiler/backend/proofs/data_to_word_gcProofScript.sml b/compiler/backend/proofs/data_to_word_gcProofScript.sml index 9c73887bab..7fab4baef3 100644 --- a/compiler/backend/proofs/data_to_word_gcProofScript.sml +++ b/compiler/backend/proofs/data_to_word_gcProofScript.sml @@ -4510,10 +4510,11 @@ Definition state_rel_thm: flat s.stack t.stack) End -val state_rel_thm = save_thm("state_rel_thm[allow_rebind]",state_rel_thm); +Theorem state_rel_thm[allow_rebind] = + state_rel_thm -val state_rel_def = save_thm("state_rel_def[allow_rebind,compute]", - state_rel_thm |> REWRITE_RULE [memory_rel_def]); +Theorem state_rel_def[allow_rebind,compute] = + state_rel_thm |> REWRITE_RULE [memory_rel_def] Theorem state_rel_with_clock: state_rel a b c s1 s2 d e ⇒ @@ -4779,8 +4780,9 @@ Proof \\ srw_tac[][] \\ BasicProvers.EVERY_CASE_TAC \\ full_simp_tac(srw_ss())[mk_loc_def] QED -val LASTN_ADD1 = save_thm("LASTN_ADD1[allow_rebind]",LASTN_LENGTH_ID - |> Q.SPEC `x::xs` |> SIMP_RULE (srw_ss()) [ADD1]); +Theorem LASTN_ADD1[allow_rebind] = + LASTN_LENGTH_ID + |> Q.SPEC `x::xs` |> SIMP_RULE (srw_ss()) [ADD1] Theorem jump_exc_push_env_NONE: mk_loc (jump_exc (dec_clock s)) = @@ -5060,7 +5062,8 @@ Theorem data_get_vars_SNOC_IMP = Q.prove(` Induct \\ full_simp_tac(srw_ss())[dataSemTheory.get_vars_def] \\ srw_tac[][] \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]) |> SPEC_ALL; -val _ = save_thm("data_get_vars_SNOC_IMP[allow_rebind]",data_get_vars_SNOC_IMP); +Theorem data_get_vars_SNOC_IMP[allow_rebind] = + data_get_vars_SNOC_IMP Theorem word_get_vars_SNOC_IMP = Q.prove(` !x2 x. wordSem$get_vars (SNOC x1 x2) s = SOME x ==> @@ -5070,7 +5073,8 @@ Theorem word_get_vars_SNOC_IMP = Q.prove(` Induct \\ full_simp_tac(srw_ss())[wordSemTheory.get_vars_def] \\ srw_tac[][] \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]) |> SPEC_ALL; -val _ = save_thm("word_get_vars_SNOC_IMP[allow_rebind]",word_get_vars_SNOC_IMP); +Theorem word_get_vars_SNOC_IMP[allow_rebind] = + word_get_vars_SNOC_IMP Theorem word_ml_inv_CodePtr: word_ml_inv (heap,be,a,sp,sp1,gens) limit ts c s.refs ((CodePtr n,v)::xs) ==> @@ -5139,7 +5143,8 @@ Theorem find_code_thm = Q.prove(` \\ `get_vars (0::MAP adjust_var x2) t = SOME (Loc l1 l2::y2')` by full_simp_tac(srw_ss())[wordSemTheory.get_vars_def] \\ imp_res_tac state_rel_call_env \\ full_simp_tac(srw_ss())[]) |> SPEC_ALL; -val _ = save_thm("find_code_thm[allow_rebind]",find_code_thm); +Theorem find_code_thm[allow_rebind] = + find_code_thm Theorem cut_env_adjust_set_lookup_0: wordSem$cut_env (adjust_set r) x = SOME y ==> lookup 0 y = lookup 0 x @@ -5322,7 +5327,8 @@ Theorem find_code_thm_ret = Q.prove(` \\ match_mp_tac (state_rel_call_env_push_env |> Q.SPEC `NONE` |> SIMP_RULE std_ss [] |> GEN_ALL) \\ full_simp_tac(srw_ss())[] \\ metis_tac []) |> SPEC_ALL; -val _ = save_thm("find_code_thm_ret[allow_rebind]",find_code_thm_ret); +Theorem find_code_thm_ret[allow_rebind] = + find_code_thm_ret Theorem find_code_thm_handler = Q.prove(` !s (t:('a,'c,'ffi)wordSem$state). @@ -5361,7 +5367,8 @@ Theorem find_code_thm_handler = Q.prove(` \\ match_mp_tac (state_rel_call_env_push_env |> Q.SPEC `SOME xx` |> SIMP_RULE std_ss [] |> GEN_ALL) \\ full_simp_tac(srw_ss())[] \\ metis_tac []) |> SPEC_ALL; -val _ = save_thm("find_code_thm_handler[allow_rebind]",find_code_thm_handler); +Theorem find_code_thm_handler[allow_rebind] = + find_code_thm_handler Theorem data_find_code: dataSem$find_code dest xs code fs = SOME(ys,prog,ss) ⇒ ¬bad_dest_args dest xs @@ -7491,13 +7498,14 @@ Proof metis_tac [alloc_fail_lemma] QED -val word_exp_rw = save_thm("word_exp_rw",LIST_CONJ +Theorem word_exp_rw = + LIST_CONJ [wordSemTheory.word_exp_def, wordLangTheory.word_op_def, wordLangTheory.word_sh_def, wordSemTheory.get_var_imm_def, wordSemTheory.the_words_def, - lookup_insert]); + lookup_insert] Theorem get_var_set_var_thm: wordSem$get_var n (set_var m x y) = if n = m then SOME x else get_var n y @@ -7949,10 +7957,10 @@ Proof metis_tac [memory_rel_get_vars_IMP_lemma] QED -val memory_rel_get_var_IMP = save_thm("memory_rel_get_var_IMP", +Theorem memory_rel_get_var_IMP = memory_rel_get_vars_IMP |> Q.INST [`n`|->`[u]`] |> GEN_ALL |> SIMP_RULE std_ss [MAP,get_vars_SOME_IFF_eq,get_vars_SOME_IFF_data_eq, - PULL_EXISTS,ZIP,APPEND]); + PULL_EXISTS,ZIP,APPEND] Theorem lookup_RefByte_location: state_rel c l1 l2 x t [] locs ==> @@ -8131,10 +8139,10 @@ Proof fs [wordSemTheory.get_vars_def] \\ every_case_tac \\ fs [] \\ EQ_TAC \\ fs [] QED -val word_ml_inv_get_var_IMP = save_thm("word_ml_inv_get_var_IMP[allow_rebind]", +Theorem word_ml_inv_get_var_IMP[allow_rebind] = word_ml_inv_get_vars_IMP |> Q.INST [`n`|->`[n1]`,`x`|->`[x1]`] |> GEN_ALL |> REWRITE_RULE [get_vars_SOME_IFF,get_vars_SOME_IFF_data,MAP] - |> SIMP_RULE std_ss [Once get_vars_sing,PULL_EXISTS,get_vars_SOME_IFF,ZIP,APPEND]); + |> SIMP_RULE std_ss [Once get_vars_sing,PULL_EXISTS,get_vars_SOME_IFF,ZIP,APPEND] val _ = export_theory(); diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml index d58137ca2d..fad9a9bc32 100644 --- a/compiler/backend/proofs/data_to_word_memoryProofScript.sml +++ b/compiler/backend/proofs/data_to_word_memoryProofScript.sml @@ -1815,11 +1815,10 @@ Proof rw [data_up_to_def, list_to_BlockReps_isDataElement] QED -val list_to_BlockReps_data_up_to = save_thm ( - "list_to_BlockReps_data_up_to", +Theorem list_to_BlockReps_data_up_to = list_to_BlockReps_data_up_to_lem |> Q.INST [`h1`|->`list_to_BlockReps conf x len xs`] - |> SIMP_RULE std_ss []); + |> SIMP_RULE std_ss [] Theorem list_to_BlockReps_ForwardPointer: xs <> [] ==> FILTER isForwardPointer (list_to_BlockReps conf x len xs) = [] @@ -1891,9 +1890,9 @@ Proof \\ CASE_TAC \\ fs [el_length_def, isSomeDataElement_def, heap_lookup_def] QED -val list_to_BlockReps_Pointer = save_thm ("list_to_BlockReps_Pointer", +Theorem list_to_BlockReps_Pointer = list_to_BlockReps_Pointer_lem - |> SIMP_RULE (srw_ss()) [LET_THM]); + |> SIMP_RULE (srw_ss()) [LET_THM] Theorem list_to_v_get_refs: !xs t r ts. @@ -2084,8 +2083,8 @@ Proof Abbr`el`, BlockRep_def, heap_lookup_def] QED -val v_inv_list_to_v = save_thm ("v_inv_list_to_v", - SIMP_RULE (srw_ss()) [LET_THM] v_inv_list_to_v_lem); +Theorem v_inv_list_to_v = + SIMP_RULE (srw_ss()) [LET_THM] v_inv_list_to_v_lem (* A timestamp that is not in the *) @@ -3448,9 +3447,9 @@ val gen_state_ok_update_byte = prove( \\ rveq \\ fs [] \\ metis_tac [MEM_APPEND]); -val heap_length_Bytes = save_thm("heap_length_Bytes", +Theorem heap_length_Bytes = EVAL``heap_length [Bytes be fl bs ws]`` - |> SIMP_RULE std_ss [LENGTH_write_bytes]); + |> SIMP_RULE std_ss [LENGTH_write_bytes] val unused_space_inv_byte_update = prove( ``unused_space_inv a (sp + sp1) @@ -4334,9 +4333,9 @@ Proof \\ full_simp_tac std_ss [reachable_refs_def,MEM_APPEND] \\ metis_tac [] QED -val duplicate1_thm = save_thm("duplicate1_thm", +Theorem duplicate1_thm = duplicate_thm |> Q.INST [`xs`|->`[x1]`,`rs`|->`[r1]`] - |> SIMP_RULE std_ss [LENGTH,APPEND]); + |> SIMP_RULE std_ss [LENGTH,APPEND] (* move *) @@ -4908,8 +4907,8 @@ Proof \\ match_mp_tac word_ml_inv_num_lemma \\ fs [] QED -val word_ml_inv_zero = save_thm("word_ml_inv_zero", - word_ml_inv_num |> Q.INST [`n`|->`0`] |> SIMP_RULE (srw_ss()) []) +Theorem word_ml_inv_zero = + word_ml_inv_num |> Q.INST [`n`|->`0`] |> SIMP_RULE (srw_ss()) [] Theorem word_ml_inv_neg_num_lemma: good_dimindex (:'a) ==> (-2w && -4w * v) = -4w * v:'a word @@ -5807,8 +5806,8 @@ Proof \\ imp_res_tac EVERY2_SWAP \\ fs[] QED -val IMP_memory_rel_bignum_alt = save_thm("IMP_memory_rel_bignum_alt", - IMP_memory_rel_bignum_alt |> Q.INST [`vs`|->`[]`] |> SIMP_RULE std_ss [APPEND]); +Theorem IMP_memory_rel_bignum_alt = + IMP_memory_rel_bignum_alt |> Q.INST [`vs`|->`[]`] |> SIMP_RULE std_ss [APPEND] Theorem memory_rel_Cons1: memory_rel c be ts refs sp st m dm (ZIP (vals,ws) ++ vars) /\ @@ -6136,13 +6135,13 @@ Proof \\ Induct_on `n` \\ fs [REPLICATE] \\ rw [] \\ fs [] QED -val memory_rel_RefArray = save_thm("memory_rel_RefArray", +Theorem memory_rel_RefArray = memory_rel_Ref |> Q.INST [`vals`|->`REPLICATE n v`,`ws`|->`REPLICATE n w`] |> SIMP_RULE std_ss [ZIP_REPLICATE,LENGTH_REPLICATE] |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> (fn th => MATCH_MP th (UNDISCH memory_rel_REPLICATE)) - |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] Definition word_of_byte_def: word_of_byte (w:'a word) = @@ -6151,9 +6150,10 @@ Definition word_of_byte_def: if dimindex (:'a) = 32 then w else w << 32 || w End -val ADD_DIV_EQ = save_thm("ADD_DIV_EQ",LIST_CONJ +Theorem ADD_DIV_EQ = + LIST_CONJ [GSYM ADD_DIV_ADD_DIV, - ONCE_REWRITE_RULE [ADD_COMM] (GSYM ADD_DIV_ADD_DIV)]) + ONCE_REWRITE_RULE [ADD_COMM] (GSYM ADD_DIV_ADD_DIV)] Triviality set_byte_word_of_byte: good_dimindex (:'a) ==> @@ -9461,11 +9461,11 @@ val fix_clock_word_eq = prove( \\ PairCases_on `x` \\ fs [] \\ fs [fix_clock_def] \\ rw [] \\ imp_res_tac word_eq_LESS_EQ \\ fs []); -val word_eq_def = save_thm("word_eq_def[compute,allow_rebind]", - word_eq_def |> REWRITE_RULE [fix_clock_word_eq]); +Theorem word_eq_def[compute,allow_rebind] = + word_eq_def |> REWRITE_RULE [fix_clock_word_eq] -val word_eq_ind = save_thm("word_eq_ind[allow_rebind]", - word_eq_ind |> REWRITE_RULE [fix_clock_word_eq]); +Theorem word_eq_ind[allow_rebind] = + word_eq_ind |> REWRITE_RULE [fix_clock_word_eq] Theorem bit_pattern_1100[simp]: good_dimindex (:'a) ==> diff --git a/compiler/backend/proofs/flat_elimProofScript.sml b/compiler/backend/proofs/flat_elimProofScript.sml index 68b65bec71..2e0376f20f 100644 --- a/compiler/backend/proofs/flat_elimProofScript.sml +++ b/compiler/backend/proofs/flat_elimProofScript.sml @@ -1603,9 +1603,9 @@ Proof \\ rfs [] QED -val flat_remove_semantics = save_thm ("flat_remove_semantics", +Theorem flat_remove_semantics = MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] IMP_semantics_eq) - flat_remove_eval_sim |> SIMP_RULE (srw_ss()) []); + flat_remove_eval_sim |> SIMP_RULE (srw_ss()) [] (* syntactic results *) diff --git a/compiler/backend/proofs/lab_to_targetProofScript.sml b/compiler/backend/proofs/lab_to_targetProofScript.sml index d125d4706d..579d3bfd5c 100644 --- a/compiler/backend/proofs/lab_to_targetProofScript.sml +++ b/compiler/backend/proofs/lab_to_targetProofScript.sml @@ -9339,7 +9339,7 @@ Proof EVAL_TAC QED -val semantics_make_init = save_thm("semantics_make_init", +Theorem semantics_make_init = machine_sem_EQ_sem |> SPEC_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH |> REWRITE_RULE [] |> SIMP_RULE std_ss [init_ok_def,PULL_EXISTS,GSYM CONJ_ASSOC,GSYM AND_IMP_INTRO] @@ -9352,7 +9352,7 @@ val semantics_make_init = save_thm("semantics_make_init", cbspace coracle` |> SIMP_RULE std_ss [make_init_simp] |> MATCH_MP (MATCH_MP IMP_LEMMA IMP_state_rel_make_init) - |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] Theorem make_init_filter_skip: semantics diff --git a/compiler/backend/proofs/word_bignumProofScript.sml b/compiler/backend/proofs/word_bignumProofScript.sml index 7b8d6ab69a..42f6f201f0 100644 --- a/compiler/backend/proofs/word_bignumProofScript.sml +++ b/compiler/backend/proofs/word_bignumProofScript.sml @@ -1224,10 +1224,10 @@ val MEM_compile = prove( \\ fs [code_subset_def] \\ rw [] \\ fs []); -val compile_NIL_IMP = save_thm("compile_NIL_IMP", +Theorem compile_NIL_IMP = MEM_compile |> Q.SPECL [`k`,`l1`,`l2`,`(l,[])`] - |> SIMP_RULE std_ss [good_code_def,MEM]); + |> SIMP_RULE std_ss [good_code_def,MEM] (* correctenss judgement *) @@ -2125,7 +2125,7 @@ val code_subset_refl = prove( val mc_iop_corr_thm = fetch "-" "mc_iop_corr_thm" -val evaluate_mc_iop = save_thm("evaluate_mc_iop", +Theorem evaluate_mc_iop = mc_iop_corr_thm |> REWRITE_RULE [Corr_def] |> UNDISCH_ALL |> MATCH_MP compile_thm @@ -2169,6 +2169,6 @@ val evaluate_mc_iop = save_thm("evaluate_mc_iop", |> Q.INST [`cs2`|->`cs`] |> SIMP_RULE std_ss [code_subset_refl] |> Q.GENL [`i1`,`i2`,`l'`,`frame`,`zs`,`t`,`ret_val`, - `n`,`l`,`iop`,`p1`,`l1`,`i'`,`cs`]); + `n`,`l`,`iop`,`p1`,`l1`,`i'`,`cs`] val _ = export_theory(); diff --git a/compiler/backend/proofs/word_to_stackProofScript.sml b/compiler/backend/proofs/word_to_stackProofScript.sml index 0b8492bbcb..43f8a80b93 100644 --- a/compiler/backend/proofs/word_to_stackProofScript.sml +++ b/compiler/backend/proofs/word_to_stackProofScript.sml @@ -2569,8 +2569,8 @@ Proof \\ rw[] QED -val with_same_locals = save_thm("with_same_locals[simp]", - EQT_ELIM(SIMP_CONV(srw_ss())[state_component_equality]``s with locals := s.locals = (s:('a,'b,'c) wordSem$state)``)); +Theorem with_same_locals[simp] = + EQT_ELIM(SIMP_CONV(srw_ss())[state_component_equality]``s with locals := s.locals = (s:('a,'b,'c) wordSem$state)``) Theorem state_rel_get_var_imp: state_rel k f f' s t lens ∧ get_var (2 * x) s = SOME v ∧ x < k ⇒ FLOOKUP t.regs x = SOME v diff --git a/compiler/backend/reg_alloc/linear_scanScript.sml b/compiler/backend/reg_alloc/linear_scanScript.sml index 369e711a1c..280a5f92fd 100644 --- a/compiler/backend/reg_alloc/linear_scanScript.sml +++ b/compiler/backend/reg_alloc/linear_scanScript.sml @@ -370,11 +370,16 @@ val int_end_manip = el 3 arr_manip; val sorted_regs_manip = el 4 arr_manip; val sorted_moves_manip = el 5 arr_manip; -val colors_accessor = save_thm("colors_accessor",accessor_thm colors_manip); -val int_beg_accessor = save_thm("int_beg_accessor",accessor_thm int_beg_manip); -val int_end_accessor = save_thm("int_end_accessor",accessor_thm int_end_manip); -val sorted_regs_accessor = save_thm("sorted_regs_accessor",accessor_thm sorted_regs_manip); -val sorted_moves_accessor = save_thm("sorted_moves_accessor",accessor_thm sorted_moves_manip); +Theorem colors_accessor = + accessor_thm colors_manip +Theorem int_beg_accessor = + accessor_thm int_beg_manip +Theorem int_end_accessor = + accessor_thm int_end_manip +Theorem sorted_regs_accessor = + accessor_thm sorted_regs_manip +Theorem sorted_moves_accessor = + accessor_thm sorted_moves_manip val colors_length_def = fetch "-" "colors_length_def"; val colors_sub_def = fetch "-" "colors_sub_def"; diff --git a/compiler/backend/reg_alloc/reg_allocScript.sml b/compiler/backend/reg_alloc/reg_allocScript.sml index eb2eee97d1..6800c430a1 100644 --- a/compiler/backend/reg_alloc/reg_allocScript.sml +++ b/compiler/backend/reg_alloc/reg_allocScript.sml @@ -122,11 +122,16 @@ val degrees_manip = el 3 arr_manip; val coalesced_manip = el 4 arr_manip; val move_related_manip = el 5 arr_manip; -val adj_ls_accessor = save_thm("adj_ls_accessor",accessor_thm adj_ls_manip); -val node_tag_accessor = save_thm("node_tag_accessor",accessor_thm node_tag_manip); -val degrees_accessor = save_thm("degrees_accessor",accessor_thm degrees_manip); -val coalesced_accessor = save_thm("coalesced_accessor",accessor_thm coalesced_manip); -val move_related_accessor = save_thm("move_related_accessor",accessor_thm move_related_manip); +Theorem adj_ls_accessor = + accessor_thm adj_ls_manip +Theorem node_tag_accessor = + accessor_thm node_tag_manip +Theorem degrees_accessor = + accessor_thm degrees_manip +Theorem coalesced_accessor = + accessor_thm coalesced_manip +Theorem move_related_accessor = + accessor_thm move_related_manip (* Helper functions for defining the allocator *) diff --git a/compiler/backend/riscv/riscv_configScript.sml b/compiler/backend/riscv/riscv_configScript.sml index 11b5253299..65e2e877c2 100644 --- a/compiler/backend/riscv/riscv_configScript.sml +++ b/compiler/backend/riscv/riscv_configScript.sml @@ -40,8 +40,8 @@ Definition riscv_names_def: insert 30 4) LN:num num_map End -val riscv_names_def = save_thm("riscv_names_def[compute,allow_rebind]", - CONV_RULE (RAND_CONV EVAL) riscv_names_def); +Theorem riscv_names_def[compute,allow_rebind] = + CONV_RULE (RAND_CONV EVAL) riscv_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/backend/semantics/bviPropsScript.sml b/compiler/backend/semantics/bviPropsScript.sml index 2c1f1f4e08..da4383870f 100644 --- a/compiler/backend/semantics/bviPropsScript.sml +++ b/compiler/backend/semantics/bviPropsScript.sml @@ -131,7 +131,8 @@ val evaluate_LENGTH = Q.prove( \\ every_case_tac \\ fs[]) |> SIMP_RULE std_ss []; -val _ = save_thm("evaluate_LENGTH", evaluate_LENGTH); +Theorem evaluate_LENGTH = + evaluate_LENGTH Theorem evaluate_IMP_LENGTH: (evaluate (xs,s,env) = (Rval res,s1)) ==> (LENGTH xs = LENGTH res) diff --git a/compiler/backend/semantics/bvlPropsScript.sml b/compiler/backend/semantics/bvlPropsScript.sml index 4fac5bc5c0..d1dcd7831a 100644 --- a/compiler/backend/semantics/bvlPropsScript.sml +++ b/compiler/backend/semantics/bvlPropsScript.sml @@ -39,7 +39,8 @@ val case_eq_thms = LIST_CONJ ``:closLang$op``,``:'a ffi_result``]) val case_eq_thms = CONJ bool_case_eq (CONJ pair_case_eq case_eq_thms) -val _ = save_thm ("case_eq_thms", case_eq_thms); +Theorem case_eq_thms = + case_eq_thms val do_app_split_list = prove( ``do_app op vs s = res @@ -54,19 +55,19 @@ Proof srw_tac[][] QED -val do_app_cases_val = save_thm ("do_app_cases_val", +Theorem do_app_cases_val = ``do_app op vs s = Rval (v,s')`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) -val do_app_cases_err = save_thm ("do_app_cases_err", -``do_app op vs s = Rerr err`` |> +Theorem do_app_cases_err = + ``do_app op vs s = Rerr err`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) Theorem do_app_Rval_swap: do_app op a (s1:('a,'b) bvlSem$state) = Rval (x0,x1) /\ op <> Install /\ @@ -216,7 +217,8 @@ val evaluate_LENGTH = Q.prove( \\ REV_FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) |> SIMP_RULE std_ss []; -val _ = save_thm("evaluate_LENGTH", evaluate_LENGTH); +Theorem evaluate_LENGTH = + evaluate_LENGTH Theorem evaluate_IMP_LENGTH: (evaluate (xs,s,env) = (Rval res,s1)) ==> (LENGTH xs = LENGTH res) diff --git a/compiler/backend/semantics/closPropsScript.sml b/compiler/backend/semantics/closPropsScript.sml index c8c7fbde02..f553780f97 100644 --- a/compiler/backend/semantics/closPropsScript.sml +++ b/compiler/backend/semantics/closPropsScript.sml @@ -519,7 +519,9 @@ QED Definition fv1_def: fv1 v e = fv v [e] End -val fv1_intro = save_thm("fv1_intro[simp]",GSYM fv1_def) + +Theorem fv1_intro[simp] = + GSYM fv1_def Theorem fv1_thm = fv_def |> SIMP_RULE (srw_ss())[] @@ -625,7 +627,8 @@ val evaluate_LENGTH = prove(evaluate_LENGTH_ind |> concl |> rand, \\ BasicProvers.EVERY_CASE_TAC \\ full_simp_tac(srw_ss())[] \\ rev_full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[]) |> SIMP_RULE std_ss [FORALL_PROD] -val _ = save_thm("evaluate_LENGTH", evaluate_LENGTH); +Theorem evaluate_LENGTH = + evaluate_LENGTH Theorem evaluate_IMP_LENGTH: (evaluate (xs,s,env) = (Rval res,s1)) ==> (LENGTH xs = LENGTH res) @@ -984,10 +987,9 @@ Theorem EVERY_pure_correct = Q.prove(` >- (every_case_tac >> full_simp_tac(srw_ss())[])) |> SIMP_RULE (srw_ss()) [] -val pure_correct = save_thm( - "pure_correct", +Theorem pure_correct = EVERY_pure_correct |> Q.SPECL [`[e]`, `env`, `s`] - |> SIMP_RULE (srw_ss()) []) + |> SIMP_RULE (srw_ss()) [] Theorem evaluate_pure: evaluate (xs,env,s) = (res,t:('c,'ffi) state) ∧ EVERY pure xs ⇒ @@ -1012,42 +1014,42 @@ val do_app_split_list = prove( ?v vs1. vs = v::vs1 /\ do_app op (v::vs1) s = res``, Cases_on `vs` \\ fs []); -val do_app_cases_val = save_thm ("do_app_cases_val", +Theorem do_app_cases_val = ``do_app op vs s = Rval (v,s')`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) -val do_app_cases_err = save_thm ("do_app_cases_err", -``do_app op vs s = Rerr (Rraise v)`` |> +Theorem do_app_cases_err = + ``do_app op vs s = Rerr (Rraise v)`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) -val do_app_cases_timeout = save_thm ("do_app_cases_timeout", -``do_app op vs s = Rerr (Rabort Rtimeout_error)`` |> +Theorem do_app_cases_timeout = + ``do_app op vs s = Rerr (Rabort Rtimeout_error)`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) (* works but huge, slow, and can't be skipped by --fast -val do_app_cases_type_error = save_thm ("do_app_cases_type_error", -``do_app op vs s = Rerr (Rabort Rtype_error)`` |> +Theorem do_app_cases_type_error = + ``do_app op vs s = Rerr (Rabort Rtype_error)`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss++boolSimps.DNF_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) *) -val do_app_cases_ffi_error = save_thm ("do_app_cases_ffi_error", -``do_app op vs s = Rerr (Rabort(Rffi_error f))`` |> +Theorem do_app_cases_ffi_error = + ``do_app op vs s = Rerr (Rabort(Rffi_error f))`` |> (ONCE_REWRITE_CONV [do_app_split_list] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, case_eq_thms, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss++boolSimps.DNF_ss) [LET_THM, case_eq_thms] THENC - ALL_CONV)); + ALL_CONV) Theorem dest_closure_none_loc: !max_app l cl vs v e env rest. @@ -1688,11 +1690,11 @@ Proof imp_res_tac do_install_type_error_add_to_clock \\ fs[] QED -val evaluate_add_clock = save_thm("evaluate_add_clock", +Theorem evaluate_add_clock = evaluate_add_to_clock |> CONJUNCT1 |> SIMP_RULE std_ss [] |> SPEC_ALL |> UNDISCH |> Q.GEN `extra` - |> DISCH_ALL |> GEN_ALL); + |> DISCH_ALL |> GEN_ALL Theorem evaluate_add_clock_initial_state: evaluate (es,env,initial_state ffi ma code co cc k) = (r,s') ∧ @@ -1883,9 +1885,8 @@ Termination rpt strip_tac >> imp_res_tac v_size_lemma >> simp[] End -val vsgc_free_def = save_thm( - "vsgc_free_def[simp,allow_rebind]", - SIMP_RULE (bool_ss ++ ETA_ss) [] vsgc_free_def) +Theorem vsgc_free_def[simp,allow_rebind] = + SIMP_RULE (bool_ss ++ ETA_ss) [] vsgc_free_def Theorem vsgc_free_Unit[simp]: vsgc_free Unit @@ -1924,8 +1925,8 @@ Termination WF_REL_TAC `measure exp_size` >> simp[] >> rpt strip_tac >> imp_res_tac exp_size_MEM >> simp[] End -val esgc_free_def = save_thm("esgc_free_def[simp,compute,allow_rebind]", - SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def) +Theorem esgc_free_def[simp,compute,allow_rebind] = + SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def (* state is setglobal-closure free *) Definition ssgc_free_def: @@ -3435,7 +3436,8 @@ Termination decide_tac End -val _ = save_thm("app_call_dests_def[simp,compute,allow_rebind]",app_call_dests_def); +Theorem app_call_dests_def[simp,compute,allow_rebind] = + app_call_dests_def Overload call_dests = ``app_call_dests (SOME T)`` Overload app_dests = ``app_call_dests (SOME F)`` @@ -3450,12 +3452,12 @@ Proof Induct \\ rw[app_call_dests_def] QED -val any_dest_cons = save_thm("any_dest_cons", - app_call_dests_cons |> Q.INST [`opt`|->`NONE`]); -val call_dest_cons = save_thm("call_dest_cons", - app_call_dests_cons |> Q.INST [`opt`|->`SOME T`]); -val app_dest_cons = save_thm("app_dest_cons", - app_call_dests_cons |> Q.INST [`opt`|->`SOME F`]); +Theorem any_dest_cons = + app_call_dests_cons |> Q.INST [`opt`|->`NONE`] +Theorem call_dest_cons = + app_call_dests_cons |> Q.INST [`opt`|->`SOME T`] +Theorem app_dest_cons = + app_call_dests_cons |> Q.INST [`opt`|->`SOME F`] Theorem app_call_dests_append: ∀l1 l2. app_call_dests opt (l1 ++ l2) = @@ -3466,12 +3468,12 @@ Proof \\ fs [AC UNION_COMM UNION_ASSOC] QED -val any_dest_append = save_thm("any_dest_append", - app_call_dests_append |> Q.INST [`opt`|->`NONE`]); -val call_dest_append = save_thm("call_dest_append", - app_call_dests_append |> Q.INST [`opt`|->`SOME T`]); -val app_dest_append = save_thm("app_dest_append", - app_call_dests_append |> Q.INST [`opt`|->`SOME F`]); +Theorem any_dest_append = + app_call_dests_append |> Q.INST [`opt`|->`NONE`] +Theorem call_dest_append = + app_call_dests_append |> Q.INST [`opt`|->`SOME T`] +Theorem app_dest_append = + app_call_dests_append |> Q.INST [`opt`|->`SOME F`] Theorem app_call_dests_map: ∀ls. app_call_dests opt (MAP f ls) = diff --git a/compiler/backend/semantics/closSemScript.sml b/compiler/backend/semantics/closSemScript.sml index 85dc9f429e..b620e5954c 100644 --- a/compiler/backend/semantics/closSemScript.sml +++ b/compiler/backend/semantics/closSemScript.sml @@ -558,7 +558,8 @@ val case_eq_thms = LIST_CONJ (CaseEq"const_part" :: map prove_case_eq_thm [op_thms, list_thms, option_thms, v_thms, ref_thms, result_thms, error_result_thms, eq_result_thms, appkind_thms, word_size_thms]) -val _ = save_thm ("case_eq_thms", case_eq_thms); +Theorem case_eq_thms = + case_eq_thms Theorem do_install_clock: do_install vs s = (Rval e,s') ⇒ 0 < s.clock ∧ s'.clock = s.clock-1 @@ -698,9 +699,8 @@ Termination \\ decide_tac End -val evaluate_app_NIL = save_thm( - "evaluate_app_NIL[simp]", - ``evaluate_app loc v [] s`` |> SIMP_CONV (srw_ss()) [evaluate_def]) +Theorem evaluate_app_NIL[simp] = + ``evaluate_app loc v [] s`` |> SIMP_CONV (srw_ss()) [evaluate_def] (* We prove that the clock never increases. *) diff --git a/compiler/backend/semantics/flatPropsScript.sml b/compiler/backend/semantics/flatPropsScript.sml index e8db326739..60f607a3a4 100644 --- a/compiler/backend/semantics/flatPropsScript.sml +++ b/compiler/backend/semantics/flatPropsScript.sml @@ -865,8 +865,8 @@ Termination \\ imp_res_tac flatLangTheory.exp_size_MEM \\ fs [] End -val esgc_free_def = save_thm("esgc_free_def[simp,compute,allow_rebind]", - SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def) +Theorem esgc_free_def[simp,compute,allow_rebind] = + SIMP_RULE (bool_ss ++ ETA_ss) [] esgc_free_def Theorem elist_globals_eq_empty: elist_globals l = {||} ⇔ ∀e. MEM e l ⇒ set_globals e = {||} diff --git a/compiler/backend/semantics/flatSemScript.sml b/compiler/backend/semantics/flatSemScript.sml index 5ea1cb991b..3fb5f84094 100644 --- a/compiler/backend/semantics/flatSemScript.sml +++ b/compiler/backend/semantics/flatSemScript.sml @@ -828,7 +828,8 @@ val eqs = LIST_CONJ (map prove_case_eq_thm [op_thms, list_thms, option_thms, v_thms, store_v_thms, lit_thms, eq_v_thms, wz_thms, result_thms, ffi_result_thms, err_thms]) -val case_eq_thms = save_thm ("case_eq_thms", eqs) +Theorem case_eq_thms = + eqs Triviality pair_case_eq: pair_CASE x f = v ⇔ ?x1 x2. x = (x1,x2) ∧ f x1 x2 = v @@ -843,11 +844,11 @@ Proof srw_tac[][] QED -val do_app_cases = save_thm ("do_app_cases", -``do_app st op vs = SOME (st',v)`` |> +Theorem do_app_cases = + ``do_app st op vs = SOME (st',v)`` |> (SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, eqs, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, eqs] THENC - ALL_CONV)); + ALL_CONV) Theorem do_app_const: do_app s op vs = SOME (s',r) ⇒ s.clock = s'.clock ∧ s.c = s'.c diff --git a/compiler/backend/stackLangScript.sml b/compiler/backend/stackLangScript.sml index 6290bde7be..11a47313f7 100644 --- a/compiler/backend/stackLangScript.sml +++ b/compiler/backend/stackLangScript.sml @@ -93,9 +93,9 @@ End Definition store_consts_stub_location_def: store_consts_stub_location = gc_stub_location-1 End -val gc_stub_location_eq = save_thm("gc_stub_location_eq", - gc_stub_location_def |> CONV_RULE(RAND_CONV EVAL)); -val store_consts_stub_location_eq = save_thm("store_consts_stub_location_eq", - store_consts_stub_location_def |> CONV_RULE(RAND_CONV EVAL)); +Theorem gc_stub_location_eq = + gc_stub_location_def |> CONV_RULE(RAND_CONV EVAL) +Theorem store_consts_stub_location_eq = + store_consts_stub_location_def |> CONV_RULE(RAND_CONV EVAL) val _ = export_theory(); diff --git a/compiler/backend/word_bignumScript.sml b/compiler/backend/word_bignumScript.sml index 1a710e5443..0888c78f19 100644 --- a/compiler/backend/word_bignumScript.sml +++ b/compiler/backend/word_bignumScript.sml @@ -410,7 +410,8 @@ val def = mc_iadd_def |> to_deep val def = mc_imul_def |> to_deep val def = mc_iop_def |> to_deep -val all_code_defs = save_thm("all_code_defs", REWRITE_RULE [] (!code_defs)); +Theorem all_code_defs = + REWRITE_RULE [] (!code_defs) (* an example that produces Rec *) @@ -571,7 +572,7 @@ Definition generated_bignum_stubs_def: (n,1n,Seq x1 (Return 0 0)) :: MAP (\(x,y,z). (y,1,Seq z (Return 0 0))) cs End -val generated_bignum_stubs_eq = save_thm("generated_bignum_stubs_eq", - EVAL ``generated_bignum_stubs n`` |> SIMP_RULE std_ss [GSYM ADD_ASSOC]); +Theorem generated_bignum_stubs_eq = + EVAL ``generated_bignum_stubs n`` |> SIMP_RULE std_ss [GSYM ADD_ASSOC] val _ = export_theory(); diff --git a/compiler/backend/x64/x64_configScript.sml b/compiler/backend/x64/x64_configScript.sml index d1a77846f4..6e52b77a71 100644 --- a/compiler/backend/x64/x64_configScript.sml +++ b/compiler/backend/x64/x64_configScript.sml @@ -33,8 +33,8 @@ Definition x64_names_def: insert 15 5) LN:num num_map End -val x64_names_def = save_thm("x64_names_def[compute,allow_rebind]", - CONV_RULE (RAND_CONV EVAL) x64_names_def); +Theorem x64_names_def[compute,allow_rebind] = + CONV_RULE (RAND_CONV EVAL) x64_names_def val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) diff --git a/compiler/bootstrap/translation/inferProgScript.sml b/compiler/bootstrap/translation/inferProgScript.sml index 22478d3fe0..4ff2c69746 100644 --- a/compiler/bootstrap/translation/inferProgScript.sml +++ b/compiler/bootstrap/translation/inferProgScript.sml @@ -250,7 +250,8 @@ Theorem ts_unify_side_def[allow_rebind] = Q.prove(` val r = translate alist_nub_def; val r = translate (ns_nub_def |> DefnBase.one_line_ify NONE); -val _ = save_thm("anub_ind",REWRITE_RULE[MEMBER_INTRO]miscTheory.anub_ind) +Theorem anub_ind = + REWRITE_RULE[MEMBER_INTRO]miscTheory.anub_ind val _ = translate (REWRITE_RULE[MEMBER_INTRO] miscTheory.anub_def) val _ = (extra_preprocessing := @@ -506,12 +507,12 @@ val inter_p_lemma1 = prove( val x_var = inter_p_lemma1 |> CONJUNCT1 |> concl |> dest_eq |> fst |> rand -val infer_p_ind = save_thm("infer_p_ind", +Theorem infer_p_ind = inferTheory.infer_p_ind |> Q.SPEC `\v1 v2 v3. !^x_var. P0 v1 v2 v3 ^x_var` |> Q.SPEC `\v1 v2 v3. !^x_var. P1 v1 v2 v3 ^x_var` |> Q.GENL [`P0`,`P1`] - |> CONV_RULE (DEPTH_CONV BETA_CONV)); + |> CONV_RULE (DEPTH_CONV BETA_CONV) val res = translate inter_p_lemma1; @@ -550,14 +551,14 @@ val inter_e_lemma1 = prove( every_case_tac \\ fs []) |> REWRITE_RULE [infer_e_lemma]; -val infer_e_ind = save_thm("infer_e_ind", +Theorem infer_e_ind = inferTheory.infer_e_ind |> Q.SPEC `\v1 v2 v3. !^x_var. P0 v1 v2 v3 ^x_var` |> Q.SPEC `\v1 v2 v3. !^x_var. P1 v1 v2 v3 ^x_var` |> Q.SPEC `\v1 v2 v3 v4 v5. !^x_var. P2 v1 v2 v3 v4 v5 ^x_var` |> Q.SPEC `\v1 v2 v3. !^x_var. P3 v1 v2 v3 ^x_var` |> Q.GENL [`P0`,`P1`,`P2`,`P3`] - |> CONV_RULE (DEPTH_CONV BETA_CONV)); + |> CONV_RULE (DEPTH_CONV BETA_CONV) val res = translate inter_e_lemma1; diff --git a/compiler/bootstrap/translation/to_bvlProgScript.sml b/compiler/bootstrap/translation/to_bvlProgScript.sml index b3d34c89a8..6ef16913dd 100644 --- a/compiler/bootstrap/translation/to_bvlProgScript.sml +++ b/compiler/bootstrap/translation/to_bvlProgScript.sml @@ -79,8 +79,8 @@ val r = translate clos_to_bvlTheory.compile_def; * Do not remove this! prove_EvalPatRel depends on it (though it should be * expanded there, not added to the simpset). *) -val _ = save_thm ("same_type_def[simp]", - semanticPrimitivesTheory.same_type_def); +Theorem same_type_def[simp] = + semanticPrimitivesTheory.same_type_def val bvl_jump_jumplist_side = Q.prove(` ∀a b. bvl_jump_jumplist_side a b ⇔ T`, diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml index 154657050a..43a852aabc 100644 --- a/compiler/bootstrap/translation/to_word32ProgScript.sml +++ b/compiler/bootstrap/translation/to_word32ProgScript.sml @@ -157,7 +157,8 @@ val Smallnum_alt = prove( val _ = translate (Smallnum_alt |> inline_simp |> conv32) val _ = translate (MemEqList_def |> inline_simp |> conv32) -val _ = save_thm("n2mw_ind",multiwordTheory.n2mw_ind |> inline_simp |> conv32); +Theorem n2mw_ind = + multiwordTheory.n2mw_ind |> inline_simp |> conv32 val _ = translate (multiwordTheory.n2mw_def |> inline_simp |> conv32); val _ = translate (multiwordTheory.i2mw_def |> inline_simp |> conv32); val _ = translate (get_Word_def |> inline_simp |> conv32); @@ -305,7 +306,8 @@ val data_to_word_assign_side = Q.prove(` metis_tac[word_op_type_nchotomy,option_nchotomy,NOT_NONE_SOME,list_distinct]) |> update_precondition *) -val _ = save_thm ("comp_ind",data_to_wordTheory.comp_ind|> conv32|> wcomp_simp) +Theorem comp_ind = + data_to_wordTheory.comp_ind|> conv32|> wcomp_simp (* Inlines the let k = 8 manually *) val _ = translate (comp_def |> conv32 |> wcomp_simp |> conv32 |> SIMP_RULE std_ss[LET_THM |> INST_TYPE [alpha|->``:num``]]); diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml index 626326de5d..c372fe0b70 100644 --- a/compiler/bootstrap/translation/to_word64ProgScript.sml +++ b/compiler/bootstrap/translation/to_word64ProgScript.sml @@ -154,7 +154,8 @@ val Smallnum_alt = prove( val _ = translate (Smallnum_alt |> inline_simp |> conv64) val _ = translate (MemEqList_def |> inline_simp |> conv64) -val _ = save_thm("n2mw_ind",multiwordTheory.n2mw_ind |> inline_simp |> conv64); +Theorem n2mw_ind = + multiwordTheory.n2mw_ind |> inline_simp |> conv64 val _ = translate (multiwordTheory.n2mw_def |> inline_simp |> conv64); val _ = translate (multiwordTheory.i2mw_def |> inline_simp |> conv64); val _ = translate (get_Word_def |> inline_simp |> conv64); @@ -295,7 +296,8 @@ val data_to_word_assign_side = Q.prove(` metis_tac[word_op_type_nchotomy,option_nchotomy,NOT_NONE_SOME,list_distinct]) |> update_precondition *) -val _ = save_thm ("comp_ind",data_to_wordTheory.comp_ind|> conv64|> wcomp_simp) +Theorem comp_ind = + data_to_wordTheory.comp_ind|> conv64|> wcomp_simp (* Inlines the let k = 8 manually *) val _ = translate (comp_def |> conv64 |> wcomp_simp |> conv64 |> SIMP_RULE std_ss[LET_THM |> INST_TYPE [alpha|->``:num``]]); diff --git a/compiler/encoders/ag32/ag32_targetScript.sml b/compiler/encoders/ag32/ag32_targetScript.sml index df67dd0387..0d374f5c8e 100644 --- a/compiler/encoders/ag32/ag32_targetScript.sml +++ b/compiler/encoders/ag32/ag32_targetScript.sml @@ -257,7 +257,9 @@ End val (ag32_config, ag32_asm_ok) = asmLib.target_asm_rwts [] ``ag32_config`` -val ag32_config = save_thm("ag32_config", ag32_config) -val ag32_asm_ok = save_thm("ag32_asm_ok", ag32_asm_ok) +Theorem ag32_config = + ag32_config +Theorem ag32_asm_ok = + ag32_asm_ok val () = export_theory () diff --git a/compiler/encoders/arm7/arm7_targetScript.sml b/compiler/encoders/arm7/arm7_targetScript.sml index 5661daf38b..86f7514b22 100644 --- a/compiler/encoders/arm7/arm7_targetScript.sml +++ b/compiler/encoders/arm7/arm7_targetScript.sml @@ -299,7 +299,9 @@ End val (arm7_config, arm7_asm_ok) = asmLib.target_asm_rwts [] ``arm7_config`` -val arm7_config = save_thm("arm7_config", arm7_config) -val arm7_asm_ok = save_thm("arm7_asm_ok", arm7_asm_ok) +Theorem arm7_config = + arm7_config +Theorem arm7_asm_ok = + arm7_asm_ok val () = export_theory () diff --git a/compiler/encoders/arm8/arm8_targetScript.sml b/compiler/encoders/arm8/arm8_targetScript.sml index 069450a137..514fad991b 100644 --- a/compiler/encoders/arm8/arm8_targetScript.sml +++ b/compiler/encoders/arm8/arm8_targetScript.sml @@ -328,8 +328,10 @@ val (arm8_config, arm8_asm_ok) = [DECIDE ``a < 32 /\ a <> 26 /\ a <> 31n <=> a <> 26 /\ a < 31``] ``arm8_config`` -val arm8_config = save_thm("arm8_config", arm8_config) -val arm8_asm_ok = save_thm("arm8_asm_ok", arm8_asm_ok) +Theorem arm8_config = + arm8_config +Theorem arm8_asm_ok = + arm8_asm_ok (* lemmas used in bootstrap translation *) diff --git a/compiler/encoders/asm/asmPropsScript.sml b/compiler/encoders/asm/asmPropsScript.sml index d94817263b..81d5bb0ea7 100644 --- a/compiler/encoders/asm/asmPropsScript.sml +++ b/compiler/encoders/asm/asmPropsScript.sml @@ -192,7 +192,8 @@ QED val all_pcs = Theory.save_thm ("all_pcs", numLib.SUC_RULE all_pcs_def) -val asserts_eval = save_thm("asserts_eval",let +Theorem asserts_eval = + let fun genlist f 0 = [] | genlist f n = genlist f (n-1) @ [f (n-1)] fun suc_num 0 = ``0:num`` @@ -200,7 +201,7 @@ val asserts_eval = save_thm("asserts_eval",let fun gen_rw n = ``asserts ^(suc_num n) next (s:'a) P Q`` |> ONCE_REWRITE_CONV [asserts_def] |> SIMP_RULE std_ss [] - in LIST_CONJ (genlist gen_rw 20) end) + in LIST_CONJ (genlist gen_rw 20) end Theorem asserts_IMP_FOLDR_COUNT_LIST: ∀n next ms P Q. asserts n next ms P Q ⇒ @@ -262,11 +263,12 @@ Proof \\ strip_tac \\ fs[] ) QED -val asserts2_eval = save_thm("asserts2_eval",let +Theorem asserts2_eval = + let fun gen_rw n = ``asserts2 ^(numSyntax.term_of_int n) fi fc (s:'a) P`` |> ONCE_REWRITE_CONV [asserts2_def] |> SIMP_RULE std_ss [] - in LIST_CONJ (List.tabulate(21,gen_rw)) end) + in LIST_CONJ (List.tabulate(21,gen_rw)) end Theorem asserts2_change_interfer: asserts2 n fi fc ms P ∧ diff --git a/compiler/encoders/mips/mips_targetScript.sml b/compiler/encoders/mips/mips_targetScript.sml index 086797789b..8163ba6241 100644 --- a/compiler/encoders/mips/mips_targetScript.sml +++ b/compiler/encoders/mips/mips_targetScript.sml @@ -340,13 +340,15 @@ Definition mips_reg_ok_def: mips_reg_ok n = ~MEM n mips_config.avoid_regs End -val mips_reg_ok = save_thm("mips_reg_ok", - GSYM (SIMP_RULE (srw_ss()) [mips_config_def] mips_reg_ok_def)) +Theorem mips_reg_ok = + GSYM (SIMP_RULE (srw_ss()) [mips_config_def] mips_reg_ok_def) val (mips_config, mips_asm_ok) = asmLib.target_asm_rwts [mips_reg_ok] ``mips_config`` -val mips_config = save_thm("mips_config", mips_config) -val mips_asm_ok = save_thm("mips_asm_ok", mips_asm_ok) +Theorem mips_config = + mips_config +Theorem mips_asm_ok = + mips_asm_ok val () = export_theory () diff --git a/compiler/encoders/monadic_enc/monadic_enc32Script.sml b/compiler/encoders/monadic_enc/monadic_enc32Script.sml index a2a36f01a2..9a66ace603 100644 --- a/compiler/encoders/monadic_enc/monadic_enc32Script.sml +++ b/compiler/encoders/monadic_enc/monadic_enc32Script.sml @@ -47,7 +47,8 @@ val arr_manip = define_MFarray_manip_funs val hash_tab_32_manip = el 1 arr_manip; -val hash_tab_32_accessor = save_thm("hash_tab_32_accessor",accessor_thm hash_tab_32_manip); +Theorem hash_tab_32_accessor = + accessor_thm hash_tab_32_manip Definition lookup_ins_table_32_def: lookup_ins_table_32 enc n a = diff --git a/compiler/encoders/monadic_enc/monadic_enc64Script.sml b/compiler/encoders/monadic_enc/monadic_enc64Script.sml index 73d83de596..67a4a87dbe 100644 --- a/compiler/encoders/monadic_enc/monadic_enc64Script.sml +++ b/compiler/encoders/monadic_enc/monadic_enc64Script.sml @@ -47,7 +47,8 @@ val arr_manip = define_MFarray_manip_funs val hash_tab_64_manip = el 1 arr_manip; -val hash_tab_64_accessor = save_thm("hash_tab_64_accessor",accessor_thm hash_tab_64_manip); +Theorem hash_tab_64_accessor = + accessor_thm hash_tab_64_manip Definition lookup_ins_table_64_def: lookup_ins_table_64 enc n a = diff --git a/compiler/encoders/riscv/riscv_targetScript.sml b/compiler/encoders/riscv/riscv_targetScript.sml index 32ced79e7f..b4719a7e03 100644 --- a/compiler/encoders/riscv/riscv_targetScript.sml +++ b/compiler/encoders/riscv/riscv_targetScript.sml @@ -308,7 +308,9 @@ End val (riscv_config, riscv_asm_ok) = asmLib.target_asm_rwts [] ``riscv_config`` -val riscv_config = save_thm("riscv_config", riscv_config) -val riscv_asm_ok = save_thm("riscv_asm_ok", riscv_asm_ok) +Theorem riscv_config = + riscv_config +Theorem riscv_asm_ok = + riscv_asm_ok val () = export_theory () diff --git a/compiler/encoders/x64/x64_targetScript.sml b/compiler/encoders/x64/x64_targetScript.sml index a36e187eb1..b5dbb23a62 100644 --- a/compiler/encoders/x64/x64_targetScript.sml +++ b/compiler/encoders/x64/x64_targetScript.sml @@ -257,7 +257,9 @@ End val (x64_config, x64_asm_ok) = asmLib.target_asm_rwts [alignmentTheory.aligned_0] ``x64_config`` -val x64_config = save_thm("x64_config", x64_config) -val x64_asm_ok = save_thm("x64_asm_ok", x64_asm_ok) +Theorem x64_config = + x64_config +Theorem x64_asm_ok = + x64_asm_ok val () = export_theory () diff --git a/compiler/inference/inferPropsScript.sml b/compiler/inference/inferPropsScript.sml index 8127ac5894..b0dc1dac17 100644 --- a/compiler/inference/inferPropsScript.sml +++ b/compiler/inference/inferPropsScript.sml @@ -536,7 +536,8 @@ val constrain_op_success = PULL_EXISTS] ) -val _ = save_thm ("constrain_op_success", constrain_op_success); +Theorem constrain_op_success = + constrain_op_success Triviality get_next_uvar_success: !st v st'. @@ -716,7 +717,8 @@ val success_eqns = check_ctor_types_success, check_ctors_success]; -val _ = save_thm ("success_eqns", success_eqns); +Theorem success_eqns = + success_eqns Theorem remove_pair_lem: (!f v. (\(x,y). f x y) v = f (FST v) (SND v)) ∧ diff --git a/compiler/inference/unifyScript.sml b/compiler/inference/unifyScript.sml index 4891fd6731..9433b23a7a 100644 --- a/compiler/inference/unifyScript.sml +++ b/compiler/inference/unifyScript.sml @@ -2064,7 +2064,8 @@ qpat_x_assum `∀u. Q u ⇒ P u` ho_match_mp_tac >> rw [FLOOKUP_o_f, encode_infer_t_def] QED -val t_vwalk_ind = save_thm("t_vwalk_ind", (UNDISCH o Q.SPEC `s`) t_vwalk_ind') +Theorem t_vwalk_ind = + (UNDISCH o Q.SPEC `s`) t_vwalk_ind' Theorem t_vwalk_eqn: !s. @@ -2777,7 +2778,8 @@ rw [] >> metis_tac [t_unify_unifier] QED -val t_unify_strongind = save_thm("t_unify_strongind", SIMP_RULE (bool_ss) [] t_unify_strongind'); +Theorem t_unify_strongind = + SIMP_RULE (bool_ss) [] t_unify_strongind' Triviality encode_walkstar: !s t. diff --git a/compiler/parsing/cmlPEGScript.sml b/compiler/parsing/cmlPEGScript.sml index df150d1198..dd828c28a9 100644 --- a/compiler/parsing/cmlPEGScript.sml +++ b/compiler/parsing/cmlPEGScript.sml @@ -554,13 +554,12 @@ in ths end -val FDOM_cmlPEG = save_thm( - "FDOM_cmlPEG", +Theorem FDOM_cmlPEG = SIMP_CONV (srw_ss()) [cmlPEG_def, finite_mapTheory.FRANGE_FUPDATE_DOMSUB, finite_mapTheory.DOMSUB_FUPDATE_THM, finite_mapTheory.FUPDATE_LIST_THM] - ``FDOM cmlPEG.rules``); + ``FDOM cmlPEG.rules`` val spec0 = peg_nt_thm |> Q.GEN `G` |> Q.ISPEC `cmlPEG` @@ -749,9 +748,8 @@ val topo_nts = [“nV”, “nTyvarN”, “nTypeDec”, “nTypeAbbrevDec”, “nTopLevelDecs”, “nNonETopLevelDecs” ] -val cml_wfpeg_thm = save_thm( - "cml_wfpeg_thm", - LIST_CONJ (List.foldl wfnt [] topo_nts)) +Theorem cml_wfpeg_thm = + LIST_CONJ (List.foldl wfnt [] topo_nts) (* set_diff (TypeBase.constructors_of ``:MMLnonT``) @@ -765,8 +763,7 @@ Proof simp[subexprs_def, pnt_def] QED -val PEG_exprs = save_thm( - "PEG_exprs", +Theorem PEG_exprs = ``Gexprs cmlPEG`` |> SIMP_CONV (srw_ss()) [Gexprs_def, subexprs_def, @@ -775,7 +772,7 @@ val PEG_exprs = save_thm( peg_longV_def, peg_linfix_def, peg_StructName_def, peg_TypeDec_def, peg_UQConstructorName_def, pred_setTheory.INSERT_UNION_EQ - ]) + ] Theorem PEG_wellformed[simp]: wfG cmlPEG @@ -789,19 +786,16 @@ Proof simp(cml_wfpeg_thm :: wfpeg_rwts @ peg0_rwts @ npeg0_rwts) QED -val parse_TopLevelDecs_total = save_thm( - "parse_TopLevelDecs_total", +Theorem parse_TopLevelDecs_total = MATCH_MP peg_exec_total PEG_wellformed - |> REWRITE_RULE [peg_start] |> Q.GEN `i`); + |> REWRITE_RULE [peg_start] |> Q.GEN `i` -val coreloop_TopLevelDecs_total = save_thm( - "coreloop_TopLevelDecs_total", +Theorem coreloop_TopLevelDecs_total = MATCH_MP coreloop_total PEG_wellformed - |> REWRITE_RULE [peg_start] |> Q.GEN `i`); + |> REWRITE_RULE [peg_start] |> Q.GEN `i` -val owhile_TopLevelDecs_total = save_thm( - "owhile_TopLevelDecs_total", - SIMP_RULE (srw_ss()) [coreloop_def] coreloop_TopLevelDecs_total); +Theorem owhile_TopLevelDecs_total = + SIMP_RULE (srw_ss()) [coreloop_def] coreloop_TopLevelDecs_total local val c = concl FDOM_cmlPEG diff --git a/compiler/parsing/ocaml/camlPEGScript.sml b/compiler/parsing/ocaml/camlPEGScript.sml index a4448f12bb..97bb03c0b2 100644 --- a/compiler/parsing/ocaml/camlPEGScript.sml +++ b/compiler/parsing/ocaml/camlPEGScript.sml @@ -842,13 +842,12 @@ in ths end -val FDOM_camlPEG = save_thm( - "FDOM_camlPEG", +Theorem FDOM_camlPEG = SIMP_CONV (srw_ss()) [camlPEG_def, finite_mapTheory.FRANGE_FUPDATE_DOMSUB, finite_mapTheory.DOMSUB_FUPDATE_THM, finite_mapTheory.FUPDATE_LIST_THM] - ``FDOM camlPEG.rules``); + ``FDOM camlPEG.rules`` val spec0 = peg_nt_thm |> Q.GEN `G` |> Q.ISPEC `camlPEG` @@ -1072,9 +1071,8 @@ val topo_nts = “nCakeMLPragma”, “nModuleTypeDef”, “nModExpr”, “nDefinition”, “nDefItem”, “nModuleItem”, “nModuleItems”, “nStart”]; -val cml_wfpeg_thm = save_thm( - "cml_wfpeg_thm", - LIST_CONJ (List.foldl wfnt [] topo_nts)) +Theorem cml_wfpeg_thm = + LIST_CONJ (List.foldl wfnt [] topo_nts) Triviality subexprs_pnt: subexprs (pnt n) = {pnt n} diff --git a/examples/bot/compile/x64/bot_x64CompileScript.sml b/examples/bot/compile/x64/bot_x64CompileScript.sml index 0b927dfb3e..4e0733df2d 100644 --- a/examples/bot/compile/x64/bot_x64CompileScript.sml +++ b/examples/bot/compile/x64/bot_x64CompileScript.sml @@ -20,7 +20,8 @@ max_print_depth := 10 val _ = intermediate_prog_prefix := "bot_"; (* Produce .S files *) -val x64 = save_thm("bot_x64", compile_x64 500 500 (folder_str ^ "/bot_x64") bot_prog_def); +Theorem bot_x64 = + compile_x64 500 500 (folder_str ^ "/bot_x64") bot_prog_def val _ = intermediate_prog_prefix := ""; diff --git a/examples/catProgScript.sml b/examples/catProgScript.sml index c3b7d963af..8edf8aa9ec 100644 --- a/examples/catProgScript.sml +++ b/examples/catProgScript.sml @@ -214,9 +214,8 @@ Proof simp[file_contents_add_stdout] \\ xsimpl QED -val cat_spec = save_thm( - "cat_spec", - cat_spec0 |> SIMP_RULE (srw_ss()) []) +Theorem cat_spec = + cat_spec0 |> SIMP_RULE (srw_ss()) [] val _ = process_topdecs ` fun cat1 f = diff --git a/examples/diffProgScript.sml b/examples/diffProgScript.sml index f95eed14fb..950123d619 100644 --- a/examples/diffProgScript.sml +++ b/examples/diffProgScript.sml @@ -205,9 +205,9 @@ Definition diff_prog_def: diff_prog = ^prog_tm End -val diff_semantics = save_thm("diff_semantics", +Theorem diff_semantics = sem_thm |> REWRITE_RULE[GSYM diff_prog_def] |> DISCH_ALL - |> SIMP_RULE(srw_ss())[GSYM CONJ_ASSOC,AND_IMP_INTRO]); + |> SIMP_RULE(srw_ss())[GSYM CONJ_ASSOC,AND_IMP_INTRO] val _ = export_theory (); diff --git a/examples/divScript.sml b/examples/divScript.sml index 163f5b6613..a7009e24e9 100644 --- a/examples/divScript.sml +++ b/examples/divScript.sml @@ -532,7 +532,8 @@ Proof \\ irule REPLICATE_LIST_LREPEAT \\ fs [] QED -val yes_spec = save_thm("yes_spec", yes_spec_lemma |> SPEC_ALL |> UNDISCH_ALL); +Theorem yes_spec = + yes_spec_lemma |> SPEC_ALL |> UNDISCH_ALL (* An IO-conditional loop with side effects *) diff --git a/examples/echoProgScript.sml b/examples/echoProgScript.sml index b93c506eff..15410f0266 100644 --- a/examples/echoProgScript.sml +++ b/examples/echoProgScript.sml @@ -66,9 +66,9 @@ Definition echo_prog_def: echo_prog = ^echo_prog_tm End -val echo_semantics = save_thm("echo_semantics", +Theorem echo_semantics = call_thm_echo |> ONCE_REWRITE_RULE[GSYM echo_prog_def] |> DISCH_ALL - |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC] val _ = export_theory(); diff --git a/examples/filterProgScript.sml b/examples/filterProgScript.sml index 7d3223aae2..d002e9f854 100644 --- a/examples/filterProgScript.sml +++ b/examples/filterProgScript.sml @@ -23,12 +23,11 @@ val _ = translation_extends"MapProg"; val regexp_compilation_results as {certificate, aux, ...} = regexpLib.gen_dfa regexpLib.HOL (Regexp_Type.fromString the_regexp); -val matcher_certificate = save_thm - ("matcher_certificate", - certificate +Theorem matcher_certificate = + certificate |> valOf |> CONV_RULE(QUANT_CONV(LHS_CONV (REWRITE_CONV [MAP]))) -); + (*---------------------------------------------------------------------------*) (* Define a named matcher function *) diff --git a/examples/grepProgScript.sml b/examples/grepProgScript.sml index 256c1dad2d..3cb6bd04b6 100644 --- a/examples/grepProgScript.sml +++ b/examples/grepProgScript.sml @@ -126,7 +126,8 @@ val _ = translate balanced_mapTheory.fromList_def; val r = translate regexp_compareW_def; val _ = add_preferred_thy "-"; -val r = save_thm("mergesortN_ind", mergesortTheory.mergesortN_ind |> REWRITE_RULE[GSYM mllistTheory.drop_def]); +Theorem mergesortN_ind = + mergesortTheory.mergesortN_ind |> REWRITE_RULE[GSYM mllistTheory.drop_def] val r = translate (mergesortTheory.mergesortN_def |> REWRITE_RULE[GSYM mllistTheory.drop_def]); val _ = use_mem_intro := true; @@ -1027,8 +1028,8 @@ Definition grep_prog_def: grep_prog = ^prog_tm End -val grep_semantics = save_thm("grep_semantics", +Theorem grep_semantics = sem_thm |> REWRITE_RULE[GSYM grep_prog_def] - |> DISCH_ALL |> SIMP_RULE(srw_ss())[AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> DISCH_ALL |> SIMP_RULE(srw_ss())[AND_IMP_INTRO,GSYM CONJ_ASSOC] val _ = export_theory (); diff --git a/examples/helloErrProgScript.sml b/examples/helloErrProgScript.sml index df4ea1b299..c98252d528 100644 --- a/examples/helloErrProgScript.sml +++ b/examples/helloErrProgScript.sml @@ -50,8 +50,8 @@ Definition helloErr_prog_def: helloErr_prog = ^helloErr_prog_tm End -val helloErr_semantics = save_thm("helloErr_semantics", +Theorem helloErr_semantics = helloErr_sem_thm |> ONCE_REWRITE_RULE[GSYM helloErr_prog_def] - |> DISCH_ALL |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> DISCH_ALL |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC] val _ = export_theory () diff --git a/examples/helloProgScript.sml b/examples/helloProgScript.sml index 31cd51c71f..2f1e90f5da 100644 --- a/examples/helloProgScript.sml +++ b/examples/helloProgScript.sml @@ -43,8 +43,8 @@ Definition hello_prog_def: hello_prog = ^hello_prog_tm End -val hello_semantics = save_thm("hello_semantics", +Theorem hello_semantics = call_thm_hello |> ONCE_REWRITE_RULE[GSYM hello_prog_def] - |> DISCH_ALL |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC]); + |> DISCH_ALL |> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC] val _ = export_theory () diff --git a/examples/opentheory/monadIO/compilation/readerIOCompileScript.sml b/examples/opentheory/monadIO/compilation/readerIOCompileScript.sml index fdec3b20d3..39692809b5 100644 --- a/examples/opentheory/monadIO/compilation/readerIOCompileScript.sml +++ b/examples/opentheory/monadIO/compilation/readerIOCompileScript.sml @@ -5,7 +5,7 @@ open preamble compilationLib readerIOProgTheory val _ = new_theory "readerIOCompile" -val readerIO_compiled = save_thm("readerIO_compiled", - compile_x64 "readerIO" readerIO_prog_def); +Theorem readerIO_compiled = + compile_x64 "readerIO" readerIO_prog_def val _ = export_theory (); diff --git a/examples/opentheory/monadIO/readerIOProgScript.sml b/examples/opentheory/monadIO/readerIOProgScript.sml index f74454cf94..0c472445a2 100644 --- a/examples/opentheory/monadIO/readerIOProgScript.sml +++ b/examples/opentheory/monadIO/readerIOProgScript.sml @@ -22,11 +22,11 @@ val _ = m_translation_extends "reader_commonProg" val r = m_translate readLine_wrap_def val r = m_translate init_reader_wrap_def -val init_reader_wrap_spec = save_thm ("init_reader_wrap_spec", - mk_app_of_ArrowP (theorem "init_reader_wrap_v_thm")); +Theorem init_reader_wrap_spec = + mk_app_of_ArrowP (theorem "init_reader_wrap_v_thm") -val readline_wrap_spec = save_thm ("readline_wrap_spec", - mk_app_of_ArrowP (theorem "readline_wrap_v_thm")); +Theorem readline_wrap_spec = + mk_app_of_ArrowP (theorem "readline_wrap_v_thm") (* ------------------------------------------------------------------------- *) (* Set up translation to 'resume' from reader_commonProg *) @@ -330,8 +330,8 @@ val readMain_side = Q.prove ( \\ imp_res_tac EVERY_TL \\ rfs [clFFITheory.validArg_def]) |> update_precondition; -val readMain_spec = save_thm ("readMain_spec", - cfMonadLib.mk_app_of_ArrowP (theorem "readmain_v_thm")); +Theorem readMain_spec = + cfMonadLib.mk_app_of_ArrowP (theorem "readmain_v_thm") Theorem readMain_spec_wp: wfcl st.cl /\ diff --git a/examples/opentheory/reader_commonProgScript.sml b/examples/opentheory/reader_commonProgScript.sml index 5cead5675b..3e21d4ccc1 100644 --- a/examples/opentheory/reader_commonProgScript.sml +++ b/examples/opentheory/reader_commonProgScript.sml @@ -96,8 +96,8 @@ val r = translate stringTheory.isDigit_def; val _ = (use_mem_intro := true); val _ = translate rev_assocd_def -val tymatch_ind = save_thm ("tymatch_ind", - REWRITE_RULE [GSYM rev_assocd_thm] holSyntaxExtraTheory.tymatch_ind); +Theorem tymatch_ind = + REWRITE_RULE [GSYM rev_assocd_thm] holSyntaxExtraTheory.tymatch_ind val _ = add_preferred_thy"-"; val r = holSyntaxExtraTheory.tymatch_def |> REWRITE_RULE [GSYM rev_assocd_thm] diff --git a/examples/patchProgScript.sml b/examples/patchProgScript.sml index 7ebe81d9f0..b7a74f6099 100644 --- a/examples/patchProgScript.sml +++ b/examples/patchProgScript.sml @@ -90,9 +90,9 @@ val depatch_line_side = Q.prove( `∀x. depatch_line_side x = T`, EVAL_TAC \\ rw[]) |> update_precondition; -val r = save_thm("patch_aux_ind", +Theorem patch_aux_ind = patch_aux_ind |> REWRITE_RULE (map GSYM [mllistTheory.take_def, - mllistTheory.drop_def])); + mllistTheory.drop_def]) val _ = add_preferred_thy"-"; val _ = translate(patch_aux_def |> REWRITE_RULE (map GSYM [mllistTheory.take_def, mllistTheory.drop_def])); @@ -243,9 +243,9 @@ Definition patch_prog_def: patch_prog = ^prog_tm End -val patch_semantics = save_thm("patch_semantics", +Theorem patch_semantics = sem_thm |> REWRITE_RULE[GSYM patch_prog_def] |> DISCH_ALL - |> SIMP_RULE(srw_ss())[GSYM CONJ_ASSOC,AND_IMP_INTRO]); + |> SIMP_RULE(srw_ss())[GSYM CONJ_ASSOC,AND_IMP_INTRO] val _ = export_theory (); diff --git a/misc/miscScript.sml b/misc/miscScript.sml index 11b9c4e90c..43df11e097 100644 --- a/misc/miscScript.sml +++ b/misc/miscScript.sml @@ -37,7 +37,8 @@ val asm_exists_tac = first_assum(match_exists_tac o concl) val _ = numLib.temp_prefer_num(); (* theorem behind impl_tac *) -val IMP_IMP = save_thm("IMP_IMP",METIS_PROVE[]``(P /\ (Q ==> R)) ==> ((P ==> Q) ==> R)``); +Theorem IMP_IMP = + METIS_PROVE[]``(P /\ (Q ==> R)) ==> ((P ==> Q) ==> R)`` (* used elsewhere in cakeml *) Theorem SUBSET_IMP: @@ -166,12 +167,18 @@ QED Overload LLOOKUP = “λl n. oEL n l” -val LLOOKUP_def = save_thm("LLOOKUP_def", listTheory.oEL_def); -val LLOOKUP_EQ_EL = save_thm("LLOOKUP_EQ_EL", listTheory.oEL_EQ_EL); -val LLOOKUP_THM = save_thm("LLOOKUP_THM", listTheory.oEL_THM); -val LLOOOKUP_DROP = save_thm("LLOOKUP_DROP", listTheory.oEL_DROP); -val LLOOKUP_TAKE_IMP = save_thm("LLOOKUP_TAKE_IMP", listTheory.oEL_TAKE_E); -val LLOOKUP_LUPDATE = save_thm("LLOOKUP_LUPDATE", listTheory.oEL_LUPDATE); +Theorem LLOOKUP_def = + listTheory.oEL_def +Theorem LLOOKUP_EQ_EL = + listTheory.oEL_EQ_EL +Theorem LLOOKUP_THM = + listTheory.oEL_THM +Theorem LLOOKUP_DROP = + listTheory.oEL_DROP +Theorem LLOOKUP_TAKE_IMP = + listTheory.oEL_TAKE_E +Theorem LLOOKUP_LUPDATE = + listTheory.oEL_LUPDATE (* app_list stuff should be in an app_list theory *) Datatype: @@ -1775,10 +1782,10 @@ Proof \\ MP_TAC (Q.SPEC `x::xs` LASTN_LENGTH_ID) \\ full_simp_tac(srw_ss())[ADD1] QED -val LASTN_TL = save_thm("LASTN_TL", +Theorem LASTN_TL = LASTN_CONS |> Q.SPECL[`n+1`,`xs`] |> C MP (DECIDE``n < LENGTH xs ⇒ n + 1 ≤ LENGTH xs`` |> UNDISCH) - |> SPEC_ALL |> DISCH_ALL); + |> SPEC_ALL |> DISCH_ALL Theorem LASTN_LENGTH_LESS_EQ: !xs n. LENGTH xs <= n ==> LASTN n xs = xs @@ -1815,8 +1822,8 @@ Proof QED (* NB: this is weaker: -val MAP_EQ_MAP_IMP = save_thm("MAP_EQ_MAP_IMP", - INJ_MAP_EQ |> SIMP_RULE (srw_ss()) [INJ_DEF]); +Theorem MAP_EQ_MAP_IMP = + INJ_MAP_EQ |> SIMP_RULE (srw_ss()) [INJ_DEF] *) Theorem INJ_MAP_EQ_2: @@ -2608,9 +2615,8 @@ Proof Induct_on `l` >> simp[findi_def, bool_case_eq, ADD1] >> metis_tac[] QED -val NOT_MEM_findi = save_thm( (* more useful as conditional rewrite *) - "NOT_MEM_findi", - NOT_MEM_findi_IFF |> EQ_IMP_RULE |> #1); +Theorem NOT_MEM_findi = + NOT_MEM_findi_IFF |> EQ_IMP_RULE |> #1 Theorem ORD_eq_0: (ORD c = 0 ⇔ c = CHR 0) ∧ (0 = ORD c ⇔ c = CHR 0) @@ -3061,8 +3067,8 @@ rw[FUN_EQ_THM] QED (* used once *) -val SUM_COUNT_LIST = save_thm("SUM_COUNT_LIST", - SUM_MAP_COUNT_LIST |> Q.SPECL [`n`,`0`] |> SIMP_RULE (srw_ss()) []); +Theorem SUM_COUNT_LIST = + SUM_MAP_COUNT_LIST |> Q.SPECL [`n`,`0`] |> SIMP_RULE (srw_ss()) [] Theorem OPTION_MAP_I[simp]: OPTION_MAP I x = x @@ -3234,11 +3240,11 @@ Proof rw[] \\ Cases_on `x` \\ Cases_on `y` \\ fs[] QED -val _ = save_thm("option_eq_some", - LIST_CONJ [ +Theorem option_eq_some = + LIST_CONJ [ OPTION_IGNORE_BIND_EQUALS_OPTION, OPTION_BIND_EQUALS_OPTION, - OPTION_CHOICE_EQUALS_OPTION]); + OPTION_CHOICE_EQUALS_OPTION] Theorem ALL_DISTINCT_alist_to_fmap_REVERSE: ALL_DISTINCT (MAP FST ls) ⇒ alist_to_fmap (REVERSE ls) = alist_to_fmap ls @@ -3398,8 +3404,8 @@ Proof \\ srw_tac [] [ADD1] QED -val IN_EVEN = - save_thm("IN_EVEN", SIMP_CONV std_ss [IN_DEF] ``x ∈ EVEN``); +Theorem IN_EVEN = + SIMP_CONV std_ss [IN_DEF] ``x ∈ EVEN`` Theorem FOLDL_OPTION_CHOICE_EQ_SOME_IMP_MEM: FOLDL OPTION_CHOICE x ls = SOME y ⇒ MEM (SOME y) (x::ls) diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index 379b71c554..7ea4357001 100644 --- a/pancake/parser/panPEGScript.sml +++ b/pancake/parser/panPEGScript.sml @@ -337,13 +337,12 @@ Definition pancake_peg_def[nocompute]: End (** Compute pancake parser domain lookup function. *) -val FDOM_pancake_peg = save_thm( - "FDOM_pancake_peg", +Theorem FDOM_pancake_peg = SIMP_CONV (srw_ss()) [pancake_peg_def, finite_mapTheory.FRANGE_FUPDATE_DOMSUB, finite_mapTheory.DOMSUB_FUPDATE_THM, finite_mapTheory.FUPDATE_LIST_THM] - ``FDOM pancake_peg.rules``); + ``FDOM pancake_peg.rules`` val pancake_peg_nt_thm = @@ -687,13 +686,11 @@ end; (** This time include the top-level program non-terminal which is * well-formed. *) -val pancake_wfpeg_thm = save_thm( - "pancake_wfpeg_thm", - LIST_CONJ (List.foldl (wfnt “pancake_peg”) [] (topo_nts @ [“ProgNT”, “FunListNT”]))) +Theorem pancake_wfpeg_thm = + LIST_CONJ (List.foldl (wfnt “pancake_peg”) [] (topo_nts @ [“ProgNT”, “FunListNT”])) -val pancake_wfpeg_thm2 = save_thm( - "pancake_wfpeg_FunNT_thm", - LIST_CONJ (List.foldl (wfnt “pancake_peg with start := mknt FunNT”) [] (topo_nts @ [“ProgNT”]))) +Theorem pancake_wfpeg_FunNT_thm = + LIST_CONJ (List.foldl (wfnt “pancake_peg with start := mknt FunNT”) [] (topo_nts @ [“ProgNT”])) Triviality subexprs_mknt: subexprs (mknt n) = {mknt n} diff --git a/pancake/semantics/crepSemScript.sml b/pancake/semantics/crepSemScript.sml index 0d015f08de..4848f5ef71 100644 --- a/pancake/semantics/crepSemScript.sml +++ b/pancake/semantics/crepSemScript.sml @@ -369,11 +369,11 @@ Proof \\ imp_res_tac evaluate_clock \\ fs [GSYM NOT_LESS, state_component_equality] QED -val evaluate_ind = save_thm("evaluate_ind[allow_rebind]", - REWRITE_RULE [fix_clock_evaluate] evaluate_ind); +Theorem evaluate_ind[allow_rebind] = + REWRITE_RULE [fix_clock_evaluate] evaluate_ind -val evaluate_def = save_thm("evaluate_def[allow_rebind,compute]", - REWRITE_RULE [fix_clock_evaluate] evaluate_def); +Theorem evaluate_def[allow_rebind,compute] = + REWRITE_RULE [fix_clock_evaluate] evaluate_def (* observational semantics *) diff --git a/pancake/semantics/panSemScript.sml b/pancake/semantics/panSemScript.sml index 344afe9875..e0c1d75d57 100644 --- a/pancake/semantics/panSemScript.sml +++ b/pancake/semantics/panSemScript.sml @@ -551,11 +551,11 @@ Proof QED (* we save evaluate theorems without fix_clock *) -val evaluate_ind = save_thm("evaluate_ind[allow_rebind]", - REWRITE_RULE [fix_clock_evaluate] evaluate_ind); +Theorem evaluate_ind[allow_rebind] = + REWRITE_RULE [fix_clock_evaluate] evaluate_ind -val evaluate_def = save_thm("evaluate_def[allow_rebind,compute]", - REWRITE_RULE [fix_clock_evaluate] evaluate_def); +Theorem evaluate_def[allow_rebind,compute] = + REWRITE_RULE [fix_clock_evaluate] evaluate_def (* observational semantics *) diff --git a/semantics/proofs/cmlPtreeConversionPropsScript.sml b/semantics/proofs/cmlPtreeConversionPropsScript.sml index b0a569113f..ae3f9d5d7b 100644 --- a/semantics/proofs/cmlPtreeConversionPropsScript.sml +++ b/semantics/proofs/cmlPtreeConversionPropsScript.sml @@ -345,7 +345,8 @@ fun okify c q th = |> SIMP_RULE (srw_ss()) [] |> DISCH_ALL |> SIMP_RULE (srw_ss()) [AND_IMP_INTRO, GSYM CONJ_ASSOC] -val Type_OK = save_thm("Type_OK", okify CONJUNCT1 `nType` Type_OK0); +Theorem Type_OK = + okify CONJUNCT1 `nType` Type_OK0 Theorem V_OK: valid_ptree cmlG pt ∧ ptree_head pt = NT (mkNT nV) ∧ @@ -468,7 +469,8 @@ Proof >- (irule V_OK \\ gs [SF SFY_ss]) QED -val Pattern_OK = save_thm("Pattern_OK", okify CONJUNCT1 `nPattern` Pattern_OK0); +Theorem Pattern_OK = + okify CONJUNCT1 `nPattern` Pattern_OK0 Theorem Eseq_encode_OK: ∀l. l <> [] ⇒ ∃e. Eseq_encode l = SOME e @@ -584,10 +586,10 @@ Proof asm_match `0 < LENGTH pl` >> Cases_on `pl` >> fs[oHD_def] >> std) QED -val E_OK = save_thm("E_OK", okify CONJUNCT1 `nE` E_OK0) -val AndFDecls_OK = save_thm( - "AndFDecls_OK", - okify (last o #1 o front_last o CONJUNCTS) `v` E_OK0); +Theorem E_OK = + okify CONJUNCT1 `nE` E_OK0 +Theorem AndFDecls_OK = + okify (last o #1 o front_last o CONJUNCTS) `v` E_OK0 Theorem PTbase_OK: valid_ptree cmlG pt ∧ ptree_head pt = NN nPTbase ∧ diff --git a/semantics/proofs/gramPropsScript.sml b/semantics/proofs/gramPropsScript.sml index 8270fd382d..1dc50740b8 100644 --- a/semantics/proofs/gramPropsScript.sml +++ b/semantics/proofs/gramPropsScript.sml @@ -138,8 +138,8 @@ in save_thm("cmlG_applied", LIST_CONJ ths) end -val cmlG_FDOM = save_thm("cmlG_FDOM", - SIMP_CONV (srw_ss()) [cmlG_def] ``FDOM cmlG.rules``) +Theorem cmlG_FDOM = + SIMP_CONV (srw_ss()) [cmlG_def] ``FDOM cmlG.rules`` Triviality paireq: (x,y) = z ⇔ x = FST z ∧ y = SND z @@ -346,8 +346,7 @@ Proof simp[stringTheory.isUpper_def] QED -val parsing_ind = save_thm( - "parsing_ind", +Theorem parsing_ind = relationTheory.WF_INDUCTION_THM |> Q.ISPEC `inv_image (measure (LENGTH:((token,MMLnonT)grammar$symbol # locs) list @@ -357,6 +356,6 @@ val parsing_ind = save_thm( (λpt. (real_fringe pt, ptree_head pt))` |> SIMP_RULE (srw_ss()) [pairTheory.WF_LEX, relationTheory.WF_inv_image] |> SIMP_RULE (srw_ss()) [relationTheory.inv_image_def, - pairTheory.LEX_DEF]); + pairTheory.LEX_DEF] val _ = export_theory() diff --git a/semantics/proofs/primSemEnvScript.sml b/semantics/proofs/primSemEnvScript.sml index a859660937..e20c15902b 100644 --- a/semantics/proofs/primSemEnvScript.sml +++ b/semantics/proofs/primSemEnvScript.sml @@ -17,8 +17,8 @@ open typeSysPropsTheory; val _ = new_theory "primSemEnv"; -val prim_sem_env_eq = save_thm ("prim_sem_env_eq", - EVAL ``prim_sem_env (ffi:'ffi ffi_state)``); +Theorem prim_sem_env_eq = + EVAL ``prim_sem_env (ffi:'ffi ffi_state)`` Theorem prim_type_sound_invariants: ∀type_ids sem_st prim_env. diff --git a/semantics/proofs/semanticPrimitivesPropsScript.sml b/semantics/proofs/semanticPrimitivesPropsScript.sml index a944cda138..9c2b0065e7 100644 --- a/semantics/proofs/semanticPrimitivesPropsScript.sml +++ b/semantics/proofs/semanticPrimitivesPropsScript.sml @@ -246,11 +246,11 @@ Proof srw_tac[][] QED -val do_app_cases = save_thm ("do_app_cases", -``do_app (s,t) op vs = SOME (st',v)`` |> +Theorem do_app_cases = + ``do_app (s,t) op vs = SOME (st',v)`` |> (SIMP_CONV (srw_ss()++COND_elim_ss) [PULL_EXISTS, do_app_def, eqs, pair_case_eq, pair_lam_lem] THENC SIMP_CONV (srw_ss()++COND_elim_ss) [LET_THM, eqs] THENC - ALL_CONV)); + ALL_CONV) Theorem do_opapp_cases: ∀env' vs v. diff --git a/semantics/proofs/typeSysPropsScript.sml b/semantics/proofs/typeSysPropsScript.sml index 92b7d1a1c7..7def506f29 100644 --- a/semantics/proofs/typeSysPropsScript.sml +++ b/semantics/proofs/typeSysPropsScript.sml @@ -916,11 +916,11 @@ val thms = [ op_thms, list_thms, t_thms, word_size_thms, id_thms ]; val eqs = ([pair_case_eq,bool_case_eq]@(List.map prove_case_eq_thm thms)); val elims = List.map prove_case_elim_thm thms; -val type_op_cases = save_thm("type_op_cases", +Theorem type_op_cases = ``type_op op ts t3`` |> (SIMP_CONV(srw_ss())(type_op_def::eqs@elims) THENC SIMP_CONV (bool_ss++DNF_ss) [ - PULL_EXISTS])); + PULL_EXISTS]) (* ---------- type_p ---------- *) diff --git a/translator/ml_progScript.sml b/translator/ml_progScript.sml index f4c7b72749..7058832efd 100644 --- a/translator/ml_progScript.sml +++ b/translator/ml_progScript.sml @@ -638,13 +638,13 @@ Proof rewrite_tac[prim_sem_env_eq,THE_DEF,init_state_def,init_env_def] QED -val nsLookup_init_env_pfun_eqs = save_thm("nsLookup_init_env_pfun_eqs", +Theorem nsLookup_init_env_pfun_eqs = [``nsLookup_Short init_env.c``, ``nsLookup_Short init_env.v``, ``nsLookup_Mod1 init_env.c``, ``nsLookup_Mod1 init_env.v``] |> map (SIMP_CONV bool_ss [init_env_def, nsLookup_Short_Bind, nsLookup_Mod1_def, namespace_case_def, sem_env_accfupds, K_DEF]) - |> LIST_CONJ); + |> LIST_CONJ end @@ -1110,11 +1110,11 @@ Proof rw [namespacePropsTheory.nsLookup_nsBind] QED -val nsLookup_nsAppend = save_thm("nsLookup_nsAppend[compute]", +Theorem nsLookup_nsAppend[compute] = nsLookup_merge_env |> SIMP_RULE (srw_ss()) [merge_env_def] |> Q.INST [`e1`|->`<|c:=e1c;v:=e1v|>`,`e2`|->`<|c:=e2c;v:=e2v|>`] - |> SIMP_RULE (srw_ss()) []); + |> SIMP_RULE (srw_ss()) [] (* Base case for mod_defined (?) *) Theorem mod_defined_base[compute]: diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index 9be9806e94..6359dd8997 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -862,8 +862,8 @@ val FUN_EXISTS_Eq = Q.prove( `(FUN_EXISTS x. Eq a x) = a`, SIMP_TAC std_ss [FUN_EQ_THM,FUN_EXISTS,Eq_def]) |> GEN_ALL; -val FUN_QUANT_SIMP = save_thm("FUN_QUANT_SIMP", - LIST_CONJ [FUN_EXISTS_Eq,FUN_FORALL_PUSH1,FUN_FORALL_PUSH2]); +Theorem FUN_QUANT_SIMP = + LIST_CONJ [FUN_EXISTS_Eq,FUN_FORALL_PUSH1,FUN_FORALL_PUSH2] Theorem Eval_Recclosure_ALT: !funs fname name body. @@ -1033,8 +1033,8 @@ Proof fs [num_of_int_def] \\ intLib.COOPER_TAC QED -val Eval_num_of_int = save_thm("Eval_num_of_int", - Eval_Num_ABS |> REWRITE_RULE [GSYM num_of_int_def]); +Theorem Eval_num_of_int = + Eval_Num_ABS |> REWRITE_RULE [GSYM num_of_int_def] Theorem Eval_int_of_num: Eval env x1 (NUM n) ==> @@ -1074,40 +1074,40 @@ Definition sub_nocheck_def: sub_nocheck (n:num) m = n - m End -val Eval_NUM_SUB_nocheck = save_thm("Eval_NUM_SUB_nocheck", +Theorem Eval_NUM_SUB_nocheck = Eval_INT_SUB |> Q.SPECL [`&n`,`&m`] |> UNDISCH_ALL |> DISCH ``PRECONDITION ((m:num) <= n)`` |> SIMP_RULE std_ss [GSYM NUM_def,INT_SUB,PRECONDITION_def] |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def])) |> DISCH ``Eval env x2 (INT (&m))`` |> DISCH ``Eval env x1 (INT (&n))`` - |> SIMP_RULE std_ss [GSYM NUM_def,GSYM sub_nocheck_def]); + |> SIMP_RULE std_ss [GSYM NUM_def,GSYM sub_nocheck_def] -val Eval_NUM_ADD = save_thm("Eval_NUM_ADD", +Theorem Eval_NUM_ADD = Eval_INT_ADD |> Q.SPECL [`&n1`,`&n2`] - |> REWRITE_RULE [GSYM NUM_def,INT_ADD]); + |> REWRITE_RULE [GSYM NUM_def,INT_ADD] -val Eval_NUM_MULT = save_thm("Eval_NUM_MULT", +Theorem Eval_NUM_MULT = Eval_INT_MULT |> Q.SPECL [`&n1`,`&n2`] - |> REWRITE_RULE [GSYM NUM_def,INT_MUL]); + |> REWRITE_RULE [GSYM NUM_def,INT_MUL] -val Eval_NUM_DIV = save_thm("Eval_NUM_DIV", +Theorem Eval_NUM_DIV = Eval_INT_DIV |> Q.SPECL [`&n1`,`&n2`] |> UNDISCH_ALL |> DISCH ``PRECONDITION (&n2 <> 0:int)`` |> SIMP_RULE std_ss [GSYM NUM_def,INT_DIV,PRECONDITION_def,INT_INJ] |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def])) |> DISCH ``Eval env x2 (INT (&n2))`` |> DISCH ``Eval env x1 (INT (&n1))`` - |> SIMP_RULE std_ss [GSYM NUM_def,INT_DIV]); + |> SIMP_RULE std_ss [GSYM NUM_def,INT_DIV] -val Eval_NUM_MOD = save_thm("Eval_NUM_MOD", +Theorem Eval_NUM_MOD = Eval_INT_MOD |> Q.SPECL [`&n1`,`&n2`] |> UNDISCH_ALL |> DISCH ``PRECONDITION (&n2 <> 0:int)`` |> SIMP_RULE std_ss [GSYM NUM_def,INT_MOD,PRECONDITION_def,INT_INJ] |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def])) |> DISCH ``Eval env x2 (INT (&n2))`` |> DISCH ``Eval env x1 (INT (&n1))`` - |> SIMP_RULE std_ss [GSYM NUM_def,INT_MOD]); + |> SIMP_RULE std_ss [GSYM NUM_def,INT_MOD] val Eval_NUM_MULT = Eval_INT_MULT |> Q.SPECL [`&n1`,`&n2`] @@ -1148,23 +1148,23 @@ QED end; -val Eval_NUM_LESS = save_thm("Eval_NUM_LESS", +Theorem Eval_NUM_LESS = Eval_INT_LESS |> Q.SPECL [`&n1`,`&n2`] - |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt]); + |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt] -val Eval_NUM_LESS_EQ = save_thm("Eval_NUM_LESS_EQ", +Theorem Eval_NUM_LESS_EQ = Eval_INT_LESS_EQ |> Q.SPECL [`&n1`,`&n2`] - |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt]); + |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt] -val Eval_NUM_GREATER = save_thm("Eval_NUM_GREATER", +Theorem Eval_NUM_GREATER = Eval_INT_GREATER |> Q.SPECL [`&n1`,`&n2`] |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt] - |> REWRITE_RULE [GSYM GREATER_DEF, GSYM GREATER_EQ]); + |> REWRITE_RULE [GSYM GREATER_DEF, GSYM GREATER_EQ] -val Eval_NUM_GREATER_EQ = save_thm("Eval_NUM_GREATER_EQ", +Theorem Eval_NUM_GREATER_EQ = Eval_INT_GREATER_EQ |> Q.SPECL [`&n1`,`&n2`] |> REWRITE_RULE [GSYM NUM_def,INT_LT,INT_LE,int_ge,int_gt] - |> REWRITE_RULE [GSYM GREATER_DEF, GSYM GREATER_EQ]); + |> REWRITE_RULE [GSYM GREATER_DEF, GSYM GREATER_EQ] Theorem Eval_NUM_EQ_0: !n. Eval env x (NUM n) ==> @@ -2366,8 +2366,8 @@ val UNCURRY3 = Q.prove( `pair_CASE (x,y) f = f x y`, EVAL_TAC) |> GEN_ALL; -val UNCURRY_SIMP = save_thm("UNCURRY_SIMP", - LIST_CONJ [UNCURRY1,UNCURRY2,UNCURRY3]); +Theorem UNCURRY_SIMP = + LIST_CONJ [UNCURRY1,UNCURRY2,UNCURRY3] Theorem num_case_thm: num_CASE = \n b f. if n = 0 then b else f (n-1) @@ -2376,8 +2376,8 @@ Proof \\ EVAL_TAC \\ SIMP_TAC std_ss [] QED -val PUSH_FORALL_INTO_IMP = save_thm("PUSH_FORALL_INTO_IMP", - METIS_PROVE [] ``!P Q. (!x. P x ==> Q x) ==> (!x. P x) ==> (!x. Q x)``); +Theorem PUSH_FORALL_INTO_IMP = + METIS_PROVE [] ``!P Q. (!x. P x ==> Q x) ==> (!x. P x) ==> (!x. Q x)`` Definition FALSE_def: FALSE = F @@ -2641,7 +2641,8 @@ Proof \\ EVAL_TAC QED -val PRECONDITION_T = save_thm("PRECONDITION_T",EVAL ``PRECONDITION T``); +Theorem PRECONDITION_T = + EVAL ``PRECONDITION T`` Definition no_change_refs_def: no_change_refs (Lit _) = T /\ @@ -2769,8 +2770,8 @@ Proof SIMP_TAC std_ss [] QED -val EQ_COND_INTRO = save_thm("EQ_COND_INTRO", - METIS_PROVE[]``(b ==> c) ==> (c = if b then T else c)``); +Theorem EQ_COND_INTRO = + METIS_PROVE[]``(b ==> c) ==> (c = if b then T else c)`` Theorem LIST_TYPE_And: LIST_TYPE (And a P) = And (LIST_TYPE a) (EVERY (P:'a->bool)) @@ -2869,8 +2870,8 @@ Proof fs [PreImp_def,PRECONDITION_def] QED -val SUC_SUB1_LEMMA = save_thm("SUC_SUB1_LEMMA", - Q.SPECL [`n`,`1`] ADD_SUB |> REWRITE_RULE [GSYM ADD1]); +Theorem SUC_SUB1_LEMMA = + Q.SPECL [`n`,`1`] ADD_SUB |> REWRITE_RULE [GSYM ADD1] Theorem LENGTH_EQ_SUC_IMP: LENGTH xs = SUC n ==> xs <> [] diff --git a/translator/ml_translator_demoScript.sml b/translator/ml_translator_demoScript.sml index a4980e115a..ffad6a19ce 100644 --- a/translator/ml_translator_demoScript.sml +++ b/translator/ml_translator_demoScript.sml @@ -31,12 +31,12 @@ val Decls_thm = |> REWRITE_RULE [ml_progTheory.ML_code_def]; (* the qsort program successfully evaluates to an env, called auto_env3 *) -val evaluate_prog_thm = save_thm("evaluate_prog_thm", - Decls_thm |> REWRITE_RULE [ml_progTheory.Decls_def]); +Theorem evaluate_prog_thm = + Decls_thm |> REWRITE_RULE [ml_progTheory.Decls_def] (* looking up "qsort" in this env finds the qsort value (qsort_v) *) -val lookup_qsort = save_thm("lookup_qsort", - EVAL ``nsLookup ^(concl Decls_thm |> rator |> rand).v (Short "qsort")``); +Theorem lookup_qsort = + EVAL ``nsLookup ^(concl Decls_thm |> rator |> rand).v (Short "qsort")`` (* --- a more concrete example, not much use --- *) diff --git a/translator/monadic/examples/doubleArgProgScript.sml b/translator/monadic/examples/doubleArgProgScript.sml index 21a24629cd..35e04e1d3b 100644 --- a/translator/monadic/examples/doubleArgProgScript.sml +++ b/translator/monadic/examples/doubleArgProgScript.sml @@ -51,7 +51,7 @@ val double_tail_rec_v = double_tail_rec_def |> translate; val double_ref_v = double_ref_def |> m_translate; -val double_ref_thm = save_thm("double_ref_thm", - cfMonadLib.mk_app_of_ArrowP double_ref_v |> SPEC_ALL); +Theorem double_ref_thm = + cfMonadLib.mk_app_of_ArrowP double_ref_v |> SPEC_ALL val _ = export_theory (); diff --git a/translator/monadic/examples/helloProgScript.sml b/translator/monadic/examples/helloProgScript.sml index d09733528c..96fd059a7a 100644 --- a/translator/monadic/examples/helloProgScript.sml +++ b/translator/monadic/examples/helloProgScript.sml @@ -80,7 +80,7 @@ End val res = m_translate hello_def; -val hello_app_thm = save_thm("hello_app_thm", - cfMonadLib.mk_app_of_ArrowP res |> SPEC_ALL); +Theorem hello_app_thm = + cfMonadLib.mk_app_of_ArrowP res |> SPEC_ALL val _ = export_theory (); diff --git a/translator/monadic/examples/poly_array_sortProgScript.sml b/translator/monadic/examples/poly_array_sortProgScript.sml index 6089a3a2fb..16d7569bed 100644 --- a/translator/monadic/examples/poly_array_sortProgScript.sml +++ b/translator/monadic/examples/poly_array_sortProgScript.sml @@ -1319,7 +1319,8 @@ val qsort_v_thm = qsort_v_thm |> DISCH_ALL |> (qsort_v_precond |> SPEC_ALL |> UNDISCH_ALL)) |> DISCH_ALL -val _ = save_thm("qsort_v_thm[allow_rebind]", qsort_v_thm) +Theorem qsort_v_thm[allow_rebind] = + qsort_v_thm (******************************************************************************* diff --git a/translator/monadic/ml_monadStoreScript.sml b/translator/monadic/ml_monadStoreScript.sml index 7fa04ce556..1ff33e09e8 100644 --- a/translator/monadic/ml_monadStoreScript.sml +++ b/translator/monadic/ml_monadStoreScript.sml @@ -8,13 +8,14 @@ open packLib val _ = new_theory "ml_monadStore" -val HCOND_EXTRACT = save_thm("HCOND_EXTRACT", cfLetAutoTheory.HCOND_EXTRACT); +Theorem HCOND_EXTRACT = + cfLetAutoTheory.HCOND_EXTRACT -val SEP_EXISTS_SEPARATE = save_thm("SEP_EXISTS_SEPARATE", - List.hd(SPEC_ALL SEP_CLAUSES |> CONJUNCTS) |> GSYM |> GEN_ALL); +Theorem SEP_EXISTS_SEPARATE = + List.hd(SPEC_ALL SEP_CLAUSES |> CONJUNCTS) |> GSYM |> GEN_ALL -val SEP_EXISTS_INWARD = save_thm("SEP_EXISTS_INWARD", - List.nth(SPEC_ALL SEP_CLAUSES |> CONJUNCTS, 1) |> GSYM |> GEN_ALL); +Theorem SEP_EXISTS_INWARD = + List.nth(SPEC_ALL SEP_CLAUSES |> CONJUNCTS, 1) |> GSYM |> GEN_ALL Theorem ALLOCATE_ARRAY_evaluate: !env s n xname xv. diff --git a/translator/monadic/ml_monad_translatorScript.sml b/translator/monadic/ml_monad_translatorScript.sml index e838529e81..297207c589 100644 --- a/translator/monadic/ml_monad_translatorScript.sml +++ b/translator/monadic/ml_monad_translatorScript.sml @@ -748,8 +748,8 @@ val FUN_EXISTS_Eq = Q.prove( `(FUN_EXISTS x. Eq a x) = a`, SIMP_TAC std_ss [FUN_EQ_THM,FUN_EXISTS,Eq_def]) |> GEN_ALL; -val M_FUN_QUANT_SIMP = save_thm("M_FUN_QUANT_SIMP", - LIST_CONJ [FUN_EXISTS_Eq,M_FUN_FORALL_PUSH1,M_FUN_FORALL_PUSH2,M_FUN_FORALL_PUSH3]); +Theorem M_FUN_QUANT_SIMP = + LIST_CONJ [FUN_EXISTS_Eq,M_FUN_FORALL_PUSH1,M_FUN_FORALL_PUSH2,M_FUN_FORALL_PUSH3] Theorem EvalM_Eq: EvalM ro env st exp (PURE a x) H ==> EvalM ro env st exp (PURE (Eq a x) x) ^H @@ -3521,17 +3521,17 @@ Proof fs[lookup_cons_def] QED -val LOOKUP_ASSUM_SIMP = save_thm("LOOKUP_ASSUM_SIMP", +Theorem LOOKUP_ASSUM_SIMP = LIST_CONJ[nsBind_to_write,Eval_Var_SIMP,Eval_lookup_var, nsLookup_write_simp,sem_env_same_components,lookup_cons_write_simp, - lookup_cons_build_rec_env_simp]); + lookup_cons_build_rec_env_simp] -val EVAL_T_F = save_thm("EVAL_T_F", +Theorem EVAL_T_F = LIST_CONJ [EVAL ``ml_translator$CONTAINER ml_translator$TRUE``, - EVAL ``ml_translator$CONTAINER ml_translator$FALSE``]); + EVAL ``ml_translator$CONTAINER ml_translator$FALSE``] -val EVAL_PRECONDITION_T = save_thm("EVAL_PRECONDITION_T", - EVAL (``ml_translator$PRECONDITION T``)); +Theorem EVAL_PRECONDITION_T = + EVAL (``ml_translator$PRECONDITION T``) Theorem H_STAR_emp: H * emp = H diff --git a/translator/monadic/monad_base/ml_monadBaseScript.sml b/translator/monadic/monad_base/ml_monadBaseScript.sml index e08c46023b..03daf1f5ce 100644 --- a/translator/monadic/monad_base/ml_monadBaseScript.sml +++ b/translator/monadic/monad_base/ml_monadBaseScript.sml @@ -550,7 +550,8 @@ val monad_eqs = LIST_CONJ [ st_ex_return_success, st_ex_bind_success, otherwise_eq, can_success, Marray_length_success, Marray_sub_eq, Marray_update_eq, Marray_alloc_success ]; -val _ = save_thm ("monad_eqs", monad_eqs); +Theorem monad_eqs = + monad_eqs (* Run *) Definition run_def: diff --git a/translator/okasaki-examples/LazyPairingHeapScript.sml b/translator/okasaki-examples/LazyPairingHeapScript.sml index 8f5108dbcc..b2062ff78f 100644 --- a/translator/okasaki-examples/LazyPairingHeapScript.sml +++ b/translator/okasaki-examples/LazyPairingHeapScript.sml @@ -125,11 +125,13 @@ QED (* Remove the size constraints *) val merge_def = SIMP_RULE (srw_ss()) [merge_size_lem, LET_THM] merge_def; -val _ = save_thm ("merge_def[compute,allow_rebind]",merge_def); +Theorem merge_def[compute,allow_rebind] = + merge_def val merge_ind = SIMP_RULE (srw_ss()) [merge_size_lem, LET_THM] (fetch "-" "merge_ind"); -val _ = save_thm ("merge_ind[allow_rebind]",merge_ind); +Theorem merge_ind[allow_rebind] = + merge_ind Triviality merge_thm: merge get_key leq a b = diff --git a/translator/other-examples/auxiliary/ninetyOneScript.sml b/translator/other-examples/auxiliary/ninetyOneScript.sml index 7eb1c2f5e1..02f30b44f2 100644 --- a/translator/other-examples/auxiliary/ninetyOneScript.sml +++ b/translator/other-examples/auxiliary/ninetyOneScript.sml @@ -128,8 +128,10 @@ val (N_def,N_ind) = Defn.tprove THEN POP_ASSUM MP_TAC THEN FULL_SIMP_TAC arith_ss [DECIDE ``x+y < p ==> ((p-y)+y = p)``]); -val _ = save_thm ("N_def", N_def); -val _ = save_thm ("N_ind", N_ind); +Theorem N_def = + N_def +Theorem N_ind = + N_ind Theorem N_correct: !x. N x = if x > 100 then x - 10 else 91 diff --git a/translator/other-examples/auxiliary/regexpMatchScript.sml b/translator/other-examples/auxiliary/regexpMatchScript.sml index 856f9ecc27..c5ecceda1e 100644 --- a/translator/other-examples/auxiliary/regexpMatchScript.sml +++ b/translator/other-examples/auxiliary/regexpMatchScript.sml @@ -217,8 +217,10 @@ val (match_def, match_ind) = Defn.tprove PURE_ONCE_REWRITE_TAC [GSYM arithmeticTheory.LESS_OR_EQ] THEN RW_TAC list_ss [front_starHeight_def, starHeight_def]); -val _ = save_thm ("match_def", match_def); -val _ = save_thm ("match_ind", match_ind); +Theorem match_def = + match_def +Theorem match_ind = + match_ind (* ------------------------------------------------------------------------- *) (* Correctness Proof *) diff --git a/translator/std_preludeScript.sml b/translator/std_preludeScript.sml index d71ceb0eea..309527cda9 100644 --- a/translator/std_preludeScript.sml +++ b/translator/std_preludeScript.sml @@ -94,7 +94,8 @@ Proof THEN METIS_TAC [FUNPOW] QED -val OWHILE_ind = save_thm("OWHILE_ind",WHILE_ind); +Theorem OWHILE_ind = + WHILE_ind val _ = add_preferred_thy "-"; diff --git a/tutorial/wordcountProgScript.sml b/tutorial/wordcountProgScript.sml index 36315c6c0d..230aca015e 100644 --- a/tutorial/wordcountProgScript.sml +++ b/tutorial/wordcountProgScript.sml @@ -267,10 +267,10 @@ val spec = wordcount_whole_prog_spec |> UNDISCH_ALL val (sem_thm,prog_tm) = whole_prog_thm (get_ml_prog_state()) "wordcount" spec val wordcount_prog_def = mk_abbrev"wordcount_prog" prog_tm; -val wordcount_semantics = save_thm("wordcount_semantics", +Theorem wordcount_semantics = sem_thm |> PURE_REWRITE_RULE[GSYM wordcount_prog_def] |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC,LENGTH] - |> SIMP_RULE (srw_ss()) []); + |> SIMP_RULE (srw_ss()) [] val _ = export_theory();