*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplification problem*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 19 Dec 2011 07:56:04 +0100*In-reply-to*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com>*References*: <09BCA867-0CB5-4DF5-9889-A28E4491B5C2@jacelridge.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0

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

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

- Previous by Date: [isabelle] Simplification problem
- Next by Date: Re: [isabelle] Simplification problem
- Previous by Thread: [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