I'm looking at a way to prove that one recovers, under ad hoc assumptions, classical mechanics from quantum theory. Usually, we can find in textbooks that the propagator
$$K(x,x_0;t)=\langle x|e^{-i \hat H t/\hbar}|x_0\rangle$$
is given in the classical limit by using the path integral formulation
$$K(x,x_0;t)\propto e^{i S[q_c(t)]}$$
where $S[q]$ is the classical action and $q_c(t)$ is the classical path from $x_0$ to $x$ in a time t (which minimizes $S$).
But this is not very satisfying, as $K$ is a probability amplitude, which is really not what we would like in the classical limit. The least we would like to obtain is that the probability to be in $x$ at time $t$ is given by
$$P_t(x)=\delta(x-q_c(t)) \tag{1}$$
or something equivalent. My naive approach to recover this result would be the following. The propagator is not enough, as the "classicalness" of the motion should be given by the initial state. It seems natural to choose the initial wave-function to be a wave-packet peaked around the initial position (at x=0 from now on) with spread $\Delta x$ and with momentum $p$, for example
$$\psi(x)=\dfrac{e^{-\frac{x^2}{2\Delta x^2}-i p x/\hbar}}{\pi^{1/4}\sqrt{\Delta x}}$$
We would say that the dynamics will be classical at least if $\Delta p\propto \hbar/\Delta x \ll p$. There is maybe other constraints, for instance the the dynamics is classical only at times $t$ long enough, but this is still not clear to me.
Finally, the classical probability is given by (or at least proportional to)
$$P_t(x)=|\int d x_0 K(x,x_0;t) \psi(x_0)|^2\propto |\int d x_0 e^{i S[q_c(t)]} \psi(x_0)|^2. \tag{2}$$
My question is : is there a way to show/prove that under these assumptions, we can get (1) from (2) for any Hamiltonian? I have looked at the simplest case of a free particle, and it seems to work (I still have some issues to get the final result, but my feeling is that it works). If it helps, I could post the calculation later. But a general proof would be great.