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: Dec 21 2024 at 16:20 UTC