isabelle - 在伊莎贝尔中组合战术一定次数

Question

我发现自己正在解决一个目标，该目标使用 safe 拆分为 32 个子目标。这是一个相当代数的目标，所以总的来说我需要使用 argo、algebra 和 auto。我想知道是否有一种方法可以指定自动应用 2 次，然后代数 10 次等。以后我应该在哪里寻找这种语法？它是艾斯巴赫的一部分吗？

Answer 1

$ISABELLE_HOME/src/Pure/tactical.ML 中有 REPEAT_DETERM_N 战术，我从未使用过它，所以我不能 100% 确定它是您需要的。

或者，您的功能可以像这样完成:

theory NTimes
imports
Main
"~~/src/HOL/Eisbach/Eisbach"
begin

ML ‹

infixr 2 TIMES

fun 0 TIMES _ = all_tac
  | n TIMES tac = tac THEN (n - 1) TIMES tac
›

notepad
begin
  fix A B C D
  have test1: "A ∧ B ∧ C ∧ D ⟹ True"
    apply (tactic ‹3 TIMES eresolve_tac @{context} [@{thm conjE}] 1›)
    apply (rule TrueI)
    done
  fix E
  have test2: "A ∧ B ∧ C ∧ D ∧ E ⟹ True"
    apply (tactic ‹2 TIMES 2 TIMES eresolve_tac @{context} [@{thm conjE}] 1›)
    apply (rule TrueI)
    done

end

(* For good examples for working
with higher order methods in ML see $ISABELLE_HOME/src/HOL/Eisbach/Eisbach.thy *)

method_setup ntimes = ‹
  Scan.lift Parse.nat -- Method.text_closure >>
  (fn (n, closure) => fn ctxt => fn facts => 
    let
      val tac = method_evaluate closure ctxt facts
    in
     SIMPLE_METHOD (n TIMES tac) facts
    end)
›

notepad
begin
  fix A B C D
  have test1: "A ∧ B ∧ C ∧ D ⟹ True"
    apply (ntimes 3 ‹erule conjE›)
    apply (rule TrueI)
    done
  fix E
  have test2: "A ∧ B ∧ C ∧ D ∧ E ⟹ True"
    apply (ntimes 2 ‹ntimes 2 ‹erule conjE››)
    apply (rule TrueI)
    done
  have test3: "A ∧ B ∧ C ∧ D ∧ E ⟹ True"
    apply (ntimes 3 ‹erule conjE›)
    apply (rule TrueI)
    done
  have test4: "A = A" "B = B" "C = C"
    apply -
    apply (ntimes 2 ‹fastforce›)
    apply (rule refl)
    done
(* in some examples one can instead use subgoal ranges *)
  have test5: "A = A" "B = B" "C = C"
    apply -
    apply (fastforce+)[2] 
    apply (rule refl)
    done

end

end

我不是 Isabelle/ML 编程方面的专家，因此这段代码的质量可能很低，但我希望这对您来说是一个好的起点!