[isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients?
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients?
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Thu, 31 Oct 2013 04:38:10 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
There are no PDF documents for the new HOL-BNF sessions at this site:
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,
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,
imports Complex_Main BNF "~~/src/HOL/Library/Code_Target_Nat"
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, Sp[Nt[4,7],Nt[5,3,3]] ] )"
This archive was generated by a fusion of
Pipermail (Mailman edition) and