如何在Isabelle策略模式中仅对新生成的证明目标应用auto？

我希望让apply auto仅处理上一个apply命令生成的所有证明目标，而非全局所有目标。目前我只会通过将代码包裹在subgoal块中的方式实现，请问有没有更简洁的方法？

正确但繁琐的实现（子目标包裹法） #

lemma bar:
  assumes p: "⋀a b. length a = b ⟹ (a ! 0) > b ⟹ P a"
      and q: "⋀x. x = ([2] @ [3]) ⟹ Q x"
    shows "x = ([2] @ [3]) ⟹ y = [5,6] ⟹ P y ∧ Q x"
  apply (rule conjI)
  subgoal
    apply (rule p)
     apply auto
    done
  apply (erule q)
  done

不使用子目标的失败案例 #

如果直接连续使用apply，auto会处理所有当前目标，包括原本的Q x目标，导致后续erule q无法匹配：

lemma bar:
  assumes p: "⋀a b. length a = b ⟹ (a ! 0) > b ⟹ P a"
      and q: "⋀x. x = ([2] @ [3]) ⟹ Q x"
    shows "x = ([2] @ [3]) ⟹ y = [5,6] ⟹ P y ∧ Q x"
  apply (rule conjI)
   apply (rule p)
    apply auto
(* 此时剩余目标：⟦x = [2, 3]; y = [5, 6]⟧ ⟹ Q [2, 3] *)
  apply (erule q) ― ‹无法工作，因为auto修改了原本的Q x目标›
  done

使用;或,的无效尝试 #

用顺序组合符;会让auto处理rule p生成的子目标后，继续处理所有后续目标；用并行组合符,则等价于连续apply，同样会让auto处理全局目标：

lemma bar':
  assumes p: "⋀ra rb. length ra = rb ⟹ (ra ! 0) > rb ⟹ P ra"
      and q: "⋀x. x = ([2] @ [3]) ⟹ Q x"
    shows "x = ([2] @ [3]) ⟹ y = [5,6] ⟹ P y ∧ Q x"
  apply (rule conjI)
   apply (rule p; auto)
(* 剩余目标：
 1. ⟦x = [2, 3]; y = [5, 6]⟧ ⟹ Suc (Suc 0) < 5
 2. ⟦x = [2] @ [3]; y = [5, 6]⟧ ⟹ Q x
*)
  apply simp ― ‹额外需要simp处理残留目标›
  apply (erule q)
  done

lemma bar'':
  assumes p: "⋀ra rb. length ra = rb ⟹ (ra ! 0) > rb ⟹ P ra"
      and q: "⋀x. x = ([2] @ [3]) ⟹ Q x"
    shows "x = ([2] @ [3]) ⟹ y = [5,6] ⟹ P y ∧ Q x"
  apply (rule conjI)
   apply (rule p, auto)
(* 剩余目标：⟦x = [2, 3]; y = [5, 6]⟧ ⟹ Q [2, 3] *)
  apply (erule q) ― ‹无法工作，auto仍修改了目标›
  done

简洁解决方案：使用目标选择器 #

Isabelle支持通过目标选择器指定方法作用的目标范围，无需嵌套subgoal块。具体来说，在apply auto后加上目标索引范围，限制其仅处理上一步rule p生成的子目标：

lemma bar_simple:
  assumes p: "⋀a b. length a = b ⟹ (a ! 0) > b ⟹ P a"
      and q: "⋀x. x = ([2] @ [3]) ⟹ Q x"
    shows "x = ([2] @ [3]) ⟹ y = [5,6] ⟹ P y ∧ Q x"
  apply (rule conjI)
   apply (rule p)
    apply auto[1-2] ― ‹仅处理第1、2个目标，即rule p生成的子目标›
  apply (erule q)
  done

原理说明 #

• 执行rule conjI后，生成两个目标：P y和Q x
• 执行rule p后，第一个目标被拆分为两个子目标（总共有3个目标）
• auto[1-2]指定auto仅处理前两个目标，第三个Q x目标保持原样，后续erule q可正常匹配

你也可以用单个索引（如auto[1]）处理特定目标，或者用auto[-1]处理最后一个目标，灵活控制方法作用范围。

内容的提问来源于stack exchange，提问作者Mathieu Paturel