Having the following theory:
datatype bitvector = BTM | BITV bool bitvector
lemma "∀ x1 x2 y1 y2. (BITV x1 x2 = BITV y1 y2) = (x1=y1) ∧ (x2=y2)"
I get the following proof state:
proof (prove): step 0
goal (1 subgoal):
1. ∀x1 x2 y1 y2. (BITV x1 x2 = BITV y1 y2) = (x1 = y1) ∧ x2 = y2
Auto Quickcheck found a counterexample:
x1 = False
x2 = BITV True BTM
y1 = False
y2 = BTM
What kind of equality is this here? It is obvious that it is not the structural equality that is of Standard ML. Or, is there a bug in this formalisation?
Best How To :
Be careful with equality of boolean-type expressions. Due to operator precedence, the proposition of your lemma is actually the following:
lemma "∀ x1 x2 y1 y2. ((BITV x1 x2 = BITV y1 y2) = (x1=y1)) ∧ (x2=y2)"
This is obviously false. What you should write is:
lemma "∀ x1 x2 y1 y2. (BITV x1 x2 = BITV y1 y2) = ((x1=y1) ∧ (x2=y2))"
In fact, due to these operator precedence issues, I prefer using
⟷ for equality of boolean expressions:
lemma "∀ x1 x2 y1 y2. BITV x1 x2 = BITV y1 y2 ⟷ x1 = y1 ∧ x2 = y2"
Moreover, one would normally write a lemma such as this without the HOL universal quantifiers and instead use the following, which is equivalent:
lemma "BITV x1 x2 = BITV y1 y2 ⟷ x1 = y1 ∧ x2 = y2"
All of these lemmas are easily proven by the simplifier, as they are direct consequences of the injectivity lemmas that are automatically provided by the
I should also mention that instead of defining bit vectors yourself, you may want to use the predefined formalisation of bit vectors in
src/HOL/Word. Some examples exist in