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
it prints
           let "?case" = "0 + 1 = 1 + 0"
           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"
         fix n
         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 0
         show ?case
         case (Suc n)
         show ?case

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 MHonArc.