Merge pull request #653 from CakeML/cleanup

Move theorems to HOL
CakeML · May 30, 2019 · 4581b24 · 4581b24
2 parents 6553fc5 + a2cd3fb
commit 4581b24
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 179 deletions.
diff --git a/compiler/bootstrap/translation/ag32ProgScript.sml b/compiler/bootstrap/translation/ag32ProgScript.sml
@@ -82,7 +82,7 @@ fun format_def def = def
                        wordsTheory.word_bits_mask,wordsTheory.WORD_MUL_LSL,
                        wordsTheory.word_mul_n2w,addressTheory.word_arith_lemma2,
                        wordsTheory.WORD_LT,word_msb_word_bit,ag32_constant_def,
-                       EVAL ``dimindex (:32)``,miscTheory.word_bit_test]
+                       EVAL ``dimindex (:32)``,wordsTheory.word_bit_test]
   |> REWRITE_RULE [word_neg];
 
 val r = translate (format_def ag32_jump_constant_def);

diff --git a/misc/miscScript.sml b/misc/miscScript.sml
@@ -943,13 +943,6 @@ Proof
   simp[numposrepTheory.l2n_lt]
 QED
 
-Theorem word_bit_test:
-   word_bit n w <=> ((w && n2w (2 ** n)) <> 0w:'a word)
-Proof
-  srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss]
-    [wordsTheory.word_index, DECIDE ``0n < d ==> (n <= d - 1) = (n < d)``]
-QED
-
 val least_from_def = Define`
   least_from P n = if (∃x. P x ∧ n ≤ x) then $LEAST (λx. P x ∧ n ≤ x) else $LEAST P`
 
@@ -3562,78 +3555,6 @@ Proof
   \\ blastLib.BBLAST_TAC
 QED
 
-(* TODO - candidate for move to HOL *)
-Theorem byte_align_aligned:
-   byte_aligned x ⇔ (byte_align x = x)
-Proof
-EVAL_TAC
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem byte_aligned_add:
-   byte_aligned x ∧ byte_aligned y ⇒ byte_aligned (x+y)
-Proof
-  rw[alignmentTheory.byte_aligned_def]
-  \\ metis_tac[alignmentTheory.aligned_add_sub_cor]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem align_ls:
-   align p n <=+ n
-Proof
-  simp[WORD_LS]
-  \\ Cases_on`n`
-  \\ fs[alignmentTheory.align_w2n]
-  \\ qmatch_asmsub_rename_tac`n < _`
-  \\ DEP_REWRITE_TAC[LESS_MOD]
-  \\ conj_asm2_tac >- fs[]
-  \\ DEP_REWRITE_TAC[GSYM X_LE_DIV]
-  \\ simp[]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem align_lo:
-   ¬aligned p n ⇒ align p n <+ n
-Proof
-  simp[WORD_LO]
-  \\ Cases_on`n`
-  \\ fs[alignmentTheory.align_w2n, alignmentTheory.aligned_def]
-  \\ strip_tac
-  \\ qmatch_goalsub_abbrev_tac`a < b`
-  \\ `a ≤ b` suffices_by fs[]
-  \\ qmatch_asmsub_rename_tac`n < _`
-  \\ simp[Abbr`a`]
-  \\ DEP_REWRITE_TAC[LESS_MOD]
-  \\ conj_asm2_tac >- fs[]
-  \\ DEP_REWRITE_TAC[GSYM X_LE_DIV]
-  \\ simp[]
-QED
-
-Theorem aligned_between:
-   ¬aligned p n ∧ aligned p m ∧ align p n <+ m ⇒ n <+ m
-Proof
-  rw[WORD_LO]
-  \\ fs[alignmentTheory.align_w2n, alignmentTheory.aligned_def]
-  \\ Cases_on`n` \\ Cases_on`m` \\ fs[]
-  \\ CCONTR_TAC \\ fs[NOT_LESS]
-  \\ qmatch_asmsub_abbrev_tac`n DIV d * d`
-  \\ `n DIV d * d <= n` by (
-    DEP_REWRITE_TAC[GSYM X_LE_DIV] \\ fs[Abbr`d`] )
-  \\ fs[]
-  \\ qmatch_asmsub_rename_tac`(d * (m DIV d)) MOD _`
-  \\ `m DIV d * d <= m` by (
-    DEP_REWRITE_TAC[GSYM X_LE_DIV] \\ fs[Abbr`d`] )
-  \\ fs[]
-  \\ `d * (n DIV d) <= m` by metis_tac[]
-  \\ pop_assum mp_tac
-  \\ simp_tac pure_ss [Once MULT_COMM]
-  \\ DEP_REWRITE_TAC[GSYM X_LE_DIV]
-  \\ conj_tac >- simp[Abbr`d`]
-  \\ simp[NOT_LESS_EQUAL]
-  \\ `d * (m DIV d) < d * (n DIV d)` suffices_by fs[]
-  \\ metis_tac[]
-QED
-
 Theorem byte_align_IN_IMP_IN_range:
    byte_align a ∈ dm ∧
    (dm = { w | low <=+ w ∧ w <+ hi }) ∧
@@ -3655,57 +3576,6 @@ Proof
   \\ fs[alignmentTheory.byte_align_def]
 QED
 
-local
-  open alignmentTheory
-  val aligned_add_mult_lemma = Q.prove(
-    `aligned k (w + n2w (2 ** k)) = aligned k w`,
-    fs [aligned_add_sub,aligned_pow2]) |> GEN_ALL
-  val aligned_add_mult_any = Q.prove(
-    `!n w. aligned k (w + n2w (n * 2 ** k)) = aligned k w`,
-    Induct \\ fs [MULT_CLAUSES,GSYM word_add_n2w] \\ rw []
-    \\ pop_assum (qspec_then `w + n2w (2 ** k)` mp_tac)
-    \\ fs [aligned_add_mult_lemma]) |> GEN_ALL
-in
-  val aligned_add_pow = save_thm("aligned_add_pow[simp]",
-    CONJ aligned_add_mult_lemma aligned_add_mult_any)
-end
-
-Theorem align_add_aligned_gen:
-   ∀a. aligned p a ⇒ (align p (a + b) = a + align p b)
-Proof
-  completeInduct_on`w2n b`
-  \\ rw[]
-  \\ Cases_on`w2n b < 2 ** p`
-  >- (
-    simp[alignmentTheory.align_add_aligned]
-    \\ `align p b = 0w` by simp[lt_align_eq_0]
-    \\ simp[] )
-  \\ fs[NOT_LESS]
-  \\ Cases_on`w2n b = 2 ** p`
-  >- (
-    `aligned p b` by(
-      simp[alignmentTheory.aligned_def,alignmentTheory.align_w2n]
-      \\ metis_tac[n2w_w2n] )
-    \\ `aligned p (a + b)` by metis_tac[alignmentTheory.aligned_add_sub_cor]
-    \\ fs[alignmentTheory.aligned_def])
-  \\ fs[LESS_EQ_EXISTS]
-  \\ qmatch_asmsub_rename_tac`w2n b = z + _`
-  \\ first_x_assum(qspec_then`z`mp_tac)
-  \\ impl_keep_tac >- fs[]
-  \\ `z < dimword(:'a)` by metis_tac[w2n_lt, LESS_TRANS]
-  \\ disch_then(qspec_then`n2w z`mp_tac)
-  \\ impl_tac >- simp[]
-  \\ strip_tac
-  \\ first_assum(qspec_then`a + n2w (2 ** p)`mp_tac)
-  \\ impl_tac >- fs[]
-  \\ rewrite_tac[word_add_n2w, GSYM WORD_ADD_ASSOC]
-  \\ Cases_on`b` \\ fs[GSYM word_add_n2w]
-  \\ strip_tac
-  \\ first_x_assum(qspec_then`n2w (2**p)`mp_tac)
-  \\ impl_tac >- fs[aligned_w2n]
-  \\ simp[]
-QED
-
 Theorem MULT_DIV_MULT_LEMMA:
    !m l k. 0 < m /\ 0 < l ==> (m * k) DIV (l * m) = k DIV l
 Proof
@@ -3934,54 +3804,6 @@ Proof
   \\ metis_tac[WORD_ADD_ASSOC,WORD_ADD_COMM]
 QED
 
-(* TODO - candidate for move to HOL *)
-Theorem word_bit_thm:
-   !n w:'a word. word_bit n w <=> n < dimindex (:'a) /\ w ' n
-Proof
-  fs [word_bit_def,LESS_EQ] \\ rw []
-  \\ assume_tac DIMINDEX_GT_0
-  \\ Cases_on `dimindex (:α)` \\ fs [LESS_EQ]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem word_bit_and:
-   word_bit n (w1 && w2) <=> word_bit n w1 /\ word_bit n w2
-Proof
-  fs [word_bit_def,word_and_def] \\ eq_tac \\ rw []
-  \\ assume_tac DIMINDEX_GT_0
-  \\ `n < dimindex (:'a)` by decide_tac
-  \\ fs [fcpTheory.FCP_BETA]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem word_bit_or:
-   word_bit n (w1 || w2) <=> word_bit n w1 \/ word_bit n w2
-Proof
-  fs [word_bit_def,word_or_def] \\ eq_tac \\ rw []
-  \\ assume_tac DIMINDEX_GT_0
-  \\ `n < dimindex (:'a)` by decide_tac
-  \\ fs [fcpTheory.FCP_BETA]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem word_bit_lsl:
-   word_bit n (w << i) <=>
-    word_bit (n - i) (w:'a word) /\ n < dimindex (:'a) /\ i <= n
-Proof
-  fs [word_bit_thm,word_lsl_def] \\ eq_tac \\ fs []
-  \\ rw [] \\ rfs [fcpTheory.FCP_BETA]
-QED
-
-(* TODO - candidate for move to HOL *)
-Theorem word_msb_align:
-   p < dimindex(:'a) ⇒ (word_msb (align p w) = word_msb (w:'a word))
-Proof
-  rw[alignmentTheory.align_bitwise_and,word_msb]
-  \\ rw[word_bit_and]
-  \\ rw[word_bit_lsl]
-  \\ rw[word_bit_test, MOD_EQ_0_DIVISOR, dimword_def]
-QED
-
 (* TODO: move to sptTheory *)
 
 val eq_shape_def = Define `