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
human-readable Isabelle/Isar and Isabelle/ML (see also "implementation"
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>

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


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