Re: [isabelle] Two questions of a beginner



On Fri, 18 Jan 2013, Lawrence Paulson wrote:

The answer to your second question is to use a structured proof. Non-atomic premises are all but useless in the apply style. In a structured proof, you can use such a thing exactly like an inference rule.

This is what Larry means, when spelled out in Isar:

notepad
begin

  assume r:  "A ==> C"
  have C
  proof (rule r)
    show A sorry
  qed

end

The notepad gives you a structured proof body without an outermost goal statement getting in the way, so it is usefule for experimentation and understanding things. If you intent to produce a result eventually, you can write it like this:

lemma
  assumes r:  "A ==> C"
  shows C
proof (rule r)
  show A sorry
qed

If you follow Isar proof structuring the usual way, you should rarely run into a situation where you get a goal state with the intended rule being pushed in a goal state too early, and thus prevent its easy manipulation.

(There are ways to do it nonetheless, notably the SUBPROOF and Subgoal.FOCUS combinators in Isabelle/ML. That is a completely different story, and not really on-topic for this thread.)


	Makarius






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