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

```On 12/03/18 18:23, Manuel Eberl wrote:
> 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.

The included Scratch.thy is what I made out of it, just trying to
understand it formally and writing it down again with the means of
manual section "0.1 Style and orthography").

It is getting late and I need to postpone investigating the actual
technical question behind it. Or maybe someone else can see it now on
the spot.

Makarius
```
```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>

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```

• Follow-Ups:

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