[isabelle] Proof by contradiction



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:

Suppose (u,v) is on both x = a and x = b, and a \ne b; then u = a and u =
b, so a = b. Contradiction.

With Isabelle in the back of my mind, perhaps I'd write this:

Proof: Because l is vertical, it's defined by an equation  x = a ;
similarly k is defined by x = b, and we're given that a \ne b.
Suppose T = (u,v) lies on both. Then u = a because T is on l, and u = b
because T is on k, and thus a = b. That's a contradiction with the given
fact a \ne b. Hence T cannot lie on both lines. QED.

I've attempted to mimic this proof in Isar below, and it's fairly readable,
I hope. "a2meets P m" is my way of saying "the point P is on the line m",
and it's written this way to make it consistent with other stuff I'm
writing about general affine geometries.

Although the resulting proof is wordy,  I feel as if I'm headed in the
right direction. But I cannot figure out the syntax for saying "OK, I've
proved False. Surely we can conclude the theorem by contradiction!":

theory Brief6
imports Complex_Main
begin  datatype a2pt = A2Point "real" "real"

  datatype a2ln = A2Ordinary "real" "real"
                | A2Vertical "real"
  text "Ordinary m b represents the line y = mx+b; Vertical xo is the line
x = xo "

  fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where
    "a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
    "a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"

(* Lemma: vertical lines with different x-coords are disjoint *)
lemma A2_vert: "x0 ≠ x1 ∧ l = A2Vertical x0 ∧ k = A2Vertical x1   ⟹  ¬ (∃
T. a2meets T l  ∧ a2meets T k)"
proof -
  assume diff_x: "x0 ≠ x1"
  assume l_form: "l = A2Vertical x0"
  assume k_form: "k = A2Vertical x1"
  have "¬ (∃ T. a2meets T l  ∧ a2meets T k)"
  proof (rule ccontr)
    assume "∃ T. a2meets T l  ∧ a2meets T k"
    fix u v
    assume T_form: "T = A2Point u v"
    have T_on_l: "a2meets T l"
      by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2)
a2meets.simps(2) diff_x k_form l_form)
    have T_on_k: "a2meets T k"
      by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2)
a2meets.simps(2) diff_x k_form l_form)
    have "u = x0"
      using T_form T_on_l l_form by auto
    have "u = x1"
      using T_form T_on_k k_form by auto
    have False
      using ‹u = x0› ‹u = x1› diff_x by blast
  qed
=======

I'd appreciate it if (a) someone could add whatever last line or two is
needed to finish this proof, and (b) someone could show how to make the
proof more idiomatic and perhaps briefer (which might entail rewriting the
lemma itself, and if that's necessary, it's fine with me).

--John



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