Prove word_and_lsl_eq_0

HOL-Theorem-Prover · Dec 15, 2024 · db90904 · db90904
1 parent 5fb53e4
commit db90904
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
@@ -5083,6 +5083,15 @@ Proof
   rw[l2w_def]
 QED
 
+Theorem word_and_lsl_eq_0:
+  w2n w1 < 2 ** n ==> w1 && w2 << n = 0w
+Proof
+  Cases_on`w1` \\ Cases_on`w2`
+  \\ rw[word_and_n2w, word_lsl_n2w]
+  \\ drule BITWISE_AND_SHIFT_EQ_0
+  \\ simp[]
+QED
+
 (* -------------------------------------------------------------------------
     Theorems about word_{to,from}_bin_list
    ------------------------------------------------------------------------- *)

diff --git a/src/num/extra_theories/bitScript.sml b/src/num/extra_theories/bitScript.sml
@@ -1560,4 +1560,21 @@ Proof
   \\ SRW_TAC[][BITWISE_AND_0_lemma]
 QED
 
+Theorem BITWISE_AND_SHIFT_EQ_0:
+  !w x y n.
+  x < 2 ** n ==>
+  BITWISE w $/\ x (y * 2 ** n) = 0
+Proof
+  Induct \\ SRW_TAC[][BITWISE_def, SBIT_def]
+  \\ strip_tac
+  \\ Cases_on`w < n`
+  >- ( drule BIT_SHIFT_THM3 \\ simp[]
+       \\ Q.EXISTS_TAC`y` \\ simp[])
+  \\ FULL_SIMP_TAC(srw_ss())[NOT_LESS]
+  \\ drule TWOEXP_MONO2 \\ strip_tac
+  \\ `x < 2 ** w` by METIS_TAC[LESS_LESS_EQ_TRANS]
+  \\ drule NOT_BIT_GT_TWOEXP
+  \\ simp[]
+QED
+
 val _ = export_theory()