How to prove by case analysis on a logical condition being either true or false in Isabelle/HOL?

1
votes

I know that Isabelle can do case analysis by constructors (e.g. of a list), but

Is there a way to split into cases based on whether a condition is true or false?

For example, in proving the following lemma, my logic (as indicated by the following invalid proof in invalid syntax), is that if the condition "x ∈ A" is true, the proof simplifies to something trivial; it also simplifies when the condition is false (i.e. "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)

But I don't know how to translate this "case analysis" in English into Isabelle.

Is there way in Isabelle/HOL to express this kind of case analysis by the true or false of a condition? (as of Isabelle 2021)

(Or does it require additional axioms such as the law of excluded middle?)

1
isabelle
Please note that very similar questions have been asked before: for example, see stackoverflow.com/questions/13751358/case-analysis-in-isabelle and stackoverflow.com/questions/60683091/…. I will not mark this question as a duplicate, as it adds more details and an explicit example. Nonetheless, you are encouraged to look through the previous Q&A thoroughly before posting a new question. – user9716869
@user9716869 Thanks. I've actually read the first post, and it was about cases on list constructors (as said in my question). What I asked here is about a logical condition. I'm not sure about the second one. It seems to be about function definitions. I'll read more about it. – tinlyx

1 Answers

4
votes

You've almost correctly guessed the syntax, you can write a proof by cases for any predicate with the syntax proof (cases "<pred>").

For the example you provided:

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)