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:

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.