Using partial functions to prove correctness
If I read you correctly, the intuition you have in mind goes like this:

Suppose we have a program $P$, which takes a function as an argument. Further suppose that we have two functions $f$ and $g$, such that $f$ terminates on a subset of the inputs $g$ terminates on, but agrees with $g$ whenever they both terminate.

Now, if $P\;g$ is partially correct, then you want to argue that $P\;f$ must also be partially correct. After all, the "only thing" that $P$ can do with its functional parameter is to apply it (what you call "use as an oracle"), and so $P\;f$ must compute the same values as $P\;g$, possibly terminating less often. 

This is more or less exactly the intuition underlying domain theory. The idea is that we can interpret computations at a particular type as CPPOs, or chain-complete pointed partial orders. 

That is, a CPPO is a triple $(X, \bot, \leq)$, with $X$ as the set of elements denoting computations, $\bot$ as the nonterminating computation, and $\leq$ as a partial order representing how close to fully defined a computation is. $\bot$ is the least element in this partial order, and the chain-completeness condition says that if you have a countable chain $x_0 \leq x_1 \leq \ldots$, then the chain has a least upper bound $\bigsqcup_{i \in \mathbb{N}} x_i$. 

Programs are interpreted by continuous functions between CPPOs, with the idea that continuity is a stand-in for computability. That is, a function $f : X \to Y$ should be a monotone function which preserves lubs.

In particular, the set of continuous functions $X \to Y$ also forms a CPPO, with the least element given by $\lambda x.\;\bot_Y$, and the order given pointwise, so that 

$$f \leq_{X \to Y} g \iff \forall x \in X.\; f\;x \leq_Y g\;x$$

Then the property you want follows more or less instantaneously. Suppose we have a continuous $P : (X \to Y) \to Z$. Then $f$ being "less defined" than $g$ amounts to saying that $f \leq g$. Then, by the continuity of $P$, it follows that $P\;f \leq P\;g$. 

Samson Abramsky and Achim Jung have a chapter on domain theory in the Handbook on Logic in Computer Science, which is freely available online.