Skip to content
Permalink
Browse files

Merge with latest master

  • Loading branch information...
HeikoBecker committed May 22, 2019
2 parents ba179ab + 2197558 commit 832ba913bb8d71bbd0514342d905cd372210464b
Showing 322 changed files with 53,995 additions and 38,154 deletions.

Large diffs are not rendered by default.

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

Theorem 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)
Proof
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 ]
\\ fs[set_sepTheory.one_def]);
\\ fs[set_sepTheory.one_def]
QED

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)

Theorem CommandLine_read16bit
`2 <= LENGTH a ==>
Theorem CommandLine_read16bit:
2 <= LENGTH a ==>
app (p:'ffi ffi_proj) CommandLine_read16bit_v [av]
(W8ARRAY av a)
(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
(POSTv v. W8ARRAY av a * & NUM (w2n (EL 0 a) + 256 * w2n (EL 1 a)) v)
Proof
xcf_with_def "CommandLine.read16bit" CommandLine_read16bit_v_def
\\ xlet_auto THEN1 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]
\\ rpt (asm_exists_tac \\ fs [])
\\ Cases_on `h` \\ Cases_on `h'` \\ fs []
\\ fs [INT_def] \\ intLib.COOPER_TAC);
\\ fs [INT_def] \\ intLib.COOPER_TAC
QED

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

val SUC_SUC_LENGTH = prove(
``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])`
THEN1 simp_tac std_ss [DROP_LENGTH_APPEND] \\ fs []);

Theorem CommandLine_cloop_spec
`!n nv av cv a.
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) CommandLine_cloop_v [av; nv; cv]
(COMMANDLINE cl * W8ARRAY av a)
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`
(rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)
Proof
rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
\\ simp [COMMANDLINE_def, cl_ffi_part_def, IOx_def, IO_def]
\\ xpull \\ qunabbrev_tac `Q`
\\ rpt (pop_assum mp_tac)
@@ -193,14 +200,16 @@ Theorem CommandLine_cloop_spec
\\ asm_rewrite_tac [TAKE_LENGTH_APPEND]
\\ 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[DROP_APPEND,DROP_LENGTH_TOO_LONG]);
\\ fs[DROP_APPEND,DROP_LENGTH_TOO_LONG]
QED

Theorem CommandLine_cline_spec
`UNIT_TYPE u uv ==>
Theorem CommandLine_cline_spec:
UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_cline_v [uv]
(COMMANDLINE cl)
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)`
(rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
(POSTv v. & LIST_TYPE STRING_TYPE cl v * COMMANDLINE cl)
Proof
rw [] \\ qpat_abbrev_tac `Q = $POSTv _`
\\ simp [COMMANDLINE_def,cl_ffi_part_def,IOx_def,IO_def]
\\ xpull \\ qunabbrev_tac `Q`
\\ 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]
\\ fs [LIST_TYPE_def]
\\ 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 mlstring_hd_v_thm = hd_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]

Theorem CommandLine_name_spec
`UNIT_TYPE u uv ==>
Theorem CommandLine_name_spec:
UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_name_v [uv]
(COMMANDLINE cl)
(POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)`
(xcf_with_def "CommandLine.name" CommandLine_name_v_def
(POSTv namev. & STRING_TYPE (HD cl) namev * COMMANDLINE cl)
Proof
xcf_with_def "CommandLine.name" CommandLine_name_v_def
\\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
>-(xapp \\ rw[] \\ fs [])
\\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] )
\\ 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 mlstring_tl_v_thm = tl_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]

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

Theorem EvalM_name
`Eval env exp (UNIT_TYPE u) /\
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]
\\ metis_tac [CommandLine_name_spec]);
(COMMANDLINE,p:'ffi ffi_proj)
Proof
ho_match_mp_tac EvalM_from_app \\ rw [name_def]
\\ metis_tac [CommandLine_name_spec]
QED

Theorem CommandLine_arguments_spec
`UNIT_TYPE u uv ==>
Theorem CommandLine_arguments_spec:
UNIT_TYPE u uv ==>
app (p:'ffi ffi_proj) CommandLine_arguments_v [uv]
(COMMANDLINE cl)
(POSTv argv. & LIST_TYPE STRING_TYPE
(TL cl) argv * COMMANDLINE cl)`
(xcf_with_def "CommandLine.arguments" CommandLine_arguments_v_def
(TL cl) argv * COMMANDLINE cl)
Proof
xcf_with_def "CommandLine.arguments" CommandLine_arguments_v_def
\\ xlet `POSTv cs. & LIST_TYPE STRING_TYPE cl cs * COMMANDLINE cl`
>-(xapp \\ rw[] \\ fs [])
\\ Cases_on`cl=[]` >- ( fs[COMMANDLINE_def] \\ xpull \\ fs[wfcl_def] )
\\ 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 `
arguments () = (\cl. (Success (TL cl), cl))`

Theorem EvalM_arguments
`Eval env exp (UNIT_TYPE u) /\
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]
\\ metis_tac [CommandLine_arguments_spec]);
(COMMANDLINE,p:'ffi ffi_proj)
Proof
ho_match_mp_tac EvalM_from_app \\ rw [arguments_def]
\\ metis_tac [CommandLine_arguments_spec]
QED

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

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,
Theorem UNIQUE_COMMANDLINE:
!s cl1 cl2 H1 H2. VALID_HEAP s ==>
(COMMANDLINE cl1 * H1) s /\ (COMMANDLINE cl2 * H2) s ==> cl2 = cl1
Proof
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]);
\\ metis_tac[decode_encode,SOME_11]
QED

Theorem 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)
Proof
prove_hprop_inj_tac UNIQUE_COMMANDLINE
QED

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_range_unsafe_side_def = theorem"fromchars_range_unsafe_side_def";

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]);
Theorem fromchars_unsafe_side_thm:
∀n s. n ≤ LENGTH s ⇒ fromchars_unsafe_side n (strlit s)
Proof
completeInduct_on`n` \\ rw[]
\\ rw[Once fromchars_unsafe_side_def,fromchars_range_unsafe_side_def]
QED

val fromString_unsafe_side = Q.prove(
`∀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_range_side_def = theorem"fromchars_range_side_def";

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]);
Theorem fromchars_side_thm:
∀n s. n ≤ LENGTH s ⇒ fromchars_side n (strlit s)
Proof
completeInduct_on`n` \\ rw[]
\\ rw[Once fromchars_side_def,fromchars_range_side_def]
QED

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

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

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

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

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

0 comments on commit 832ba91

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