[isabelle-dev] Strange phenomenon with presburger

[Makarius]

On Tue, 10 Mar 2009, Amine Chaieb wrote:

> 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?

This is because the innermost binder "!!x. ..." cannot be internalized 
into HOL, since x is not of sort HOL.type.  Cf. these examples:

lemma "!!m n x. P x ==> Suc (2 * m) = 2 * n ==> False"
  apply (atomize (full))
  apply presburger?
  oops

lemma "!!m n x::'a. P x ==> Suc (2 * m) = 2 * n ==> False"
  apply (atomize (full))
  apply presburger
  done

The second version works, because an explicit type variable is implicitly 
decorated by default sort.  I've once tried to get similar behaviour for 
implicitly generated type variables as well -- via our new "user-space 
type system" infrastructure -- but it failed due to some extra 
complexities in locale expressions (here type-checking is repeated several 
times, leading to even more unexpected results).

In presburger you could try to "thin" out excessive premises before 
internalizing into HOL; this probably requires to "rulify" first.


> 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

This goal is not in canonical HHF form.  Many Isabelle tools will choke on 
that, and are perfectly right to do so.

Whenever you need to produce propositions in non-standard ways, you can 
apply explicit norm_hhf operations to "repair" them before passing on to 
user-space tools.  E.g. like this:

lemma "False ==> (!!uu m n x. P x --> Suc(2 *m) ~= 2 *n)"
  apply (tactic {* Goal.norm_hhf_tac 1 *})
  apply (tactic {* blast_tac HOL_cs 1 *})
  done


	Makarius