Email Gateway (Aug 19 2022 at 13:49): Email Gateway (Aug 19 2022 at 13:49):From: Gottfried Barrow <igbi@gmx.com>
I added "lifting" and "coercion" in the subject to make sure Ondrej and
Dmitriy see it, but here I keep my talk general, since it's a mailing list.
From here, I describe the three files I attach, summarize why I think I
would and wouldn't want to use the types I defined, and try to make my
case for Ondrej and Dmitriy to expand the ability of lifting and
coercion to accept type variables where they currently don't.
Well, things are good already. I'm just finishing this off.
The three files I attach are part of my attempt to make a case. The
algebra is already there in HOL, and I'm more interested in working with
abstract algebraic structures than with the rational and real numbers.
Partly, it's because they're at chapters 4, 13, and 14, where the
rationals and reals are at chapter 76 and 79 of the HOL document. It'll
take me while to get to chapter 14, let alone chapter 79.
It probably wouldn't be good to use a special type of positives just to
get rid of a few conditions in the premises, but there could be
applications where their use would be structural, such as being used to
generalize positive and negative exponents for different algebraic
structures. Also, I could use them in a datatype, as with the following,
where the types would be closed under addition:
datatype 'a::linordered_field lofD =
NNeg "'a lF0"
|NPos "'a lFN0"
Use them for what? Nothing that I can think of right now.
I tried workarounds using option, ordered pairs, and lists, and those
were good enough for what's in the file lF0_lF1.thy. In that file, I
do "Lift nothing much; Coerce everything". It occurred to me that I
didn't have to do anything but use setup_lifting.
The main thing I wanted from the lifting was the numerals, and I was
having problems proving the type class requirements with the clutter of
the types I mentioned.
That led me to Lifting_Option.thy, and I cut and pasted and modified
from there to set up a datatype in dID_lifting.thy, which is just an
identity datatype:
datatype 'a dID = dIDc 'a
I couldn't have done it without Sledgehammer, and thanks to Brian
Huffman and Ondreg for that file.
With that datatype, I was able to instantiate my typedef datatypes to
get the requirements, using lifting, for numeral, up to semiring_1,
and that file is lF0_numerals.thy.
Thanks,
GB
dID_lifting.thy
lF0_lF1.thy
lF0_numerals.thy
Last updated: Apr 27 2024 at 01:05 UTC