theory Test imports Main begin

consts precond1 :: bool
consts precond2 :: bool
consts case1 :: bool
consts case2 :: bool

lemma case_rule[consumes 2, case_names case1 case2]:
  assumes "precond1"
  assumes "precond2"
  assumes "case1 \<Longrightarrow> Q"
  assumes "case2 \<Longrightarrow> Q"
  shows "Q"
  sorry

lemma
  assumes "precond1" and "precond2"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
oops

lemma
  assumes "precond1"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
oops

end