Skip to content
Permalink
Browse files

Extirpate intermediate theorem syntax

This commit replaces all(?) occurrences of the old-style Theorem syntax

Theorem name
 `thm_statement
 `
 (tactic)

with

Theorem name:
 thm_statement
Proof
 tactic
QED

Instances of the Theorem syntax that get piped into forward reasoning
are treated specially, as per a suggestion by @mn2000. So

Theorem name
  `thm_statement`
  (tactic)
  |> forward_rules;

maps to

Theorem name = Q.prove(`
  thm_statement`,
  tactic)
  |> forward_rules;

This will produce silly output in some cases (if the forward
rules end in a call to save_thm, the theorem gets saved twice),
but it seems not worth it to try to detect this automatically.
  • Loading branch information...
IlmariReissumies committed May 20, 2019
1 parent c3cbbfd commit c0c414227216aeb093403783caa3a56449bfb337
Showing 315 changed files with 53,951 additions and 38,131 deletions.

Large diffs are not rendered by default.

@@ -30,23 +30,26 @@ val COMMANDLINE_precond = Q.prove(
rw[set_thm]) |> UNDISCH rw[set_thm]) |> UNDISCH
|> curry save_thm "COMMANDLINE_precond"; |> curry save_thm "COMMANDLINE_precond";


Theorem COMMANDLINE_FFI_part_hprop Theorem COMMANDLINE_FFI_part_hprop:
`FFI_part_hprop (COMMANDLINE x)` FFI_part_hprop (COMMANDLINE x)
(rw [COMMANDLINE_def,cfHeapsBaseTheory.IO_def,cfMainTheory.FFI_part_hprop_def, Proof
rw [COMMANDLINE_def,cfHeapsBaseTheory.IO_def,cfMainTheory.FFI_part_hprop_def,
cfHeapsBaseTheory.IOx_def, cl_ffi_part_def, cfHeapsBaseTheory.IOx_def, cl_ffi_part_def,
set_sepTheory.SEP_CLAUSES,set_sepTheory.SEP_EXISTS_THM, set_sepTheory.SEP_CLAUSES,set_sepTheory.SEP_EXISTS_THM,
set_sepTheory.cond_STAR ] set_sepTheory.cond_STAR ]
\\ fs[set_sepTheory.one_def]); \\ fs[set_sepTheory.one_def]
QED


val eq_v_thm = fetch "mlbasicsProg" "eq_v_thm" val eq_v_thm = fetch "mlbasicsProg" "eq_v_thm"
val eq_num_v_thm = MATCH_MP (DISCH_ALL eq_v_thm) (EqualityType_NUM_BOOL |> CONJUNCT1) val eq_num_v_thm = MATCH_MP (DISCH_ALL eq_v_thm) (EqualityType_NUM_BOOL |> CONJUNCT1)


Theorem CommandLine_read16bit Theorem CommandLine_read16bit:
`2 <= LENGTH a ==> 2 <= LENGTH a ==>
app (p:'ffi ffi_proj) CommandLine_read16bit_v [av] app (p:'ffi ffi_proj) CommandLine_read16bit_v [av]
(W8ARRAY av a) (W8ARRAY av a)
(POSTv v. W8ARRAY av a * & NUM (w2n (EL 0 a) + 256 * w2n (EL 1 a)) v)` (POSTv v. W8ARRAY av a * & NUM (w2n (EL 0 a) + 256 * w2n (EL 1 a)) v)
(xcf_with_def "CommandLine.read16bit" CommandLine_read16bit_v_def Proof
xcf_with_def "CommandLine.read16bit" CommandLine_read16bit_v_def
\\ xlet_auto THEN1 xsimpl \\ xlet_auto THEN1 xsimpl
\\ xlet_auto THEN1 (fs [] \\ xsimpl) \\ xlet_auto THEN1 (fs [] \\ xsimpl)
\\ xlet_auto THEN1 (fs [] \\ xsimpl) \\ xlet_auto THEN1 (fs [] \\ xsimpl)
@@ -56,22 +59,25 @@ Theorem CommandLine_read16bit
\\ Cases_on `a` \\ fs [] \\ Cases_on `t` \\ fs [NUM_def] \\ Cases_on `a` \\ fs [] \\ Cases_on `t` \\ fs [NUM_def]
\\ rpt (asm_exists_tac \\ fs []) \\ rpt (asm_exists_tac \\ fs [])
\\ Cases_on `h` \\ Cases_on `h'` \\ fs [] \\ Cases_on `h` \\ Cases_on `h'` \\ fs []
\\ fs [INT_def] \\ intLib.COOPER_TAC); \\ fs [INT_def] \\ intLib.COOPER_TAC
QED


Theorem CommandLine_write16bit Theorem CommandLine_write16bit:
`NUM n nv /\ 2 <= LENGTH a ==> NUM n nv /\ 2 <= LENGTH a ==>
app (p:'ffi ffi_proj) CommandLine_write16bit_v [av;nv] app (p:'ffi ffi_proj) CommandLine_write16bit_v [av;nv]
(W8ARRAY av a) (W8ARRAY av a)
(POSTv v. W8ARRAY av (n2w n::n2w (n DIV 256)::TL (TL a)))` (POSTv v. W8ARRAY av (n2w n::n2w (n DIV 256)::TL (TL a)))
(xcf_with_def "CommandLine.write16bit" CommandLine_write16bit_v_def Proof
xcf_with_def "CommandLine.write16bit" CommandLine_write16bit_v_def
\\ xlet_auto THEN1 xsimpl \\ xlet_auto THEN1 xsimpl
\\ xlet_auto THEN1 (fs [] \\ xsimpl) \\ xlet_auto THEN1 (fs [] \\ xsimpl)
\\ xlet_auto THEN1 (fs [] \\ xsimpl) \\ xlet_auto THEN1 (fs [] \\ xsimpl)
\\ xlet_auto THEN1 (fs [] \\ xsimpl) \\ xlet_auto THEN1 (fs [] \\ xsimpl)
\\ xapp \\ xsimpl \\ xapp \\ xsimpl
\\ Cases_on `a` \\ fs [] \\ Cases_on `t` \\ fs [NUM_def] \\ Cases_on `a` \\ fs [] \\ Cases_on `t` \\ fs [NUM_def]
\\ rpt (asm_exists_tac \\ fs []) \\ rpt (asm_exists_tac \\ fs [])
\\ EVAL_TAC); \\ EVAL_TAC
QED


val SUC_SUC_LENGTH = prove( val SUC_SUC_LENGTH = prove(
``SUC (SUC (LENGTH (TL (TL (REPLICATE (MAX 2 n) x))))) = (MAX 2 n)``, ``SUC (SUC (LENGTH (TL (TL (REPLICATE (MAX 2 n) x))))) = (MAX 2 n)``,
@@ -103,14 +109,15 @@ val DROP_SUC_LENGTH_MAP = prove(
SUC (LENGTH ys) = LENGTH (MAP f ys ⧺ [y])` SUC (LENGTH ys) = LENGTH (MAP f ys ⧺ [y])`
THEN1 simp_tac std_ss [DROP_LENGTH_APPEND] \\ fs []); THEN1 simp_tac std_ss [DROP_LENGTH_APPEND] \\ fs []);


Theorem CommandLine_cloop_spec Theorem CommandLine_cloop_spec:
`!n nv av cv a. !n nv av cv a.
LIST_TYPE STRING_TYPE (DROP n cl) cv /\ LIST_TYPE STRING_TYPE (DROP n cl) cv /\
NUM n nv /\ n <= LENGTH cl /\ LENGTH a = 2 ==> NUM n nv /\ n <= LENGTH cl /\ LENGTH a = 2 ==>
app (p:'ffi ffi_proj) CommandLine_cloop_v [av; nv; cv] app (p:'ffi ffi_proj) CommandLine_cloop_v [av; nv; cv]
(COMMANDLINE cl * W8ARRAY av a) (COMMANDLINE cl * W8ARRAY av a)
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)` (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)
(rw [] \\ qpat_abbrev_tac `Q = $POSTv _` Proof
rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
\\ simp [COMMANDLINE_def, cl_ffi_part_def, IOx_def, IO_def] \\ simp [COMMANDLINE_def, cl_ffi_part_def, IOx_def, IO_def]
\\ xpull \\ qunabbrev_tac `Q` \\ xpull \\ qunabbrev_tac `Q`
\\ rpt (pop_assum mp_tac) \\ rpt (pop_assum mp_tac)
@@ -193,14 +200,16 @@ Theorem CommandLine_cloop_spec
\\ asm_rewrite_tac [TAKE_LENGTH_APPEND] \\ asm_rewrite_tac [TAKE_LENGTH_APPEND]
\\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND,EL_LENGTH_APPEND,NULL,HD] \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND,EL_LENGTH_APPEND,NULL,HD]
\\ fs [MAP_MAP_o, CHR_w2n_n2w_ORD, GSYM mlstringTheory.implode_def] \\ fs [MAP_MAP_o, CHR_w2n_n2w_ORD, GSYM mlstringTheory.implode_def]
\\ fs[DROP_APPEND,DROP_LENGTH_TOO_LONG]); \\ fs[DROP_APPEND,DROP_LENGTH_TOO_LONG]
QED


Theorem CommandLine_cline_spec Theorem CommandLine_cline_spec:
`UNIT_TYPE u uv ==> UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_cline_v [uv] app (p:'ffi ffi_proj) CommandLine_cline_v [uv]
(COMMANDLINE cl) (COMMANDLINE cl)
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)` (POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)
(rw [] \\ qpat_abbrev_tac `Q = $POSTv _` Proof
rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
\\ simp [COMMANDLINE_def,cl_ffi_part_def,IOx_def,IO_def] \\ simp [COMMANDLINE_def,cl_ffi_part_def,IOx_def,IO_def]
\\ xpull \\ qunabbrev_tac `Q` \\ xpull \\ qunabbrev_tac `Q`
\\ xcf_with_def "CommandLine.cline" CommandLine_cline_v_def \\ xcf_with_def "CommandLine.cline" CommandLine_cline_v_def
@@ -240,80 +249,93 @@ Theorem CommandLine_cline_spec
\\ `DROP (LENGTH cl) cl = []` by fs [DROP_NIL] \\ `DROP (LENGTH cl) cl = []` by fs [DROP_NIL]
\\ fs [LIST_TYPE_def] \\ fs [LIST_TYPE_def]
\\ fs [wfcl_def] \\ rfs [two_byte_sum] \\ fs [wfcl_def] \\ rfs [two_byte_sum]
\\ rw [] \\ qexists_tac `x` \\ xsimpl); \\ rw [] \\ qexists_tac `x` \\ xsimpl
QED


val hd_v_thm = fetch "ListProg" "hd_v_thm"; val hd_v_thm = fetch "ListProg" "hd_v_thm";
val mlstring_hd_v_thm = hd_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty] val mlstring_hd_v_thm = hd_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]


Theorem CommandLine_name_spec Theorem CommandLine_name_spec:
`UNIT_TYPE u uv ==> UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_name_v [uv] app (p:'ffi ffi_proj) CommandLine_name_v [uv]
(COMMANDLINE cl) (COMMANDLINE cl)
(POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)` (POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)
(xcf_with_def "CommandLine.name" CommandLine_name_v_def Proof
xcf_with_def "CommandLine.name" CommandLine_name_v_def
\\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl` \\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
>-(xapp \\ rw[] \\ fs []) >-(xapp \\ rw[] \\ fs [])
\\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] ) \\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] )
\\ xapp_spec mlstring_hd_v_thm \\ xapp_spec mlstring_hd_v_thm
\\ xsimpl \\ instantiate \\ Cases_on `cl` \\ rw[]); \\ xsimpl \\ instantiate \\ Cases_on `cl` \\ rw[]
QED


val tl_v_thm = fetch "ListProg" "tl_v_thm"; val tl_v_thm = fetch "ListProg" "tl_v_thm";
val mlstring_tl_v_thm = tl_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty] val mlstring_tl_v_thm = tl_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]


val name_def = Define ` val name_def = Define `
name () = (\cl. (Success (HD cl), cl))`; name () = (\cl. (Success (HD cl), cl))`;


Theorem EvalM_name Theorem EvalM_name:
`Eval env exp (UNIT_TYPE u) /\ Eval env exp (UNIT_TYPE u) /\
(nsLookup env.v (Long "CommandLine" (Short "name")) = (nsLookup env.v (Long "CommandLine" (Short "name")) =
SOME CommandLine_name_v) ==> SOME CommandLine_name_v) ==>
EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "name")); exp]) EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "name")); exp])
(MONAD STRING_TYPE exc_ty (name u)) (MONAD STRING_TYPE exc_ty (name u))
(COMMANDLINE,p:'ffi ffi_proj)` (COMMANDLINE,p:'ffi ffi_proj)
(ho_match_mp_tac EvalM_from_app \\ rw [name_def] Proof
\\ metis_tac [CommandLine_name_spec]); ho_match_mp_tac EvalM_from_app \\ rw [name_def]
\\ metis_tac [CommandLine_name_spec]
QED


Theorem CommandLine_arguments_spec Theorem CommandLine_arguments_spec:
`UNIT_TYPE u uv ==> UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_arguments_v [uv] app (p:'ffi ffi_proj) CommandLine_arguments_v [uv]
(COMMANDLINE cl) (COMMANDLINE cl)
(POSTv argv. & LIST_TYPE STRING_TYPE (POSTv argv. & LIST_TYPE STRING_TYPE
(TL cl) argv * COMMANDLINE cl)` (TL cl) argv * COMMANDLINE cl)
(xcf_with_def "CommandLine.arguments" CommandLine_arguments_v_def Proof
xcf_with_def "CommandLine.arguments" CommandLine_arguments_v_def
\\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl` \\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
>-(xapp \\ rw[] \\ fs []) >-(xapp \\ rw[] \\ fs [])
\\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] ) \\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] )
\\ xapp_spec mlstring_tl_v_thm \\ xsimpl \\ instantiate \\ xapp_spec mlstring_tl_v_thm \\ xsimpl \\ instantiate
\\ Cases_on `cl` \\ rw[TL_DEF]); \\ Cases_on `cl` \\ rw[TL_DEF]
QED


val arguments_def = Define ` val arguments_def = Define `
arguments () = (\cl. (Success (TL cl), cl))` arguments () = (\cl. (Success (TL cl), cl))`


Theorem EvalM_arguments Theorem EvalM_arguments:
`Eval env exp (UNIT_TYPE u) /\ Eval env exp (UNIT_TYPE u) /\
(nsLookup env.v (Long "CommandLine" (Short "arguments")) = (nsLookup env.v (Long "CommandLine" (Short "arguments")) =
SOME CommandLine_arguments_v) ==> SOME CommandLine_arguments_v) ==>
EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "arguments")); exp]) EvalM F env st (App Opapp [Var (Long "CommandLine" (Short "arguments")); exp])
(MONAD (LIST_TYPE STRING_TYPE) exc_ty (arguments u)) (MONAD (LIST_TYPE STRING_TYPE) exc_ty (arguments u))
(COMMANDLINE,p:'ffi ffi_proj)` (COMMANDLINE,p:'ffi ffi_proj)
(ho_match_mp_tac EvalM_from_app \\ rw [arguments_def] Proof
\\ metis_tac [CommandLine_arguments_spec]); ho_match_mp_tac EvalM_from_app \\ rw [arguments_def]
\\ metis_tac [CommandLine_arguments_spec]
QED


fun prove_hprop_inj_tac thm = fun prove_hprop_inj_tac thm =
rw[HPROP_INJ_def, GSYM STAR_ASSOC, SEP_CLAUSES, SEP_EXISTS_THM, HCOND_EXTRACT] >> rw[HPROP_INJ_def, GSYM STAR_ASSOC, SEP_CLAUSES, SEP_EXISTS_THM, HCOND_EXTRACT] >>
EQ_TAC >-(DISCH_TAC >> IMP_RES_TAC thm >> rw[]) >> rw[]; EQ_TAC >-(DISCH_TAC >> IMP_RES_TAC thm >> rw[]) >> rw[];


Theorem UNIQUE_COMMANDLINE Theorem UNIQUE_COMMANDLINE:
`!s cl1 cl2 H1 H2. VALID_HEAP s ==> !s cl1 cl2 H1 H2. VALID_HEAP s ==>
(COMMANDLINE cl1 * H1) s /\ (COMMANDLINE cl2 * H2) s ==> cl2 = cl1` (COMMANDLINE cl1 * H1) s /\ (COMMANDLINE cl2 * H2) s ==> cl2 = cl1
(rw[COMMANDLINE_def,cfHeapsBaseTheory.IOx_def,cl_ffi_part_def, Proof
rw[COMMANDLINE_def,cfHeapsBaseTheory.IOx_def,cl_ffi_part_def,
GSYM STAR_ASSOC] GSYM STAR_ASSOC]
\\ IMP_RES_TAC FRAME_UNIQUE_IO \\ IMP_RES_TAC FRAME_UNIQUE_IO
\\ fs[] \\ rw[] \\ fs[] \\ rw[]
\\ metis_tac[decode_encode,SOME_11]); \\ metis_tac[decode_encode,SOME_11]
QED


Theorem COMMANDLINE_HPROP_INJ[hprop_inj] Theorem COMMANDLINE_HPROP_INJ[hprop_inj]:
`!cl1 cl2. HPROP_INJ (COMMANDLINE cl1) (COMMANDLINE cl2) (cl2 = cl1)` !cl1 cl2. HPROP_INJ (COMMANDLINE cl1) (COMMANDLINE cl2) (cl2 = cl1)
(prove_hprop_inj_tac UNIQUE_COMMANDLINE); Proof
prove_hprop_inj_tac UNIQUE_COMMANDLINE
QED


val _ = export_theory(); val _ = export_theory();
@@ -93,10 +93,12 @@ val fromstring_unsafe_side_def = definition"fromstring_unsafe_side_def";
val fromchars_unsafe_side_def = theorem"fromchars_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_range_unsafe_side_def = theorem"fromchars_range_unsafe_side_def";


Theorem fromchars_unsafe_side_thm Theorem fromchars_unsafe_side_thm:
`∀n s. n ≤ LENGTH s ⇒ fromchars_unsafe_side n (strlit s)` ∀n s. n ≤ LENGTH s ⇒ fromchars_unsafe_side n (strlit s)
(completeInduct_on`n` \\ rw[] Proof
\\ rw[Once fromchars_unsafe_side_def,fromchars_range_unsafe_side_def]); completeInduct_on`n` \\ rw[]
\\ rw[Once fromchars_unsafe_side_def,fromchars_range_unsafe_side_def]
QED


val fromString_unsafe_side = Q.prove( val fromString_unsafe_side = Q.prove(
`∀x. fromstring_unsafe_side x = T`, `∀x. fromstring_unsafe_side x = T`,
@@ -123,10 +125,12 @@ val fromstring_side_def = definition"fromstring_side_def";
val fromchars_side_def = theorem"fromchars_side_def"; val fromchars_side_def = theorem"fromchars_side_def";
val fromchars_range_side_def = theorem"fromchars_range_side_def"; val fromchars_range_side_def = theorem"fromchars_range_side_def";


Theorem fromchars_side_thm Theorem fromchars_side_thm:
`∀n s. n ≤ LENGTH s ⇒ fromchars_side n (strlit s)` ∀n s. n ≤ LENGTH s ⇒ fromchars_side n (strlit s)
(completeInduct_on`n` \\ rw[] Proof
\\ rw[Once fromchars_side_def,fromchars_range_side_def]); completeInduct_on`n` \\ rw[]
\\ rw[Once fromchars_side_def,fromchars_range_side_def]
QED


val fromString_side = Q.prove( val fromString_side = Q.prove(
`∀x. fromstring_side x = T`, `∀x. fromstring_side x = T`,
@@ -23,8 +23,7 @@ val res = translate LENGTH_AUX_def;
val _ = ml_prog_update open_local_in_block; val _ = ml_prog_update open_local_in_block;


val result = next_ml_names := ["length"] val result = next_ml_names := ["length"]
val res = translate val res = translate LENGTH_AUX_THM;
(LENGTH_AUX_THM |> Q.SPECL [`xs`,`0`] |> SIMP_RULE std_ss [] |> GSYM);


val _ = ml_prog_update open_local_block; val _ = ml_prog_update open_local_block;
val res = translate REV_DEF; val res = translate REV_DEF;
@@ -78,10 +77,12 @@ val MAP_let = prove(
| (y::ys) => let z = f y in z :: MAP f ys``, | (y::ys) => let z = f y in z :: MAP f ys``,
Cases_on `xs` \\ fs []); Cases_on `xs` \\ fs []);


Theorem MAP_ind Theorem MAP_ind:
`∀P. (∀f xs. (∀y ys z. xs = y::ys ∧ z = f y ⇒ P f ys) ⇒ P f xs) ⇒ ∀P. (∀f xs. (∀y ys z. xs = y::ys ∧ z = f y ⇒ P f ys) ⇒ P f xs) ⇒
∀f xs. P f xs` ∀f xs. P f xs
(ntac 2 strip_tac \\ Induct_on `xs` \\ fs []); Proof
ntac 2 strip_tac \\ Induct_on `xs` \\ fs []
QED


val _ = add_preferred_thy "-"; (* so that the translator finds MAP_ind above *) val _ = add_preferred_thy "-"; (* so that the translator finds MAP_ind above *)


0 comments on commit c0c4142

Please sign in to comment.
You can’t perform that action at this time.