Làm thế nào để sử dụng cú pháp "THE" trong Isabelle / HOL?

Jan 12 2021

Tôi đang cố gắng học cách sử dụng THEcú pháp trong Isabelle / HOL (2020). Trong hướng dẫn main.pdf, có:

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

Tôi có thể hiểu ý của những người khác, nhưng không phải câu cuối cùng là "THE x. P". Dự đoán tốt nhất của tôi là "(có thể là duy nhất) x thỏa mãn tính chất P". Vì vậy, tôi đã cố gắng phát biểu một bổ đề đồ chơi như sau:

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

, có nghĩa là x là cả ge và le 0 đều là 0.

Nhưng tôi gặp lỗi trong Isabelle / jEdit với phần đánh dấu trên từ "THE".

Tôi đã cố gắng tìm kiếm với các từ khóa Isabelle và "THE", nhưng rõ ràng từ "THE" bị các công cụ tìm kiếm bỏ qua. Do đó câu hỏi ở đây.

Ai đó có thể giúp giải thích ý nghĩa và cách sử dụng cú pháp "THE", hy vọng với ví dụ ở đây?

Trả lời

3 MathiasFleury Jan 12 2021 at 13:09

Bạn cần thêm dấu ngoặc đơn.

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

SOME (tương ứng với THE) là (một biến thể của) toán tử epsilon của Hilbert trả về một (the) phần tử tôn trọng một thuộc tính nhất định. Nếu không có (không có hoặc nhiều hơn một) tồn tại, một phần tử không xác định được trả về.

SOME và THE không thực thi được. Chúng hiếm khi hữu ích cho người mới bắt đầu.