专注于艾斯巴赫的新子目标

Question

在 Eisbach 中，我可以使用 ; 将方法应用于方法创建的所有新子目标。但是，我经常知道创建了多少个子目标，并且想对新的子目标应用不同的方法。有没有办法说 "apply method X to the first new subgoal and method Y to the second new subgoal"?

这是一个简单的用例：

我想开发一种适用于 2 个任意长度但具有相同结构的连词的方法。该方法应该可用于通过显示蕴涵对每个组件成立来表明连取 1 蕴含连取 2。它应该可以像这样使用：

lemma example:
  assumes c: "a 0 ∧ a 1 ∧ a 2  ∧ a 3"
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
proof (conj_one_by_one pre: c)
  show "a 0 ⟹ a' 0" by (rule imp)
  show "a 1 ⟹ a' 1" by (rule imp)
  show "a 2 ⟹ a' 2" by (rule imp)
  show "a 3 ⟹ a' 3" by (rule imp)
qed

在艾斯巴赫实现此方法时，使用rule conjI后出现问题。我有两个要递归处理的子目标，但我想对这两种情况使用不同的事实。

我想出了以下解决方法，它对两个子目标使用了人工标记，有点难看：

definition "marker_L x ≡ x"
definition "marker_R x ≡ x"

lemma conjI_marked: 
  assumes "marker_L P" and "marker_R Q"
  shows "P ∧ Q"
  using assms unfolding marker_L_def marker_R_def by simp


method conj_one_by_one uses pre = (
    match pre in 
      p: "?P ∧ ?Q" ⇒ ‹
        (unfold marker_L_def marker_R_def)?, 
        rule conjI_marked;( 
            (match conclusion in "marker_L _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct1])?›)
          | (match conclusion in "marker_R _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct2])?›))›)
    | ((unfold marker_L_def marker_R_def)?, insert pre)

Answer 1

这不是一个完整的答案，但您或许可以从此处陈述的内容中获得一些有用的信息。

In Eisbach I can use ; to apply a method to all new subgoals created by a method. However, I often know how many subgoals are created and would like to apply different methods to the new subgoals. Is there a way to say something like "apply method X to the first new subgoal and method Y to the second new subgoal"?

您可以使用标准战术 RANGE 来定义您自己的可以应用于连续子目标的战术。我在下面提供了一个非常专业且大大简化的用例：

ML‹

fun mytac ctxt thms = thms
  |> map (fn thm => resolve_tac ctxt (single thm))
  |> RANGE

›

lemma 
  assumes A: A and B: B and C: C
  shows "A ∧ B ∧ C"
  apply(intro conjI)
  apply(tactic‹mytac @{context} [@{thm A}, @{thm B}, @{thm C}] 1›)
  done

希望将它扩展到更复杂的用例应该相当容易（同时对子目标索引比我更小心：您可能还需要 SELECT_GOAL 以确保实现安全）。虽然在上面的示例中 mytac 接受定理列表，但应该很容易看出这些定理如何被策略替换，并且通过一些进一步的工作，策略可以包装为高阶方法。

I want to develop a method that works on 2 conjunctions of arbitrary length but with the same structure. The method should be usable to show that conjunction 1 implies conjunction 2 by showing that the implication holds for each component. It should be usable like this:

更新

重新审视这个问题，似乎存在一个更自然的解决方案。解决方案遵循原始答案的大纲，但元蕴涵被替换为 HOL 的对象逻辑蕴涵（'to and fro' 转换可以使用 atomize (full) 和 intro impI 实现）：

lemma arg_imp2: "(a ⟶ b) ⟹ (c ⟶ d) ⟹ ((a ∧ c) ⟶ (b ∧ d))" by auto

lemma example:
  assumes "a 0 ∧ a 1 ∧ a 2 ∧ a 3" 
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
  apply(insert assms(1), atomize (full))
  apply(intro arg_imp2; intro impI; intro imp; assumption)
  done

LEGACY（这是原始答案的一部分，但由于上面建议的更新几乎不相关）

如果这是您唯一想到的应用程序，也许有一个基于以下迭代过程的合理自然的解决方案：

lemma arg_imp2: "(a ⟹ b) ⟹ (c ⟹ d) ⟹ ((a ∧ c) ⟹ (b ∧ d))" by auto

lemma example:
  assumes c: "a 0 ∧ a 1 ∧ a 2 ∧ a 3"
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
  using c
  apply(intro arg_imp2[of ‹a 0› ‹a' 0› ‹a 1 ∧ a 2 ∧ a 3› ‹a' 1 ∧ a' 2 ∧ a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(intro arg_imp2[of ‹a 1› ‹a' 1› ‹a 2 ∧ a 3› ‹a' 2 ∧ a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(intro arg_imp2[of ‹a 2› ‹a' 2› ‹a 3› ‹a' 3›])
  apply(rule imp)
  apply(assumption)
  apply(rule imp)
  apply(assumption+)
  done

我不确定用 Eisbach 表达这一点有多容易，但用 Isabelle/ML.

表达应该相当容易

Answer 2

使用来自 user9716869 的指针，我能够编写一个方法来执行我想要的操作：

ML‹

fun split_with_tac (tac1:  int -> tactic) (ts: (int -> tactic) list) (i: int) (st: thm): thm Seq.seq =
    let 
      val st's = tac1 i st
      fun next st' = 
        let 
          val new_subgoals_count = 1 + Thm.nprems_of st' - Thm.nprems_of st 
        in
          if new_subgoals_count <> length ts then Seq.empty
          else
            RANGE ts i st'
        end
    in
      st's |> Seq.maps next
    end


fun tok_to_method_text ctxt tok =
    case Token.get_value tok of
      SOME (Token.Source src) => Method.read ctxt src
    | _ =>
        let
          val (text, src) = Method.read_closure_input ctxt (Token.input_of tok);
          val _ = Token.assign (SOME (Token.Source src)) tok;
        in text end 

val readText: Token.T Token.context_parser = Scan.lift (Parse.token Parse.text)

val text_and_texts_closure: (Method.text * Method.text list) Token.context_parser =
  (Args.context -- readText -- (Scan.lift \<^keyword>‹and› |-- Scan.repeat readText)) >> (fn ((ctxt, tok), t) =>
    (tok_to_method_text ctxt tok, map (tok_to_method_text ctxt) t));

›

method_setup split_with = 
‹text_and_texts_closure >> (fn (m, ms) => fn ctxt => fn facts =>
   let
     fun tac m st' =
       method_evaluate m ctxt facts
     fun tac' m i st' =
       Goal.restrict i 1 st'
       |> method_evaluate m ctxt facts
       |> Seq.map (Goal.unrestrict i)
      handle THM _ => Seq.empty
     val initialT: int -> tactic = tac' m
     val nextTs: (int -> tactic) list = map tac' ms
   in SIMPLE_METHOD (HEADGOAL (split_with_tac initialT nextTs)) facts end)
›



lemma 
  assumes r: "P ⟹ Q ⟹ R"
    and p: "P" 
    and q: "Q"
  shows "R"
  by (split_with ‹rule r› and ‹rule p›  ‹rule q›)

method conj_one_by_one uses pre = (
    match pre in 
      p: "?P ∧ ?Q" ⇒ ‹split_with ‹rule conjI› and 
                            ‹conj_one_by_one pre: p[THEN conjunct1]›
                            ‹conj_one_by_one pre: p[THEN conjunct2]››
      | insert pre)

lemma example:
  assumes c: "a 0 ∧ a 1 ∧ a 2  ∧ a 3"
    and imp: "⋀i. a i ⟹ a' i"
  shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
proof (conj_one_by_one pre: c)
  show "a 0 ⟹ a' 0" by (rule imp)
  show "a 1 ⟹ a' 1" by (rule imp)
  show "a 2 ⟹ a' 2" by (rule imp)
  show "a 3 ⟹ a' 3" by (rule imp)
qed

专注于艾斯巴赫的新子目标

Focussing on new subgoals in Eisbach

isabelle