Re: [isabelle] Simplification problem

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

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

exception ?x ?xa3 ∈ epsilon_11

cx ≡ cx

Hope this helps,


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.

- John Ridgway
Visiting Assistant Professor
Trinity College
Hartford, CT

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