[isabelle] Another newbie question...case-based proofs



I'd like to write an Isar proof about lines in the cartesian plane in a
deliberately basic way.

I've got distinct points (x0,y0) and (x1, y1), and want to show that
there's a line between them. "lines" are represented either by a pair (m,
b), describing the line y = mx + b, or by a number c, representing the line
x = c.

The natural proof for me as a mathematician splits into two cases: 1. where
x0 = x1 (in which case we know that y0 is not equal to y1, and can build
the vertical line at x = x0) , or
2. Where x0 is not equal to x1, in which case I can compute the slope and
intercept and construct an ordinary line to show existence.

I've made choices about datatypes that you may find non-idiomatic, but I
made them on purpose, and I suspect that every if they're not idiomatic,
they should be usable --- they don't seem to me to express anything that's
an incorrect model of my geometric question. My *real* question is about
how to write case-based proofs of the kind described above.

So here's what I tried:

  datatype a2pt = A2Point "real" "real"

  datatype a2ln = A2Ordinary "real" "real"
                | A2Vertical "real"


  lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"


When I typed

  proof cases

I was offered a template for case-proofs, namely
proof cases
    case True
    then show ?thesis sorry
  next
    case False
    then show ?thesis sorry
  qed

but the line 'case True' (which I frankly don't understand) was highlighted
with the response 'Illegal schematic variable(s) in case "True" '

I tried editing a little, to
proof
    fix x0 y0 assume "P = (A2Point x0 y0)"
    fix x1 y1 assume "Q = (A2Point x1 y1)"
    proof cases

...but that got me a "Illegal application of proof command in "state" mode"
error, which I cannot find in any of the explanatory material I've seen
about Isabelle (indeed, the term "state mode" eludes me as well).

Putting the two "fix" lines within the cases proof helped a little:

proof cases
    fix x0 y0 assume "P = (A2Point x0 y0)"
    fix x1 y1 assume "Q = (A2Point x1 y1)"
    case True
    then show ?thesis sorry...

but the "case True" still produced an error. I thought maybe I could state
a case that actually meant what I intended, so I tried

lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof cases
    fix x0 y0 assume "P = (A2Point x0 y0)"
    fix x1 y1 assume "Q = (A2Point x1 y1)"
    case "(x0 = x1)"
    ...

but that base statement generated an error "Undefined case: "(x0 = x1)"⌂".

I'd appreciate any hints you can give.



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