# [isabelle] Applying n-ary monotonicity of "eventually" in ML

Suppose I have a theorem of the form "A ?x ⟹ B ?x ⟹ C ?x ⟹ D ?x" and the
three theorems "eventually A F", "eventually B F", "eventually C F".
I now want to get the theorem "eventually D F" in ML, but not just for
three theorems, but for an arbitrary number of premises. In the end, I'd
like a function that takes a theorem that is an n-ary implication (like
above) and a list of n elements, each corresponding to one of the premises.
This is a bit like the "eventually_elim" method, but in a forward
manner. My current solution is as outlined below, but it strikes me as
somewhat ugly and fragile. In particular, I dislike the "Thm.assumption"
in the end, but I don't know how to avoid it.
Manuel
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'])
|> Thm.assumption (SOME ctxt) 1
|> Seq.list_of
|> the_single
end

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*