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



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




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