Re: [isabelle] Can I assume an interpretation

On Mon, 7 Apr 2008, David Streader wrote:

> p.s. Isar is proofs have been very much more robust than any proofs I 
> previously constructed in Isabelle.

BTW, Isar proofs work out more smoothly when presenting statements in 
natural rule format.  This prevents having to walk through the outermost 
structure first, both in the proof and the application of the result later 
on.  E.g. compare these two versions:

lemma transitive1: "a <= b --> b <= c --> a <= c"
  assume ab: "a <= b"
  show "b <= c --> a <= c"
    assume bc: "b <= c"
    show "a <= c"
      using ab bc sorry

lemma transitive2:
  assumes ab: "a <= b"
    and bc: "b <= c"
  shows "a <= c"
proof -
  show ?thesis using ab bc sorry


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