Bằng chứng thành ngữ do mâu thuẫn trong Isabelle?

Question

Cho đến nay tôi đã viết chứng minh bởi sự mâu thuẫn trong phong cách sau đây trong Isabelle (sử dụng một mô hình bằng Jeremy Siek):

lemma "<expression>" 
proof - 
    { 
    assume "¬ <expression>" 
    then have False sorry 
    } 
    then show ?thesis by blast 
qed 

Có cách nào mà làm việc mà không có giấy tờ chứng minh liệu lồng nhau chặn { ... }?

Answer 1

Có sự cai trị ccontr cho bằng chứng cổ điển bởi sự mâu thuẫn:

have "<expression>" 
proof (rule ccontr) 
    assume "¬ <expression>" 
    then show False sorry 
qed 

Nó đôi khi có thể giúp đỡ để sử dụng by contradiction để chứng minh bước cuối cùng.

Ngoài ra còn có các quy tắc classical (mà có vẻ ít trực quan):

have "<expression>" 
proof (rule classical) 
    assume "¬ <expression>" 
    then show "<expression>" sorry 
qed 

Đối với ví dụ hơn nữa sử dụng classical, xem $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

Đối hiểu rõ hơn về quy tắc classical nó có thể được in trong phong cách Isar có cấu trúc như thế này:

print_statement classical 

Đầu ra:

theorem classical: 
    obtains "¬ thesis" 

Do đó, cái ác thuần túy đối với trực giác xuất hiện trực quan hơn một chút: để chứng minh một số luận án tùy ý, chúng ta có thể giả định rằng phủ định của nó.

Các kinh điển mẫu bằng chứng tương ứng là:

notepad 
begin 
    have A 
    proof (rule classical) 
    assume "¬ ?thesis" 
    then show ?thesis sorry 
    qed 
end 

đây ?thesis là luận án cụ thể của tuyên bố trên của A, mà có thể là một tuyên bố tùy tiện phức tạp. Điều này trừu tượng gần như thông qua chữ viết tắt ?thesis là điển hình cho thành ngữ Isar, để nhấn mạnh cấu trúc của lý luận.