Having the following theory:

```
theory BitVector
imports Main
begin
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 `datatype`

command.

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 `src/HOL/Word/Examples`

.