Re: [isabelle] Type change
On Tuesday 24 October 2006 12:13, 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).
in fact anything that would allow you to deduce "k = j - Suc 0" from your
premise would be unsound, because "k <= j - Suc 0" is a sufficient condition
for "(k - (j - Suc 0)) mod n = (0::nat)".
If subtraction on type "nat" is not accurately modelling what you want to
formalize, then maybe using type "int" in your formulas in the first place
might solve your problem.
> There is a way to change automatically the type of a formula from nat to
> int so using the integer theorems?
No, because a theorem that holds for type "nat" may not hold for type "int",
and vice versa. (One particular example is "m <= n ==> m - n = 0".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and