Applying a particular rule to a held (or unevaluated) function

Question

I am a very novice Mathematica user and still can't get my head around its evaluation control, all possible constructs related to it (e.g. Hold, Unevaluated, etc.) and how they work, despite the thorough documentation and the numerous StackExchange and StackOverflow questions discussing this topic. So, apologies for any possible duplicates.

My use case is the following: I have a function (say f) defined by thousands of rules and patterns (DownValues). I want to start from an unrolled representation of f[expr] (for some expr) and get the result of applying a single, particular rule to f[expr]. I want the result to stay unrolled as well.

As a particular example, suppose we have the following:

 In[1]: nat[0] := 0
 In[2]: nat[n_] := 1 + nat[n - 1]
 In[3]: DownValues[nat]
Out[3]: {HoldPattern[nat[0]] :> 0, HoldPattern[nat[n_]] :> 1 + nat[n - 1]}
 In[4]: nat[10]
Out[4]: 10

Now, I want to start from an expression represented as nat[10] (unevaluated!) and want to specifically apply the second rule (HoldPattern[nat[n_]] :> 1 + nat[n - 1]) to obtain the expression in the form of 1 + nat[9]. Analogously, shall I wish to apply the first rule (HoldPattern[nat[0]] :> 0), I would expect the result to stay unchanged in its original form, i.e. nat[10].

Thank you for your help!

Answer 1

Consider applying specific rules instead of defining your function.

ClearAll[nat];
rule1=nat[0]:>0;
rule2=nat[n_]:>1+nat[n-1];
(* The :> will change into a single character as you type. *)

Then apply use Replace (/.) with the rule you want to use like this.

nat[10]/.rule2
(* 1+nat[9] *)

You can do the following to see what happens after applying the rule several times.

useRule2[expr_]:=expr/.rule2;
Nest[useRule2,nat[10],4]
(* 4+nat[6] *)

However, experienced used do that as follows instead.

Nest[#/.rule2&,nat[10],4]
(* 4+nat[6] *)

to learn how to use #& read about Function at http://www.verbeia.com/mathematica/tips/HTMLLinks/Tricks_A-K_34.html and https://reference.wolfram.com/language/ref/Function.html?q=Function

Answer 2

Inspired by Ted Ersek's answer, I figured that the following steps work for me so far without having to explicitly convert and rewrite nat's preexisting definitions (as I am working with third-party code where the function of interest is defined by literally thousands of rules).

 In[6] rules = DownValues[nat]                                                 
Out[6] {HoldPattern[nat[0]] :> 0, HoldPattern[nat[n_]] :> 1 + nat[n - 1]}

 In[7] DownValues[nat] = {}                                                    
Out[7] {}

 In[8] nat[10]                                                                 
Out[8] nat[10]

 In[9] nat[10] /. rules[[1]]                                                   
Out[9] nat[10]

 In[10] nat[10] /. rules[[2]]                                                  
Out[10] 1 + nat[9]