Email Gateway (Aug 18 2022 at 20:01): Email Gateway (Aug 18 2022 at 20:01):From: "Ridgway, John V. E." <John.Ridgway@trincoll.edu>
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
Email Gateway (Aug 18 2022 at 20:01):From: Lawrence Paulson <lp15@cam.ac.uk>
The intention of auto is to do all possible obvious steps to all goals, and return whatever is left over. And auto is supposed to return fairly quickly.
The intention of force is to throw everything at the first goal, and never give up until it is proved.
Larry Paulson
Email Gateway (Aug 18 2022 at 20:01):From: Ramana Kumar <rk436@cam.ac.uk>
That might mean your goal is unprovable (and you should double-check your
theorem statement...).
(It could also mean that there are contradictions in your assumptions or
context somewhere that auto hasn't noticed.)
I guess apply(force) in that place is "never giving up" (as Larry said)
trying to prove an unprovable goal, and therefore running forever.
Email Gateway (Aug 18 2022 at 20:01):From: Lars Noschinski <noschinl@in.tum.de>
Have you looked at the simplifier trace, whether it tries to apply said
rule? The trace can be enabled by adding "using [[simp_trace]]") before
applying simp. To see how the simplifier handles conditional rules. You
might want to increase the tracing depth with "using
[[simp_trace_depth_limit=n]]" for some appropriate value of n.
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC