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:

notepad
begin
  assume B
  then have "A --> A" and B by - blast
end

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.


	Makarius





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