Re: [isabelle] Simplification problem

Tom, your analysis is not quite accurate: the rewrite rules coming out
of the hypothesis do not rewrite *any* natural number. The simplifier is
intelligent enough to avoid that. As I pointed out in my previous email,
it derives the rewrite rule

(?x', ?y') : xys ==>  (?x'=x) = True
(?x', ?y') : xys ==>  (?y'=y) = True

They are harmless. However, I failed to see that it also derives

(?x', ?y') : xys ==>  x = ?x'
(?x', ?y') : xys ==>  y = ?y'

Either of them causes a problem together with (x,y) : xys, because they
allow x = x = x = ... or y = y = y = ... .


Am 20/12/2011 01:38, schrieb Thomas Sewell:
> 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.