Re: [isabelle] Proof by contradiction



> 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.