3

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

私は本当に助けが必要です。

4

2 に答える 2

4

bbyte_inc に単純な規則を適用できるように、パラメーターの大文字と小文字を区別する必要があります。「by (cases b rule: byte_inc.cases, simp_all)」を実行するだけです

于 2013-09-15T17:22:15.763 に答える
3

また、ビットを超える機械語の既存のライブラリを確認する必要があります。$ISABELLE_HOME/src/HOL/Word/Word.thy

ただし、これは非常に高度な機能ですが、実際のアプリケーションでは、時間をかけてその仕組みを理解する価値があります。

于 2013-10-09T19:23:35.720 に答える