theory Scratch
  imports Main
begin

ML \<open>
fun eventually_mono_OF _ thm [] = thm
  | eventually_mono_OF ctxt thm thms =
      let
        val conv = Conv.rewr_conv @{thm conj_imp_eq_imp_imp [symmetric]}
        fun go conv' n =
          if n <= 0 then conv' else go (conv then_conv conv') (n - 1)
        val conv = go Conv.all_conv (length thms - 1)
        val thm' = Conv.fconv_rule conv thm
        fun go' thm [] = thm
          | go' thm (thm' :: thms) = go' (@{thm eventually_conj} OF [thm, thm']) thms
        val thm'' = go' (hd thms) (tl thms)
      in
        (@{thm eventually_mono} OF [thm'', thm'])
        |> @{print}
        |> Thm.assumption (SOME ctxt) 1
        |> Seq.list_of
        |> the_single
      end
\<close>

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]}
        fun conjs_conv cv n =
          if n <= 0 then cv else conjs_conv (conj_conv then_conv cv) (n - 1)
        val conj_rule = rule |> Conv.fconv_rule (conjs_conv Conv.all_conv (length thms - 1))
        val eventually_conj = foldl1 (fn (P, Q) => @{thm eventually_conj} OF [P, Q])
      in
        (@{thm eventually_mono} OF [eventually_conj thms, conj_rule])
        |> @{print}
        |> 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"

  ML_val \<open>
    eventually_mono_OF @{context} @{thm rule} @{thms thms};
    eventually_mono_OF' @{context} @{thm rule} @{thms thms}
  \<close>

end

end