[isabelle] Simplifier divergence in Isabelle 2014 release candidates.



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.