Re: [isabelle] Another newbie proofs

Dear all,

just as another data point.

I am currently using the approach advertised (I think) by Makarius that
Peter mentioned before, in an Isabelle course.

Up to now there was only a single (3 hour) session, but maybe the first
one is most critical.

In this session I never even opened either the output or state panels
(neither did I use "apply", for that matter).

Instead I told students to start from a proof attempt along the lines of

  by (induction ...) auto

and then consult the resulting error message (click on the squiggly
underline) for what they might be missing.

By the end of the session all (18) students had solved all exercises and
I am not aware of any confusion caused by not using the output panel.



On 3/11/19 7:00 PM, Peter Lammich wrote:
> I second this request, but I remember that, a few years ago, there were
> strong arguments for using Isabelle without the output display at all,
> and use mouse hovering over the squiggly lines to review errors and
> warnings ... I never got used to this, in particular b/c of the waiting
> time until the tooltip pops up after hovering and the keyboard/mouse
> switching. It simply interferes with my workflow.
> --
>   Peter
> On Mo, 2019-03-11 at 17:33 +0000, Nagashima, Yutaka wrote:
>> 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 [cl-isabelle-users-bo
>> unces at] on behalf of Thomas Sewell [sewell at
>> ]
>> Sent: Saturday, 9 March 2019 8:08 PM
>> To: John F. Hughes; Cl-isabelle Users
>> Subject: Re: [isabelle] Another newbie 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 <cl-isabelle-users-bo
>> unces at> on behalf of John F. Hughes <jfh at>
>> Sent: Saturday, March 9, 2019 6:44:04 PM
>> To: Cl-isabelle Users
>> Subject: [isabelle] Another newbie 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.