theory Scratch
  imports Main
begin

ML \<open>
  fun eventually_elim_tac facts =
    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
      let
        val mp_facts = facts RL @{thms eventually_rev_mp}
        val rule =
          @{thm eventuallyI}
          |> fold (fn mp_fact => fn th => th RS mp_fact) mp_facts
          |> funpow (length facts) (fn th => @{thm impI} RS th)
        val cases_prop =
          Thm.prop_of (Rule_Cases.internalize_params (rule RS Goal.init (Thm.cterm_of ctxt goal)))
        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
      in CONTEXT_CASES cases (resolve_tac ctxt [rule] i) (ctxt, st) end)
\<close>

method_setup eventually_elim = \<open>
  Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1))
\<close> "elimination of eventually quantifiers"


ML \<open>
fun eventually_mono_OF _ rule [] = rule
  | eventually_mono_OF ctxt rule thms =
      let
        val conj_conv = Conv.rewr_conv @{thm conj_imp_eq_imp_imp [symmetric]}
        val conjs_conv = Conv.every_conv (replicate (length thms - 1) conj_conv)
        val eventually_conj = foldl1 (fn (P, Q) => @{thm eventually_conj} OF [P, Q])
      in
        (@{thm eventually_mono} OF [eventually_conj thms, Conv.fconv_rule conjs_conv rule])
        |> Thm.assumption (SOME ctxt) 1
        |> Seq.list_of
        |> the_single
      end
\<close>

notepad
begin
  fix A B C D :: "'a \<Rightarrow> bool"
  fix F :: "'a filter"
  assume rule: "A x \<Longrightarrow> B x \<Longrightarrow> C x \<Longrightarrow> D x" for x
  assume thms: "eventually A F" "eventually B F" "eventually C F"

  text \<open>Backward refinement -- proof method\<close>
  from thms have "eventually D F"
  proof eventually_elim
    show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x \<Longrightarrow> D x" by (fact rule)
  qed

  text \<open>Forward inference -- attribute\<close>
  ML_val \<open>eventually_mono_OF @{context} @{thm rule} @{thms thms}\<close>
end

end