*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Tue, 12 Aug 2014 17:50:53 +1000*In-reply-to*: <53E9A03C.7040109@nicta.com.au>*References*: <53E9A03C.7040109@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

Apologies once again, Thomas. On 12/08/14 15:03, Thomas Sewell wrote:

Hello Isabelle users.I've been putting a little time into updating the l4.verified proofsto isabelle-2014 (partly because I wanted to know what fraction of theproblems would be caused by my hypsubst change). I've had a fewproblems I will soon report on. The simplest problem to reportinvolves the simplifier.I haven't been following closely, but I take it the simplifier is nowa bit more aggressive in figuring out how to instantiate assumptions.This is probably a good thing, and has shrunk a few of the proofs inthe 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 (pasPolicyinitial_aag) (OrdinaryLabel a))(λx. pasIRQAbs initial_aag x ∈ subjectReads (pasPolicyinitial_aag) (OrdinaryLabel a))(λx. pasASIDAbs initial_aag x ∈ subjectReads (pasPolicyinitial_aag) (OrdinaryLabel a))(λx. pasDomainAbs initial_aag x ∈ subjectReads (pasPolicyinitial_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. Idon't know what any of this means either, and it turns out it doesn'tmatter. The behaviour is the same in a scratch theory with none of theconstants defined.This problem will cause "simp" or "(simp only: )" to loop. It will besolved immediately by clarify or blast. It can be solved by metis ifwe adjust the problem a little to ensure the type variables all havesorts.The news file suggests that [[simp_legacy_precond]] might be relevantto this issue, but it doesn't seem to change anything.In detail, this problem is solved by simplifying the implication whosepremise is already known, i.e. apply (drule(1) mp). It happens thescript "apply (drule(1) mp, simp)" solves the goal.This weakness of simp is quite frustrating. To generate the abovegoal, I had to work around the possible simp divergence by simplifyingin stages:apply (simp add: uwr_def sameFor_def sameFor_subject_def) apply clarify apply (simp(no_asm_use)) apply clarifyI'm willing to accept the argument that this is not a bug but rather atradeoff, with the default behaviour now being to solve more problemsbut sometimes time out more often. However I'd really like a way toturn this off. I've already had to dance around the problem in acouple of places, and it seems to be a generally unpleasantexperience. 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.

**Follow-Ups**:**Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.***From:*Thomas Sewell

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

- Previous by Date: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Next by Date: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Previous by Thread: Re: [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