[isabelle] Problem with simplifier trace (part 2)



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.