表達的功能是一組常數

我想表達的是一個功能f是一組S不變，價值r我的第一個想法是表達的功能是一組常數

f ` S = {r}

但是，這並不工作，因爲S可以是空的。所以我目前正在與

f ` S ⊆ {r}

它的工作原理okish，但我覺得這仍然不是理想的標準自動化。特別是，auto將無法離開這個目標（不相關的事實擦除）

2. ⋀xa. thunks (delete x Γ) ⊆ thunks Γ ⟹ 
     ae ` thunks Γ ⊆ {up⋅0} ⟹ 
     xa ∈ thunks (delete x Γ) ⟹ 
     ae xa = up⋅0

大錘當然也沒有問題（metis image_eqI singletonD subsetCE），但也有這樣一些事件。（一般來說，⊆似乎與我預期的auto一樣好）。

有沒有更好的方式來表達這一點，即當假設發生時可以更容易地使用auto？

來源

2014-09-30 Joachim Breitner

使用'！ X。至少在'自動'的限制被強調的情況下，x∈S⟹fx = r似乎工作得不合適，並且比'∀x∈S. fx = r'更好... – 2014-09-30 10:17:45

我沒試過，因爲我沒有任何方便的例子。但是你可以嘗試下面的設置。

definition "const f S r ≡ ∀x ∈ S. f x = r"

即相當於自己的定義：

lemma 
    "const f S r ⟷ f ` S ⊆ {r}" 
    by (auto simp: const_def)

然後採用下列SIMP規則：

lemma [simp]: 
    "const f S r ⟹ x ∈ S ⟹ f x = r" 
    by (simp add: const_def)

來源

2014-09-30 10:25:50 chris

@JoachimBreitner哦，對不起，你只是在評論中寫了類似的東西（在我開始輸入我的答案之後）;） – chris 2014-09-30 10:26:54

這不是相似的;你引入一個新的名字並依靠簡化器來建立連接。如果簡單的兩個假設都是可用的，它可能會工作得很好，但它仍然可能比直接使用元蘊涵更弱，可以用'auto'來「嘗試」。 – 2014-09-30 10:33:23

你也可以使用[簡單]作爲破壞規則與自動。如果所有的用例都只需要實例來求解結論中的等式，那麼也可以使用相似的規則：const f S r ==> x：S ==> r = r'==> fx = r'消除規則。我的感覺是，具有正確的intro/elim/dest規則的獨立常量比帶有'image'的解決方案更好，因爲'image'需要幾個推理步驟，您可以將它們合併爲一個獨立的常量。 – 2014-09-30 14:41:36

表達的功能是一組常數

回答

相關問題