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.