Isabelle / HOL'da “THE” sözdizimi nasıl kullanılır?

Question

THEIsabelle / HOL (2020) ' de sözdizimini nasıl kullanacağımı öğrenmeye çalışıyorum . Eğitici main.pdf'de şunlar bulunur:

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

Diğerlerinin ne anlama geldiğini anlayabiliyorum ama sonuncusu "THE x. P" yi anlayamıyorum. En iyi tahminim "P özelliğini karşılayan (belki benzersiz) x" dir. Bu yüzden bir oyuncak lemmayı şu şekilde ifade etmeye çalıştım:

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

bu, hem ge hem de le 0 olan x'in 0 olduğu anlamına gelir.

Ama Isabelle / jEdit'te "THE" kelimesinin vurgulandığı bir hata alıyorum.

Isabelle ve "THE" anahtar kelimeleriyle aramaya çalıştım, ama açıkça "THE" kelimesi arama motorları tarafından görmezden geliniyor. Dolayısıyla soru burada.

Birisi "THE" sözdiziminin anlamını ve kullanımını açıklamaya yardımcı olabilir mi, umarım buradaki örnekle?

Answer 1

Daha fazla paranteze ihtiyacınız var.

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

SOME (veya THE), belirli bir özelliğe saygı duyan bir (the) elementi döndüren Hilbert'in epsilon operatörünün bir çeşididir. Hiçbiri (hiç veya birden fazla) yoksa, yetersiz belirtilmiş bir öğe döndürülür.

SOME ve THE çalıştırılabilir değildir. Yeni başlayanlar için nadiren faydalıdırlar.