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



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"

This and similar changes helped to shorten the overall formalisation from 1145 to 1045 lines (see http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy). 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. Is there a single, up to date reference manual that documents all proof methods?

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?

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

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





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