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"
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
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)
then show ?case by simp
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)" ...
Cheers, and thanks for any help,
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and