Prove a basic lemma in Isabelle

Question

I'm working on a project using Isabelle.

For some reason I have to simulate a bit/byte system, like this:

type_synonym bit = bool
datatype byte = B bit bit bit bit bit bit bit bit

fun byte_inc :: "byte => byte" where
"byte_inc (B a7 a6 a5 a4 a3 a2 a1 False) = (B a7 a6 a5 a4 a3 a2 a1 True)" |
"byte_inc (B a7 a6 a5 a4 a3 a2 False True) = (B a7 a6 a5 a4 a3 a2 True False)" |
"byte_inc (B a7 a6 a5 a4 a3 False True True) = (B a7 a6 a5 a4 a3 True False False)" |
"byte_inc (B a7 a6 a5 a4 False True True True) = (B a7 a6 a5 a4 True False False False)" |
"byte_inc (B a7 a6 a5 False True True True True) = (B a7 a6 a5 True False False False False)" |
"byte_inc (B a7 a6 False True True True True True) = (B a7 a6 True False False False False False)" |
"byte_inc (B a7 False True True True True True True) = (B a7 True False False False False False False)" |
"byte_inc (B False True True True True True True True) = (B True False False False False False False False)" |
"byte_inc (B True True True True True True True True) = (B False False False False False False False False)"

lemma [simp]: "b ≠ byte_inc b"
sorry

I use (B T T T T T T T T) to represent (11111111), (B F F F F F F F F) to represent (00000000).

But I can not prove such an obvious lemma: b != b + 1

I really need some help.

Answer 1

You should also take a look at the existing library for machine words over bits: $ISABELLE_HOME/src/HOL/Word/Word.thy

That is quite advanced stuff, though, but for real applications it is worth investing time to figure out how it works.

Answer 2

You will need to make a case distinction over the parameter b so that you can apply the simp rules for byte_inc. Just do "by (cases b rule: byte_inc.cases, simp_all)"