Combining tactics a certain number of times in Isabelle

Question

I find myself solving a goal that with safe splits to 32 subgoals. It is a quite algebraic goal so overall I need to use argo, algebra and auto. I was wondering if there is a way to specify that auto should be applied say 2 times, then algebra 10 times etc. Where should I look for this syntax in the future? Is it part of eisbach?

Answer 1

There is the REPEAT_DETERM_N tactical in $ISABELLE_HOME/src/Pure/tactical.ML I never used it so I'm not 100% sure it's what you need.

Alternatively your functionality can be done somewhat like that:

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

I'm not an expert in Isabelle/ML Programming so this code is likely of low quality, but I hope it's a good starting point for you!