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 :)

```
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

ah! awesome, thanks :)

Last updated: Dec 07 2023 at 08:19 UTC