I have the following lemma that I was expecting to be used to simplify a proof goal:

```
lemma index_update[simp]:
"n < CARD('b::finite) ⟹ index (update (f::'a['b]) n x) n = x"
by (simp add: update_def)
```

This lemma is a part of the C-to-Isabelle parser, and as you can see is marked as a simplification rule by default. I have the following proof goal that is not considering this rule, and I'm wondering why:

```
1. ⋀s. 0 ≤ i ⟹
i < 10 ⟹
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED ⟹
server_orders.[unat (word_of_int i)] =
Arrays.update (client_orders_'' s) (unat (word_of_int i))
(server_orders.[unat (word_of_int i)]).[unat (word_of_int i)]
```

This is a translation of some C code where `client_orders`

and `server_orders`

are both arrays of size 10. The index being used to read values out of these arrays is `i`

, and the assumptions here show that `i`

is between 0 and 10, i.e. `i < 10`

. Intuitively I would expect this rule to apply here, since this proof goal is just showing that the `client_orders`

array is being updated to contain the value at `i`

in `server_orders`

.

Of course, I see that the proof goal is not in the exact same shape as the lemma - there is an additional assumption here, namely:

```
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED ⟹
```

Is this what's preventing the simplification rule from being considered? Some background, this assumption is coming from an if statement in the C code that I've parsed. There are actual 2 proof goals here, the other one being the else case of the code. Can that be used to aid in the proof?

I also am thinking that because `i`

is an `int`

, it is not finite, so that may also be causing the lemma to not be used.

What happens if you do `apply (subst index_update)`

? If it doesn't work, try putting a `using [[show_sorts, unify_trace_failure]]`

before it and check the output.

Adding `apply (subst index_update)`

leads to this proof state:

```
1. ⋀s::lifted_globals.
(0::int) ≤ i ⟹
i < (10::int) ⟹
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED ⟹
unat (word_of_int i) < CARD(10)
2. ⋀s::lifted_globals.
(0::int) ≤ i ⟹
i < (10::int) ⟹
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED ⟹
server_orders.[unat (word_of_int i)] =
server_orders.[unat (word_of_int i)]
3. ⋀s::lifted_globals.
(0::int) ≤ i ⟹
i < (10::int) ⟹
client_orders_'' s.[unat (word_of_int i)] ≠ NOT_CACHED ⟹
server_orders.[unat (word_of_int i)] =
client_orders_'' s.[unat (word_of_int i)]
```

It looks like it introduces a new goal, #1, but makes #2 trivial (`apply(auto)`

afterwards discharges that goal).

I think adding `using [[show_sorts, unify_trace_failure]]`

is showing that there's a type mismatch somewhere, here's part of the output:

```
The following types do not unify:
32 word[10] ⇒ nat ⇒ 32 word
(nat ⇒ 32 word)[?'b::finite] ⇒ nat ⇒ nat ⇒ 32 word
```

There are other similar errors, but there's quite a bit of output - I won't post it all unless you think it's helpful.

I'm assuming there's a type issue with subgoal 1: `unat (word_of_int i) < CARD(10)`

. CARD is defined in the `Cardinality`

theory as:

```
translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)"
```

I've honestly never seen a definition like this so I don't know how to interpret it.

Hm, depending on where you got that goal from, one possibility might be that the polymorphism of `word_of_int`

is the problem here. `word_of_int`

probably has a type something like `int ⇒ 'a :: finite word`

, so if you just write `unat (word_of_int n)`

in two different places, Isabelle will infer the most general situation, which is that the two occurances of `word_of_int`

can have different bit-width.

Type annotations to fix the bit width here would help with that.

Last updated: Aug 15 2022 at 02:13 UTC