จะใช้ไวยากรณ์“ THE” ใน Isabelle / HOL ได้อย่างไร?

Question

ฉันกำลังพยายามเรียนรู้วิธีใช้THEไวยากรณ์ใน Isabelle / 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" การคาดเดาที่ดีที่สุดของฉันคือ "x (อาจจะไม่ซ้ำกัน) x ที่ตอบสนองคุณสมบัติ P" ดังนั้นฉันจึงพยายามระบุคำศัพท์ของเล่นดังนี้:

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

ซึ่งหมายความว่า x ที่เป็นทั้ง ge และ le 0 คือ 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 (resp. THE) คือ (ตัวแปรของ) ตัวดำเนินการ epsilon ของ Hilbert ที่ส่งคืนองค์ประกอบ (the) ที่เคารพคุณสมบัติบางอย่าง หากไม่มี (ไม่มีหรือมากกว่าหนึ่ง) องค์ประกอบที่ไม่ระบุจะถูกส่งกลับ

บางส่วนและบางส่วนไม่สามารถใช้งานได้ ไม่ค่อยมีประโยชน์สำหรับผู้เริ่มต้น