Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]

Am 22/11/2012 15:13, schrieb Christoph LANGE:
> Dear Larry, dear all,
> I'm now back at our auction formalisation and catching up with emails.
> I have taken into account the advice I got from you and the others; basically I
> managed to change my statements from
> shows "!i . p x --> q x"
> to
> fixes ... and i
> assumes "p x"
> shows "q x"

Unless you want to give the type of i, you don't need to fix it.

> This and similar changes helped to shorten the overall formalisation from 1145
> to 1045 lines (see
>  I'm sure I can do even better.
> I have not yet made any further simplifications, such as doing a lot of things
> at once in a style like
> ... by (induct i arbitrary: xs) (case_tac xs, simp_all)+
> that Chris used in his example of a lemma about lists.  At the moment I don't
> even know how to get started using such proof methods.
> 2012-11-01 12:03 Lawrence Paulson:
>> You should look at the documentation on the induct/induction proof methods.
> Where can I find that documentation?  The Tutorial mainly uses
> apply(induct_tac), which is probably something else.

This is what I suggested to you 3 weeks back:

"If you look at the documentation page you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply"."

That is also where you find the induction method.

> Is there a single, up to
> date reference manual that documents all proof methods?

Yes, the reference manual (more or less).

> BTW, changing induction proofs to "assumes ... shows ..." did not always make
> them shorter.  Is there a way of not having to explicitly restate the assumption
> for (Suc n) in the induction step?

Indeed, for inductions, the most convenient way is stating them as implications
(with ==>). The manuals above will also tell you about the naming conventions of
assumptions in each case.


> E.g. I have one lemma of the following structure, which proves some property of
> a function "fun maximum":
> lemma maximum_sufficient :
>   fixes n::nat and ...
>   assumes assm1: "p n"
>       and assm2: "q n"
>       and assm3: "r n"
>   shows "s n"
>     using assms (* <-- now this became necessary,
>       otherwise even "case 0" would fail, but why? *)
> proof (induct n)
>   case 0
>   then show ?case by simp
> next
>   case (Suc n)
>   (* and now I have to explicitly restate all assumptions: *)
>   assume assm1: "p (Suc n)"
>   assume assm2: "q (Suc n)"
>   assume assm3: "r (Suc n)"
>   ...
>   show "s (Suc n)" ...
> qed
> Cheers, and thanks for any help,
> Christoph

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