Ориентируясь на новые подцели в Айсбахе

Question

В Eisbach я могу использовать ;, чтобы применить метод ко всем новым подцелям, созданным методом. Однако я часто знаю, сколько подцелей создано, и хотел бы применить различные методы к новым подцелям. Есть ли способ сказать что-то вроде «применить метод X к первой новой подцели и метод Y ко второй новой подцели»?

Вот простой пример использования:

Я хочу разработать метод, который работает на 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

При реализации этого метода в Eisbach у меня возникла проблема после использования 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

Это не полный ответ, но вы можете извлечь некоторую полезную информацию из того, что здесь изложено.

В Айсбахе я могу использовать; применить метод ко всем новым подцелям, созданным методом. Однако я часто знаю, сколько подцелей создано, и хотел бы применить различные методы к новым подцелям. Есть ли способ сказать что-то вроде «применить метод X к первой новой подцели и метод Y ко второй новой подцели»?

Вы можете использовать стандартную тактическую RANGE, чтобы определить свои собственные тактики c, которые вы можете применять к последовательным подзадачам. Ниже я приведу очень специализированный и значительно упрощенный вариант использования:

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 принимает список теорем, должно быть легко увидеть, как эти теоремы могут быть заменены тактикой, и с некоторой дальнейшей работой tacti c может быть упакован как метод более высокого порядка.

---

Я хочу разработать метод, который работает на 2 соединениях произвольной длины, но с одинаковой структурой. Метод должен быть применим, чтобы показать, что конъюнкция 1 подразумевает конъюнкцию 2, показывая, что импликация выполняется для каждого компонента. Его можно использовать следующим образом:

ОБНОВЛЕНИЕ

После еще одного взгляда на проблему кажется, что существует существенно более естественное решение. Решение следует плану из исходного ответа, но мета-импликация заменяется импликацией объекта HOL logi c (преобразование «туда и сюда» может быть достигнуто с использованием 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

Я не уверен, насколько легко было бы express это в Айсбахе, но это должно быть достаточно просто express в 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