# [isabelle] Simplifier divergence in Isabelle 2014 release candidates.

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
• From: Thomas Sewell <thomas.sewell at nicta.com.au>
• Date: Tue, 12 Aug 2014 15:03:56 +1000
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

```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.

```
```theory Scratch

imports Main

begin

lemma foo:
"\<And>a aa b ba ab bb bc.
pasDomainAbs initial_aag (cur_domain b)
\<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<Longrightarrow>
u = Partition a \<Longrightarrow>
s = ((aa, b), ba) \<Longrightarrow>
s' = ((ab, bb), bc) \<Longrightarrow>
states_equiv_for
(\<lambda>x. pasObjectAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
(\<lambda>x. pasIRQAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
(\<lambda>x. pasASIDAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
(\<lambda>x. pasDomainAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
(\<lambda>x. ptr_range x 12) b bb \<Longrightarrow>
pasDomainAbs initial_aag (cur_domain b)
\<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<longrightarrow>
cur_domain b = cur_domain bb \<and>
globals_equiv b bb \<and>
scheduler_action b = scheduler_action bb \<and>
work_units_completed b = work_units_completed bb \<and>
equiv_irq_state (machine_state b) (machine_state bb) \<and>
(user_modes ba \<longrightarrow> aa = ab) \<and>
ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<Longrightarrow>
pasDomainAbs initial_aag (cur_domain bb)
\<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<longrightarrow>
cur_domain b = cur_domain bb \<and>
globals_equiv b bb \<and>
scheduler_action b = scheduler_action bb \<and>
work_units_completed b = work_units_completed bb \<and>
equiv_irq_state (machine_state b) (machine_state bb) \<and>
(user_modes ba \<longrightarrow> aa = ab) \<and>
ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<Longrightarrow>
(user_modes ba \<longrightarrow> aa = ab) \<and> ba = bc
"
using [[simp_legacy_precond = true ]]
apply simp
apply fast
apply (drule(1) mp, simp)
apply clarify

end
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.