isabelle - 在 Isabelle 中证明一个基本引理

Question

我正在使用 Isabelle 进行一个项目。

出于某种原因，我必须模拟一个位/字节系统，如下所示：

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

我用（BTTTTTTTT）代表（11111111），（BFFFFFFFF）代表（00000000）。

但我无法证明如此明显的引理： b != b + 1

我真的需要一些帮助。

Answer 1

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

Answer 2

您还应该查看现有的机器字库：$ISABELLE_HOME/src/HOL/Word/Word.thy

不过，这是相当先进的东西，但对于真正的应用程序，值得花时间弄清楚它是如何工作的。