# [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?

Peace
- John Ridgway
Visiting Assistant Professor
Trinity College
Hartford, CT

```

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