Hello,

tl;dr: I'd like to know what the best/correct way is to fix a variable in Isar with some restrictions.

Long:

For a bigger proof I need a fact of the form `∀x ∈ xs. predicate x`

and I can show this fact in the bigger context with `fix x`

and `assume "x ∈ xs"`

.

Obviously, if the fact is proven on the top-level, the goal of the surrounding context can not be proven due to the additional `assume`

. If the fact is proven in an own block instead, it becomes `?x2 ∈ xs ⟹ ∀x∈ xs. predicate x`

which is not what I expected it to be.

Thus, it seems necessary to fix the `x`

in a way which restricts it to an element of `xs`

, but which does not rely on an `assume`

. Is there such a way and how would it work?

Is opening a new scope is sufficient for your purpose?

```
proof -
...
have H: "∀x ∈ xs. predicate x"
proof
for x
assume "x∈ xs"
show "predicate x"
sorry
qed
.... [where you can use H]...
```

I think the real point here is to use the introduction rule `ballI`

, which is what `proof`

does.

Ahhhh... good point.

Thanks for your answers and insights. I'm not certain how I could directly apply ballI to fit my use case but the indirection of a nested proof was enough to solve the problem. :D

`proof`

is the same as `proof standard`

, which in that case means `proof (rule ballI)`

It's good to remember that HOL quantifiers are opaque to Isar. They are just functions like any other function.

Yes, certainly. The thing I struggled here most was how to structure my proof :D Especially, because this would influence my choice on how to formalise some underlying property. With this out of the way, I'm positive that all else follows easily. Therefore, thanks again.

(Update: all followed more or less easily. Now on to the really interesting stuff :sweat_smile: )

If this was the biggest problem in your formalisation project, you are a lucky person indeed. :wink:

Last updated: Feb 27 2024 at 08:17 UTC