Replace export_rewrites with simp where possible (#1264)

There are a few things worth pointing out:

1. I've slightly restructured some new_specification calls. In particular, I
factored out the proof into a local theorem, and more importantly, I factored
out the string name into a variable (see clFFIScript.sml). The motivation for
the latter was to ultimately ban `export_rewrites["`, but it turns out that
there are still good uses for this (for example when adding definitions/theorems
from other theories to the simpset). Arguably, it gets rid of some duplication,
which is why I haven't reverted it.

2. I've adjusted various tutorial files to use simp tags, since presumably we
want newcomers to be exposed to that. simple_bstScript.sml still mentions what
it desugars to at some point, so it should be fine.

3. I deleted astPropsScript.sml -- there was a TODO that said to do it, and it
also had commented out export_rewrites.

Author: dnezam

basis/DoubleFFIScript.sml

@@ -123,11 +123,12 @@ Proof
   qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]
 QED
 
+val decode_encode_name = "decode_encode";
 val decode_encode = new_specification(
-  "decode_encode",
+  decode_encode_name,
   ["decode"],
   encode_decode_exists);
-val _ = export_rewrites ["decode_encode"];
+val _ = export_rewrites [decode_encode_name];
 
 Definition double_ffi_part_def:
   double_ffi_part = (encode,decode,
@@ -140,4 +141,3 @@ Definition double_ffi_part_def:
      ("double_ln",ffi_ln);
      ("double_floor",ffi_floor)])
 End
-

basis/basis_ffiScript.sml

@@ -287,16 +287,14 @@ Theorem extract_stdo_extract_fs
   \\ rw[] \\ fs[]
   stdo_def
 
-Definition is_write_def:
+Definition is_write_def[simp]:
   (is_write fd (IO_event name _ ((fd',st)::_)) ⇔ name="write" ∧ fd' = fd ∧ st = 0w) ∧
   (is_write _ _ ⇔ F)
 End
-val _ = export_rewrites["is_write_def"];
 
-Definition extract_write_def:
+Definition extract_write_def[simp]:
   extract_write (IO_event _ _ (_::(_,nw)::bytes)) = TAKE (w2n nw) (MAP FST bytes)
 End
-val _ = export_rewrites["extract_write_def"];
 
 Definition extract_writes_def:
   extract_writes fd io_events =

basis/clFFIScript.sml

@@ -81,10 +81,18 @@ Proof
   \\ drule encode_list_11 \\ fs [mlstringTheory.explode_11]
 QED
 
-val decode_encode = new_specification("decode_encode",["decode"],
-  prove(``?decode. !cls. decode (encode cls) = SOME cls``,
-        qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]));
-val _ = export_rewrites ["decode_encode"];
+Theorem encode_decode_exists[local]:
+  ?decode. !cls. decode (encode cls) = SOME cls
+Proof
+  qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]
+QED
+
+val decode_encode_name = "decode_encode";
+val decode_encode = new_specification(
+  decode_encode_name,
+  ["decode"],
+  encode_decode_exists);
+val _ = export_rewrites [decode_encode_name];
 
 Definition cl_ffi_part_def:
   cl_ffi_part = (encode,decode,

basis/fsFFIScript.sml

@@ -383,10 +383,18 @@ Proof
   \\ fs [IO_fs_component_equality]
 QED
 
-val decode_encode = new_specification("decode_encode",["decode"],
-  prove(``?decode. !cls. decode (encode cls) = SOME cls``,
-        qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]));
-val _ = export_rewrites ["decode_encode"];
+Theorem encode_decode_exists[local]:
+  ?decode. !cls. decode (encode cls) = SOME cls
+Proof
+  qexists_tac `\f. some c. encode c = f` \\ fs [encode_11]
+QED
+
+val decode_encode_name = "decode_encode";
+val decode_encode = new_specification(
+  decode_encode_name,
+  ["decode"],
+  encode_decode_exists);
+val _ = export_rewrites [decode_encode_name];
 
 Definition fs_ffi_part_def:
   fs_ffi_part =
@@ -397,4 +405,3 @@ Definition fs_ffi_part_def:
        ("write",ffi_write);
        ("close",ffi_close)])
 End
-

basis/pure/mlstringScript.sml

@@ -25,11 +25,11 @@ Definition implode_def:
   implode = strlit
 End
 
-Definition strlen_def:
+Definition strlen_def[simp]:
   strlen (strlit s) = LENGTH s
 End
 
-Definition strsub_def:
+Definition strsub_def[simp]:
   strsub (strlit s) n = EL n s
 End
 
@@ -51,14 +51,11 @@ Proof
 EVAL_TAC
 QED
 
-val _ = export_rewrites["strlen_def","strsub_def"];
-
-Definition explode_aux_def:
+Definition explode_aux_def[simp]:
   (explode_aux s n 0 = []) ∧
   (explode_aux s n (SUC len) =
     strsub s n :: (explode_aux s (n + 1) len))
 End
-val _ = export_rewrites["explode_aux_def"];
 
 Theorem explode_aux_thm:
    ∀max n ls.
@@ -1369,23 +1366,21 @@ Definition escape_char_def:
   escape_char c = implode ("#\"" ++ char_escaped c ++ "\"")
 End
 
-Theorem ALL_DISTINCT_MAP_implode:
+Theorem ALL_DISTINCT_MAP_implode[simp]:
    ALL_DISTINCT ls ⇒ ALL_DISTINCT (MAP implode ls)
 Proof
   strip_tac >>
   match_mp_tac ALL_DISTINCT_MAP_INJ >>
   rw[implode_def]
 QED
-val _ = export_rewrites["ALL_DISTINCT_MAP_implode"]
 
-Theorem ALL_DISTINCT_MAP_explode:
+Theorem ALL_DISTINCT_MAP_explode[simp]:
    ∀ls. ALL_DISTINCT (MAP explode ls) ⇔ ALL_DISTINCT ls
 Proof
   gen_tac >> EQ_TAC >- MATCH_ACCEPT_TAC ALL_DISTINCT_MAP >>
   STRIP_TAC >> MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >>
   simp[explode_11]
 QED
-val _ = export_rewrites["ALL_DISTINCT_MAP_explode"]
 
 (* optimising mlstring app_list *)
 

candle/overloading/monadic/holKernelProofScript.sml

@@ -4248,12 +4248,11 @@ Proof
   \\ res_tac \\ fs []
 QED
 
-Definition sizeof'_def:
+Definition sizeof'_def[simp]:
   (sizeof' (Comb s t) = 1 + sizeof' s + sizeof' t) ∧
   (sizeof' (Abs v t) = 1 + sizeof' v + sizeof' t) ∧
   (sizeof' _ = 1n)
 End
-val _ = export_rewrites["sizeof'_def"];
 
 Theorem sizeof'_rev_assocd:
    ∀x  l d.

candle/overloading/semantics/holBoolScript.sml

@@ -131,14 +131,13 @@ End
 
 Overload is_bool_interpretation_ext = ``is_bool_interpretation_ext0 ^mem``
 
-Theorem boolrel_in_funspace:
+Theorem boolrel_in_funspace[simp]:
   is_set_theory ^mem ⇒ Boolrel R <: Funspace boolset (Funspace boolset boolset)
 Proof
   rw[Boolrel_def] >> match_mp_tac (UNDISCH abstract_in_funspace) >> rw[] >>
   match_mp_tac (UNDISCH abstract_in_funspace) >> rw[boolean_in_boolset]
 QED
 
-val _ = export_rewrites["boolrel_in_funspace"]
 
 val Defs = [TrueDef_def, AndDef_def, ImpliesDef_def, ForallDef_def, ExistsDef_def, OrDef_def, FalseDef_def, NotDef_def]
 

candle/overloading/semantics/holSemanticsScript.sml

@@ -77,7 +77,7 @@ Definition terms_of_frag_def:
         /\ set(allTypes t) ⊆ tys /\ welltyped t}
 End
 
-Definition TYPE_SUBSTf_def:
+Definition TYPE_SUBSTf_def[simp]:
   (TYPE_SUBSTf i (Tyvar v) = i v) ∧
   (TYPE_SUBSTf i (Tyapp v tys) =
     Tyapp v (MAP (λa. TYPE_SUBSTf i a) tys))
@@ -87,7 +87,6 @@ Termination
    simp[] >> res_tac >> simp[]
 End
 
-val _ = export_rewrites["TYPE_SUBSTf_def"]
 
 Definition terms_of_frag_uninst_def:
   terms_of_frag_uninst (tys,consts) sigma =