Transformation of one system of ODE's into another Can someone please tell me how one can (rigorously)  transform the system $\begin{cases}
y & =\dot{x}\\
\dot{y} & =-x
\end{cases}$ of ODE's to the system $\begin{cases}
y & =\dot{x}\\
y' & =-\frac{x}{y}
\end{cases}$ (where $y,x:I\rightarrow\mathbb{R}$)  ?
The motivation behind this is that the first system arises by reducing the second order ODE $\ddot{x}+x=0$ to the first of the above two systems.
In class we then did the transformation $-x=\frac{dy}{dt}=\frac{dy}{dx}\cdot\frac{dx}{dt}=y'\cdot y$ to get to the second system, but I don't know what this means, since all the manipulations with the $d$'s are just mnemonics and not real/rigorous math. My professor, when asked, muttered something about using the implicit function theorem to do that transformation rigorously, but I couldn't follow him (I suspect that the two $y$'s don't represent the same function). Could you maybe explain what he meant with that ?
Please bare with me, that I'm just at the beginning of a differential equations course.
 A: To do what you want to show, you need an implicit assumption (no pun intended) that you are working in a neighbourhood of values for $(x,y,t)$ such that $x = f(t)$ is invertible. Locally doing the inversion we can write $t = f^{-1}(x)$ and rewrite $y = y(t) = y\circ f^{-1}(x) =: y(x)$. From which we can do the usual chain rule that $\frac{d}{dx} y = \frac{d}{dt}y \cdot \frac{d}{dx}f^{-1}$. Now using that the derivative of the "inverse function" (at points where the function is locally invertible) is equal to the inverse of the derivative, that is -- if $x = f(t)$, then $\frac{1}{\frac{d}{dt} f(t)} = \frac{d}{dx} f^{-1} (x)$ -- we can write
$$ \frac{d}{dx}y = \frac{\dot{y}}{\dot{x}} = \frac{\dot{y}}{y} $$
It is worth emphasizing that this only works in a neighbourhood where $x$, as a function of $t$, is invertible; and a sufficiently condition to guarantee that this is possible, via the inverse/implicit function theorem is that $\dot{x} \neq 0$ at the point. To see what can go on when $x$ is not invertible as a function of $t$: consider the system
$$ y = \dot{x} + t \qquad \dot{y} = 1-x $$
A solution to the system is $y = t$ and $x = 0$. The same formal change of variable as above would give
$$ y' = (1-x) / (y - t) $$
from which we won't be able to derive the solution shown above. 

To address your "suspicion": you are partially correct in saying that the two $y$s aren't the same function. The main idea behind this transformation is that the original system is written with two dependent variables $(x,y)$ and one independent variable $t$. Together this means that (the graph of) your solution is expected to be a one-dimensional curve inside the three dimensional space $(x,y,t)$. 
Now, think back to your course in algebra-precalculus: a one-dimensional curve is the graph of a function over a chosen independent variable if it passes the "vertical line/plane test". What's happening in the construction you described is that in writing the equation $y' = x / y$, you've changed from using $t$ as the independent variable, to describing the solution curve $(x,y,t)$ using $x$ as the independent variable. This is allowed when the curve in $(x,y,t)$ passes the "vertical line test" with respect to $x$ being the independent variable. For this to hold true locally, this is equivalent to saying that the relation between $x$ and $t$ is invertible locally. 
So whether two "$y$" represent the same function depends a bit on what you take as a function. If you consider the function as its graph as a curve in $(x,y,t)$ space, then the two $y$s should represent the same function, whenever, the $x$-$t$ inversion can be done. On the other hand, if you think of a function as the relation that sends a value in the domain to a value in the range, then the description of $y$ as a function of the independent variable $t$ is different from the description of $y$ as a function of the independent variable $x$. 
