Докажите основную лемму в 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), (В F F F F F F F F) для представления (00000000).

Но я не могу доказать такую ​​очевидную лемму: Ь = Ь + 1

мне очень нужна помощь!.

Answer 1

Вы также должны взглянуть на существующую библиотеку для машинных слов над битами: $ISABELLE_HOME/src/HOL/Word/Word.thy

Это довольно продвинутый материал, хотя, но для реальных приложений стоит потратить время на то, чтобы выяснить, как это работает.

Answer 2

Вам нужно будет сделать различие в случае параметра b, чтобы вы могли применять правила simp для byte_inc. Просто делать «по (случаи правил б: byte_inc.cases, simp_all)»