*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: "John F. Hughes" <jfh at cs.brown.edu>*Date*: Sat, 9 Mar 2019 14:02:52 -0500*In-reply-to*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com>

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

**References**:**[isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

- Previous by Date: [isabelle] Another newbie question...case-based proofs
- Next by Date: Re: [isabelle] Another newbie question...case-based proofs
- Previous by Thread: [isabelle] Another newbie question...case-based proofs
- Next by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Cl-isabelle-users March 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list