Re: [isabelle] Type change
This is part of the arith tactic preprocessing and is due to Grosser
Meister. You can first rewrite with The following rules
and the split rule zdiff_int_split
These turn "conventional" formulae over nat in to formulae where the "int"
is in front of all terms.
After this you can rewrite with the following theorems
and cong rules : conj_le_cong imp_le_cong
These "eliminate" the "int" in favour of "int (nat ..)" which can be
eliminated easily. Note that the "nat" variables have to be quantified!!!
Please include the appropriate rules to cover the predicates and functions
you use in the same scheme.
On Tue, 24 Oct 2006, Gabriele Pozzani wrote:
> I have a formula involving the "mod" operator and so on nat type, but when I
> eliminate the "mod" operator using the rule Divides.mod_eqD or
> Divides.mod_eq_0D I want use the int type.
> In particular I have:
> (k - (j - Suc 0)) mod n = (0::nat)
> eliminate the mod operator obtaining:
> EXISTS q. (k - (j - Suc 0)) = n * q
> but in natural if q is 0 then (k - (j - Suc 0)) --> k <= (j - Suc
> 0) not k = (j - Suc 0).
> There is a way to change automatically the type of a formula from nat to int
> so using the integer theorems?
> I seen the int::nat => int but I must introduce it manually and if I use it
> there are many unification errors with others formula.
> Gabriele Pozzani
This archive was generated by a fusion of
Pipermail (Mailman edition) and