# Re: [isabelle] Feature suggestions: More useful output

```On Fri, 23 Nov 2012, Joachim Breitner wrote:

```
```Last on my list for today is a more interactive variant of print_cases.
When I currently write
lemma "n + 1 = 1 + (n::nat)"
proof(induct n)
I have
proof (state): step 1

goal (2 subgoals):
1. 0 + 1 = 1 + 0
2. ⋀n. n + 1 = 1 + n ⟹ Suc n + 1 = 1 + Suc n
and with
print_cases
it prints
cases:
0:
let "?case" = "0 + 1 = 1 + 0"
Suc:
fix n_
let "?case" = "Suc n_ + 1 = 1 + Suc n_"
assume Suc.hyps: "n_ + 1 = 1 + n_" and Suc.prems:

What I am missing is a combination of both that is ready to be used as
the structure of an Isar proof, e.g. either completely explicit:

show "0 + 1 = 1 + 0"
sorry
next
fix n
assume "n + 1 = 1 + (n::nat)"
show "Suc n + 1 = 1 + Suc n"
sorry
qed

or, depending on personal preference and number and complexity of the
hypotheses, using the provided case names (and using "case goal1..." if
there are no case names):

case 0
show ?case
sorry
next
case (Suc n)
show ?case
sorry
qed

From there I guess it would be a small step to allow the user to insert
the output of this command (say print_isar_structure) into the proof
document with one click, similar to how sledgehammer works.
```
```
```
'print_cases' is indeed a dinosaur from the TTY age. Producing proof outlines for induction proofs is the standard application for smart templating, I have it on my list for a long time already. This summer I got quite close to see how it can be implemented relatively easily, at least the abstract case / show ?case form, because printing of terms in a parsable way is still needs further investigation. It is unlikely to happen for the coming release, though.
```
```
Also note that goal1, ..., goal42 are not Isar-conformant at all: they produce fragile proofs with lots of funny indices. It is often better make an unstructured script in the traditional manner here.
```

Makarius```

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