Let $T = \text{Th}(\mathbb{Z}, s)$ where $s$ is the successor function. I want to show quantifier elimination (QE) for $T$ and construct a concrete $\omega$-saturated model. However, I am unsure whether my approach to such problems is correct/efficient and with the right level of detail.
My idea: we use that $T$ has QE iff every local isomorphism (with finite domain) from a model of $T$ to an $\omega$-saturated model of $T$ can be extended with a single element. To extend the local isomorphism $f : \{m_1, \dots, m_k\} \subset M \to N$ with $m \in M$, it suffices to find $f(m) \in N$ such that the $\text{dist}(m_i, m) = \text{dist}(f(m_i), f(m))$ for all $i \in \{1, \dots, k\}$. Here $\text{dist}(a, b)$ is defined as the number of +1 steps between $a$ and $b$, which is possibly infinite. Two observations:
Finite distances are easily matched because every model of $T$ locally looks like $\mathbb{Z}$.
$\omega$-saturated models of $T$ have an infinite subset of elements at infinite distance from each other. Therefore, as only finitely many elements are considered, infinite distances can also be matched.
This established QE for $T$. Using QE we immediately see that the model of countable many copies of $\mathbb{Z}$ is $\omega$-saturated.
I have the same question for the theory $T = \text{Th}(\mathbb{Z}, <, s)$, but its analysis appears to me identical.
Your argument looks correct to me. In the case of $\text{Th}(\mathbb{Z},<,s)$, Case 2 is a bit more complicated, since "infinite distance" isn't enough. You also need to ensure that the order relation is preserved. So you need to argue that in an $\omega$-saturated model, the set of $\mathbb{Z}$-chains is ordered like a dense linear order without endpoints.