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

lib: miscellaneous word lemmas

This commit is contained in:
Matthew Brecknell 2018-04-04 08:38:52 +10:00 committed by Joel Beeren
parent dc2069aba0
commit 1ec4a8b12c
2 changed files with 19 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/Word_Lib/Word_Lemmas.thy
View File

@ -5558,6 +5558,18 @@ lemma max_word_not_0:
"max_word \<noteq> 0"
by (simp add: max_word_minus)
lemma ucast_zero_is_aligned:
"UCAST('a::len \<rightarrow> 'b::len) w = 0 \<Longrightarrow> n \<le> LENGTH('b) \<Longrightarrow> is_aligned w n"
by (clarsimp simp: is_aligned_mask word_eq_iff word_size nth_ucast)
lemma unat_ucast_eq_unat_and_mask:
"unat (UCAST('b::len \<rightarrow> 'a::len) w) = unat (w && mask LENGTH('a))"
proof -
have "unat (UCAST('b \<rightarrow> 'a) w) = unat (UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) w))"
by (cases "LENGTH('a) < LENGTH('b)"; simp add: is_down ucast_ucast_a unat_ucast_up_simp)
thus ?thesis using ucast_ucast_mask by simp
qed
(* Miscellaneous conditional injectivity rules. *)
lemma drop_eq_mono:

14
lib/Word_Lib/Word_Lib.thy
View File

@ -131,13 +131,6 @@ lemma shiftl_power:
lemmas of_bl_reasoning = to_bl_use_of_bl of_bl_append
(*TODO: delete, this will be in the Isabelle main distribution in future*)
lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
unfolding bl_to_bin_def
proof(induction bs)
case(Cons b bs) with bl_to_bin_lt2p_aux[where w=1] show ?case by simp
qed simp
lemma uint_of_bl_is_bl_to_bin_drop:
"length (dropWhile Not l) \<le> len_of TYPE('a) \<Longrightarrow> uint (of_bl l :: 'a::len word) = bl_to_bin l"
apply (simp add: of_bl_def)
@ -191,6 +184,10 @@ lemma AND_twice [simp]:
"(w && m) && m = w && m"
by (simp add: word_eqI)
lemma word_combine_masks:
"w && m = z \<Longrightarrow> w && m' = z' \<Longrightarrow> w && (m || m') = (z || z')"
by (auto simp: word_eq_iff)
lemma nth_w2p_same:
"(2^n :: 'a :: len word) !! n = (n < len_of TYPE('a))"
by (simp add : nth_w2p)
@ -258,6 +255,9 @@ lemma and_mask_arith:
lemma mask_2pm1: "mask n = 2 ^ n - 1"
by (simp add : mask_def)
lemma word_and_mask_le_2pm1: "w && mask n \<le> 2 ^ n - 1"
by (simp add: mask_2pm1[symmetric] word_and_le1)
lemma is_aligned_AND_less_0:
"u && mask n = 0 \<Longrightarrow> v < 2^n \<Longrightarrow> u && v = 0"
apply (drule less_mask_eq)