[isabelle-dev] Strange phenomenon with presburger

[Amine Chaieb]

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