theory IntDiv_ZF_IML imports Int_ZF_1 IntDiv_ZF
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 prems , Int_ZF_1_L2 , raw_zmod_zdiv_equalityIf \(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 \ \$ < 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 prems , zdiv_zmult_self1 , zdiv_zmult_self2 , Int_ZF_1_L8 , Int_ZF_1_L2The 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 \ \$ \times 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 \ \$ < 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 \ \$ < 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:
\( PositiveSet(G,P,r) \equiv \)
\( \{x\in G.\ \langle TheNeutralElement(G,P),x\rangle \in r \wedge 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 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} _+ \)
