*To*: Makarius <makarius at sketis.net>, "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*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 14 Mar 2018 15:43:19 +0100*In-reply-to*: <4c5f8a2c-5234-8d0e-7633-54a8f1cfa80f@sketis.net>*References*: <7ceb42ff-0196-5250-6729-97c7edf16f18@in.tum.de> <b7190ce4-a7f9-3331-78f4-0079b436992d@sketis.net> <4c5f8a2c-5234-8d0e-7633-54a8f1cfa80f@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

I now think that the best way is probably having a HOL-forall quantifier to explicitly select the variable we're talking about and then have an attribute to lift the theorem. The situation where I need this is the following: I have a theorem like this: ∀x. 0 ≤ l1 x ⟶ 0 ≤ l2 x ⟶ f x ∈ {l1 x..u1 x} ⟶ g x ∈ {l2 x..u2 x} ⟶ f x * g x ∈ {l1 x * l2 x..u1 x * u2 x} And I am now in a situation (in ML) where I know that all of these preconditions hold for large enough x. I then want to use that to get the theorem "eventually (%x. f x * g x ∈ {l1 x * l2 x..u1 x * u2 x}) at_top". I packaged this in an attribute called "eventuallized". Since this is all HOL quantifiers and HOL implication, I avoid these higher-order problems entirely. My application is still very experimental, so I'll continue working on it before I decide how to tackle this specific issue exactly. But what I have seems sufficient for now. Manuel On 2018-03-14 15:34, Makarius wrote: > On 13/03/18 23:07, Makarius wrote: >> 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. > Here is another version of both the proof method from theory HOL.Filter > and the above forward inference in ML (which could be an attribute). > > Apart from further fine-tuning of Isabelle/ML "style and orthography", I > did not change anything significant. So for now I would say that your > original approach to go from rule: "A x ⟹ B x ⟹ C x ⟹ D x" for x to the > "eventually" rule is fine -- including the Thm.assumption operation. > (Incidently the same happens in the Isar proof snippet given at the > bottom, to fit the result of fix/assume/show into the pending goal; > similarly in the "by fact" step). > > Of course, it implicitly depends on well-behaved HO-unification problems > given to this operation. > > > Where does the situation "Suppose I have a theorem of the form ..." > actually emerge? > > That rule is in Isabelle standard form, as HO Horn clause with removed > outer quantification. So fitting it into a goal usually requires > unification to recover the lost information of the quantifier prefix. In > principle, the rule could be made a closed form (in HOL or non-standard > Pure form) and applied with some low-level inference. It does not get > automatically better, though, but depends on the actual application. > > > Makarius

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

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

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

- Previous by Date: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Next by Date: [isabelle] Binding the type variable in the Axiom of Choice – Re: Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Previous by Thread: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Next by Thread: [isabelle] Mathematical Logics and Logical Frameworks
- 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