[isabelle-dev] Strange phenomenon with presburger
Amine Chaieb
ac638 at cam.ac.uk
Tue Mar 10 12:12:05 CET 2009
Hi Florian,
This is due to the followin different behavior after using
ObjectLogic.full_atomize_tac. Don't ask me why this happens :)
In the first instance the preprocessor arrives at a stage:
!!uu. ALL uu. uu --> (ALL m n. Suc (2 * m) ~= 2 * n)
then there is an other subtactic which eliminates irrelevant premises
for presburger. It assumes the goal to be completely in object logic.
In the second instance, the following happens (even after full_atomize_tac)
the term sent to the filter is:
!!uu m n x. P x --> Suc (2 * m) ~= 2 * n
In fact if you apply full_atomize_tac to this it stays as it is --- this
is strange isn't it?
Anyway, the subtactic thin_prems_tac then does not get rid of the P x
part in fact it thinks all the term is irrelevant and tries to prove:
"False ==> (!!uu m n x. P x --> Suc(2 *m) ~= 2 *n)"
using blast_tac HOL_cs 1, but that fails, don't ask me why either :(
Maybe I messed things up when implementing this, but I don't see the
exact problem :(
Try this:
ML {* Goal "!! a b. P a --> Q b"*}
ML{* by ( ObjectLogic.full_atomize_tac 1)*}
full_atomize_tac does nothing, is this the intended behavior?
Amine.
Florian Haftmann wrote:
> lemma "\<And>m n x. x \<in> P \<Longrightarrow> Suc (2 * m) = 2 * n
> \<Longrightarrow> False"
> apply presburger done
>
> lemma "\<And>m n x. P x \<Longrightarrow> Suc (2 * m) = 2 * n
> \<Longrightarrow> False"
> apply presburger -- fails
>
> This phenomenon already occurs in Isabelle 2008 and still persists. The
> confusing fact is that neither x nor P matter anyway.
>
> Any idea?
>
> Florian
>
>
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
More information about the isabelle-dev
mailing list