# Re: [isabelle] Proof by contradiction

*To*: "John F. Hughes" <jfh at cs.brown.edu>
*Subject*: Re: [isabelle] Proof by contradiction
*From*: Lawrence Paulson <lp15 at cam.ac.uk>
*Date*: Thu, 28 Mar 2019 14:18:29 +0000
*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
*In-reply-to*: <CAJ=ZMJK-Liu5JGNE0YqK+vwXEo9Bq7=ryczAP8H5mHcJ-164vw@mail.gmail.com>
*References*: <CAJ=ZMJK-Liu5JGNE0YqK+vwXEo9Bq7=ryczAP8H5mHcJ-164vw@mail.gmail.com>

> On 28 Mar 2019, at 13:39, John F. Hughes <jfh at cs.brown.edu> wrote:
>
> I'm struggling with trying to encode a proof by contradiction in Isar.
>
> In the euclidean plane, I'm trying to prove that if two vertical lines l
> and k lie at different x-coordinates, then they have no points in common.
> In a math book, I'd write:
Maybe you are over complicating things with your definitions. Isn’t your statement simply the thing below?
lemma "a ≠ b ⟹ disjnt (range (λy. (a,y))) (range (λy. (b,y)))"
by (auto simp: disjnt_def)
Larry Paulson

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