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



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.