> You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones.

I don't see how you can. This is why I posed my question originally. Let me make the question sharper.

Here's some Isabelle code on the very simple function `double` that just doubles a natural number.

  theory Double
    imports Main
  begin
  
  fun double :: "nat => nat" where
    "double 0 = 0"
  | "double (Suc n) = Suc (Suc (double n))"
  
  lemma double_eq_plus: "double x = x + x"
    by (induction x) auto
  
  lemma double_eq_times: "double x = 2 \* x"
    by (induction x) auto
  
  end

How do I even begin to write the formal argument that `double` has asymptotic runtime complexity that is linear in the size of its argument without resorting to `time_f`-style shenanigans?

I don't know how to even state it in Isabelle. Let alone prove it.