Word_Lib: sync with AFP
This commit is contained in:
parent
62b0ab207b
commit
04f4336a5f
|
@ -286,6 +286,18 @@ lemma le_imp_diff_le:
|
||||||
"(j::nat) \<le> k \<Longrightarrow> j - n \<le> k"
|
"(j::nat) \<le> k \<Longrightarrow> j - n \<le> k"
|
||||||
by simp
|
by simp
|
||||||
|
|
||||||
|
lemma fromEnum_upto_nth:
|
||||||
|
fixes start :: "'a :: enumeration_both"
|
||||||
|
assumes "n < length [start .e. end]"
|
||||||
|
shows "fromEnum ([start .e. end] ! n) = fromEnum start + n"
|
||||||
|
proof -
|
||||||
|
have less_sub: "\<And>m k m' n. \<lbrakk> (n::nat) < m - k ; m \<le> m' \<rbrakk> \<Longrightarrow> n < m' - k" by fastforce
|
||||||
|
note upt_Suc[simp del]
|
||||||
|
show ?thesis using assms
|
||||||
|
by (fastforce simp: upto_enum_red
|
||||||
|
dest: less_sub[where m'="Suc (fromEnum maxBound)"] intro: maxBound_is_bound)
|
||||||
|
qed
|
||||||
|
|
||||||
lemma length_upto_enum_le_maxBound:
|
lemma length_upto_enum_le_maxBound:
|
||||||
fixes start :: "'a :: enumeration_both"
|
fixes start :: "'a :: enumeration_both"
|
||||||
shows "length [start .e. end] \<le> Suc (fromEnum (maxBound :: 'a))"
|
shows "length [start .e. end] \<le> Suc (fromEnum (maxBound :: 'a))"
|
||||||
|
|
|
@ -13,7 +13,7 @@ section "Lemmas with Generic Word Length"
|
||||||
theory Word_Lemmas
|
theory Word_Lemmas
|
||||||
imports
|
imports
|
||||||
Complex_Main
|
Complex_Main
|
||||||
Aligned
|
Word_Next
|
||||||
Word_Enum
|
Word_Enum
|
||||||
"HOL-Library.Sublist"
|
"HOL-Library.Sublist"
|
||||||
begin
|
begin
|
||||||
|
@ -611,18 +611,6 @@ lemma upto_enum_set_conv2:
|
||||||
shows "set [a .e. b] = {a .. b}"
|
shows "set [a .e. b] = {a .. b}"
|
||||||
by auto
|
by auto
|
||||||
|
|
||||||
lemma fromEnum_upto_nth:
|
|
||||||
fixes start :: "'a :: enumeration_both"
|
|
||||||
assumes "n < length [start .e. end]"
|
|
||||||
shows "fromEnum ([start .e. end] ! n) = fromEnum start + n"
|
|
||||||
proof -
|
|
||||||
have less_sub: "\<And>m k m' n. \<lbrakk> (n::nat) < m - k ; m \<le> m' \<rbrakk> \<Longrightarrow> n < m' - k" by fastforce
|
|
||||||
note upt_Suc[simp del]
|
|
||||||
show ?thesis using assms
|
|
||||||
by (fastforce simp: upto_enum_red
|
|
||||||
dest: less_sub[where m'="Suc (fromEnum maxBound)"] intro: maxBound_is_bound)
|
|
||||||
qed
|
|
||||||
|
|
||||||
lemma of_nat_unat [simp]:
|
lemma of_nat_unat [simp]:
|
||||||
"of_nat \<circ> unat = id"
|
"of_nat \<circ> unat = id"
|
||||||
by (rule ext, simp)
|
by (rule ext, simp)
|
||||||
|
@ -1556,20 +1544,6 @@ lemma minus_one_helper5:
|
||||||
shows "\<lbrakk>y \<noteq> 0; x \<le> y - 1 \<rbrakk> \<Longrightarrow> x < y"
|
shows "\<lbrakk>y \<noteq> 0; x \<le> y - 1 \<rbrakk> \<Longrightarrow> x < y"
|
||||||
using le_m1_iff_lt word_neq_0_conv by blast
|
using le_m1_iff_lt word_neq_0_conv by blast
|
||||||
|
|
||||||
lemma plus_one_helper[elim!]:
|
|
||||||
"x < n + (1 :: 'a :: len word) \<Longrightarrow> x \<le> n"
|
|
||||||
apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
|
|
||||||
apply (case_tac "1 + n = 0")
|
|
||||||
apply simp
|
|
||||||
apply (subst(asm) unatSuc, assumption)
|
|
||||||
apply arith
|
|
||||||
done
|
|
||||||
|
|
||||||
lemma plus_one_helper2:
|
|
||||||
"\<lbrakk> x \<le> n; n + 1 \<noteq> 0 \<rbrakk> \<Longrightarrow> x < n + (1 :: 'a :: len word)"
|
|
||||||
by (simp add: word_less_nat_alt word_le_nat_alt field_simps
|
|
||||||
unatSuc)
|
|
||||||
|
|
||||||
lemma not_greatest_aligned:
|
lemma not_greatest_aligned:
|
||||||
"\<lbrakk> x < y; is_aligned x n; is_aligned y n \<rbrakk>
|
"\<lbrakk> x < y; is_aligned x n; is_aligned y n \<rbrakk>
|
||||||
\<Longrightarrow> x + 2 ^ n \<noteq> 0"
|
\<Longrightarrow> x + 2 ^ n \<noteq> 0"
|
||||||
|
@ -2577,20 +2551,6 @@ lemma enum_word_div:
|
||||||
apply simp
|
apply simp
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma less_x_plus_1:
|
|
||||||
fixes x :: "'a :: len word" shows
|
|
||||||
"x \<noteq> max_word \<Longrightarrow> (y < (x + 1)) = (y < x \<or> y = x)"
|
|
||||||
apply (rule iffI)
|
|
||||||
apply (rule disjCI)
|
|
||||||
apply (drule plus_one_helper)
|
|
||||||
apply simp
|
|
||||||
apply (subgoal_tac "x < x + 1")
|
|
||||||
apply (erule disjE, simp_all)
|
|
||||||
apply (rule plus_one_helper2 [OF order_refl])
|
|
||||||
apply (rule notI, drule max_word_wrap)
|
|
||||||
apply simp
|
|
||||||
done
|
|
||||||
|
|
||||||
lemma of_bool_nth:
|
lemma of_bool_nth:
|
||||||
"of_bool (x !! v) = (x >> v) && 1"
|
"of_bool (x !! v) = (x >> v) && 1"
|
||||||
apply (rule word_eqI)
|
apply (rule word_eqI)
|
||||||
|
@ -5574,15 +5534,6 @@ lemma sign_extend_eq:
|
||||||
"w && mask (Suc n) = v && mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v"
|
"w && mask (Suc n) = v && mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v"
|
||||||
by (rule word_eqI, fastforce dest: word_eqD simp: sign_extend_bitwise_if' word_size)
|
by (rule word_eqI, fastforce dest: word_eqD simp: sign_extend_bitwise_if' word_size)
|
||||||
|
|
||||||
lemma unat_minus_one_word:
|
|
||||||
"unat (-1 :: 'a :: len word) = 2 ^ len_of TYPE('a) - 1"
|
|
||||||
by (subst minus_one_word)
|
|
||||||
(subst unat_sub_if', clarsimp)
|
|
||||||
|
|
||||||
lemma of_nat_eq_signed_scast:
|
|
||||||
"(of_nat x = (y :: ('a::len) signed word))
|
|
||||||
= (of_nat x = (scast y :: 'a word))"
|
|
||||||
by (metis scast_of_nat scast_scast_id(2))
|
|
||||||
|
|
||||||
lemma sign_extended_add:
|
lemma sign_extended_add:
|
||||||
assumes p: "is_aligned p n"
|
assumes p: "is_aligned p n"
|
||||||
|
@ -5685,6 +5636,60 @@ proof -
|
||||||
then show ?thesis by auto
|
then show ?thesis by auto
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
(* usually: x,y = (len_of TYPE ('a)) *)
|
||||||
|
lemma bitmagic_zeroLast_leq_or1Last:
|
||||||
|
"(a::('a::len) word) AND (mask len << x - len) \<le> a OR mask (y - len)"
|
||||||
|
by (meson le_word_or2 order_trans word_and_le2)
|
||||||
|
|
||||||
|
|
||||||
|
lemma zero_base_lsb_imp_set_eq_as_bit_operation:
|
||||||
|
fixes base ::"'a::len word"
|
||||||
|
assumes valid_prefix: "mask (len_of TYPE('a) - len) AND base = 0"
|
||||||
|
shows "(base = NOT mask (len_of TYPE('a) - len) AND a) \<longleftrightarrow>
|
||||||
|
(a \<in> {base .. base OR mask (len_of TYPE('a) - len)})"
|
||||||
|
proof
|
||||||
|
have helper3: "x OR y = x OR y AND NOT x" for x y ::"'a::len word" by (simp add: word_oa_dist2)
|
||||||
|
from assms show "base = NOT mask (len_of TYPE('a) - len) AND a \<Longrightarrow>
|
||||||
|
a \<in> {base..base OR mask (len_of TYPE('a) - len)}"
|
||||||
|
apply(simp add: word_and_le1)
|
||||||
|
apply(metis helper3 le_word_or2 word_bw_comms(1) word_bw_comms(2))
|
||||||
|
done
|
||||||
|
next
|
||||||
|
assume "a \<in> {base..base OR mask (len_of TYPE('a) - len)}"
|
||||||
|
hence a: "base \<le> a \<and> a \<le> base OR mask (len_of TYPE('a) - len)" by simp
|
||||||
|
show "base = NOT mask (len_of TYPE('a) - len) AND a"
|
||||||
|
proof -
|
||||||
|
have f2: "\<forall>x\<^sub>0. base AND NOT mask x\<^sub>0 \<le> a AND NOT mask x\<^sub>0"
|
||||||
|
using a neg_mask_mono_le by blast
|
||||||
|
have f3: "\<forall>x\<^sub>0. a AND NOT mask x\<^sub>0 \<le> (base OR mask (len_of TYPE('a) - len)) AND NOT mask x\<^sub>0"
|
||||||
|
using a neg_mask_mono_le by blast
|
||||||
|
have f4: "base = base AND NOT mask (len_of TYPE('a) - len)"
|
||||||
|
using valid_prefix by (metis mask_eq_0_eq_x word_bw_comms(1))
|
||||||
|
hence f5: "\<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT mask (len_of TYPE('a) - len) =
|
||||||
|
base OR x\<^sub>6 AND NOT mask (len_of TYPE('a) - len)"
|
||||||
|
using word_ao_dist by (metis)
|
||||||
|
have f6: "\<forall>x\<^sub>2 x\<^sub>3. a AND NOT mask x\<^sub>2 \<le> x\<^sub>3 \<or>
|
||||||
|
\<not> (base OR mask (len_of TYPE('a) - len)) AND NOT mask x\<^sub>2 \<le> x\<^sub>3"
|
||||||
|
using f3 dual_order.trans by auto
|
||||||
|
have "base = (base OR mask (len_of TYPE('a) - len)) AND NOT mask (len_of TYPE('a) - len)"
|
||||||
|
using f5 by auto
|
||||||
|
hence "base = a AND NOT mask (len_of TYPE('a) - len)"
|
||||||
|
using f2 f4 f6 by (metis eq_iff)
|
||||||
|
thus "base = NOT mask (len_of TYPE('a) - len) AND a"
|
||||||
|
by (metis word_bw_comms(1))
|
||||||
|
qed
|
||||||
|
qed
|
||||||
|
|
||||||
|
lemma unat_minus_one_word:
|
||||||
|
"unat (-1 :: 'a :: len word) = 2 ^ len_of TYPE('a) - 1"
|
||||||
|
by (subst minus_one_word)
|
||||||
|
(subst unat_sub_if', clarsimp)
|
||||||
|
|
||||||
|
lemma of_nat_eq_signed_scast:
|
||||||
|
"(of_nat x = (y :: ('a::len) signed word))
|
||||||
|
= (of_nat x = (scast y :: 'a word))"
|
||||||
|
by (metis scast_of_nat scast_scast_id(2))
|
||||||
|
|
||||||
lemma word_ctz_le:
|
lemma word_ctz_le:
|
||||||
"word_ctz (w :: ('a::len word)) \<le> LENGTH('a)"
|
"word_ctz (w :: ('a::len word)) \<le> LENGTH('a)"
|
||||||
apply (clarsimp simp: word_ctz_def)
|
apply (clarsimp simp: word_ctz_def)
|
||||||
|
|
|
@ -0,0 +1,84 @@
|
||||||
|
section\<open>Increment and Decrement Machine Words Without Wrap-Around\<close>
|
||||||
|
|
||||||
|
theory Word_Next
|
||||||
|
imports
|
||||||
|
Aligned
|
||||||
|
begin
|
||||||
|
|
||||||
|
text\<open>Previous and next words addresses, without wrap around.\<close>
|
||||||
|
|
||||||
|
definition word_next :: "'a::len word \<Rightarrow> 'a::len word" where
|
||||||
|
"word_next a \<equiv> if a = max_word then max_word else a + 1"
|
||||||
|
|
||||||
|
definition word_prev :: "'a::len word \<Rightarrow> 'a::len word" where
|
||||||
|
"word_prev a \<equiv> if a = 0 then 0 else a - 1"
|
||||||
|
|
||||||
|
text\<open>Examples:\<close>
|
||||||
|
|
||||||
|
lemma "word_next (2:: 8 word) = 3" by eval
|
||||||
|
lemma "word_next (255:: 8 word) = 255" by eval
|
||||||
|
lemma "word_prev (2:: 8 word) = 1" by eval
|
||||||
|
lemma "word_prev (0:: 8 word) = 0" by eval
|
||||||
|
|
||||||
|
|
||||||
|
lemma plus_one_helper[elim!]:
|
||||||
|
"x < n + (1 :: 'a :: len word) \<Longrightarrow> x \<le> n"
|
||||||
|
apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
|
||||||
|
apply (case_tac "1 + n = 0")
|
||||||
|
apply simp
|
||||||
|
apply (subst(asm) unatSuc, assumption)
|
||||||
|
apply arith
|
||||||
|
done
|
||||||
|
|
||||||
|
lemma plus_one_helper2:
|
||||||
|
"\<lbrakk> x \<le> n; n + 1 \<noteq> 0 \<rbrakk> \<Longrightarrow> x < n + (1 :: 'a :: len word)"
|
||||||
|
by (simp add: word_less_nat_alt word_le_nat_alt field_simps
|
||||||
|
unatSuc)
|
||||||
|
|
||||||
|
lemma less_x_plus_1:
|
||||||
|
fixes x :: "'a :: len word" shows
|
||||||
|
"x \<noteq> max_word \<Longrightarrow> (y < (x + 1)) = (y < x \<or> y = x)"
|
||||||
|
apply (rule iffI)
|
||||||
|
apply (rule disjCI)
|
||||||
|
apply (drule plus_one_helper)
|
||||||
|
apply simp
|
||||||
|
apply (subgoal_tac "x < x + 1")
|
||||||
|
apply (erule disjE, simp_all)
|
||||||
|
apply (rule plus_one_helper2 [OF order_refl])
|
||||||
|
apply (rule notI, drule max_word_wrap)
|
||||||
|
apply simp
|
||||||
|
done
|
||||||
|
|
||||||
|
|
||||||
|
lemma word_Suc_leq: fixes k::"'a::len word" shows "k \<noteq> max_word \<Longrightarrow> x < k + 1 \<longleftrightarrow> x \<le> k"
|
||||||
|
using less_x_plus_1 word_le_less_eq by auto
|
||||||
|
|
||||||
|
lemma word_Suc_le: fixes k::"'a::len word" shows "x \<noteq> max_word \<Longrightarrow> x + 1 \<le> k \<longleftrightarrow> x < k"
|
||||||
|
by (meson not_less word_Suc_leq)
|
||||||
|
|
||||||
|
lemma word_lessThan_Suc_atMost: fixes k::"'a::len word" shows "k \<noteq> max_word \<Longrightarrow> {..< k + 1} = {..k}"
|
||||||
|
by(simp add: lessThan_def atMost_def word_Suc_leq)
|
||||||
|
|
||||||
|
lemma word_atLeastLessThan_Suc_atLeastAtMost:
|
||||||
|
fixes l::"'a::len word" shows "u \<noteq> max_word \<Longrightarrow> {l..< u + 1} = {l..u}"
|
||||||
|
by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)
|
||||||
|
|
||||||
|
lemma word_atLeastAtMost_Suc_greaterThanAtMost: fixes l::"'a::len word"
|
||||||
|
shows "m \<noteq> max_word \<Longrightarrow> {m<..u} = {m + 1..u}"
|
||||||
|
by(simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)
|
||||||
|
|
||||||
|
lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
|
||||||
|
fixes l::"'a::len word"
|
||||||
|
assumes "m \<noteq> max_word" and "l \<le> m" and "m \<le> u"
|
||||||
|
shows "{l..m} \<union> {m+1..u} = {l..u}"
|
||||||
|
proof -
|
||||||
|
from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} \<union> {m<..u}" by blast
|
||||||
|
with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
|
||||||
|
qed
|
||||||
|
|
||||||
|
lemma word_adjacent_union:
|
||||||
|
"word_next e = s' \<Longrightarrow> s \<le> e \<Longrightarrow> s' \<le> e' \<Longrightarrow> {s..e} \<union> {s'..e'} = {s .. e'}"
|
||||||
|
by (metis Un_absorb2 atLeastatMost_subset_iff ivl_disj_un_two(7) max_word_max
|
||||||
|
word_atLeastLessThan_Suc_atLeastAtMost word_le_less_eq word_next_def linorder_not_le)
|
||||||
|
|
||||||
|
end
|
|
@ -11,8 +11,7 @@
|
||||||
section "Displaying Phantom Types for Word Operations"
|
section "Displaying Phantom Types for Word Operations"
|
||||||
|
|
||||||
theory Word_Type_Syntax
|
theory Word_Type_Syntax
|
||||||
imports
|
imports "HOL-Word.Word"
|
||||||
"HOL-Word.Word"
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
|
|
Loading…
Reference in New Issue