Re: [isabelle] Isabelle2013-RC2 available for testing



On Wed, 6 Feb 2013, Yannick wrote:

Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too.  Cf. print_claset.

I'm not sure to understand what it implies, but will learn “print_claset”, as you mention it.

It means that the "rule" method in HOL has additional rules available: the ones of Pure (print_rules) and the ones of the classical reasoner context (print_claset). It is wired up in a way that you normally get what you expect in the first place.


Before I came to Isabelle, at the time I didn't knew any prover system, I tried to imagine such things, and in my mind, this was always coming with this: “if it automate some proof or proof step, the user should be able to learn what the steps was, it should be visible in some way”. That's important, as the matter, I feel, is not only about the prover understanding a proof, but also about the human author and human reader, understanding it too.

Yes, this implicit use of single-step rules from the context according to the structure of your problem, is an important aspect of Isar -- the "Intellegible semi-automated reasoning" so to say. Fully automated reasoning is used in different spots.

Until proper IDE feedback for "rule" steps arrives you can use rule_trace as crude approximation:

notepad
begin
  note [[rule_trace]]

  have "A ∧ B"
  proof  -- trace
    show A sorry
    show B sorry
  qed

  from `A ∧ B` obtain A and B ..-- trace

end

This gives you the unfiltered uninstantiated candiates that the method guesses from the situation.

(In Isabelle2012 the trace output needs to be enabled by the check-box in the output panel; in Isabelle2013 it is always there.)


	Makarius


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