*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML*From*: Makarius <makarius at sketis.net>*Date*: Tue, 13 Mar 2018 23:07:48 +0100*In-reply-to*: <7ceb42ff-0196-5250-6729-97c7edf16f18@in.tum.de>*References*: <7ceb42ff-0196-5250-6729-97c7edf16f18@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

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

**Follow-Ups**:

**References**:**[isabelle] Applying n-ary monotonicity of "eventually" in ML***From:*Manuel Eberl

- Previous by Date: [isabelle] New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix
- Next by Date: [isabelle] Call for Papers AVoCS'18 @FLOC 2018
- Previous by Thread: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Next by Thread: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list