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

Word_Lib: add le_mask_shiftl_le_mask

This commit is contained in:
Matthew Brecknell 2017-04-26 14:18:02 +10:00 committed by Alejandro Gomez-Londono
parent 220fa70586
commit 0bbfb85d85
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/Word_Lib/Word_Lemmas.thy
View File

@ -2021,6 +2021,9 @@ lemma and_mask_shiftl_comm:
"m+n \<le> size w \<Longrightarrow> (w && mask m) << n = (w << n) && mask (m+n)"
by (simp add: and_mask word_size shiftl_shiftl) (simp add: shiftl_shiftr1)
lemma le_mask_shiftl_le_mask: "s = m + n \<Longrightarrow> x \<le> mask n \<Longrightarrow> x << m \<le> mask s"
by (simp add: le_mask_iff shiftl_shiftr3)
lemma and_not_mask_twice:
"(w && ~~ mask n) && ~~ mask m = w && ~~ mask (max m n)"
apply (simp add: and_not_mask)