Email Gateway (Aug 22 2022 at 16:56): Email Gateway (Aug 22 2022 at 16:56):From: Manuel Eberl <eberlm@in.tum.de>
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.
Manuel
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'])
|> Thm.assumption (SOME ctxt) 1
|> Seq.list_of
|> the_single
end
Email Gateway (Aug 22 2022 at 16:56):From: Makarius <makarius@sketis.net>
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
Scratch.thy
Email Gateway (Aug 22 2022 at 16:57):From: Makarius <makarius@sketis.net>
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
Scratch.thy
Email Gateway (Aug 22 2022 at 16:57):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC