Email Gateway (Aug 22 2022 at 15:20): Email Gateway (Aug 22 2022 at 15:20):From: Thomas.Sewell@data61.csiro.au
My understanding is that the function declaration process can be split,
with definitions in one place and proofs of termination to follow.
The function is fully defined in the intermediate state, but key facts
for proving anything about it are not present.
If that is still the case, you can make progress on your problem by
having your package perform all definitions (with all polymorphic type
magic) and then have a collective second phase of termination requirements.
You could either require multiple "termination" steps to conclude, each
provoking its own proof, or it might be possible to pack all the proof
obligations into a single proof.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 15:20):From: Lars Hupel <hupel@in.tum.de>
Dear Thomas,
I've been arguing about a scheme similar to that with Peter and Ondrej.
The theory updates in my command are function definitions. Before I can
continue defining functions, I need to prove termination and congruence
rules of the earlier ones. Especially the cong rules cannot be proven
without termination. So it's difficult to make progress without having the
theorems at hand.
Another option would be to do a "trial run", where I would invoke the
function package beforehand, ignore the updated theory, but look at the
resulting proof obligations. I can collect and present those to the user
and perform the actual definitions in the "after_qed" step. This would work
but also slow down the command by a factor of two.
I'm a bit reluctant to introduce two commands (let's call them "embed" and
"embed_termination"), because in principle, there could be arbitrarily many
invocations of the latter before the process is concluded. To me it seems a
little strange to require that.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:20):From: Makarius <makarius@sketis.net>
My impression is that this is going into the right direction.
Conceptually, a definitional package with a proof can indirectly get
hold of that via the after_qed continuation, which is part of all
relevant Isabelle/ML interfaces.
The function/termination package merely needs to expose this in the
usual way, with after_qed and after_qed_termination arguments in the
initial function command.
Thus a user-defined command can make a function definition in
Isabelle/ML, such that its corresponding 'termination' command produces
further function definitions, again with corresponding 'termination'
proofs by the user. Thus several 'termination' commands (each with its
own Isar proof) can be somehow chained together.
There is certainly a challenge here, because of the loose coupling of
'function' and 'termination': termination commands might follow in any
order and there might be unrelated function/termination commands in
between. Additional care is required to cope with a potential change of
local_theory targets between 'function' and 'termination' parts, but
that situation can already happen in the existing package setup.
Makarius
Email Gateway (Aug 22 2022 at 15:20):From: Lars Hupel <hupel@in.tum.de>
The function/termination package merely needs to expose this in the
usual way, with after_qed and after_qed_termination arguments in the
initial function command.
It seems to me that implementing that wouldn't be very complicated.
There are not many occurrences of "Function.*" in the distribution/AFP,
so this might be feasible to do in a day or two. I will investigate this.
There is certainly a challenge here, because of the loose coupling of
'function' and 'termination': termination commands might follow in any
order and there might be unrelated function/termination commands in
between. Additional care is required to cope with a potential change of
local_theory targets between 'function' and 'termination' parts, but
that situation can already happen in the existing package setup.
That's true. In my case, I'm interacting with the code generator, which
has a global setup anyway. I don't have a good story yet about what I'd
do if the code setup changed in between.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:26):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm trying to define a command that needs to emit multiple proof
obligations to the user. The catch is that these proof obligations can
only be generated after some interspersed theory updates. More concretely:
I need to call the function package to define some functions. Of course,
this means that in general I have to ask the user for a proof
obligation. That by itself is not a problem – I could just use
"Outer_Syntax.local_theory_to_proof".
However, I need to define multiple functions one after the other,
according to some specific ordering. In general, because of
polymorphism, I can't define them all at once and then ask the user to
proof all obligations, but I need to "open_target"/"close_target" in
between.
A possible trace of my command could be:
Because "Outer_Syntax.command" requires a transition transformer of type
"Toplevel.transition -> Toplevel.transition", I naively tried to compose
multiple of these, like so:
val multi_proof =
Toplevel.local_theory_to_proof NONE NONE
(Proof.theorem NONE (K I) [[(@{prop True}, [])]])
#> Toplevel.local_theory_to_proof NONE NONE
(Proof.theorem NONE (K I) [[(@{prop "id True"}, [])]])
When I execute the command, I get the initial proof obligation as
expected. After typing "done", I don't get another proof state.
After studying the sources and isar-ref I have formed the understanding
that I have only constructed a single transition that may try multiple
different things (in this case: two), of which the first one succeeds.
Is there any way to achieve what I want?
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:26):From: Makarius <makarius@sketis.net>
On 03/04/17 17:01, Lars Hupel wrote:
I'm trying to define a command that needs to emit multiple proof
obligations to the user. The catch is that these proof obligations can
only be generated after some interspersed theory updates.
Is there any way to achieve what I want?
This is not going to work. Isar commands can have 0 or 1 Isar proofs.
You need to come up with a different approach, i.e. disprove your "I
need" and "I want" statements.
Because "Outer_Syntax.command" requires a transition transformer of type
"Toplevel.transition -> Toplevel.transition", I naively tried to compose
multiple of these, like so:val multi_proof =
Toplevel.local_theory_to_proof NONE NONE
(Proof.theorem NONE (K I) [[(@{prop True}, [])]])
#> Toplevel.local_theory_to_proof NONE NONE
(Proof.theorem NONE (K I) [[(@{prop "id True"}, [])]])When I execute the command, I get the initial proof obligation as
expected. After typing "done", I don't get another proof state.
Toplevel.transition transformers compose a sequential union of
transactions; see also the "implementation" manual section 9.1.2.
Also note that the canonical composition operator for transition
transformers is "o" instead of "#>".
Makarius
Last updated: Apr 26 2024 at 12:28 UTC