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



Gene Stark points out that without the whole Theory file, it's not clear
what I'm up to. I've attached it here, in hopes that this gets it to the
rest of the distribution list.
-John


On Sat, Mar 9, 2019 at 12:44 PM John F. Hughes <jfh at cs.brown.edu> wrote:

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

Attachment: Question4.thy
Description: Binary data



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