Re: [isabelle] Does it mean busy or something else? (purple background)
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Does it mean busy or something else? (purple background)
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Tue, 07 Jan 2014 11:52:56 +0100
- In-reply-to: <op.w8kfl4doule2fv@cardamome>
- References: <op.w8kfl4doule2fv@cardamome>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20131103 Icedove/17.0.10
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
> thus ?thesis by simp
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and