Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] MOC-generating functions and succinct proofs.

Email Gateway (Aug 22 2022 at 15:17):

From: Raymond Rogers <raymond.rogers72@gmail.com>
Towards more succinct proofs using Method Of Coefficients (MOC) and
Generating functions.
If I define a derived data types, GenF and MOC, from Formal_Power_Series
(fps's) and define terms as members of this, then will:
The automatic proof process use the definitions and lemmas on this type,
Genf, first? In preference to burrowing down to the underlying fsp facts.
I realize I could use the definitions and lemmas explicitly but I would
like the auto/simp functionality to give preference to these, hopefully
short and general, properties first. While assuring that the underlying
facts about fps's are adhered to.

Ray

Email Gateway (Aug 22 2022 at 15:18):

From: Manuel Eberl <eberlm@in.tum.de>
Sorry, but I don't understand at all what you mean. auto and simp use
facts from the simp set and, in case of auto, the claset (intro, dest,
elim rules).

I do not understand what derived data types you want to define and what
you want to do with them and what you mean by defining terms as
‘members’ of them.

Manuel

Last updated: Apr 25 2024 at 16:19 UTC