"Illegal schematic variable(s)" 在证明生成的代码中（案例规则：...）`

Question

我为 case_option 定义了一个案例规则，希望能使一些证明更具可读性。但是，当将它与 proof (cases rule: ...) 一起应用并使用 proof 语句建议的代码片段时， Isar case 语法告诉我 Illegal schematic variable(s) in case ...，即使该规则在其他情况下也有效。

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

有办法解决这个问题吗？

Answer 1

正如 Javier 指出的那样，解决方案是 实例化变量 （似乎只需要 x）。
但是，cases 已经内置了这个：

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

请注意，生成的代码仍然失败，因为 ?thesis 与应用 cases 后的新目标不匹配。相反，必须明确说明目标。

更好（虽然不太直观），使用 induction 代替 cases 自动实例化相关变量，额外的好处是提供正确的目标为 ?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

"Illegal schematic variable(s)" 在证明生成的代码中（案例规则：...）`

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

isabelle

isar