Merge pull request #572 from CakeML/cleanup

Cleanup: some progress on #414 and #549

basis/CommandLineProofScript.sml

@@ -30,9 +30,9 @@ val COMMANDLINE_precond = Q.prove(
   rw[set_thm]) |> UNDISCH
   |> curry save_thm "COMMANDLINE_precond";
 
-val COMMANDLINE_FFI_part_hprop = Q.store_thm("COMMANDLINE_FFI_part_hprop",
-  `FFI_part_hprop (COMMANDLINE x)`,
-  rw [COMMANDLINE_def,cfHeapsBaseTheory.IO_def,cfMainTheory.FFI_part_hprop_def,
+Theorem COMMANDLINE_FFI_part_hprop
+  `FFI_part_hprop (COMMANDLINE x)`
+  (rw [COMMANDLINE_def,cfHeapsBaseTheory.IO_def,cfMainTheory.FFI_part_hprop_def,
       cfHeapsBaseTheory.IOx_def, cl_ffi_part_def,
       set_sepTheory.SEP_CLAUSES,set_sepTheory.SEP_EXISTS_THM,
       set_sepTheory.cond_STAR ]
@@ -43,12 +43,12 @@ val eq_num_v_thm = MATCH_MP (DISCH_ALL eq_v_thm) (EqualityType_NUM_BOOL |> CONJU
 
 val st = get_ml_prog_state();
 
-val CommandLine_read16bit_spec = Q.store_thm("CommandLine_read16bit",
+Theorem CommandLine_read16bit
   `2 <= LENGTH a ==>
    app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.read16bit" st) [av]
      (W8ARRAY av a)
-     (POSTv v. W8ARRAY av a * & NUM (w2n (EL 0 a) + 256 * w2n (EL 1 a)) v)`,
-  xcf "CommandLine.read16bit" st
+     (POSTv v. W8ARRAY av a * & NUM (w2n (EL 0 a) + 256 * w2n (EL 1 a)) v)`
+  (xcf "CommandLine.read16bit" st
   \\ xlet_auto THEN1 xsimpl
   \\ xlet_auto THEN1 (fs [] \\ xsimpl)
   \\ xlet_auto THEN1 (fs [] \\ xsimpl)
@@ -60,12 +60,12 @@ val CommandLine_read16bit_spec = Q.store_thm("CommandLine_read16bit",
   \\ Cases_on `h` \\ Cases_on `h'` \\ fs []
   \\ fs [INT_def] \\ intLib.COOPER_TAC);
 
-val CommandLine_write16bit_spec = Q.store_thm("CommandLine_write16bit",
+Theorem CommandLine_write16bit
   `NUM n nv /\ 2 <= LENGTH a ==>
    app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.write16bit" st) [av;nv]
      (W8ARRAY av a)
-     (POSTv v. W8ARRAY av (n2w n::n2w (n DIV 256)::TL (TL a)))`,
-  xcf "CommandLine.write16bit" st
+     (POSTv v. W8ARRAY av (n2w n::n2w (n DIV 256)::TL (TL a)))`
+  (xcf "CommandLine.write16bit" st
   \\ xlet_auto THEN1 xsimpl
   \\ xlet_auto THEN1 (fs [] \\ xsimpl)
   \\ xlet_auto THEN1 (fs [] \\ xsimpl)
@@ -105,14 +105,14 @@ val DROP_SUC_LENGTH_MAP = prove(
              SUC (LENGTH ys) = LENGTH (MAP f ys ⧺ [y])`
   THEN1 simp_tac std_ss [DROP_LENGTH_APPEND] \\ fs []);
 
-val CommandLine_cloop_spec = Q.store_thm("CommandLine_cloop_spec",
+Theorem CommandLine_cloop_spec
   `!n nv av cv a.
      LIST_TYPE STRING_TYPE (DROP n cl) cv /\
      NUM n nv /\ n <= LENGTH cl /\ LENGTH a = 2 ==>
      app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.cloop" st) [av; nv; cv]
       (COMMANDLINE cl * W8ARRAY av a)
-      (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`,
-  Induct \\ rw []
+      (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`
+  (Induct \\ rw []
   THEN1
    (xcf "CommandLine.cloop" st
     \\ xlet_auto THEN1 xsimpl
@@ -180,12 +180,12 @@ val CommandLine_cloop_spec = Q.store_thm("CommandLine_cloop_spec",
   \\ fs [MAP_MAP_o, CHR_w2n_n2w_ORD, GSYM mlstringTheory.implode_def]
   \\ fs[DROP_APPEND,DROP_LENGTH_TOO_LONG]);
 
-val CommandLine_cline_spec = Q.store_thm("CommandLine_cline_spec",
+Theorem CommandLine_cline_spec
   `UNIT_TYPE u uv ==>
    app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.cline" st) [uv]
     (COMMANDLINE cl)
-    (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`,
-  xcf "CommandLine.cline" st
+    (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`
+  (xcf "CommandLine.cline" st
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
   \\ qmatch_goalsub_rename_tac `W8ARRAY av`
@@ -219,12 +219,12 @@ val CommandLine_cline_spec = Q.store_thm("CommandLine_cline_spec",
 val hd_v_thm = fetch "ListProg" "hd_v_thm";
 val mlstring_hd_v_thm = hd_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]
 
-val CommandLine_name_spec = Q.store_thm("CommandLine_name_spec",
+Theorem CommandLine_name_spec
   `UNIT_TYPE u uv ==>
     app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.name" st) [uv]
     (COMMANDLINE cl)
-    (POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)`,
-  xcf "CommandLine.name" st
+    (POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)`
+  (xcf "CommandLine.name" st
   \\ xlet `POSTv vz. & UNIT_TYPE () vz * COMMANDLINE cl`
   >-(xcon \\ xsimpl)
   \\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
@@ -239,23 +239,23 @@ val mlstring_tl_v_thm = tl_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring
 val name_def = Define `
   name () = (\cl. (Success (HD cl), cl))`;
 
-val EvalM_name = Q.store_thm("EvalM_name",
+Theorem EvalM_name
   `Eval env exp (UNIT_TYPE u) /\
     (nsLookup env.v (Long "CommandLine" (Short "name")) =
       SOME CommandLine_name_v) ==>
     EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "name")); exp])
       (MONAD STRING_TYPE exc_ty (name u))
-      (COMMANDLINE,p:'ffi ffi_proj)`,
-  ho_match_mp_tac EvalM_from_app \\ rw [name_def]
+      (COMMANDLINE,p:'ffi ffi_proj)`
+  (ho_match_mp_tac EvalM_from_app \\ rw [name_def]
   \\ metis_tac [CommandLine_name_spec]);
 
-val CommandLine_arguments_spec = Q.store_thm("CommandLine_arguments_spec",
+Theorem CommandLine_arguments_spec
   `UNIT_TYPE u uv ==>
     app (p:'ffi ffi_proj) ^(fetch_v "CommandLine.arguments" st) [uv]
     (COMMANDLINE cl)
     (POSTv argv. & LIST_TYPE STRING_TYPE
-       (TL cl) argv * COMMANDLINE cl)`,
-  xcf "CommandLine.arguments" st
+       (TL cl) argv * COMMANDLINE cl)`
+  (xcf "CommandLine.arguments" st
   \\ xlet `POSTv vz. & UNIT_TYPE () vz * COMMANDLINE cl`
   >-(xcon \\ xsimpl)
   \\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
@@ -267,31 +267,31 @@ val CommandLine_arguments_spec = Q.store_thm("CommandLine_arguments_spec",
 val arguments_def = Define `
   arguments () = (\cl. (Success (TL cl), cl))`
 
-val EvalM_arguments = Q.store_thm("EvalM_arguments",
+Theorem EvalM_arguments
   `Eval env exp (UNIT_TYPE u) /\
     (nsLookup env.v (Long "CommandLine" (Short "arguments")) =
        SOME CommandLine_arguments_v) ==>
     EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "arguments")); exp])
       (MONAD (LIST_TYPE STRING_TYPE) exc_ty (arguments u))
-      (COMMANDLINE,p:'ffi ffi_proj)`,
-  ho_match_mp_tac EvalM_from_app \\ rw [arguments_def]
+      (COMMANDLINE,p:'ffi ffi_proj)`
+  (ho_match_mp_tac EvalM_from_app \\ rw [arguments_def]
   \\ metis_tac [CommandLine_arguments_spec]);
 
 fun prove_hprop_inj_tac thm =
     rw[HPROP_INJ_def, GSYM STAR_ASSOC, SEP_CLAUSES, SEP_EXISTS_THM, HCOND_EXTRACT] >>
       EQ_TAC >-(DISCH_TAC >> IMP_RES_TAC thm >> rw[]) >> rw[];
 
-val UNIQUE_COMMANDLINE = Q.store_thm("UNIQUE_COMMANDLINE",
+Theorem UNIQUE_COMMANDLINE
   `!s cl1 cl2 H1 H2. VALID_HEAP s ==>
-     (COMMANDLINE cl1 * H1) s /\ (COMMANDLINE cl2 * H2) s ==> cl2 = cl1`,
-  rw[COMMANDLINE_def,cfHeapsBaseTheory.IOx_def,cl_ffi_part_def,
+     (COMMANDLINE cl1 * H1) s /\ (COMMANDLINE cl2 * H2) s ==> cl2 = cl1`
+  (rw[COMMANDLINE_def,cfHeapsBaseTheory.IOx_def,cl_ffi_part_def,
      GSYM STAR_ASSOC]
   \\ IMP_RES_TAC FRAME_UNIQUE_IO
   \\ fs[] \\ rw[]
   \\ metis_tac[decode_encode,SOME_11]);
 
-val COMMANDLINE_HPROP_INJ = Q.store_thm("COMMANDLINE_HPROP_INJ[hprop_inj]",
-  `!cl1 cl2. HPROP_INJ (COMMANDLINE cl1) (COMMANDLINE cl2) (cl2 = cl1)`,
-  prove_hprop_inj_tac UNIQUE_COMMANDLINE);
+Theorem COMMANDLINE_HPROP_INJ[hprop_inj]
+  `!cl1 cl2. HPROP_INJ (COMMANDLINE cl1) (COMMANDLINE cl2) (cl2 = cl1)`
+  (prove_hprop_inj_tac UNIQUE_COMMANDLINE);
 
 val _ = export_theory();

basis/Holmakefile

@@ -10,7 +10,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
 all: $(TARGETS) basis_ffi.o README.md
 .PHONY: all
 
-README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) $(wildcard *.c)
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) $(wildcard *.c) dependency-order
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)

basis/IntProgScript.sml

@@ -75,9 +75,9 @@ val fromstring_unsafe_side_def = definition"fromstring_unsafe_side_def";
 val fromchars_unsafe_side_def = theorem"fromchars_unsafe_side_def";
 val fromchars_range_unsafe_side_def = theorem"fromchars_range_unsafe_side_def";
 
-val fromchars_unsafe_side_thm = Q.store_thm("fromchars_unsafe_side_thm",
-  `∀n s. n ≤ LENGTH s ⇒ fromchars_unsafe_side n (strlit s)`,
-  completeInduct_on`n` \\ rw[]
+Theorem fromchars_unsafe_side_thm
+  `∀n s. n ≤ LENGTH s ⇒ fromchars_unsafe_side n (strlit s)`
+  (completeInduct_on`n` \\ rw[]
   \\ rw[Once fromchars_unsafe_side_def,fromchars_range_unsafe_side_def]);
 
 val fromString_unsafe_side = Q.prove(
@@ -103,9 +103,9 @@ val fromstring_side_def = definition"fromstring_side_def";
 val fromchars_side_def = theorem"fromchars_side_def";
 val fromchars_range_side_def = theorem"fromchars_range_side_def";
 
-val fromchars_side_thm = Q.store_thm("fromchars_side_thm",
-  `∀n s. n ≤ LENGTH s ⇒ fromchars_side n (strlit s)`,
-  completeInduct_on`n` \\ rw[]
+Theorem fromchars_side_thm
+  `∀n s. n ≤ LENGTH s ⇒ fromchars_side n (strlit s)`
+  (completeInduct_on`n` \\ rw[]
   \\ rw[Once fromchars_side_def,fromchars_range_side_def]);
 
 val fromString_side = Q.prove(

basis/MarshallingProgScript.sml

@@ -30,17 +30,17 @@ val _ = ml_prog_update (close_module NONE);
 
 open ml_translatorTheory
 
-val n2w2_UNICITY_R = Q.store_thm("n2w2_UNICITY_R[xlet_auto_match]",
- `!n1 n2.n1 < 256**2 ==> ((n2w2 n1 = n2w2 n2 /\ n2 < 256**2) <=> n1 = n2)`,
- rw[n2w2_def] >> eq_tac >> rw[DIV_MOD_MOD_DIV] >>
+Theorem n2w2_UNICITY_R[xlet_auto_match]
+ `!n1 n2.n1 < 256**2 ==> ((n2w2 n1 = n2w2 n2 /\ n2 < 256**2) <=> n1 = n2)`
+ (rw[n2w2_def] >> eq_tac >> rw[DIV_MOD_MOD_DIV] >>
  `0 < (256 : num)` by fs[] >> imp_res_tac DIVISION >> fs[] >>
  first_assum (assume_tac o Q.SPEC`n1`) >> fs[] >>
  first_x_assum (assume_tac o Q.SPEC`n2`) >> fs[]);
 
-val WORD_n2w2_UNICITY_L = Q.store_thm("WORD_n2w2_UNICITY[xlet_auto_match]",
+Theorem WORD_n2w2_UNICITY_L[xlet_auto_match]
  `!n1 n2 f. n1 < 256**2 /\ LIST_TYPE WORD (n2w2 n1) f ==>
-   (LIST_TYPE WORD (n2w2 n2) f /\ n2 < 256**2 <=> n1 = n2)`,
- rw[] >> eq_tac >> rw[] >> fs[n2w2_def,LIST_TYPE_def] >> rw[] >>
+   (LIST_TYPE WORD (n2w2 n2) f /\ n2 < 256**2 <=> n1 = n2)`
+ (rw[] >> eq_tac >> rw[] >> fs[n2w2_def,LIST_TYPE_def] >> rw[] >>
  imp_res_tac Word8ProgTheory.WORD_UNICITY_L >> rw[] >> fs[n2w_11] >> rw[] >>
  `(n1 DIV 256) MOD 256 = (n1 DIV 256)` by fs[DIV_LT_X] >>
  `(n2 DIV 256) MOD 256 = (n2 DIV 256)` by fs[DIV_LT_X] >>
@@ -49,9 +49,9 @@ val WORD_n2w2_UNICITY_L = Q.store_thm("WORD_n2w2_UNICITY[xlet_auto_match]",
  first_x_assum (assume_tac o Q.SPEC`n2`) >> fs[]);
 
 (* needed? *)
-val n2w8_UNICITY_R = Q.store_thm("n2w8_UNICITY_R[xlet_auto_match]",
-  `!n1 n2.n1 < 256**8 ==> ((n2w8 n1 = n2w8 n2 /\ n2 < 256**8) <=> n1 = n2)`,
-  rw[] >> eq_tac >> rw[DIV_MOD_MOD_DIV] >>
+Theorem n2w8_UNICITY_R[xlet_auto_match]
+  `!n1 n2.n1 < 256**8 ==> ((n2w8 n1 = n2w8 n2 /\ n2 < 256**8) <=> n1 = n2)`
+  (rw[] >> eq_tac >> rw[DIV_MOD_MOD_DIV] >>
   `0 < (256 : num)` by fs[] >> imp_res_tac DIVISION >> fs[] >> rw[] >>
   NTAC 7(
     qmatch_abbrev_tac`x1 = x2` >>
@@ -68,10 +68,10 @@ val n2w8_UNICITY_R = Q.store_thm("n2w8_UNICITY_R[xlet_auto_match]",
   unabbrev_all_tac >> fs[DIV_DIV_DIV_MULT] >> rw[] >>
   fs[LESS_DIV_EQ_ZERO]);
 
-val WORD_n2w8_UNICITY_L = Q.store_thm("WORD_n2w8_UNICITY[xlet_auto_match]",
+Theorem WORD_n2w8_UNICITY_L[xlet_auto_match]
  `!n1 n2 f. n1 < 256**8 /\ LIST_TYPE WORD (n2w8 n1) f ==>
-   (LIST_TYPE WORD (n2w8 n2) f /\ n2 < 256**8 <=> n1 = n2)`,
- rw[] >> eq_tac >> rw[] >> fs[n2w8_def,LIST_TYPE_def] >> rw[] >>
+   (LIST_TYPE WORD (n2w8 n2) f /\ n2 < 256**8 <=> n1 = n2)`
+ (rw[] >> eq_tac >> rw[] >> fs[n2w8_def,LIST_TYPE_def] >> rw[] >>
  imp_res_tac Word8ProgTheory.WORD_UNICITY_L >> rw[] >> fs[n2w_11] >> rw[] >>
  mp_tac (Q.SPEC `256` DIVISION) >> rw[] >>
 
@@ -81,24 +81,24 @@ val WORD_n2w8_UNICITY_L = Q.store_thm("WORD_n2w8_UNICITY[xlet_auto_match]",
         unabbrev_all_tac >> fs[DIV_DIV_DIV_MULT]) >>
  fs[LESS_DIV_EQ_ZERO]);
 
-val n2w2_spec = Q.store_thm("n2w2_spec",
+Theorem n2w2_spec
  `!n off b nv offv bl. NUM n nv /\ NUM off offv /\ off + 2 <= LENGTH b ==>
     app (p:'ffi ffi_proj) ^(fetch_v "Marshalling.n2w2" (get_ml_prog_state())) [nv; bl; offv]
        (W8ARRAY bl b)
-       (POSTv u. &UNIT_TYPE () u * W8ARRAY bl (insert_atI (n2w2 n) off b))`,
-  xcf "Marshalling.n2w2" (get_ml_prog_state()) >>
+       (POSTv u. &UNIT_TYPE () u * W8ARRAY bl (insert_atI (n2w2 n) off b))`
+  (xcf "Marshalling.n2w2" (get_ml_prog_state()) >>
   NTAC 6 (xlet_auto >- xsimpl) >>
   xcon >> xsimpl >>
   fs[n2w2_def] >>
   Cases_on`b` >- fs[] >> Cases_on`t` >>
   fs[insert_atI_CONS,insert_atI_def,LUPDATE_commutes]);
 
-val w22n_spec = Q.store_thm("w22n_spec",
+Theorem w22n_spec
  `!off b offv bl. NUM off offv /\ off + 2 <= LENGTH b ==>
     app (p:'ffi ffi_proj) ^(fetch_v "Marshalling.w22n" (get_ml_prog_state())) [bl; offv]
        (W8ARRAY bl b)
-       (POSTv nv. &NUM (w22n [EL off b; EL (off+1) b]) nv * W8ARRAY bl b)`,
-  xcf "Marshalling.w22n" (get_ml_prog_state()) >>
+       (POSTv nv. &NUM (w22n [EL off b; EL (off+1) b]) nv * W8ARRAY bl b)`
+  (xcf "Marshalling.w22n" (get_ml_prog_state()) >>
   NTAC 6 (xlet_auto >- xsimpl) >>
   xapp >> xsimpl  >> fs[w22n_def,NUM_def,INT_def,integerTheory.INT_ADD]);
 

basis/MarshallingScript.sml

@@ -26,24 +26,24 @@ val w82n_def = Define`
   256 * ( 256 * ( 256 * ( 256 * ( 256 * ( 256 * ( 256 *
   w2n b7 + w2n b6) + w2n b5) + w2n b4) + w2n b3) + w2n b2) + w2n b1) + w2n b0`
 
-val w22n_n2w2 = Q.store_thm("w22n_n2w2",
-  `!i. i < 2**(2*8) ==> w22n (n2w2 i) = i`,
-  rw[w22n_def,n2w2_def] >>
+Theorem w22n_n2w2
+  `!i. i < 2**(2*8) ==> w22n (n2w2 i) = i`
+  (rw[w22n_def,n2w2_def] >>
   `0 < (256 : num)` by fs[] >> imp_res_tac DIVISION >> fs[] >>
   first_x_assum (assume_tac o Q.SPEC`i`) >> fs[]);
 
-val n2w2_w22n = Q.store_thm("n2w2_w22n",
-  `!b. LENGTH b = 2 ==> n2w2 (w22n b) = b`,
-  Cases_on`b` >> fs[] >> Cases_on`t` >> rw[w22n_def,n2w2_def]
+Theorem n2w2_w22n
+  `!b. LENGTH b = 2 ==> n2w2 (w22n b) = b`
+  (Cases_on`b` >> fs[] >> Cases_on`t` >> rw[w22n_def,n2w2_def]
   >-(PURE_REWRITE_TAC[Once MULT_COMM] >> fs[ADD_DIV_ADD_DIV] >>
      fs[LESS_DIV_EQ_ZERO,w2n_lt_256]) >>
   fs[GSYM word_add_n2w,GSYM word_mul_n2w] >>
   `256w : word8 = 0w` by fs[GSYM n2w_dimword] >>
   first_x_assum (fn x => PURE_REWRITE_TAC[x]) >> fs[]);
 
-val w82n_n2w8 = Q.store_thm("w82n_n2w8",
-  `!i. i <= 256**8 - 1 ==> w82n (n2w8 i) = i`,
-  rw[w82n_def,n2w8_def] >>
+Theorem w82n_n2w8
+  `!i. i <= 256**8 - 1 ==> w82n (n2w8 i) = i`
+  (rw[w82n_def,n2w8_def] >>
   `0 < (256 : num)` by fs[] >> imp_res_tac DIVISION >> fs[] >> rw[] >>
   NTAC 6(qmatch_abbrev_tac`256* i0 + x MOD 256 = x` >>
       `i0 = x DIV 256` suffices_by fs[] >>
@@ -56,9 +56,9 @@ val w82n_n2w8 = Q.store_thm("w82n_n2w8",
   fs[DIV_LE_X]);
 
 
-val nw8_w8n = Q.store_thm("nw8_nw8",
-  `!b. LENGTH b = 8 ==> n2w8 (w82n b) = b`,
-  Cases_on`b` >> fs[] >>
+Theorem nw8_w8n
+  `!b. LENGTH b = 8 ==> n2w8 (w82n b) = b`
+  (Cases_on`b` >> fs[] >>
   NTAC 4 (Cases_on`t` >> fs[] >> Cases_on`t'` >> fs[]) >>
   fs[w82n_def,n2w8_def] >> rpt (TRY strip_tac
   >-(rpt(qmatch_goalsub_abbrev_tac`(a + 256 * b) DIV m` >>
@@ -76,11 +76,11 @@ val nw8_w8n = Q.store_thm("nw8_nw8",
      `256w : word8 = 0w` by fs[GSYM n2w_dimword] >>
      first_x_assum (fn x => PURE_REWRITE_TAC[x]) >> fs[])));
 
-val LENGTH_n2w2 = Q.store_thm("LENGTH_n2w2",
-  `!n. LENGTH(n2w2 n) = 2`,
-  fs[n2w2_def]);
+Theorem LENGTH_n2w2
+  `!n. LENGTH(n2w2 n) = 2`
+  (fs[n2w2_def]);
 
-val LENGTH_n2w8 = Q.store_thm("LENGTH_n2w8",
-  `!n. LENGTH(n2w8 n) = 8`,
-  fs[n2w8_def])
+Theorem LENGTH_n2w8
+  `!n. LENGTH(n2w8 n) = 8`
+  (fs[n2w8_def])
 val _ = export_theory()

basis/README.md

@@ -106,6 +106,10 @@ Instantiate the CakeML FFI oracle for the oracle of the basis library.
 [clFFIScript.sml](clFFIScript.sml):
 Logical model of the commandline state: simply a list of mlstrings
 
+[dependency-order](dependency-order):
+This file records the current, linear dependency order between the
+translation/CF theories making up the basis library verification.
+
 [fsFFIPropsScript.sml](fsFFIPropsScript.sml):
 Lemmas about the file system model used by the proof about TextIO.