isabelle2021-1 word_lib: tweak word_eqI method
More controlled simpset setup, so we don't get warnings if we have bit_simps in the simpset already. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
a0bf14024e
commit
c9f8e023f4
|
@ -59,12 +59,15 @@ method word_eqI uses simp simp_del split split_del cong flip =
|
||||||
(* turn x < 2^n assumptions into mask equations: *)
|
(* turn x < 2^n assumptions into mask equations: *)
|
||||||
((drule less_mask_eq)+)?,
|
((drule less_mask_eq)+)?,
|
||||||
(* expand and distribute test_bit everywhere: *)
|
(* expand and distribute test_bit everywhere: *)
|
||||||
(clarsimp simp: bit_simps word_eqI_simps simp not_less not_le simp del: simp_del simp flip: flip
|
(simp only: bit_simps word_eqI_simps)?,
|
||||||
|
(* clarsimp normal form again, also resolve negated < and \<le> *)
|
||||||
|
(clarsimp simp: simp not_less not_le simp del: simp_del simp flip: flip
|
||||||
split: split split del: split_del cong: cong)?,
|
split: split split del: split_del cong: cong)?,
|
||||||
(* add any additional word size constraints to new indices: *)
|
(* add any additional word size constraints to new indices: *)
|
||||||
((drule test_bit_lenD)+)?,
|
((drule test_bit_lenD)+)?,
|
||||||
(* try to make progress (can't use +, would loop): *)
|
(* try to make progress (can't use +, would loop): *)
|
||||||
(clarsimp simp: bit_simps word_eqI_simps simp simp del: simp_del simp flip: flip
|
(simp only: bit_simps word_eqI_simps)?,
|
||||||
|
(clarsimp simp: simp simp del: simp_del simp flip: flip
|
||||||
split: split split del: split_del cong: cong)?,
|
split: split split del: split_del cong: cong)?,
|
||||||
(* helps sometimes, rarely: *)
|
(* helps sometimes, rarely: *)
|
||||||
(simp add: simp test_bit_conj_lt del: simp_del flip: flip split: split split del: split_del cong: cong)?)
|
(simp add: simp test_bit_conj_lt del: simp_del flip: flip split: split split del: split_del cong: cong)?)
|
||||||
|
@ -72,7 +75,7 @@ method word_eqI uses simp simp_del split split_del cong flip =
|
||||||
method word_eqI_solve uses simp simp_del split split_del cong flip dest =
|
method word_eqI_solve uses simp simp_del split split_del cong flip dest =
|
||||||
solves \<open>word_eqI simp: simp simp_del: simp_del split: split split_del: split_del
|
solves \<open>word_eqI simp: simp simp_del: simp_del split: split split_del: split_del
|
||||||
cong: cong simp flip: flip;
|
cong: cong simp flip: flip;
|
||||||
(fastforce dest: dest simp: bit_simps word_eqI_simps simp flip: flip
|
(fastforce dest: dest simp: simp flip: flip
|
||||||
simp: simp simp del: simp_del split: split split del: split_del cong: cong)?\<close>
|
simp: simp simp del: simp_del split: split split del: split_del cong: cong)?\<close>
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -1020,11 +1020,11 @@ lemma word_and_less':
|
||||||
|
|
||||||
lemma shiftr_w2p:
|
lemma shiftr_w2p:
|
||||||
"x < LENGTH('a) \<Longrightarrow> 2 ^ x = (2 ^ (LENGTH('a) - 1) >> (LENGTH('a) - 1 - x) :: 'a :: len word)"
|
"x < LENGTH('a) \<Longrightarrow> 2 ^ x = (2 ^ (LENGTH('a) - 1) >> (LENGTH('a) - 1 - x) :: 'a :: len word)"
|
||||||
by (rule bit_word_eqI) (auto simp add: bit_simps)
|
by word_eqI_solve
|
||||||
|
|
||||||
lemma t2p_shiftr:
|
lemma t2p_shiftr:
|
||||||
"\<lbrakk> b \<le> a; a < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ a >> b = 2 ^ (a - b)"
|
"\<lbrakk> b \<le> a; a < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ a >> b = 2 ^ (a - b)"
|
||||||
by (rule bit_word_eqI) (auto simp add: bit_simps)
|
by word_eqI_solve
|
||||||
|
|
||||||
lemma scast_1[simp]:
|
lemma scast_1[simp]:
|
||||||
"scast (1 :: 'a :: len signed word) = (1 :: 'a word)"
|
"scast (1 :: 'a :: len signed word) = (1 :: 'a word)"
|
||||||
|
@ -1360,7 +1360,7 @@ lemma unat_2tp_if:
|
||||||
|
|
||||||
lemma mask_of_mask:
|
lemma mask_of_mask:
|
||||||
"mask (n::nat) AND mask (m::nat) = (mask (min m n) :: 'a::len word)"
|
"mask (n::nat) AND mask (m::nat) = (mask (min m n) :: 'a::len word)"
|
||||||
by (rule bit_word_eqI) (auto simp add: bit_simps)
|
by word_eqI_solve
|
||||||
|
|
||||||
lemma unat_signed_ucast_less_ucast:
|
lemma unat_signed_ucast_less_ucast:
|
||||||
"LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat (ucast (x :: 'a :: len word) :: 'b :: len signed word) = unat x"
|
"LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat (ucast (x :: 'a :: len word) :: 'b :: len signed word) = unat x"
|
||||||
|
|
Loading…
Reference in New Issue