equal
deleted
inserted
replaced
86 else |
86 else |
87 if #0$<b then negDivAlg (<a,b>) |
87 if #0$<b then negDivAlg (<a,b>) |
88 else negateSnd (posDivAlg (<$-a,$-b>))" |
88 else negateSnd (posDivAlg (<$-a,$-b>))" |
89 |
89 |
90 definition |
90 definition |
91 zdiv :: "[i,i]=>i" (infixl "zdiv" 70) where |
91 zdiv :: "[i,i]=>i" (infixl \<open>zdiv\<close> 70) where |
92 "a zdiv b == fst (divAlg (<intify(a), intify(b)>))" |
92 "a zdiv b == fst (divAlg (<intify(a), intify(b)>))" |
93 |
93 |
94 definition |
94 definition |
95 zmod :: "[i,i]=>i" (infixl "zmod" 70) where |
95 zmod :: "[i,i]=>i" (infixl \<open>zmod\<close> 70) where |
96 "a zmod b == snd (divAlg (<intify(a), intify(b)>))" |
96 "a zmod b == snd (divAlg (<intify(a), intify(b)>))" |
97 |
97 |
98 |
98 |
99 (** Some basic laws by Sidi Ehmety (need linear arithmetic!) **) |
99 (** Some basic laws by Sidi Ehmety (need linear arithmetic!) **) |
100 |
100 |