[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.