lib: add lemmas relating the maxium word and -1

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
seL4 · Oct 2, 2024 · 1eb4955 · 1eb4955
1 parent 83a161d
commit 1eb4955
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/lib/Word_Lib/Word_32.thy b/lib/Word_Lib/Word_32.thy
@@ -172,6 +172,10 @@ lemma word32_and_max_simp:
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 
+lemma max_minus_one_word32:
+  "(0xFFFFFFFF :: word32) = - 1"
+  by (simp add: maxBound_word)
+
 end
 
 end
diff --git a/lib/Word_Lib/Word_64.thy b/lib/Word_Lib/Word_64.thy
@@ -144,6 +144,10 @@ lemma word64_and_max_simp:
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 
+lemma max_minus_one_word64:
+  "(0xFFFFFFFFFFFFFFFF :: word64) = - 1"
+  by (simp add: maxBound_word)
+
 end
 
 end