*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>, "makarius at sketis.net" <makarius at sketis.net>*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: "Nagashima, Yutaka" <Yutaka.Nagashima at uibk.ac.at>*Date*: Mon, 11 Mar 2019 17:33:07 +0000*Accept-language*: en-AU, de-AT, en-US*In-reply-to*: <2315a38013d645bfa7ed4a7a37948817@chalmers.se>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com>, <2315a38013d645bfa7ed4a7a37948817@chalmers.se>*Thread-index*: AQHU1qBjc68TD4bwgEedYLCwxq6qUqYDmQaAgAMTrQ8=*Thread-topic*: [isabelle] Another newbie question...case-based proofs

Hi Dr. Wenzel and other Isabelle developers, > One more note on your email, if you tick the "Proof state" box in the output panel, > you'll see that parser for structure proofs alternates > between "proof (state)" mode and "proof (prove)" mode. Would it be possible to have this "proof state" box ticked by default in the next official Isabelle distribution? It is a small thing that could help new Isabelle users, I think. Last week I gave an introductory lecture about Isabelle to Mathematics students. With the "proof state" box unticked, all the four students were confused about their proof attempts, until I looked into their displays and told them to tick the box. ...And it was their second Isabelle session. I saw a similar confusion when my (CS) colleagues installed Isabelle for the first time. Regards, Yutaka ________________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Thomas Sewell [sewell at chalmers.se] Sent: Saturday, 9 March 2019 8:08 PM To: John F. Hughes; Cl-isabelle Users Subject: Re: [isabelle] Another newbie question...case-based proofs Hi John. It's raining where I am, so I had a go at your proof. BTW, when posting examples like this, it can be useful to include all relevant definitions. I had to guess at your definition of "a2meets", so it's possible my proof script below won't work for you. It looks like you've hit a few cases involving unexpected defaults. Firstly, to explain your problem, when you type "proof cases" the system has gone into a strange state involving a thing called a schematic variable. It's not actually irrecoverable, but you generally don't want this. Usually cases takes an argument, which is a term whose type has a case-division principle. In the absence of an argument, it's picked an unknown (schematic) value of type bool, with cases True and False. In one of your later attempts, BTW, you've hit another slightly unusual default. If you just type "proof" without saying what kind of proof, the system tries to perform one step by a default rule. Here it picked the rule ex1I, which you can have a look at ( type thm ex1I somewhere ). Until you understand the system better, I'd recommend you type "proof -", which is proof without any steps. One more note on your email, if you tick the "Proof state" box in the output panel, you'll see that parser for structure proofs alternates between "proof (state)" mode and "proof (prove)" mode. I would describe the first as forward-style, where you're expected to state some new fact to prove, and the second as backward-style, where you're expected to work on a goal that has been somehow stated. Anyway. Since we want to use ex1I eventually, I had a go at building a structured proof in which I construct the required premises. The thesis in each case is then proven "by auto", which knew to use the default rules. I haven't proven all the bits, and if your a2meets definition is different to mine then my proof steps might not apply. I hope that clarifies a bit. Cheers, Thomas. fun pt_x :: "a2pt ⇒ real" where "pt_x (A2Point x y) = x" fun pt_y :: "a2pt ⇒ real" where "pt_y (A2Point x y) = y" definition "a2meets P l = (case l of A2Ordinary m b ⇒ pt_y P = (m * pt_x P) + b | A2Vertical c ⇒ pt_x P = c)" lemma A2_a1: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l" proof (cases "pt_x P = pt_x Q") case True assume PQ: "P ≠ Q" define l where "l = A2Vertical (pt_x P)" have meets: "a2meets P l ∧ a2meets Q l" by (simp add: l_def a2meets_def True) from PQ True have iff: "a2meets P l' ∧ a2meets Q l' ⟶ l' = l" for l' apply (clarsimp simp: a2meets_def l_def split: a2ln.split) apply (cases P; cases Q; clarsimp) done from meets iff show ?thesis by auto next case False define m where "m = (pt_y Q - pt_y P) / (pt_x Q - pt_x P)" have "∃b. a2meets P (A2Ordinary m b) ∧ a2meets Q (A2Ordinary m b)" apply (simp add: a2meets_def m_def) apply (simp add: algebra_simps) sorry then obtain b where b: "a2meets P (A2Ordinary m b) ∧ a2meets Q (A2Ordinary m b)" .. define l where "l = A2Ordinary m b" note meets = b[folded l_def] have iff: "a2meets P l' ∧ a2meets Q l' ⟶ l' = l" for l' sorry from meets iff show ?thesis by auto qed ________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of John F. Hughes <jfh at cs.brown.edu> Sent: Saturday, March 9, 2019 6:44:04 PM To: Cl-isabelle Users Subject: [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.

**Follow-Ups**:**Re: [isabelle] Another newbie question...case-based proofs***From:*Peter Lammich

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

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

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

- Previous by Date: [isabelle] Researcher positions (postdoc) within the ERC Consolidator grant “Certified Quantum Security”
- Next by Date: Re: [isabelle] Another newbie question...case-based proofs
- Previous by Thread: Re: [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