# 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
nat_number_of_def
zdvd_int
int_int_eq[symmetric]
zle_int[symmetric]
zless_int[symmetric]
zadd_int[symmetric]
zmult_int[symmetric]
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
nat_0_le
all_nat
ex_nat
number_of1
number_of2
int_0
int_1
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.
Amine.
On Tue, 24 Oct 2006, Gabriele Pozzani wrote:
> 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.*