Isabelle / HOL에서 "THE"구문을 사용하는 방법은 무엇입니까?

Question

THEIsabelle / HOL (2020)에서 구문 을 사용하는 방법을 배우려고합니다 . 튜토리얼 main.pdf에는 다음이 있습니다.

The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.

나는 다른 것들이 무엇을 의미하는지 이해할 수 있지만 마지막 "THE x. P"는 아닙니다. 내 추측으로는 "속성 P를 충족하는 (아마도 고유 한) x"입니다. 그래서 다음과 같이 장난감 기본형을 말하려고했습니다.

lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"

즉, ge와 le 0 인 x는 0입니다.

하지만 Isabelle / jEdit에서 "THE"단어가 강조 표시된 오류가 발생합니다.

키워드 Isabelle 및 "THE"로 검색을 시도했지만 "THE"라는 단어는 검색 엔진에서 무시됩니다. 따라서 여기에 질문이 있습니다.

누군가가 "THE"구문의 의미와 사용을 설명하는 데 도움을 줄 수 있습니까?

Answer 1

괄호가 더 필요합니다.

lemma "0 = (THE x::nat. (x ≥ 0 ∧ x ≤ 0))"
  (*the proof*)
  using theI[of ‹λx::nat. (x ≥ 0 ∧ x ≤ 0)› 0]
  by auto

SOME (각각 THE)은 특정 속성을 존중하는 (the) 요소를 반환하는 Hilbert의 엡실론 연산자 (의 변형)입니다. 없는 경우 (하나 이상) 지정되지 않은 요소가 반환됩니다.

SOME 및 THE는 실행 가능하지 않습니다. 초보자에게는 거의 유용하지 않습니다.