From 0bbfb85d8505531bb989b45afaa02fee35ad483c Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Date: Wed, 26 Apr 2017 14:18:02 +1000
Subject: [PATCH] Word_Lib: add le_mask_shiftl_le_mask

---
 lib/Word_Lib/Word_Lemmas.thy | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy
index dac9bf242..287c4e2c0 100644
--- a/lib/Word_Lib/Word_Lemmas.thy
+++ b/lib/Word_Lib/Word_Lemmas.thy
@@ -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)