## Stream: Beginner Questions

### Topic: Isar: Fix with restriction

#### Florian Sextl (Jan 06 2021 at 10:31):

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?

#### Mathias Fleury (Jan 06 2021 at 10:37):

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]...
``````

#### Manuel Eberl (Jan 06 2021 at 10:38):

I think the real point here is to use the introduction rule `ballI`, which is what `proof` does.

#### Mathias Fleury (Jan 06 2021 at 10:43):

Ahhhh... good point.

#### Florian Sextl (Jan 06 2021 at 10:50):

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

#### Mathias Fleury (Jan 06 2021 at 10:52):

`proof` is the same as `proof standard`, which in that case means `proof (rule ballI)`

#### Manuel Eberl (Jan 06 2021 at 10:56):

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

#### Florian Sextl (Jan 06 2021 at 10:59):

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: )

#### Manuel Eberl (Jan 06 2021 at 11:04):

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

Last updated: Sep 25 2022 at 22:23 UTC