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 (state): step 1
goal (2 subgoals):
1. 0 + 1 = 1 + 0
2. ⋀n. n + 1 = 1 + n ⟹ Suc n + 1 = 1 + Suc n
let "?case" = "0 + 1 = 1 + 0"
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"
assume "n + 1 = 1 + (n::nat)"
show "Suc n + 1 = 1 + Suc n"
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 (Suc n)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and