Stream: Beginner Questions

Topic: subcases in cases

view this post on Zulip Salvatore Francesco Rossetta (Mar 26 2024 at 09:22):

Hi, if I have this lemma

lemma l1:
  shows "func4 a b c = 4"
proof(cases "a = b")
  case True
  then show ?thesis
  proof(cases "b = c")
    case True
    have "b = c" using True by simp
    have "a = b" by ???
    then show ?thesis sorry
  next
   [...]

In the subcase b = c, how can I use the major case a = b?

view this post on Zulip Lukas Stevens (Mar 26 2024 at 10:41):

There are different options. You can quote the fact literally with ‹a = b› or you can rename one of the cases like this case a_eq_b: True.

Last updated: Dec 21 2024 at 16:20 UTC