Email Gateway (Aug 22 2022 at 09:29): Email Gateway (Aug 22 2022 at 09:29):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have a number of theorems that contain some constant p both in their
assumptions and in their conclusions.
I now want to derive modified theorems from them by adding an assumption
"p = ?q" (for a schematic variable ?q) and replace all occurrences of p
in the assumptions and the conclusion with ?q. Ideally in ML.
What is the easiest way to do that?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:30):From: Joachim Breitner <breitner@kit.edu>
Hi,
foo[unfolded eq_thm] or foo[folded eq_thm] do it in Isabelle/Isar; not
sure about Isabelle/ML.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 09:31):From: Joachim Breitner <breitner@kit.edu>
ignore me, misread your question.
signature.asc
Email Gateway (Aug 22 2022 at 09:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I think you’ll have to instantiate the “subst” theorem with the right “P” and “s” (using “Drule.cterm_instantiate” or other similar functions), then you can use resolution with your original theorems (e.g. “RS” or “OF” in ML). This is a bit tricky, but a good opportunity to exercise forward theorem derivations in Isabelle.
Alternative: A backward proof. You construct the statement of the theorem you want to prove and write a little tactic to solve it. Here, both forward and backward are about equally difficult, because you need to build some terms (the “P” instance in the forward proof, the goal statement in the backward proof).
Jasmin
Email Gateway (Aug 22 2022 at 09:34):From: Manuel Eberl <eberlm@in.tum.de>
It occurred to me to simply use theorem rewriting. The following piece
of code seems to do what I want to do. Am I doing anything in there that
I should not do or do differently?
ML {*
fun generalize_master_thm ctxt thm =
let
val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt
val p' = Free (p', HOLogic.realT)
val a = @{term "nth as"} $ Bound 0
val b = @{term "Transcendental.powr"} $ (@{term "nth bs"} $ Bound 0)
$ p'
val f = Abs ("i", HOLogic.natT, @{term "op * :: real => real =>
real"} $ a $ b)
val setsum = @{term "setsum :: (nat => real) => nat set => real"} $
f $ @{term "{..<k}"}
val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (setsum, @{term
"1::real"}))
val cprop = Thm.cterm_of ctxt' prop
in
thm
|> Local_Defs.unfold ctxt' [Thm.assume cprop RS @{thm p_unique}]
|> Thm.implies_intr cprop
|> rotate_prems 1
|> singleton (Variable.export ctxt' ctxt)
end
val _ = Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of
@{thm master1}))
val _ = Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of
(generalize_master_thm @{context} @{thm master1})))
*}
Input theorem:
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
f ∈ Θ(λx. real x powr p)
Output theorem:
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
(∑i<k. as ! i * bs ! i powr ?p''1) = 1 ⟹
f ∈ Θ(λx. real x powr ?p''1)
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:34):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
On 02.04.2015, at 23:16, Manuel Eberl <eberlm@in.tum.de> wrote:
It occurred to me to simply use theorem rewriting. The following piece
of code seems to do what I want to do. Am I doing anything in there that
I should not do or do differently?
I don’t know, but this
Input theorem:
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
f ∈ Θ(λx. real x powr p)Output theorem:
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
(∑i<k. as ! i * bs ! i powr ?p''1) = 1 ⟹
f ∈ Θ(λx. real x powr ?p'’1)
looks different from what you described abstractly in your previous email.
Jasmin
Email Gateway (Aug 22 2022 at 09:35):From: Manuel Eberl <eberlm@in.tum.de>
Yes, I do another step. I do not assume the equation directly, but
something that implies it. A function that does what I actually asked is
this:
fun generalize_master_thm ctxt thm =
let
val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt
val p' = Free (p', HOLogic.realT)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (@{term "p"}, p'))
val cprop = Thm.cterm_of ctxt prop
in
thm
|> Local_Defs.unfold ctxt' [Thm.assume cprop]
|> Thm.implies_intr cprop
|> rotate_prems 1
|> singleton (Variable.export ctxt' ctxt)
end
with input theorem
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
f ∈ Θ(λx. real x powr p)
and output theorem
g ∈ O(λx. real x powr ?p') ⟹
1 < (∑i<k. as ! i * bs ! i powr ?p') ⟹
eventually (λx. 0 < f x) sequentially ⟹
p = ?p''1 ⟹
f ∈ Θ(λx. real x powr ?p''1)
What I would like to know is whether any of the things I do are
considered bad style.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:35):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Manuel,
Normally, when allocating names, I would (following an idiom I learned from Dmitriy) still use the original context without the names and thread that one through the program, i.e. “unfold ctxt” without prime. I think you can get into trouble if you start using “ctxt’ ”, e.g. if you define new types or constants. Typically, the only place where you need “ctxt’ ” is in an “export” or when allocating further names. Dmitriy usually calls these contexts “ctxt_names”, to clarify their role.
Otherwise, if you’re an eta-macho, you can kill the “thm” argument and change all “|>”’s to “#>”’s. It’s quite tempting in your example, actually. ;)
Jasmin
Email Gateway (Aug 22 2022 at 09:35):From: Makarius <makarius@sketis.net>
Just the usual hints on context-conformance of Isabelle/ML snippets:
The @{term} antiquotations mention free variables "as", "bs", "k". To
which context do they belong? If they are undeclared, the code will
crash in a context that declares them locally.
@{term "nth as"} is polymorphic, i.e. in invents a locally fixed type 'a
(depending on the compilation context). This is likely to break down
when used in a different context.
As a general rule of thumb, @{term} antiquotations are only useful for
well-defined closed terms, such as @{term "1::real"}. Variables need to
be constructed explicitly at run-time, like p' above.
The global context above is not immediately clear, making it hard to
test. Morover, it seems to use an undefined repository version, instead
of the latest release.
Makarius
Email Gateway (Aug 22 2022 at 09:35):From: Manuel Eberl <eberlm@in.tum.de>
This code runs in the context of a locale in which as and bs are fixed
and have type "real list". I should have mentioned that.
I have to use the repository version because I require some
measure-theoretic theories that are not present in the latest release.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:36):From: Makarius <makarius@sketis.net>
What is the context where "p" in @{term "p"} comes from and belongs to?
The prop belongs to ctxt' by construction, so further contextual
operations need to use that, or a monotonic extension of it. So
Thm.cterm_of ctxt should be Thm.cterm_of ctxt'. Otherwise, one needs a
semantic proof, why ctxt is sufficient, but it merely obscures the code.
The main point of Thm.cterm_of acting on Proof.context in coming
Isabelle2015 is to make Isabelle/ML tool implementations more conformant
to normal context discplines, and not drop out into some global thy value
from the background.
Makarius
Email Gateway (Aug 22 2022 at 09:36):From: Makarius <makarius@sketis.net>
"The" repository version is undefined, until "hg id" is used.
Makarius
Email Gateway (Aug 22 2022 at 09:36):From: Makarius <makarius@sketis.net>
Another variation: fix q locally, then work with non-schematic material
inside the extended context (which is usually easier and more robust),
then export the result into the original context to make q schematic.
Makarius
Email Gateway (Aug 22 2022 at 09:36):From: Manuel Eberl <eberlm@in.tum.de>
- What is the context where "p" in @{term "p"} comes from and belongs to?
p is an abbreviation of type real defined in terms of as and bs in the
locale context.
- The prop belongs to ctxt' by construction, so further contextual
operations need to use that, or a monotonic extension of it. So
Thm.cterm_of ctxt should be Thm.cterm_of ctxt'. Otherwise, one needs a
semantic proof, why ctxt is sufficient, but it merely obscures the
code.
Ah, I see.
"The" repository version is undefined, until "hg id" is used.
e83ecf0a0ee1. I usually make a point of pulling the latest version
regularly to keep my developments up-to-date.
Another variation: fix q locally, then work with non-schematic
material inside the extended context (which is usually easier and more
robust), then export the result into the original context to make q
schematic.
Is that not what I did in the end? (q being p')
Cheers,
Manuel
On 07/04/15 11:54, Makarius wrote:
On Fri, 3 Apr 2015, Manuel Eberl wrote:
Yes, I do another step. I do not assume the equation directly, but
something that implies it. A function that does what I actually asked is
this:fun generalize_master_thm ctxt thm =
let
val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt
val p' = Free (p', HOLogic.realT)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (@{term "p"}, p'))
val cprop = Thm.cterm_of ctxt prop
in
thm
|> Local_Defs.unfold ctxt' [Thm.assume cprop]
|> Thm.implies_intr cprop
|> rotate_prems 1
|> singleton (Variable.export ctxt' ctxt)
endThe main point of Thm.cterm_of acting on Proof.context in coming
Isabelle2015 is to make Isabelle/ML tool implementations more
conformant to normal context discplines, and not drop out into some
global thy value from the background.Makarius
Email Gateway (Aug 22 2022 at 09:36):From: Makarius <makarius@sketis.net>
On Tue, 7 Apr 2015, Manuel Eberl wrote:
"The" repository version is undefined, until "hg id" is used.
e83ecf0a0ee1. I usually make a point of pulling the latest version
regularly to keep my developments up-to-date.
"The latest" is only meaningful for an instant of time in your private
context that nobody else knows about. Any public discussion on it is
invalidated rather quickly, by new incoming changes. Luckily Mercurial has
a unique value-oriented id for arbitrary points in history.
"Latest" versions also have the tendency to become outdated rather
quickly, paradoxically to become older than the truely latest release
version.
Another variation: fix q locally, then work with non-schematic
material inside the extended context (which is usually easier and more
robust), then export the result into the original context to make q
schematic.
Is that not what I did in the end? (q being p')
Ah, I did not see that. Maybe I was confused by the many p', p''. The
system already takes care of renamings, so if you mean a local "x" you fix
that and call it x in ML. If you mean p' you call it p' etc.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC