adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

word_lib: laws about min, max, and NOT 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-02-25 12:18:52 +11:00
parent d163d41b63
commit b72e177677
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
2 changed files with 27 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
lib/Word_Lib/Word_Lemmas.thy
View File

@ -16,6 +16,7 @@ theory Word_Lemmas
Enumeration_Word
Aligned
Bit_Shifts_Infix_Syntax
Boolean_Inequalities
Word_EqI
begin
@ -25,6 +26,32 @@ context
includes bit_operations_syntax
begin
lemma word_max_le_or:
"max x y \<le> x OR y" for x :: "'a::len word"
by (simp add: word_bool_le_funs)
lemma word_and_le_min:
"x AND y \<le> min x y" for x :: "'a::len word"
by (simp add: word_bool_le_funs)
lemma word_not_le_eq:
"(NOT x \<le> y) = (NOT y \<le> x)" for x :: "'a::len word"
by transfer (auto simp: take_bit_not_eq_mask_diff)
lemma word_not_le_not_eq[simp]:
"(NOT y \<le> NOT x) = (x \<le> y)" for x :: "'a::len word"
by (subst word_not_le_eq) simp
lemma not_min_eq:
"NOT (min x y) = max (NOT x) (NOT y)" for x :: "'a::len word"
unfolding min_def max_def
by auto
lemma not_max_eq:
"NOT (max x y) = min (NOT x) (NOT y)" for x :: "'a::len word"
unfolding min_def max_def
by auto
lemma ucast_le_ucast_eq:
fixes x y :: "'a::len word"
assumes x: "x < 2 ^ n"

1
lib/Word_Lib/Word_Lib_Sumo.thy
View File

@ -16,7 +16,6 @@ imports
Bits_Int
Bitwise_Signed
Bitwise
Boolean_Inequalities
Enumeration_Word
Generic_set_bit
Hex_Words