伊莎貝爾/ HOL使用加法/減法關聯

Question

我想證明的形式

lemma assoc: "b + (c - d) = (b + c) - d" 

AFAIK關聯性定理是圖書館的一部分，但並未標註簡化的東西，所以我需要給手動添加它們。他們在什麼地方定義了哪些合適的名稱？哪些是theory？

Answer 1

這樣的目標通常用定理集合algebra_simps來解決。只需寫by (simp add: algebra_simps)。

請注意，您說明定理的方式，您將無法證明它，因爲您沒有指定b，c和d是組的元素。你需要寫類似

lemma assoc: "(b :: 'a :: group_add) + (c - d) = (b + c) - d" 

或

lemma assoc: 
    fixes b c d :: "'a :: group_add" 
    shows "b + (c - d) = (b + c) - d" 

或更多的東西特別，像nat或int，而不是'a :: group_add。

事實上，當你這樣做時，IDE會通知你，已經有這樣的引理：Groups.group_add_class.add_diff_eq

thm add_diff_eq 
> ?a + (?b - ?c) = ?a + ?b - ?c