Re: [isabelle-dev] sets and code generation
On 03/23/2012 11:45 AM, Jesus Aransay wrote: I know there is an alternative way to get that, by means of sparse matrices (SparseMatrix.thy), but it demands translating every operation over the matrix type to its equivalent version for sparse matrices, which may be sometimes hard work. Code generation often requires translating or transfering every operation from one type to another. At the moment, users have to do this manually (which can be hard work as you said), but we are working on a mechanism that should soon automate this. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On Fri, 23 Mar 2012, Christian Sternagel wrote: Maybe the AFP entry for executable matrix operations is useful for you. http://afp.sourceforge.net/entries/Matrix.shtml (HOL/Matrix/Matrix.thy). Note that in current Isabelle/08c22e8ffe70 HOL/Matrix is actually called HOL/Matrix_LP, in order to avoid a name clash of the AFP/HOL-Matrix session (the latter was introduced later, but AFP names are not so easy to change as I understand it). Technically, the motivation is to get globally unique session names for official Isabelle + AFP sessions. Then when we eventually get a decent build system (based on Isabelle/Scala), the user can refer to sessions robustly without tinkering IsaMakefiles or funny search paths. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient.invariant
Absolutely, thanks. Constants should be hidden if they are internal to some package. Especially with such a universal name as invariant. Tobias Am 23/03/2012 17:34, schrieb Makarius: Just a note on the following changeset: changeset: 47095:3ea48c19673e user:kuncar date:Fri Mar 23 14:25:31 2012 +0100 files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/Quotient/quotient_type.ML description: generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command setup_lifting command: setups Quotient infrastructure from a typedef theorem It introduces a constant called invariant in main HOL. It might be a candidate for hide_const (open). Some experts on the Isabelle/HOL library can probably say more. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient.invariant
On 03/23/2012 05:34 PM, Makarius wrote: Just a note on the following changeset: changeset: 47095:3ea48c19673e user: kuncar date: Fri Mar 23 14:25:31 2012 +0100 files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/Quotient/quotient_type.ML description: generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command setup_lifting command: setups Quotient infrastructure from a typedef theorem It introduces a constant called invariant in main HOL. It might be a candidate for hide_const (open). Some experts on the Isabelle/HOL library can probably say more. At this point it's not clear if this constant will be used only for internal purposes. The original idea was to allow users to write definitions like this one: quotient_type 'a foo = 'a bar / invariant P If it turns out that we need this constant only internally, it will be hidden. Ondrej ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient.invariant
If it turns out that the constant is not internal-only, it should get a more specific name. invariant really is a name that should be available to users without shadowing. Cheers, Gerwin On 24/03/2012, at 4:06, Ondřej Kunčar kun...@in.tum.de wrote: On 03/23/2012 05:34 PM, Makarius wrote: Just a note on the following changeset: changeset: 47095:3ea48c19673e user: kuncar date: Fri Mar 23 14:25:31 2012 +0100 files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_term.ML src/HOL/Tools/Quotient/quotient_type.ML description: generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command setup_lifting command: setups Quotient infrastructure from a typedef theorem It introduces a constant called invariant in main HOL. It might be a candidate for hide_const (open). Some experts on the Isabelle/HOL library can probably say more. At this point it's not clear if this constant will be used only for internal purposes. The original idea was to allow users to write definitions like this one: quotient_type 'a foo = 'a bar / invariant P If it turns out that we need this constant only internally, it will be hidden. Ondrej ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
