tl;dr: I'd like to know what the best/correct way is to fix a variable in Isar with some restrictions.
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
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: Sep 25 2022 at 22:23 UTC