[isabelle] Type change
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and