Re: [isabelle] Proof by contradiction

Am Donnerstag, den 28.03.2019, 12:14 -0400 schrieb John F. Hughes:
> Can you suggest somewhere that I can learn the distinction between
> "obtain" and "fix"? The reference manual has a paragraph that's too
> cryptic for my current understanding of logic (which is quite
> basic); Ballarin's tutorial slides basically say "they're different".
> I think I need something in the middle. :)

Have you studied the tutorial “Programming and Proving in Isabelle/HOL”
(`prog-prove`)? I find it extremely helpful for getting started with
Isabelle. It also mentions `obtain`.

You use `fix` if you want to prove a `⋀`-statement; `fix x` means that
the following lines work under the assumption that an `x` is given to
you. You use `obtain x where P` if you can prove that there is an `x`
for which `P` is true and you want to get hold of such an `x`.

All the best,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.