Saya tahu bahwa Isabelle dapat melakukan analisis kasus oleh konstruktor (mis. Dari daftar), tetapi

Apakah ada cara untuk membagi dalam kasus berdasarkan apakah suatu kondisi benar atau salah?

Misalnya, dalam membuktikan lemma berikut, logika saya (seperti yang ditunjukkan oleh bukti tidak valid berikut dalam sintaksis yang tidak valid), adalah bahwa jika kondisinya "x ∈ a" benar, bukti menyederhanakan sesuatu yang sepele; Ini juga menyederhanakan ketika kondisinya salah (mis. "x ∉ A"):

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (case "x ∈ A")
  (* ... case true *)
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  have "x ∈ B ∧ x ∈ C" by simp
  show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)

Tetapi saya tidak tahu bagaimana menerjemahkan "analisis kasus" ini dalam bahasa Inggris ke Isabelle.

Apakah ada cara di Isabelle / Holl untuk mengekspresikan analisis kasus semacam ini dengan benar atau salah suatu kondisi? (pada Isabelle 2021)

(Atau apakah itu membutuhkan aksioma tambahan seperti hukum menengah yang dikecualikan?)

0
tinlyx 4 April 2021, 18:24

1 menjawab

Jawaban Terbaik

Anda telah hampir menebak sintaks, Anda dapat menulis bukti dengan kasus untuk predikat apa pun dengan sintaks proof (cases "<pred>").

Untuk contoh Anda berikan:

lemma "(x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) ⟹ x ∈ A ∨ (x ∈ B ∧ x ∈ C)"
proof (cases "x ∈ A")
  (* ... case true *)
  case True
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI1)
next (* ... case false *)
  case False
  then have "x ∈ B ∧ x ∈ C" sorry (* by simp*)
  then show "x ∈ A ∨ (x ∈ B ∧ x ∈ C)" by (rule disjI2)
3
braewebb 5 April 2021, 03:56