Re: [isabelle] Composing toplevel transitions



On 04/04/17 04:00, Thomas.Sewell at data61.csiro.au wrote:
> 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.

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





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