[isabelle] Type change



Hello,
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.

Thanks
Gabriele Pozzani




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.