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"
proof
  assume ab: "a <= b"
  show "b <= c --> a <= c"
  proof
    assume bc: "b <= c"
    show "a <= c"
      using ab bc sorry
  qed
qed

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


	Makarius





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