# 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.*