\ <setminus> Isabelle語法

Question

我只是無法找到從集合中刪除一個術語的語法。

我有以下幾點：

typedecl STUDENT 

definition LeaveHall :: 
"STUDENT set => STUDENT set => STUDENT set => STUDENT set => STUDENT => 
bool" 
where 
"LeaveHall badminton' badminton hall' hall leaver == 
(
(leaver \<in> hall) \<and> (hall' = hall \<setminus> {(leaver)}) 
<and> 
(badminton' = badminton) 
)" 

它不喜歡我的表達 「（廳」 =廳\ {（離校生）}） 」

我想說的是什麼設置大廳'是設置大廳減去離開這個詞。 但它只是不喜歡它。我試着把括號和東西，它 仍然無法正常工作。

Answer 1

儘管∖符號以名稱\<setminus>存在於伊莎貝爾，但目前尚未使用。爲差集的正確的語法是很簡單-，所以此工程：

definition LeaveHall :: "STUDENT set ⇒ STUDENT set ⇒ STUDENT set ⇒ STUDENT set ⇒ STUDENT ⇒ bool" 
    where "LeaveHall badminton' badminton hall' hall leaver ⟷ 
      leaver ∈ hall ∧ hall' = hall - {leaver} ∧ badminton' = badminton" 

如果你想使用\<setminus>，就可以了，當然，定義的縮寫與語法：

abbreviation setminus (infixl "∖" 65) where "setminus ≡ op -" 

或者

abbreviation (input) setminus (infixl "∖" 65) where "setminus ≡ op -" 

在一個不相關的注意事項：，只允許這個輸入條件，但不打印條件時使用它由多個單詞標識符（典型值）在伊莎貝爾書寫下劃線，而不是駱駝案。當然，你可以隨意調用你的標識符，但是約定是使用下劃線而不是駱駝案例。

另外請注意，我用⟷在LeaveHall上面的定義，而不是平等元≡（像你一樣）或常規平等=。不鼓勵在定義中使用元相等運算符≡（儘管它沒有真正的缺點）。

布爾等價運算符⟷僅僅是布爾平等上的縮寫（因此它與編寫=完全相同）。那爲什麼要用⟷？因爲它的優先級低於=，這意味着您通常需要較少的括號：P a = Q a ∧ R a被解析爲(P a = Q a) ∧ R a，而P a ⟷ Q a ∧ R a被解析爲P a = (Q a ∧ R a)。