*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Change in behavior of "simp" from Isabelle 2014 to Isabelle2015*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 01 Jun 2015 11:02:41 +0200*In-reply-to*: <556A2B38.7080105@starkeffect.com>*References*: <556A2B38.7080105@starkeffect.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.7.0

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

- Previous by Date: Re: [isabelle] sig-alternate.cls
- Next by Date: [isabelle] antiquotation for a class
- Previous by Thread: [isabelle] postdoc position (6 years) in Innsbruck
- Next by Thread: Re: [isabelle] Change in behavior of "simp" from Isabelle 2014 to Isabelle2015
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list