Re: [isabelle] Simplification problem

I now have a bare-bones theory which demonstrates this problem:

theory temp imports Main begin

lemma "
  \<lbrakk> (x::nat,y::nat) \<in> xys;
    \<forall>x' y'. (x', y') \<in> xys \<longrightarrow> x'=x \<and> y'=y;
    y'' = y \<rbrakk> \<Longrightarrow>


Note that I'm importing from Main (HOL), so nothing I've added is causing any problems.  If I can't do this, how do I say that a particular constructed value is in a set, and that any constructed value in the set is equal to this one?  The y''=y premise is essential to causing the simplifier to loop (x''=x also causes a loop).  I'm at a loss.

- John

On Dec 19, 2011, at 1:56 AM, Tobias Nipkow wrote:

> 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.