*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proof by contradiction*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Thu, 28 Mar 2019 22:47:13 +0200*In-reply-to*: <CAJ=ZMJLuFFvFcW088OHaTzkPnAdLeK8C1k1c3nctF8mdy6h7FQ@mail.gmail.com>*References*: <CAJ=ZMJK-Liu5JGNE0YqK+vwXEo9Bq7=ryczAP8H5mHcJ-164vw@mail.gmail.com> <AFF3A3EA-DFC5-4649-A85E-A644D0F7CF49@gmail.com> <CAJ=ZMJLuFFvFcW088OHaTzkPnAdLeK8C1k1c3nctF8mdy6h7FQ@mail.gmail.com>

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, Wolfgang

**References**:**[isabelle] Proof by contradiction***From:*John F. Hughes

**Re: [isabelle] Proof by contradiction***From:*Mathias Fleury

**Re: [isabelle] Proof by contradiction***From:*John F. Hughes

- Previous by Date: [isabelle] Datatype definition in locale context
- Next by Date: [isabelle] Open Position: Lecturer in Cybersecurity - University of Exeter
- Previous by Thread: Re: [isabelle] Proof by contradiction
- Next by Thread: [isabelle] New in the AFP: The Transcendence of Certain Infinite Series
- Cl-isabelle-users March 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list