Re: [isabelle] Problem with simplifier trace (part 2)

• To: Christoph Feller <c_feller at informatik.uni-kl.de>
• Subject: Re: [isabelle] Problem with simplifier trace (part 2)
• From: Tobias Nipkow <nipkow at in.tum.de>
• Date: Wed, 01 Apr 2009 11:20:24 +0200
• Cc: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
• In-reply-to: <a1e5e35a0903310244x2d78edb4i91dd6382ca20127f@mail.gmail.com>
• References: <a1e5e35a0903310244x2d78edb4i91dd6382ca20127f@mail.gmail.com>
• User-agent: Thunderbird 2.0.0.19 (Macintosh/20081209)

```I suspect the problem is here:

> [1]Trying to rewrite:
> [| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
> ==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
> Concrete_AST_w_st.stypv P ?st1 v

You have a premise with an uninstantiated higher-order variable. The
simplifier probably managed to instantiate ?st1 with something that
returns False, eg %_ _. False.

The simplifier is not predictable on rules with higher-order variables
in the premises that are not in the conclusion. You have given it the
license to replace such variables with anything...

Tobias

Christoph Feller schrieb:
> Hallo,
>
> I got the same problem as before just at another place. This time I
> supply an actual subtrace. This part gets repeated over and over.
> Simplifier depth is set to 3. Why do I think this trace is strange?
> Well the simplifier tries to use the rule in the first line/block (of
> the trace). So it has to show both assumption. It instantiates ?s1 and
> ?st with the same value and then finds that it can simplify the second
> assumption to False (see line/block six). But then the trace continues
> with "succeeded", with no indication why it succeeded and I don't want
> it to - but I've no way to find the reason for this success.
>
> By the way, if I delete st_in_st_not_ref (see line/block five) from
> the simpset the simplifier doesn't loop.
>
> Can anyone make sense of this?
>
> [1]Applying instance of rewrite rule "local.P.st_in_st_stypv":
> [| ?st1 st_in_prog P; (?s1, ?st1) : st_in_st |] ==>
> Concrete_AST_w_st.stypv P ?s1 ?v1 == Concrete_AST_w_st.stypv P ?st1
> ?v1
>
> [1]Trying to rewrite:
> [| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
> ==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
> Concrete_AST_w_st.stypv P ?st1 v
>
> [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
> ?st1 st_in_prog P
>
> [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
> ([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) : st_in_st
>
> [2]Applying instance of rewrite rule "local.P.st_in_st_not_ref":
> (?st1, ?st1) : st_in_st == False
>
> [2]Rewriting:
> ([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) :
> st_in_st == False
>
> [1]SUCCEEDED
> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v
>
> Thanks,
>
> Christoph Feller

```

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