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

我用(B T T T T T T T T)代表(11111111)，(B F F F F F F F F)代表(00000000)。

但是我无法证明这样一个明显的引理:b != b + 1

我真的需要一些帮助。

Answer 1

您需要区分参数 b 的大小写，以便可以对 byte_inc 应用 simp 规则。只需执行“by(cases b 规则:byte_inc.cases，simp_all)”