[isabelle-dev] Strange phenomenon with presburger
Makarius
makarius at sketis.net
Tue Mar 10 17:19:33 CET 2009
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
More information about the isabelle-dev
mailing list