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



2012-11-22 16:04 Lars Noschinski:
On 22.11.2012 15:13, Christoph LANGE wrote:
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 (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)"
...

You don't need to restate your assumptions here: They are all stored in
"Suc" (or Suc.prems, which omits the hypotheses added by induction).

Thanks, that's very helpful!

For readability I'd sometimes like to make it explicit to what assumption I'm referring when there is more than one.

When explicitly restating them with 'assume "... (Suc n) ..."' that's no problem. With "Suc" I found, e.g., Suc.prems(1) to work. A symbolic name, e.g. Suc.prems(foo), if the original statement says 'assumes foo: "..."', would be even nicer – but that's not possible, I suppose.

Cheers,

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.