[isabelle] 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






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