Theory More_Methods

theory More_Methods
  imports Main Reordering_Quantifiers "HOL-Eisbach.Eisbach" ML_Util
begin

ML ‹fun mini_ex ctxt = SIMPLE_METHOD (mini_ex_tac ctxt 1)›
ML ‹fun defer_ex ctxt = SIMPLE_METHOD (defer_ex_tac ctxt 1)›

method_setup mini_existential =
  ‹Scan.succeed mini_ex› ‹Miniscope existential quantifiers›
method_setup defer_existential =
  ‹Scan.succeed defer_ex› ‹Rotate first conjunct under existential quantifiers to last position›

method mini_ex = ((simp only: ex_simps[symmetric])?, mini_existential, (simp)?)
method defer_ex = ((simp only: ex_simps[symmetric])?, defer_existential, (simp)?)
method defer_ex' = (defer_existential, (simp)?)

method solve_triv =
  fo_assumption | refl_match | simp; fail | assumption | (erule image_eqI[rotated], solve_triv)

method solve_ex_triv2 = (((rule exI)+)?, (rule conjI)+, solve_triv)

method solve_conj_triv = solve_triv | (rule conjI, solve_conj_triv)

method solve_conj_triv2 =
  (match conclusion in
    "_ ∧ _" ⇒ ‹rule conjI, solve_conj_triv2›
  ¦ _ ⇒ solve_triv)

method solve_ex_triv = (((rule exI)+)?, solve_conj_triv)

named_theorems intros
named_theorems elims

lemmas [intros] =
  allI ballI exI bexI[rotated] conjI impI
and [elims] =
  bexE exE bexE conjE impE

method intros uses add  = (intro add intros)
method elims  uses add  = (elim  add elims)

text ‹Test case›
lemma all_mp:
  "∀ x. P x ⟶ R x" if "∀ x. P x ⟶ Q x" "⋀ x. P x ⟹ Q x ⟹ R x"
  using that by (intros; elims add: allE)

method rprem =
  (match premises in R: _ ⇒ ‹rule R›)

text ‹Test case for @{method rprem}.›
lemma
  "A ⟹ (A ⟹ C) ⟹ (A ⟹ B) ⟹ B"
  by rprem

ML ‹
fun all_forward_tac ctxt n thms nsubgoal =
  let
    val assumes = replicate n (assume_tac ctxt nsubgoal)
    fun forward thm = forward_tac ctxt [thm] nsubgoal :: assumes |> EVERY |> TRY
  in EVERY (map forward thms) end;
›

ML ‹
fun xrule_meth tac =
  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
  (fn (n, ths) => fn ctxt => SIMPLE_METHOD (tac ctxt n ths 1));
val all_forward_meth = xrule_meth all_forward_tac
›

method_setup all_forward = ‹all_forward_meth› "Apply each rule exactly once in forward manner"

named_theorems forward1
named_theorems forward2
named_theorems forward3
named_theorems forward4

method frule1 = changed ‹all_forward forward1›
method frule2 = changed ‹all_forward (1) forward2›
method frule3 = changed ‹all_forward (2) forward3›
method frule4 = changed ‹all_forward (3) forward4›

method frules = changed ‹
  all_forward (0) forward1,
  all_forward (1) forward2,
  all_forward (2) forward3,
  all_forward (3) forward4
›

ML ‹
fun dedup_prems_tac ctxt =
  let
    fun Then NONE tac = SOME tac
      | Then (SOME tac) tac' = SOME (tac THEN' tac');
    fun thins H (tac, n) =
      if H then (tac, n + 1)
      else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0);
    fun member x = List.exists (fn y => x = y)
    fun mark_dups _ [] = []
    |   mark_dups passed (x :: xs) =
        if member x passed
        then false :: mark_dups passed xs
        else true :: mark_dups (x :: passed) xs
  in
    SUBGOAL (fn (goal, i) =>
      let
        val Hs = Logic.strip_assums_hyp goal
        val marked = mark_dups [] Hs
      in
        (case fst (fold thins marked (NONE, 0)) of
          NONE => no_tac
        | SOME tac => tac i)
      end)
  end;
›

method_setup dedup_prems =
  ‹Scan.succeed (fn ctxt => SIMPLE_METHOD' (fn i => CHANGED (dedup_prems_tac ctxt i)))›
  "Remove duplicate premises"

method repeat methods m =
  determ ‹(changed m, repeat m)?›

ML ‹
fun REPEAT_ROTATE tac =
  let
    fun repeat (trm, i) = let
      val num_prems = Logic.strip_assums_hyp trm |> length
      val tac2 = TRY (tac i) THEN rotate_tac 1 i
      val tacs = replicate num_prems tac2
    in DETERM (EVERY tacs) end
in SUBGOAL repeat end
›

method_setup repeat_rotate =
 ‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
   let
     fun tac st' = method_evaluate m ctxt facts st'
   in SIMPLE_METHOD (REPEAT_ROTATE (K tac) 1) facts end)
›

end (* Theory *)