How does one formally define sampling from a probability distribution? Every introduction to probability that I have seen describes sampling from a distribution based on an intuitive notion of a fair coin flip.

I have never seen "fair coin flip" formally defined. Is the definition implied by the axioms of probability theory?

Is probability theory predicated on some notion of an atomic coin flip operation that is not further formalized?
Probability is formalized in terms of measure theory. One usually talks about a probability space $(\Omega, \mathcal{F}, P)$. Here $\Omega$ is the set of all "outcomes," $\mathcal{F}$ is the set of all "events," and $P:\mathcal{F} \to [0,1]$ is a probability measure, i.e., given an event $E \in \mathcal{F}$, $P(E)$ is the probability of $E$. These satisfy all sorts of axioms which I won't get into. It's good to have a running example, so let's say $\Omega$ is the set of possible outcomes when a red and a green die are rolled, so
$$\Omega = \{(1,1),(1,2),\dots,(6,6)\}.$$

Now a random variable is defined as a function $X:\Omega \to \mathbb{R}$. For instance, $X$ might be the sum of the red and the green dice. Thus $X(a,b) = a+b$. Usually we do not use function notation for $X$ because we are not concerned with the particular value $X(a,b)$, but rather the many values that $X$ could take on, and the distribution of those values. $X$ induces a probability measure on $\mathbb{R}$, namely if $A \subseteq \mathbb{R}$ then the measure of $A$ is $\mu(A) = P(X \in A)$. 

This measure and the distribution of $X$ are completely captured by the distribution function $F(x)=P(X \leq x)$. In our example, $F(x)$ will be a step function. In general, distribution functions are nondecreasing, right-continuous, and have $\lim_{x \to -\infty}F(x)=0$ and $\lim_{x \to \infty}F(x)=1$. Moreover, every function with those properties is a distribution function. 

I have just described how to go from a random variable to its distribution function, but we can go the other way. Namely, given a distribution, we can sample a random variable from it, by which we mean we choose a probability space $(\Omega,\mathcal{F},P)$ and a function $X:\Omega \to \mathbb{R}$ satisfying $P(X \leq x) = F(x)$ for all $x \in \mathbb{R}$. It is not obvious that such a random variable must exist! But in fact one does provided you have a valid distribution function.
In probability parlance, it means you are analyzing independent, identically distributed random variables with a given distribution.  

However, when you get into the realm of statistics, the whole business of designing sampling schemes becomes a high and complex art.  In the real world, the assumption that observations are independent (or identically distributed) can be a muddy one.