[isabelle] interpret/moreover/ultimately



Hi there,

recently I experienced some strange behavior (Isabelle2011-1 in jedit) which is reproduced in the small example below:

notepad begin
  fix l le B
  interpret preorder l le sorry
  moreover have "B" sorry
  ultimately have "class.preorder l le & B" by blast
end

in the "ultimately" line but before "by blast", the current state looks as follows:

proof (prove): step 8

using this:
  class.preorder l le
  B

goal (1 subgoal):
 1. class.preorder l le & B

but blast (and auto, .., simp, force, best, ...) does not solve the goal. If I write instead

notepad begin
  fix l le B
  interpret preorder l le sorry
  have "B" sorry
  from `class.preorder l le` and `B`
    have "class.preorder l le & B" by blast
end

everything works fine. The corresponding state is


proof (prove): step 7

using this:
  class.preorder l le
  B

goal (1 subgoal):
 1. class.preorder l le ∧ B

So the only immediately conceivable difference is "step 7" instead of "step 8".

cheers

chris





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