*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplification problem*From*: John Ridgway <john at jacelridge.com>*Date*: Mon, 19 Dec 2011 17:28:58 -0500*Cc*: John Ridgway <john at jacelridge.com>*In-reply-to*: <4EEEE004.1050905@in.tum.de>*References*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com> <4EEEE004.1050905@in.tum.de>

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:*Thomas Sewell

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

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

- Previous by Date: [isabelle] Ph.D. and postdoctoral positions at IMDEA Software Institute
- 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