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



On Wed, Apr 1, 2009 at 11:20, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 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.

I just used infix notation for st_in_prog which I shouldn't have done
as it's obviously quite misleading. It should be:

[1]Trying to rewrite:
[| st_in_prog P ?st1; ([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

where ?st1 is a statement i.e. a base value.

> [...]

Under these circumstances I would conclude that at least the tracing
algorithm isn't as helpful as it should be. Am I right?

Christoph





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