Stream: General

Topic: Proofs with orderings on Words


view this post on Zulip Lex Bailey (Jan 27 2023 at 14:47):

Hi,
as part of a larger proof for something I'm working on, I need to prove something like the following...

lemma div_pow2_le_mono:
  shows "(reg::nat) ≤ n ⟶ (reg div (2^d)) ≤ (n div (2^d))"
  by (simp add: div_le_mono)

This works as expected for the nat type, but I specifically want to use 8 word instead of nat (this is modelling a right bit shift on a byte register)
so I am trying to prove something like the following, which uses drop_bit on word types:

lemma
  shows "(reg :: 8 word) ≤ a ⟶ (drop_bit k reg) ≤ a div 2^k"
  apply transfer
  apply (simp add: div_le_mono div_pow2_le_mono)
  ...

I had hoped that with transfer I would be able to prove this for words in much the same way as with nats, but it appears not to work.
Am I missing something? Is there an easy way to do this? If not then how best to prove this lemma?
Thanks :)

view this post on Zulip Christian Pardillo Laursen (Jan 27 2023 at 18:01):

lemma "(reg :: 8 word) ≤ a ⟶ (drop_bit k reg) ≤ a div 2^k"
  by (simp add: drop_bit_eq_div word_le_nat_alt unat_div_distrib div_le_mono)

Unfolding the definition of leq for words lets you prove the same fact on naturals

view this post on Zulip Lex Bailey (Jan 29 2023 at 02:52):

ah! awesome, thanks :)


Last updated: Dec 07 2024 at 16:22 UTC