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 MHonArc.