*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Difference between "apply(auto)" and "apply(force)"*From*: "Ridgway, John V. E." <John.Ridgway at trincoll.edu>*Date*: Wed, 2 May 2012 00:04:23 +0000*Accept-language*: en-US*Cc*: "Ridgway, John V. E." <John.Ridgway at trincoll.edu>*Thread-index*: AQHNJ/ceU6PdUuLho0KMbtBIDpsD1g==*Thread-topic*: Difference between "apply(auto)" and "apply(force)"

This seems like a really simple question, but I can't find an answer in the documentation anywhere. Maybe I'm just looking in the wrong places. If so, can somebody give me a pointer? I am working on a proof, of a fairly complex lemma, and at one point I enter apply(auto) Isabelle then thinks for a while and gives me back a list of the remaining goals. I then enter apply(force) and the first of the remaining goals is discharged. I was under the impression (apparently incorrect) that apply(auto) was essentially the same as apply(force) except that it was applied to all goals. Is this wrong? Furthermore, at another place in the proof, when I try apply(auto) it ends me up with a goal of False, whereas when I try apply(force)+ I don't have the patience to wait for it to finish... Also, can someone characterize the difference between intro, intro!, and intro?; likewise, elim, elim!, and elim?. Another issue I'm having is that I have a rule that is declared simp that is not being used. I can force it with apply(subst ...) but I'd really like it to be done automatically. I suspect that there's an issue that it's buried too deep. The rule is: lemma popframecx_newframecx_same [simp]: " \<lbrakk> (ctrltoprimmech (exntoctrlmech cx), R_cx) \<in> validmechanism \<rbrakk> \<Longrightarrow> popframecx cx (newframecx cx F R_cx) = Some (F, R_cx)" and the goal it's not being applied in is: \<exists>aa b. popframecx (relatedexceptionhandler a) (newframecx (relatedexceptionhandler a) (Restore r R_r) (newframecx (relatedexceptionhandler a) (Replace (ctrltoprimmech (conttoctrlmech a)) R_a) R_cx)) = Some (aa, b) If this is indeed a case of the simplification just being too buried, how can I request that Isabelle look deeper? If that isn't the case, then why does apply(subst popframecx_newframecx_same) work when simp doesn't? And yes, the premise of popframecx_newframecx_same can be solved by apply(simp). Am I making myself clear? More importantly perhaps, is there some piece of documentation available that would clarify all of this for me? Thank you for your attention, and apologies for troubling you if this is a silly question. Peace - John

**Follow-Ups**:**Re: [isabelle] Difference between "apply(auto)" and "apply(force)"***From:*Lawrence Paulson

**Re: [isabelle] Difference between "apply(auto)" and "apply(force)"***From:*Ramana Kumar

**Re: [isabelle] Difference between "apply(auto)" and "apply(force)"***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Multi-dimensional arrays
- Next by Date: Re: [isabelle] Linear Ordering for nat list
- Previous by Thread: Re: [isabelle] Linear Ordering for nat list
- Next by Thread: Re: [isabelle] Difference between "apply(auto)" and "apply(force)"
- Cl-isabelle-users May 2012 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