*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplification problem*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 20 Dec 2011 11:38:57 +1100*Cc*: john at jacelridge.com*In-reply-to*: <AE32AD82-8767-4773-A797-9C4B81AEDA2D@jacelridge.com>*References*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com> <4EEEE004.1050905@in.tum.de> <AE32AD82-8767-4773-A797-9C4B81AEDA2D@jacelridge.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1

In summary: before thinking, always blindly type a bunch of nonsense.

"ALL x' y'. ((x', y') : xys) = (x' = x & y' = y & xys ~= {})" (This can be proven equal to your assumption by fast)

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

**Follow-Ups**:**Re: [isabelle] Simplification problem***From:*John Ridgway

**Re: [isabelle] Simplification problem***From:*Tobias Nipkow

**References**:**[isabelle] Simplification problem***From:*John Ridgway

**Re: [isabelle] Simplification problem***From:*Tobias Nipkow

**Re: [isabelle] Simplification problem***From:*John Ridgway

- Previous by Date: Re: [isabelle] Simplification problem
- Next by Date: Re: [isabelle] Simplification problem
- Previous by Thread: Re: [isabelle] Simplification problem
- Next by Thread: Re: [isabelle] Simplification problem
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list