Re: [isabelle] Simplification problem



I actually went with 

(x,y) \<in> xys
  and
ALL x' y'. (x' \<notequal> x \<or> y' \<notequal> y) --> ((x',y') \<notin> xys)

and that seems to work better.  Thanks for your help.

Peace
- John


On Dec 19, 2011, at 7:38 PM, Thomas Sewell wrote:

> Nothing in Isabelle can really be trusted to solve your problems as a black box. In this situation you can do two things. One is to try lots of variants, and the other is to try to understand exactly how the system works.
> 
> The simp variants (simp(no_asm)) and (simp(no_asm_use)) can sometimes help with these problems by rewriting your assumptions before using them as rewrites. This won't help in this case. Many other solvers which don't call the simplifier can solve your reduced example (metis, blast, safe).
> 
> In summary: before thinking, always blindly type a bunch of nonsense.
> 
> This may not solve your real problem, and keeping the simplifier on your side is usually necessary. The simplifier (in assumption-using mode, the default) treats assumptions as rewrite rules as though they'd been supplied with [simp]. This causes it to diverge frequently since they may loop in various ways. In this case, it's treating your rule as a way of rewriting *any* natural into x or y by showing it is a component of a member of xys. This includes naturals that have already been rewritten to x or y, as well as the naturals in the assumption it must prove to use this rule (it really is that stupid). In short, you can't let this assumption stay in this form.
> 
> You can probably finesse your way around this by using the logically equivalent assumption
>  "ALL x' y'. ((x', y') : xys) = (x' = x & y' = y & xys ~= {})"
> 
> (This can be proven equal to your assumption by fast)
> 
> The simplifier is now not being given a license to rewrite any x or y, but only terms of the form (x', y') : xys. This should hopefully be a force for good and not evil.
> 
> Yours,
>    Thomas.
> 
> On 20/12/11 09:28, John Ridgway wrote:
>> 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>
>>   True"
>> apply(simp)
>> done
>> 
>> end
>> 
>> 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.
>> 
>> Peace
>> - 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.