伊莎貝爾的習慣性微積分證明

我在嘗試使用一些簡單的實際分析問題來學習伊莎貝爾。以下是我的一個證明。它檢查直到最後。伊莎貝爾的習慣性微積分證明

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

我有幾個問題：

如何完成證明嗎？它在我看來，我可以申請c5來證明最後的，但我試過的自動，簡單等各種組合似乎並沒有這樣做。
這個證明的更多isabelle-idomatic版本是什麼？我期望使用has_vector_derivative而不是has_derivative會更簡單，但我更感興趣的是用has_derivative來保持它，但重組。 Isabelle文檔中給出的例子似乎在這些陳述之間做出了更大的步驟，在這裏有沒有辦法做到這一點？
我發現我需要在這裏使用derivative_eq_intros。是否有另外一個fastforce簡介：衍生_eq_intros行會更快？現在需要幾秒鐘。
一般來說，對於這種涉及向量和演算的證明，是否還有其他規則集，比如我應該知道的derivative_eq_intros？什麼是默認使用real_inner數量與simp？我可以在這裏應用代數方法嗎？
大錘在這個證明中是無用的，我是否需要傳遞一些參數或一組定理，以便它有機會證明這裏的一些步驟？

來源

2016-11-02 AaronDefazio

您仍然需要從衍生的線性算下拉出t。你可以這樣做linear_cmult[OF c3]。然後展開o_def的功能組合，就完成了。
那裏有幾個不必要的步驟。簡化器可以完成你自己所做的大部分推理。另外，你對f的衍生物的假設很強， f在點x + s(y - x)有衍生物（我們稱之爲D）就足夠了。我在我的回答結束時提出了一個證明。
您可以爲「介紹」添加感嘆號。這告訴fastforce急切地應用規則並且沒有回溯。這應該謹慎使用（特別是對於非等價的介紹規則），因爲它很容易導致無法終止，但衍生產品的規則通常是安全的。這在這裏加快了這個過程。
有tendsto_intros和tendsto_eq_intros的限制，但它們往往比衍生物的等價物的可靠性低很多，因爲通常有幾個限制匹配規則。我在Isabelle中沒有使用過很多矢量空間，所以我不能評論這個。至於algebra，我認爲這與Gröbner的基礎上的戒指，所以我會很驚訝，如果它適用於內部產品。快速測試似乎表明它確實不是。一些規則在簡單集合中，所以簡化器將自動使用它們。其餘的，你將不得不使用find_theorems或研究各自的理論，說什麼屬性已被證明它。
不是。您可以通過using或from將其他事實鏈接起來，但大錘通常很擅長查找相關事實本身。我對此不甚瞭解，不知道爲什麼它在這裏沒有什麼幫助;根據我的經驗，有時它有效，有時不起作用。

現在，這裏的證明：

lemma line_fundamental_theorem_calculus: 
    assumes "(f has_derivative D) (at (x + s*⇩R(y-x))) " 
    shows "((λt. f(x+t*⇩R(y-x))) has_derivative (λt. t *⇩R (D (y-x)))) (at s)" 
proof - 
    let ?z = "(λt. x + t*⇩R(y-x))" and ?dzdt = "λt. t *⇩R (y-x)" 
    have lin: "linear D" using assms has_derivative_linear by auto 
    have "((f ∘ ?z) has_derivative (D ∘ ?dzdt)) (at s) " 
    using assms by (fastforce intro!: derivative_eq_intros) 
    thus ?thesis by (simp add: o_def linear_cmul[OF lin]) 
qed

來源

2016-11-02 07:51:24

只是一個簡短的話來您的進口：只導入「~~/src目錄/ HOL/Multivariate_Analysis」（將只是「~~/src目錄/ HOL /分析「）。當您使用-lHOL-Multivariate_Analysis啓動isabelle/jEdit時，您會獲得最佳結果。

您的第一條導入線導入了其他所有內容，其他線條是不必要的。如果他們意外修改了一些自動化數據庫（例如simp規則，intro/dest/elim規則等），他們可能會成爲問題

來源

2016-11-02 11:18:06 Johannes

附錄：自Isabelle 2016-1以來，Multivariate_Analysis已重命名爲Analysis，因此正確的命令行調用將是'-l HOL-Analysis'。這樣可以創建一次HOL分析堆圖像並將來使用它，這樣，每次啓動Isabelle時都不必重新處理所有理論。 –

伊莎貝爾的習慣性微積分證明

回答

相關問題