Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?




Florian Haftmann wrote:
The "prems" are, roughly, the accumulated facts within a proof, which as
a historical accident have been used implicitly by certain proof methods
-- which, following the rule of thumb "explicit is better than
implicit", turned out as a bad idea.  You can recover this behaviour by
using prems explicitly, e.g. "using prems by ..." or "by (auto simp add:
prems)" etc.  Best practice is to refer to used facts implicitly;
recall that you can quote facts by proposition using backticks ``.

Just to make sure I understand, in 2009-1, for blast/force/assumption/simp I need to say "by - the_proof_method" or add prems, since it was decided that implicit prems were undesired.

However, for auto I just need to say "by auto" and it automatically chains in the prems that I get from "case (Cons x xs) hence IH: some_IH" *without* somehow triggering that same legacy feature that blast/force/simp used to use? That's what got me confused in the first place.

Does this mean I should be writing:

next
  case (Cons x xs)
  from prems have ...

instead of

next
  case (Cons x xs)
  hence ...
?

Sincerely,

Rafal Kolanski.





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