Re: [isabelle] New error messages in Isabelle 2013
On Wed, 30 Jan 2013, René Neumann wrote:
I really like to only feed command by command to the prover ("what are
the goals exactly after the 'with'", "what does simp remove/unfold",
The Isabelle/Isar proof state consists of more than just goals. For
example, you don't want to see the goal again after 'then', 'from', 'with'
etc. because they don't change it. You might want to have some editor
support to rearrange such indications of 'using' facts.
"what goals does 'induction' give" ...).
That is in fact the standard example where you can see the limitations of
the hybrid model from 2000, which is still used often today. The "induct"
proof method knows much more about the structure of the proof than just
the new subgoals than happen to pop out after it. It could propose a
canonical proof outline for the induction pattern straight away, with
placeholders for typical "by auto" proofs to finish the cases. You don't
need funny print_cases commands and its output for that, just a tiny
little more progress in Prover IDE technology.
Another example where the state output is bad are calculation proofs in
Isar. This is a very simple and basic concept, but it becomes slightly
awkward to manage with the step-by-step approach from the old times.
This archive was generated by a fusion of
Pipermail (Mailman edition) and