Re: [isabelle] rule Unifies With Chained Facts?

On Mon, 4 Apr 2011, Makarius wrote:

On Sun, 3 Apr 2011, Rafal Kolanski wrote:

I still remain surprised whenever I have to replace "by blast" with "by - blast". As for fastsimp, force and metis... I just don't remember.

"by blast" and "by - blast" should be always the same.

Since blast is a "simple method" it first uses "insert" to dump the facts into the goal state and then tries its luck on the result.

Actually you can have a difference if the goal state has > 1 subgoals, e.g. like this:

  assume B
  then have "A --> A" and B by - blast

Here the "dumping" of facts is only weakly structured: all subgoals are augmented uniformly. The "blast" then solves the first, while the other is implicitly closed as trivial in the end.

The defaults of the Isar language attempt to maximize proof structure, e.g. one should not attempt to escape from that without good reasons.


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