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.

  -- Lars

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