# IsarMathLib

## A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory IntDiv_ZF_IML imports Int_ZF_1 ZF.IntDiv
begin

This theory translates some results form the Isabelle's IntDiv.thy theory to the notation used by IsarMathLib.

### Quotient and reminder

For any integers $$m,n$$ , $$n>0$$ there are unique integers $$q,p$$ such that $$0\leq p < n$$ and $$m = n\cdot q + p$$. Number $$p$$ in this decompsition is usually called $$m$$ mod $$n$$. Standard Isabelle denotes numbers $$q,p$$ as m zdiv n and m zmod n, resp., and we will use the same notation.

The next lemma is sometimes called the "quotient-reminder theorem".

lemma (in int0) IntDiv_ZF_1_L1:

assumes $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$

shows $$m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n)$$ using assms , Int_ZF_1_L2 , raw_zmod_zdiv_equality

If $$n$$ is greater than $$0$$ then m zmod n is between $$0$$ and $$n-1$$.

lemma (in int0) IntDiv_ZF_1_L2:

assumes A1: $$m\in \mathbb{Z}$$ and A2: $$0 \leq n$$, $$n\neq 0$$

shows $$0 \leq m\text{ zmod }n$$, $$m\text{ zmod }n \leq n$$, $$m\text{ zmod }n \neq n$$, $$m\text{ zmod }n \leq n - 1$$proof
from A2 have T: $$n \in \mathbb{Z}$$ using Int_ZF_2_L1A
from A2 have $$\ \sharp 0 \ \ \lt n$$ using Int_ZF_2_L9 , Int_ZF_1_L8
with T show $$0 \leq m\text{ zmod }n$$, $$m\text{ zmod }n \leq n$$, $$m\text{ zmod }n \neq n$$ using pos_mod , Int_ZF_1_L8 , Int_ZF_1_L8A , zmod_type , Int_ZF_2_L1 , Int_ZF_2_L9AA
then show $$m\text{ zmod }n \leq n - 1$$ using Int_ZF_4_L1B
qed

\$(m\cdot k) div $$k = m$$.

lemma (in int0) IntDiv_ZF_1_L3:

assumes $$m\in \mathbb{Z}$$, $$k\in \mathbb{Z}$$ and $$k\neq 0$$

shows $$(m\cdot k)\text{ zdiv }k = m$$, $$(k\cdot m)\text{ zdiv }k = m$$ using assms , zdiv_zmult_self1 , zdiv_zmult_self2 , Int_ZF_1_L8 , Int_ZF_1_L2

The next lemma essentially translates zdiv_mono1 from standard Isabelle to our notation.

lemma (in int0) IntDiv_ZF_1_L4:

assumes A1: $$m \leq k$$ and A2: $$0 \leq n$$, $$n\neq 0$$

shows $$m\text{ zdiv }n \leq k\text{ zdiv }n$$proof
from A2 have $$\ \sharp 0 \leq n$$, $$\ \sharp 0 \neq n$$ using Int_ZF_1_L8
with A1 have $$m\text{ zdiv }n \ \ \leq k\text{ zdiv }n$$, $$m\text{ zdiv }n \in \mathbb{Z}$$, $$m\text{ zdiv }k \in \mathbb{Z}$$ using Int_ZF_2_L1A , Int_ZF_2_L9 , zdiv_mono1
then show $$(m\text{ zdiv }n) \leq (k\text{ zdiv }n)$$ using Int_ZF_2_L1
qed

A quotient-reminder theorem about integers greater than a given product.

lemma (in int0) IntDiv_ZF_1_L5:

assumes A1: $$n \in \mathbb{Z} _+$$ and A2: $$n \leq k$$ and A3: $$k\cdot n \leq m$$

shows $$m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n)$$, $$m = (m\text{ zdiv }n)\cdot n + (m\text{ zmod }n)$$, $$(m\text{ zmod }n) \in 0 .\ .\ (n - 1 )$$, $$k \leq (m\text{ zdiv }n)$$, $$m\text{ zdiv }n \in \mathbb{Z} _+$$proof
from A2, A3 have T: $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$, $$k\in \mathbb{Z}$$, $$m\text{ zdiv }n \in \mathbb{Z}$$ using Int_ZF_2_L1A
then show $$m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n)$$ using IntDiv_ZF_1_L1
with T show $$m = (m\text{ zdiv }n)\cdot n + (m\text{ zmod }n)$$ using Int_ZF_1_L4
from A1 have I: $$0 \leq n$$, $$n\neq 0$$ using PositiveSet_def
with T show $$(m\text{ zmod }n) \in 0 .\ .\ (n - 1 )$$ using IntDiv_ZF_1_L2 , Order_ZF_2_L1
from A3, I have $$(k\cdot n\text{ zdiv }n) \leq (m\text{ zdiv }n)$$ using IntDiv_ZF_1_L4
with I, T show $$k \leq (m\text{ zdiv }n)$$ using IntDiv_ZF_1_L3
with A1, A2 show $$m\text{ zdiv }n \in \mathbb{Z} _+$$ using Int_ZF_1_5_L7
qed
end
lemma (in int0) Int_ZF_1_L2:

assumes $$a \in \mathbb{Z}$$, $$b \in \mathbb{Z}$$

shows $$a + b = a \ \ + b$$, $$a\cdot b = a \ \ * b$$
lemma (in int0) Int_ZF_2_L1A:

assumes $$m \leq n$$

shows $$m \ \ \leq n$$, $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$
lemma (in int0) Int_ZF_2_L9:

assumes $$i \leq m$$ and $$i\neq m$$

shows $$i \ \ \lt m$$
lemma (in int0) Int_ZF_1_L8: shows $$(\ \ \ \sharp 0) = 0$$, $$(\ \ \ \sharp 1) = 1$$
lemma (in int0) Int_ZF_1_L8A: shows $$0 \in \mathbb{Z}$$, $$1 \in \mathbb{Z}$$
lemma (in int0) Int_ZF_2_L1:

assumes $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$ and $$m \ \ \leq n$$

shows $$m \leq n$$
lemma (in int0) Int_ZF_2_L9AA:

assumes $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$ and $$m \ \ \lt n$$

shows $$m\leq n$$, $$m \neq n$$
lemma (in int0) Int_ZF_4_L1B:

assumes $$m \leq L$$

shows $$m = L \vee m + 1 \leq L$$, $$m = L \vee m \leq L - 1$$
lemma (in int0) IntDiv_ZF_1_L1:

assumes $$m\in \mathbb{Z}$$, $$n\in \mathbb{Z}$$

shows $$m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n)$$
lemma (in int0) Int_ZF_1_L4:

assumes $$x\in \mathbb{Z}$$, $$y\in \mathbb{Z}$$

shows $$x + y = y + x$$, $$x\cdot y = y\cdot x$$
Definition of PositiveSet: $$\text{PositiveSet}(G,P,r) \equiv$$ $$\{x\in G.\ \langle \text{TheNeutralElement}(G,P),x\rangle \in r \wedge \text{TheNeutralElement}(G,P)\neq x\}$$
lemma (in int0) IntDiv_ZF_1_L2:

assumes $$m\in \mathbb{Z}$$ and $$0 \leq n$$, $$n\neq 0$$

shows $$0 \leq m\text{ zmod }n$$, $$m\text{ zmod }n \leq n$$, $$m\text{ zmod }n \neq n$$, $$m\text{ zmod }n \leq n - 1$$
lemma Order_ZF_2_L1: shows $$x \in \text{Interval}(r,a,b) \longleftrightarrow \langle a,x\rangle \in r \wedge \langle x,b\rangle \in r$$
lemma (in int0) IntDiv_ZF_1_L4:

assumes $$m \leq k$$ and $$0 \leq n$$, $$n\neq 0$$

shows $$m\text{ zdiv }n \leq k\text{ zdiv }n$$
lemma (in int0) IntDiv_ZF_1_L3:

assumes $$m\in \mathbb{Z}$$, $$k\in \mathbb{Z}$$ and $$k\neq 0$$

shows $$(m\cdot k)\text{ zdiv }k = m$$, $$(k\cdot m)\text{ zdiv }k = m$$
lemma (in int0) Int_ZF_1_5_L7:

assumes $$a \in \mathbb{Z} _+$$ and $$a\leq b$$

shows $$b \in \mathbb{Z} _+$$
15
24
3
3