How can I bind the schematic variable ?case in a rule for proof by cases?

Question

I would like to define a rule for proof by cases, to be used with proof (cases rule: <rule-name>). I managed to use the case_names and consumes parameters, but I did not manage to bind the schematic variable ?case, so that, inside a case of a proof using my rule, one can write show ?case .... How do I bind it?

Concretely: I have the Mizar-inspired notion of a trivial set, i.e. empty or singleton set. I would like to prove properties of trivial sets by empty vs. singleton case analysis. So far I have:

definition trivial where "trivial x = (x ⊆ {the_elem x})"

lemma trivial_cases [case_names empty singleton, consumes 1]:
  assumes "trivial X"
  assumes empty: "P {}"
      and singleton: "⋀ x . X = {x} ⟹ P {x}"
  shows "P X"
using assms unfolding trivial_def by (metis subset_singletonD)

and I can make use of this as follows:

notepad
begin
  fix Q
  fix X::"'a set"
  have "trivial X" sorry
  then have "Q X"
  proof (cases rule: trivial_cases)
    case empty
    show "Q {}" sorry
  next
    case (singleton x)
    show "Q {x}" sorry
  qed
end

But I cannot use show ?case. If I try, it gives me the error message "Unbound schematic variable: ?case". print_cases inside the proof outputs the following:

cases:
  empty:
    let "?case" = "?P {}"
  singleton:
    fix x_
    let "?case" = "?P {x_}"
    assume "X = {x_}"

Which suggests that it doesn't work because ?P is not bound to trivial.

BTW: The full context in which I am using this can be seen at https://github.com/formare/auctions/blob/master/isabelle/Auction/SetUtils.thy.

Answer 1

As Joachim already mentioned, unlike induct, the cases method does not bind the schematic variable ?case. I would say the "canonical" way of conducting case analysis (as a proof method) conforms to this setup, since typically only different assumptions -- which taken together are exhaustive -- are considered, whereas the conclusion stays the same (abbreviated by ?thesis in Isabelle) throughout the different cases. I would set up your trivial_cases as follows:

lemma trivial_cases [consumes 1, case_names empty singleton]:
  assumes "trivial X" and "X = {} ⟹ P" and "⋀x . X = {x} ⟹ P"
  shows "P"
  using assms by (auto simp: trivial_def)

Then you can use it like

notepad
begin
  fix P and X :: "'a set"
  have "trivial X" sorry
  then have "P X"
  proof (cases rule: trivial_cases)
    case empty
    then show ?thesis sorry
  next
    case (singleton x)
    then show ?thesis sorry
  qed
end

where the simplifier or explicit unfolding takes care of specializing X to {} and {x}, respectively.

Side Note: You can further tune trivial_cases by adding the attribtue cases pred: trivial. Then, whenever trivial ?X is the major assumption fed to cases, the rule trivial_cases is used implicitly, i.e., you can do the following

have "trivial X" sorry
then have "P X"
proof (cases)

in the above proof.