Re: [isabelle] Does it mean busy or something else? (purple background)

On 12/23/2013 11:04 PM, Yannick Duchêne (Hibou57) wrote:
> Hi famous people,
> While I had a short test on a topic, I came to this example, with
> which I don't know how to interpret the purple background colour I get
> on “by (simp add: atomize_all atomize_eq atomize_imp)” in the sample
> below (also as attached file):
>     inductive f :: "'a list ⇒ bool"
>       where f1: "f []"
>     lemma "(⋀foo a. foo = f a) ⟹ f a"
>       proof -
>         assume h: "⋀foo a. foo = f a"
>         have "True = f a" using h by (simp add: atomize_all atomize_eq
> atomize_imp)
>         thus ?thesis by simp
>       qed
> I'm accustomed to see this background colour when it's busy, like with
> Metis, typically for a short time. Here, I wonder what it means, the
> background remains, I can't imagine the Simplifier (which I wanted on
> purpose instead of Blast) running forever like this, and the goal
> seems to be solved.

The simplifier loops on this example. To see why, enable the simplifier
trace and raise the depth limit:

    using [[simp_trace, simp_trace_depth_limit=30]]
    by (simp add: atomize_all atomize_eq atomize_imp)

In particular, have a look at the default congruence rule "imp_cong".

As long as the purple background remains, the goal is not solved!

  -- Lars

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