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=ryczAP8H5mHcJemail@example.com>
- References: <CAJ=ZMJK-Liu5JGNE0YqK+vwXEo9Bq7=ryczAP8H5mHcJfirstname.lastname@example.org>
> 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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and