Re: [isabelle] Simplification problem



This is a tricky situation. The simplifier diverges and you want to find
out why. In principle the answer is simple: switch on the simplifier
trace. In practice, this can overload the interface (Proof General and
jedit) because an infinite rewrite tends to produce an infinite trace.
You may be lucky because the infinity of the trace only manifests itself
when the trace depth is set sufficiently high (initially it is 1). Or
you may be able to abort the simp command quickly enough before the
interface freezes up.

I general it is hard to figure out why something diverges just by
looking at the initial proof state because it may involve some
unexpected interaction between the hundreds of existing rewrite rules
and the goal state. In you goal, the offending assumption will be turned
into two rewrite rules by the simplifier:

exception ?cx' ?tau_11' : epsilon_11 ==> (?cx' = cx) = True
exception ?cx' ?tau_11' : epsilon_11 ==> (?tau_11' = tau_11) = True

Not sure why that could lead to a problem.

Tobias

PS The "!! ..." prefix is not needed.

Am 19/12/2011 04:13, schrieb John Ridgway:
> 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.