[isabelle-dev] Bind raised in auto
urbanc at in.tum.de
Fri Sep 2 16:33:02 CEST 2011
> 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;
> 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
"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
"f s a b == length (filter (op= a) s) = length (filter (op= b) s)"
everything works fine. But again, this might be
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
Should have proved:
\<forall>x\<in>set (CHR ''a'' ^^^ :000). x \<noteq> ?a :000 :001 :002 :003
More information about the isabelle-dev