Re: [isabelle] Difference between "apply(auto)" and "apply(force)"
On 02.05.2012 02:04, Ridgway, John V. E. wrote:
lemma popframecx_newframecx_same [simp]: "
\<lbrakk> (ctrltoprimmech (exntoctrlmech cx), R_cx) \<in> validmechanism \<rbrakk>
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).
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and