Комбинируя тактику определенное количество раз в Изабель - PullRequest
Новая
       10

Комбинируя тактику определенное количество раз в Изабель

2 голосов
/ 29 сентября 2019

Я решаю задачу, которая с помощью safe разделяется на 32 подзадачи. Это довольно алгебраическая цель, поэтому в целом мне нужно использовать арго, алгебру и авто. Мне было интересно, есть ли способ указать, что auto следует применять, скажем, 2 раза, затем алгебру 10 раз и т. Д. Где мне искать этот синтаксис в будущем? Это часть Айсбаха?

1 Ответ

2 голосов
/ 03 октября 2019

Существует тактика REPEAT_DETERM_N в $ISABELLE_HOME/src/Pure/tactical.ML Я никогда не использовал ее, поэтому я не уверен на 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

Я не эксперт в программировании Изабель / ML, поэтому этот код, вероятно, низкого качества, но я надеюсь, что это хорошая отправная точка для вас!

...