[isabelle] Simplification problem



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







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