Merge pull request #635 from CakeML/thm

Extirpate intermediate theorem syntax
CakeML · May 22, 2019 · 2197558 · 2197558
2 parents c3cbbfd + cfefc5e
commit 2197558
Show file tree

Hide file tree

Showing 318 changed files with 54,008 additions and 38,183 deletions.
diff --git a/basis/ArrayProofScript.sml b/basis/ArrayProofScript.sml
diff --git a/basis/CommandLineProofScript.sml b/basis/CommandLineProofScript.sml
@@ -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();
diff --git a/basis/IntProgScript.sml b/basis/IntProgScript.sml
@@ -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`,

diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml
@@ -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 *)