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.


	Makarius


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