[isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients?

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, "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,

theory c
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[3], Sp[Nt[4,7],Nt[5,3,3]] ] )"

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