*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 12 Aug 2014 08:05:23 +0200*In-reply-to*: <53E9A03C.7040109@nicta.com.au>*References*: <53E9A03C.7040109@nicta.com.au>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Dear Thomas, I just tried your file with Isabelle2013-2 and simp looped. This corroborates your experience that [[simp_legacy_precond]] doesn't do anything, because the divergence is not related to it. In any case, the only simplifier change I am aware of relates to the handling of conjunctions in the premises of conditional rewrite rules, and [[simp_legacy_precond]] switches that off. Tobias On 12/08/2014 07:03, Thomas Sewell wrote: > Hello Isabelle users. > > I've been putting a little time into updating the l4.verified proofs to > isabelle-2014 (partly because I wanted to know what fraction of the problems > would be caused by my hypsubst change). I've had a few problems I will soon > report on. The simplest problem to report involves the simplifier. > > I haven't been following closely, but I take it the simplifier is now a bit more > aggressive in figuring out how to instantiate assumptions. This is probably a > good thing, and has shrunk a few of the proofs in the repository already. > > The problem is that this new mechanism sometimes leads to divergence, and I > don't know how to turn it off. Here's an example I came across (or see the > attached theory): > > theory Scratch imports Main begin > > lemma foo: > "⋀a aa b ba ab bb bc. > pasDomainAbs initial_aag (cur_domain b) > ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟹ > u = Partition a ⟹ > s = ((aa, b), ba) ⟹ > s' = ((ab, bb), bc) ⟹ > states_equiv_for > (λx. pasObjectAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) > (OrdinaryLabel a)) > (λx. pasIRQAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) > (OrdinaryLabel a)) > (λx. pasASIDAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) > (OrdinaryLabel a)) > (λx. pasDomainAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) > (OrdinaryLabel a)) > (λx. ptr_range x 12) b bb ⟹ > pasDomainAbs initial_aag (cur_domain b) > ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶ > cur_domain b = cur_domain bb ∧ > globals_equiv b bb ∧ > scheduler_action b = scheduler_action bb ∧ > work_units_completed b = work_units_completed bb ∧ > equiv_irq_state (machine_state b) (machine_state bb) ∧ > (user_modes ba ⟶ aa = ab) ∧ > ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel) kheap b > bb ⟹ > pasDomainAbs initial_aag (cur_domain bb) > ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶ > cur_domain b = cur_domain bb ∧ > globals_equiv b bb ∧ > scheduler_action b = scheduler_action bb ∧ > work_units_completed b = work_units_completed bb ∧ > equiv_irq_state (machine_state b) (machine_state bb) ∧ > (user_modes ba ⟶ aa = ab) ∧ > ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel) kheap b > bb ⟹ > (user_modes ba ⟶ aa = ab) ∧ ba = bc > " > > This is just a copy of a goal that came up in a proof somewhere. I don't know > what any of this means either, and it turns out it doesn't matter. The behaviour > is the same in a scratch theory with none of the constants defined. > > This problem will cause "simp" or "(simp only: )" to loop. It will be solved > immediately by clarify or blast. It can be solved by metis if we adjust the > problem a little to ensure the type variables all have sorts. > > The news file suggests that [[simp_legacy_precond]] might be relevant to this > issue, but it doesn't seem to change anything. > > In detail, this problem is solved by simplifying the implication whose premise > is already known, i.e. apply (drule(1) mp). It happens the script "apply > (drule(1) mp, simp)" solves the goal. > > This weakness of simp is quite frustrating. To generate the above goal, I had to > work around the possible simp divergence by simplifying in stages: > apply (simp add: uwr_def sameFor_def sameFor_subject_def) > apply clarify > apply (simp(no_asm_use)) > apply clarify > > I'm willing to accept the argument that this is not a bug but rather a tradeoff, > with the default behaviour now being to solve more problems but sometimes time > out more often. However I'd really like a way to turn this off. I've already had > to dance around the problem in a couple of places, and it seems to be a > generally unpleasant experience. My usual workarounds (simp only: ) and > (simp(no_asm_use)) can't help me here. > > I attach my scratch theory with this problem. > > I hope there's a simple fix. > > Cheers, > Thomas. > > >

**References**:**[isabelle] Simplifier divergence in Isabelle 2014 release candidates.***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] Changing axiom names in a locale
- Next by Date: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Previous by Thread: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Next by Thread: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Cl-isabelle-users August 2014 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