*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplification problem*From*: Holger Gast <gast at informatik.uni-tuebingen.de>*Date*: Mon, 19 Dec 2011 08:33:09 +0100*In-reply-to*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com>*References*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:8.0) Gecko/20111124 Thunderbird/8.0

Hi John, if you find you have to invoke the simplifier trace, you may want to try the I3P interface for the purpose: it copes with the stream of messages with minimal processing overhead (by lazy rendering) and always allows you to "interrupt" the prover to examine the message already received :) (Just revoke the command, I3P keeps sending INT to Isabelle until it succeeds. Also, there is a "local option" that turns on the trace for a single command; right-click to the left gutter in the editor.) In your example, I found that the following pattern repeats: [1]Applying instance of rewrite rule "??.unknown": exception ?x ?xa3 ∈ epsilon_11 ⟹ cx ≡ ?x [1]Trying to rewrite: exception ?x ?xa3 ∈ epsilon_11 ⟹ cx ≡ ?x [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: exception ?x ?xa3 ∈ epsilon_11 [1]SUCCEEDED cx ≡ cx Hope this helps, Holger On 12/19/2011 04:13 AM, John Ridgway wrote:

I'm having a problem. Given the following lemma: lemma " !! C tau_0 epsilon_0 rs Rs cx w tau_11 epsilon_11 tau_10 epsilon_10 y. [| C = valconfig w (exntoprimmech cx) Rs tau_11 epsilon_11; tau_0 = tau_10; epsilon_0 = epsilon_10; rs = dom Rs; Rs : validmechanisms; exntoprimmech cx : rs; (w, tau_11) : mvalhastype; exception cx tau_11 : epsilon_11; \<forall>cx' tau_11'. exception cx' tau_11' : epsilon_11 --> cx' = cx \<and> tau_11' = tau_11; tau_10 = tau_11; epsilon_10 = epsilon_11; Rs : validmechanisms; isemptyrs (exntoprimmech cx) Rs; tau_11 : istype; Rs (exntoprimmech cx) = Some y |] ==> (\<exists>C' tau_1 epsilon_1. (C, C') : onestep \<and> (C', tau_1, epsilon_1) : configurationhastype \<and> (tau_1, tau_0) : issubtype \<and> epsilon_1 \<subseteq> epsilon_0) \<or> (\<exists>w r Rs tau_0 epsilon_0. isemptyrs r Rs \<and> C = valconfig w r Rs tau_0 epsilon_0)" I try apply(simp) as the first step in my proof, and Isabelle goes away for a long time. I don't know whether it ever comes back; I gave up on it before then. Removing the premise \<forall>cx' tau_11'. exception cx' tau_11' : epsilon_11 --> cx' = cx \<and> tau_11' = tau_11; allows the whole mess to be proved by simp. What about that premise is causing the trouble? Or is it likely an interaction with other stuff? How do I figure out which it is? Thanks in advance for your help. Peace - John Ridgway Visiting Assistant Professor Trinity College Hartford, CT

**References**:**[isabelle] Simplification problem***From:*John Ridgway

- Previous by Date: Re: [isabelle] Simplification problem
- Next by Date: [isabelle] Ph.D. and postdoctoral positions at IMDEA Software Institute
- Previous by Thread: Re: [isabelle] Simplification problem
- Next by Thread: [isabelle] Ph.D. and postdoctoral positions at IMDEA Software Institute
- Cl-isabelle-users December 2011 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