[isabelle-dev] Bind raised in auto

[Christian Urban]

Makarius writes:
 > The check_conv function also provides some extra trace, if 
 > simp_trace/simp_debug is enabled.  See the sources:
 > 
 >        trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
 >        trace_term false (fn () => "Should have proved:") ss prop0;
 >        NONE
 > 
 > This indicates a problem in the subgoaler setup, but could be a mistake in 
 > the check itself, too.

The last two lines of the trace output are below. I 
did not change anything from the standard setup. 

There might also be a connection with eta-contraction
because if I define my function as

   definition
     "f s a b == length (filter (\x. x = a) s) = length (filter (\x. x = b) s)"

I receive the bind-message, but if I change it to

   definition
     "f s a b == length (filter (op= a) s) = length (filter (op= b) s)"

everything works fine. But again, this might be
just noise.

Christian


Trace output
============
.....

[2]Proved wrong thm (Check subgoaler?)
\<forall>x\<in>set (CHR ''a'' ^^^ :000). x \<noteq> ?a :000 :001 :002 :003 \<equiv>
CHR ''a'' \<noteq> ?a :000 :001 :002 :003 \<or> :000 = 0

[2]Should have proved:
\<forall>x\<in>set (CHR ''a'' ^^^ :000). x \<noteq> ?a :000 :001 :002 :003