"Illegal schematic variable(s)" in code generated by proof (cases rule: ...)`

Question

I defined a cases rule for case_option in the hope of making some proofs more readable. However, when applying it with proof (cases rule: ...) and using the code snippet suggested by the proof statement, the Isar case syntax tells me Illegal schematic variable(s) in case ..., even though the rule works in other cases.

lemma case_option_cases[case_names None Some]: (* removing the "case_names" tag does not solve the issue *)
  assumes "x = None ==> P a"
    and "!!y. x = Some y ==> P (b y)"
  shows "P (case x of None => a | Some y => b y)"
  using assms unfolding option.split_sel by blast

notepad
begin

  fix P :: "'y => bool" and x :: "'x option" and a :: "'y" and b :: "'x => 'y"

  (* sanity check *)
  assume "x = None ==> P a" and "!!y. x = Some y ==> P (b y)"
  then have "P (case x of None => a | Some y => b y)"
    by (cases rule: case_option_cases) (* also works just "by (rule ...)" *)

  have "P (case x of None => a | Some y => b y)"
  proof (cases rule: case_option_cases) (* this line generates and suggests the following structure *)
    case None (* Illegal schematic variable(s) in case "None" *)
    then show ?thesis sorry
  next
    case (Some y) (* same here *)
    then show ?thesis sorry
  qed

end

Is there a way to fix this?

Answer 1

As Javier points out, the solution is to instantiate the variables (only x seems to be required).
However, cases has this already built in:

proof (cases x rule: case_option_cases)
(* generates the following template *)
  case None
  then show ?thesis (* replace by "P a" *) sorry
next
  case (Some y)
  then show ?thesis (* replace by "P (b y)" *) sorry
qed

Note that the generated code still fails as ?thesis does not match the new goals after applying cases. Instead, the goals have to be stated explicitly.

---

Even better (although less intuitive), using induction in place of cases automatically instantiates the relevant variables, with the added bonus of providing the correct goals as ?case:

proof (induction rule: case_option_cases)
(* generates the following template *)
  case None
  then show ?case sorry
next
  case (Some y)
  then show ?case sorry
qed