Re: [isabelle] Change in behavior of "simp" from Isabelle 2014 to Isabelle2015



On 30.05.2015 23:27, Eugene W. Stark wrote:
> After getting started with Isabelle not too long ago, I settled into
> a mode of use in which I often state the fact I am trying to prove,
> enter a "using xxx yyy zzz ..." clause with as many of the lemmas that
> I am reasonably certain are relevant to the proof, and then invoke
> "try" to try to see if the fact can be proved automatically, and as
> a byproduct to learn about relevant lemmas from various theories in Main
> which I would otherwise have a hard time locating.
While this mode of proving works, you will get better results if you
learn the more directed ways of passing lemmas to proof tools: e.g.,
simplification, introduction, elimination and destruction rules. This
also has the advantage that you can declare them to be used
automatically by proof tools (using the [simp], [intro], ... attributes).
>
> With Isabelle2015, I have so far experienced a number of times the situation
> in which I enter "using foobar_def", then invoke "try" and am told
> "Try this: by (simp add: foobar_def)". Previously in Isabelle2014 it generally
> seemed to be enough to say "using foobar_def by simp", but now in Isabelle2015
> it is often necessary to explicitly add foobar_def as a simplification.
I am pretty sure that there was no change in Isabelle 2015 which would
change this behaviour in general. However, as simp rules and facts
inserted by "using" are treated differently by the simplifier, it is no
surprise that these sometimes lead to different results -- neither of
these methods is strictly more powerful then the other.
> The point is, I already know that foobar_def is going to be needed in the proof,
> but I don't necessarily know that it will have to be used as a simplification.
For a definition, anything else would be surprising (in most cases) ;)
> Also, as far as I know, the "using" clause does not provide a way to indicate
> which of the facts being used are to be used as simplifications, as opposed
> to ordinary lemmas.
For most of the (automated) proof methods, "using" does nothing else
then insert the fact into the goal, e.g.

  have "P" using `Q` apply simp

leads to the simplifier trying to solve "Q ==> P". On the other hand,
facts passed by (e.g.) "simp:" will not become part of the goal.

Sometimes, this makes "using" more powerful: Whereas a fact passed by
"simp:" will be used as-is (modulo some restricted preprocessing), the
assumptions of a subgoal will be simplified before they are used for
rewriting. This might help if the fact is not in normal form:

  notepad begin
    fix P :: "nat => bool"
    assume *: "P 1"
    have "P (2 - 1)"
       apply (simp add: *)        (* does not solve, leaves P (Suc 0) *)
       using * apply simp         (* solves, as P 1 is simplified to P
(Suc 0) *)
       done

It might also make "using" weaker:

  definition P :: "'a => bool" where "P x = True"

  notepad begin
    fix x :: 'a and y :: 'b
    have "P x = P y"
      by (simp add: P_def)      (* works *)
    have "P x = P y "
      using P_def apply simp sorry  (* fails, unfolds only one P *)
    have "P x = P y"
      using P_def P_def by simp      (* works *)

The reason is that Isabelle can not quantify over types. Polymorphic
facts are represented using schematic type variables. But these can only
be instantiated once.

Similar things happen also for other automated tools.

  -- Lars




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