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 $