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



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).

  -- Lars





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