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 <directory>")
        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)

Author: dnezam

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]);
 

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;*)

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:

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

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 *)
 

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:

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)

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

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,33 +869,33 @@ 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 >>
       simp[subterm_Comb,subterm_Abs] >> rw[] >>
       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) ⇒

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[] >>