Permalink
Browse files

Replace Q.store_thm and store_thm with Theorem

  • Loading branch information...
IlmariReissumies committed Dec 3, 2018
1 parent eb5b3cc commit 8e01964e9e482215dce3c8c122df6739789ea54d
Showing 309 changed files with 25,460 additions and 26,083 deletions.

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -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();
@@ -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(
@@ -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[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[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]);

@@ -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_nw8
`!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()
Oops, something went wrong.

0 comments on commit 8e01964

Please sign in to comment.