Email Gateway (Aug 19 2022 at 12:16): Email Gateway (Aug 19 2022 at 12:16):From: Gottfried Barrow <gottfried.barrow@gmx.com>
There are no PDF documents for the new HOL-BNF sessions at this site:
http://isabelle.in.tum.de/website-Isabelle2013-1-RC3/dist/library/HOL/index.html
A long time back, Makarius told me that he builds all the documents for
all the sessions for the distribution website. That's where I get the
theory PDFs these days. I'm not set up to build any PDFs on my machine,
and there would probably be failures if I tried.
Having the all the theories in one PDF for HOL-BNF would be convenient
for trying to get a grip on things, when the need arises.
There's a new tutorial that goes along with the new datatype,
"datatypes.pdf".
About every other email on this list the transfer and lifting packages
are mentioned. It would be nice if tutorials for those would appear in
the jEdit documentation panel, along with datatypes.pdf. A little bit of
instruction with some examples can go a long way. Someone might as well
do one for the quotient package also.
The datatypes.pdf already helped me get a little bit of proof of concept
going. I got the HOL-BNF logic built, and defined a recursive
"datatype_new" without any errors, so that's a start. It appears
datatype_new is not a complete replacement for datatype yet.
I don't know how to use fset yet, so I had to resort to using list, but
the ability to recurse with fset and multiset looks promising to come up
with a way to treat an integer as some type of combination of factor
sets and sum sets:
Thanks for the new stuff,
GB
theory c
imports Complex_Main BNF "~~/src/HOL/Library/Code_Target_Nat"
begin
type_synonym 'a mset = "('a * nat) fset"
datatype_new sumprod_m = Nt "nat multiset" | Sp "sumprod_m multiset"
datatype_new sumprod_ms = Nt "nat mset" | Sp "sumprod_ms mset"
(-------- PRODUCT OF "nat list" --------)
fun list_prod :: "nat list => nat" where
"list_prod [] = 1"
| "list_prod (n#ns) = (n * list_prod ns)"
value "list_prod [2,3]"
(-------- SUM OF PRODUCTS --------)
datatype sumprod = Nt "nat list" | Sp "sumprod list"
fun sumprod_calc :: "sumprod => nat" where
"sumprod_calc (Nt x) = list_prod x"
| "sumprod_calc (Sp []) = 0"
| "sumprod_calc (Sp (x#xs)) = (sumprod_calc x) + (sumprod_calc (Sp xs))"
value "sumprod_calc( Sp[ Nt[2,2,3], Nt[3], Sp[Nt[4,7],Nt[5,3,3]] ] )"
Email Gateway (Aug 19 2022 at 12:38):From: Makarius <makarius@sketis.net>
On Thu, 31 Oct 2013, Gottfried Barrow wrote:
There are no PDF documents for the new HOL-BNF sessions at this site:
http://isabelle.in.tum.de/website-Isabelle2013-1-RC3/dist/library/HOL/index.html
This is simply because HOL-BNF does not provide a document. There is no
obligations for Isabelle sessions to include such documents. The BNF guys
do provide a separate manual "datatypes".
I'm not set up to build any PDFs on my machine, and there would probably
be failures if I tried.
It should work after running the batch file
Isabelle2013-1-RC3\Cygwin-Latex-Setup and waiting patiently untile approx.
500 MB disk space is filled up.
Then you can produce session documents like this (via Cygwin-Terminal):
isabelle build -o browser_info -o document=pdf -v HOL-Library
For already built sessions without generated document, you might need
option -c as well.
Makarius
Email Gateway (Aug 19 2022 at 12:41):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Thanks. I'll try that someday, but I've gotten quite a ways without
doing much of that, except in the beginning.
Regards,
GB
Last updated: Apr 26 2024 at 04:17 UTC