Theory Examples

theory Examples imports Bits begin

lemma "(123::Z[5]) = (8::Z[5])"
by simp

lemma "1 + 2 * 3 = (0::Z[7])"
by simp

lemma "0b10101 AND 0b11011 = (0b10001 :: int)"
by simp

lemma "0b10100 OR 0b01001 = (0b01101 :: 4 bits)"
by simp

lemma "0b10100 OR 0b01001 ≠ (0b01101 :: 5 bits)"
by simp

lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 bits)"
proof -
  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
    by (simp only: AND_OR_distrib)
  also have "0xff00 OR 0x00ff = (-1::16 bits)"
    by simp
  also have "x AND -1 = x"
    by simp
  finally show ?thesis .
qed

end