title: Idiomatic calculus proofs in Isabelle
body: <p>I'm trying to learn Isabelle using some simple real analysis problems. Below is my attempt at a proof. It checks up until the last hence.</p>
  
  <pre><code>theory l2
    imports 
      "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
      "~~/src/HOL/Multivariate_Analysis/Derivative"
      "~~/src/HOL/Multivariate_Analysis/Integration"
      "~~/src/HOL/Complex_Main"
      "~~/src/HOL/Library/Inner_Product"
      "~~/src/HOL/Real_Vector_Spaces"
    begin
  
    thm linear.scaleR
  
    lemma line_fundamental_theorem_calculus:
      fixes x y :: "'a :: real_inner"
      and   s :: "real"
      and   f :: "'a ⇒ real"
      assumes "∀v. (f has_derivative (f' v)) (at v) "
      shows "((λt. f(x+t*⇩R(y-x))) has_derivative (λt. t *⇩R ((f'(x + s*⇩R(y-x))) (y-x)))) (at s)"
    proof -
     let ?z = "(λt. x + t*⇩R(y-x)) :: real ⇒ 'a"
     let ?dzdt = " (λt. t*⇩R(y-x))"
     have c1: "f ∘ ?z = (λt. f(x+t*⇩R(y-x)))" by auto
     have c2: "(f'(x + s*⇩R(y-x))) ∘ (λt. t*⇩R(y-x)) = (λt. (f'(x + s*⇩R(y-x))) (t*⇩R(y-x)))" by auto
     have a1: "(f has_derivative (f' (x + s*⇩R(y-x)))) (at (x + s*⇩R(y-x))) " using assms by auto
     have c3: "linear (f'(x + s*⇩R(y-x)))" using assms has_derivative_linear by auto
     have c5: "(f'(x + s*⇩R(y-x))) (t*⇩R(y-x)) = t *⇩R ((f'(x + s*⇩R(y-x))) (y-x))"  using c3 linear.scaleR by blast
  
     have h1: "(?z has_derivative ?dzdt) (at s)" by (fastforce intro: derivative_eq_intros)
     hence "((f ∘ ?z) has_derivative ((f'(x + s*⇩R(y-x))) ∘ ?dzdt)) (at s) " using assms a1 c1 by (fastforce intro: derivative_eq_intros)
     hence "((f ∘ ?z) has_derivative ((f'(x + s*⇩R(y-x))) ∘ (λt. t*⇩R(y-x)))) (at s) " by auto
     hence "((f ∘ ?z) has_derivative (λt. (f'(x + s*⇩R(y-x))) (t*⇩R(y-x)))) (at s) " by (auto simp: c2)
  
     hence "((f ∘ ?z) has_derivative (λt. t *⇩R ((f'(x + s*⇩R(y-x))) (y-x)))) (at s) " 
     then show ?thesis 
    qed                                               
  
    end
  </code></pre>
  
  <p>I have a few questions:</p>
  
  <ol>
  <li>How do I finish the proof? It looks to me that I can just apply c5 to prove the last hence, but the various combinations of auto, simp etc. that I've tried don't seem to do it.</li>
  <li>What would be a more isabelle-idomatic version of this proof? I expect that it would be simpler with has_vector_derivative instead of has_derivative, but I'm more interested in keeping it with has_derivative, but restructuring. The examples given in the Isabelle documentation seem to make larger steps between the hence statements, is there a way to do that here?</li>
  <li>I've found that I need to use derivative_eq_intros here. Is there an alternative to the fastforce intro: derivative_eq_intros line that would be quicker? It takes a few seconds at the moment.</li>
  <li>In general, for this kind of proof involving vectors and calculus, is there other rule sets like derivative_eq_intros that I should know about? What is it using by default on real_inner quantities with simp? Can I apply the algebra method here?</li>
  <li>Sledgehammer was pretty useless in this proof, do I need to pass in some parameters or sets of theorems so that it has a chance of proving some of the steps here?</li>
  </ol>