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.