IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

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 \( #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 \( #0 \leq n \), \( #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 \( (\ \$ # 0) = 0 \), \( (\ \$ # 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}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\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} _+ \)