### [isabelle-dev] Code export to Haskell and lower-case theory names

Hallo, I just noticed that when exporting code to Haskell, there is a complication when some of the theories involved have lower-case names. The code export itself will work with no error or warning, but when ghc/ghci are invoked on the generated code, they will report the lower-case module name

### Re: [isabelle-dev] Code export to Haskell and lower-case theory names

Be that as it may, even in that case, I would like the code export tool to at least output a warning or an error message. Having the code export tool export produce faulty Haskell code can hardly be intended behaviour. As an analogy: when I give invalid code to a compiler, I expect it to complain

### Re: [isabelle-dev] Partial functions

Hallo, partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is an abbreviation for 'a ⇒ 'b option. There is syntax such as [1 ↦ 2, 3 ↦ 4], meaning, basically, λx. if x = 1 then Some 2 else if x = 3 then Some 4 else None. There is also update syntax for such function, such as f(1 ↦

### [isabelle-dev] Replacing schematic/dummy variables in a term with fresh free variables

Hallo, I currently have the problem that I have a pattern, i.e. a term that may contain schematic variables, schematic type variables and, in particular,m schematic type variables originating from dummy variables. I read this term using Proof_Context.read_term_pattern and the result generally

### Re: [isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases

Hallo, The main thing still missing in Isabelle/5ccee1cb245a is a regular ML interface Fun_Cases.fun_cases. What do you mean by that? There exists an ML function Fun_Cases.mk_fun_cases : Proof.context - term - thm -- is that not an ML interface to the Fun_Cases tool? Or do you also want a

### Re: [isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases

On 30/09/13 11:49, Makarius wrote: On Mon, 23 Sep 2013, Manuel Eberl wrote: I sent my changes to Alexander Krauss last Wednesday so that he can review them. We are now getting very close to the fork-point for the release. So can you just post the changeset here, or send it to me privately

### Re: [isabelle-dev] Remaining uses of Proof General?

Hallo, I am not, as it were, a user of Proof General anymore; however, I would like, if I may, to point out one thing that annoys me in jEdit and that was, in my opinion, better in Proof General: the handling of abbreviations for Unicode characters. The current behaviour with “immediate

### Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more natural Re/Im view

types are “natural” codatatypes, so defining them as datatypes makes everything a bit more clumsy. Cheers, Manuel Eberl On 07.05.2014 16:50, Makarius wrote: On Wed, 7 May 2014, Johannes Hölzl wrote: * Theorems about complex numbers are now stated only using Re and Im, the Complex constructor

### Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more natural

Yes, but the underlying reason for that is that complex numbers are isomorphic to pairs of real numbers, and binary product types are degenerate (I would rather say very basic) co-algebraic datatypes. So my point (and I would guess Andrei's as well) is that this really has nothing to do with

### Re: [isabelle-dev] NEWS: powr

I am not terribly happy about that. I use approximation of powr in my work on Akra–Bazzi and the Master theorem. I take it that a powr b = exp (ln a * b) still holds for positive a. I could probably apply that rewrite rule before applying approximation, but it would of course be nice if I did

### Re: [isabelle-dev] Euclidean Ring

Hallo, thanks for all the good work. It's nice to finally see my work integrated so neatly into HOL. 1. Normalization. Currently, there is normalization_factor such that a div normalization_factor a yields the normalized elements. My impression is that the latter should be an operation on

### Re: [isabelle-dev] »real« considered harmful

On 24/06/15 15:55, Larry Paulson wrote: A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it says ‘constant

### Re: [isabelle-dev] »real« considered harmful

. declare [[coercion of_nat :: nat ⇒ real]] term sqrt (2 :: nat) Today the output says sqrt (real_of_nat 2). But if there would be no abbreviation for of_nat :: nat ⇒ real, how would you deduce the type of the coercion. Dmitriy On 24.06.2015 16:01, Manuel Eberl wrote: On 24/06/15 15:55, Larry

### Re: [isabelle-dev] Euclidean Ring

On 27/06/15 09:06, Florian Haftmann wrote: What about: »a = unit_factor a * normalize a« Sounds reasonable. I still had the hope that it would be possible to develop an abstract specification for gcd which would form a lattice: »gcd a a = a«. But now I cam to realize that for Gcd :: 'a set =

### Re: [isabelle-dev] Infix syntax for division?

I also vote for b). I would also like to add that I ran into situations where I required the notation of an inverse element in a ring. I defined this as ring_inv x = 1 div x. For instance, on int, we have ring_inv 1 = 1 and ring_inv (-1) = -1 and everything else is basically ill-defined, because 1

### Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode

I think the main (and only) problem is that it uses significantly more memory. On 28/05/15 11:21, Peter Lammich wrote: Hi list, When I start Isabelle, I get the following warning message on the console: ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using

### Re: [isabelle-dev] the function "real"

your help in getting some things working in the AFP. Larry On 10 Nov 2015, at 17:53, Manuel Eberl <ebe...@in.tum.de> wrote: This is very nice to hear. ‘real’ has plagued me for some time now and I am glad to see it gone. Thanks for the good work! On 10/11/15 17:45, Lawrence Paulson wrote:

### Re: [isabelle-dev] NEWS: 'consider' command and "cases" method

Ah, interesting. Thanks! On 23/09/15 08:47, Andreas Lochbihler wrote: > Dear Manuel, > > consider supports the same syntax as obtains, i.e., you can use "where" > as in > > consider "x = ∞" | "x = -∞" | y where "x = ereal y&quo

### Re: [isabelle-dev] NEWS: 'consider' command and "cases" method

Is there a way to use ‘consider’ with fixed variables? E.g. if I have a rule like ereal_cases: (⋀r. x = ereal r ⟹ thesis) ⟹ (x = ∞ ⟹ thesis) ⟹ (x = - ∞ ⟹ thesis) ⟹ thesis I would like to write consider "x = ∞" | "x = -∞" | "x = ereal x'" for x' But that syntax is not

### Re: [isabelle-dev] Towards the release

I completed the merge I mentioned in my previous email. Everything went into Multivariate_Analysis, apart form Nonpos_Ints and Periodic_Fun, which went into Library. I'm running tests overnight to make sure I did not break anything. Manuel On 01/01/16 20:50, Manuel Eberl wrote: I still

### Re: [isabelle-dev] Towards the release

I still have a few thousand lines of stuff to merge into the distribution, most notably the definition of the radius of convergence of a series and a number of convergence tests. This would be nice to have in the distribution because two results of mathematical importance rest upon it: the

### Re: [isabelle-dev] Towards the release

Ah yes, I completely forgot about that. Will do. On 05/01/16 14:27, Makarius wrote: On Mon, 4 Jan 2016, Manuel Eberl wrote: I completed the merge I mentioned in my previous email. Fine. This is Isabelle/b0f941e207cf. Do you want to write an entry for NEWS and CONTRIBUTORS? Makarius

### Re: [isabelle-dev] find_theorems and type class axioms

This particular issue has, in fact, annoyed me a great deal. I needed the ‘dist_norm’ lemma a lot lately and was never able to find it with ‘find_theorems’, which was very frustrating. I eventually found it by reading a proof that used it somewhere. I did not think much of it at the time, but

### Re: [isabelle-dev] Immediate completion does not work anymore

Lars just informed me that I didn't actually include an example in my mail (I thought I did); it was therefore probably not clear what I meant exactly, so let me explain: When I write "\ci" in a theory, it used to be completed to ∘ immediately. As of 1ca11ddfcc70, this does not happen

### [isabelle-dev] Immediate completion does not work anymore

As of the following revision, immediate completion does not work anymore in Isabelle/JEdit: changeset: 61600:1ca11ddfcc70 user:wenzelm date:Sat Nov 07 16:05:28 2015 +0100 summary: clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1); From the

### Re: [isabelle-dev] Isabelle2016-RC0: potential changes

I already moved a few small lemmas. I also defined the notion of an algebraic number; as soon as your AFP entry works with the development version of Isabelle again (is that already the case?), I will prove equivalence of my definition in Poly_Deriv.thy to your definition in Algebraic_Numbers

### Re: [isabelle-dev] Isabelle2016-RC0: potential changes

I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number. Oh, yes, you're right. It's in https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy . Its definitely not optimal, and

### Re: [isabelle-dev] Isabelle2016-RC0: potential changes

thanks a lot; in the meantime, I deleted this material from the AFP-entries. Ironically, quite a few of those facts were already proven independently in other AFP entries by Wenda Li and/or me. (e.g. the ones about pcompose) > So why should the small proof below be not integrated for the

### Re: [isabelle-dev] HOL-Codegenerator_Test error

I tried to trace this issue and I am really confused now. The problem is apparently the following code equation I added for "binomial" at the end of Binomial.thy: lemma binomial_code [code]: "(n choose k) = (if k > n then 0 else if 2 * k > n then (n choose (n - k)) else

### Re: [isabelle-dev] AFP status

I already have Sturm_Tarski running again and will commit that later today. On a related note, in faf1aa9381e0, I also removed the definition of "algebraic" from Algebraic_Numbers and updated it to use the more general definition of "algebraic" that is now in the library. Cheers, Manuel

### Re: [isabelle-dev] HOL-Codegenerator_Test error

There are actually several affected functions: Discrete.sqrt size_fset lapprox_posrat size_multiset set_encode card_UNIV_fun card_UNIV_set card_UNIV_finfun I have no idea what causes this and why my changed affected it. I also do not have the faintest idea what I could possibly do to fix it.

### Re: [isabelle-dev] HOL-Codegenerator_Test error

I commented out the code equation in question and HOL-Codegenerator_Test runs through again. Manuel On 12/01/16 15:31, Makarius wrote: On Tue, 12 Jan 2016, Manuel Eberl wrote: From what I have seen so far, it seems like there are some lingering issues with code generation in general

### Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

ave compared it with the MyRat implementation by Manuel Eberl https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski b11e8139b880 (where a comment says that it goes back to John Harrison). Further comments? Anyt

### Re: [isabelle-dev] Proper sign of gcd / lcm on type int

Florian has already hinted at it, but I will say it again explicitly: Mathematically, gcd and lcm are not operations on the elements of a ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual divisibility). In fact, these equivalence classes form a complete lattice w.r.t.

### Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

om of these problems! All of these texts were copied from HOL Light. I can fix them sometime tomorrow, or feel free to do it yourself if you prefer. --lcp On 15 Jun 2016, at 21:17, Manuel Eberl <ebe...@in.tum.de> wrote: There is one instance in Extension.thy where you wrote "real ^ n&

### Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

There is one instance in Extension.thy where you wrote "real ^ n" in a subsection heading about Urysohn's lemma. That causes an error when interpreted as LaTeX code. I suggest replacing it with "Euclidean space", which is more apt in Isabelle anyway, I should think. There are two more

### Re: [isabelle-dev] AFP config files?

This is my entry. I submitted it a few days ago, and I included the config file in my submission. I was not aware that those don't exist anymore. On 23/06/16 09:49, Florian Haftmann wrote: Dear AFP maintainers, in 79fb78da1ef0 there exists exactly one file named "config", namely

### Re: [isabelle-dev] Scala implicits

The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used to break Codegenerator_Test. I can have a look later to see whether this is still the case. If it is not, we should probably proceed to move some more of René Thiemann et al's efficient code equations from the AFP to the

### Re: [isabelle-dev] Scala implicits

Looks good. After applying the patch, HOL-Codegenerator_Test goes through with the code equation in Binomial.thy enabled. Cheers, Manuel On 23/06/16 09:48, Manuel Eberl wrote: The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used to break Codegenerator_Test. I can have

### Re: [isabelle-dev] Scala implicits

Florian, what are you plans w.r.t. merging this patch into the distribution? Manuel On 23/06/16 11:22, Manuel Eberl wrote: Looks good. After applying the patch, HOL-Codegenerator_Test goes through with the code equation in Binomial.thy enabled. Cheers, Manuel On 23/06/16 09:48, Manuel

### Re: [isabelle-dev] Isabelle2016-RC0: potential changes

I added the efficient code equations for fact and binomial, and similar ones for pochhammer and gbinomial. I also adapted everything from Square_Free_Factorization and Missing_Polynomial that seemed to be of general interest to me (especially the generalisation of the type of pderiv). I

### Re: [isabelle-dev] HOL-Codegenerator_Test error

It looks like I'm the one who broke it. It does not work after my commit 3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately before. I have no idea what causes this problem. Maybe one of our resident code generator experts could comment on it? I'll try to find out which

### [isabelle-dev] Regression in Approximation – Does this belong into NEWS?

As of 67792e4a5486, I fixed a regression in the ‘approximation’ decision procedure that was introduced with Isabelle2015: approximating terms containing ‘powr’ did not work anymore due to the changed definition of ‘powr’. It works again now and I was wondering whether this kind of thing

### Re: [isabelle-dev] buildall inconsistency

ed entries are in dire need of a major cleanup. Echelon_Form/Rings2 in particular contains a lot of interesting material. Cheers, Manuel On 28/02/16 15:45, Lawrence Paulson wrote: Looks like valuable work even if it caused some disruption. Larry On 28 Feb 2016, at 13:32, Manuel Eberl <ebe...@in.

### Re: [isabelle-dev] Factorial ring

"multiplicity" is definitely interesting; we could then probably define the "order" of a root of a polynomial in terms of "multiplicity", which simplifies things a bit. I don't see why is_prime should require an algebraic_semidom; the definition of prime elements makes sense in any

### Re: [isabelle-dev] Factorial ring

ith Euclidean rings) in a way that works well in practice and see where that leads us. Manuel On 11/03/16 13:39, Tjark Weber wrote: Florian, On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote: "multiplicity" is definitely interesting [...] I don't see why is_prime shoul

### Re: [isabelle-dev] Isabelle repository broken

Argh! You are correct. Today is /not/ my day. I'm on it. On 24/05/16 18:42, Makarius wrote: On 24/05/16 18:34, Manuel Eberl wrote: I'm confident that I'll have everyting up and running again soon. BTW, current Isabelle/8230358fab88 now looks like too much has been committed

### Re: [isabelle-dev] Isabelle repository broken

Yes, this was my fault. The problem was that I stupidly forgot to commit my changes before I pushed to the testboard and thus did not see the problems caused by my changes. I'm confident that I'll have everyting up and running again soon. Manuel On 24/05/16 17:22, Jasmin Blanchette wrote:

### [isabelle-dev] NEWS: Primes

*** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" function, the "factorial_ring" typeclass with instance proofs for nat, int, poly. * Probability: Code generation and QuickCheck for Probability Mass

### Re: [isabelle-dev] Multiset insert

I've been using multisets quite a bit myself lately. add# and add1# both sound all right to me. I would also like to point out that for some reason, intersection and union are #∪ and #∩, whereas all other multiset operations seem to have the # at the end (e.g. ⊆#). Unless there is some deeper

### Re: [isabelle-dev] NEWS: Primes

Yes, that might be a good idea. On 27/07/16 11:24, Tobias Nipkow wrote: Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible

### Re: [isabelle-dev] Theory for discrete log etc.

There's also natlog2 in src/HOL/Analysis/Summation_Tests.thy, which I introduced because I didn't know about the other ones. Manuel On 13/08/16 15:09, Florian Haftmann wrote: Hi all, after studying 28d1deca302e I realized that we have now two theories dealing with discrete functions (with

### Re: [isabelle-dev] multiplicity and prime numbers

But is it possible to adapt all lemmas accordingly? I could imagine that some statements use the fact that the support of multiplicity are the prime numbers. Not really. Some facts will still require the primality assumption, e.g. lemma prime_multiplicity_mult_distrib: assumes "is_prime_elem

### [isabelle-dev] multiplicity and prime numbers

Hallo, as some of you may already know, I am currently in the process of resructing Isabelle's definitions of prime numbers. Before these changes, we had the concept of "multiplicity". This was defined to be the multiplicity of a prime factor in the prime decomposition of a natural number or

### Re: [isabelle-dev] multiplicity and prime numbers

sure that there is no standard definition of this concept in mathematics that we should follow? Tobias On 19/07/2016 12:03, Manuel Eberl wrote: Hallo, as some of you may already know, I am currently in the process of resructing Isabelle's definitions of prime numbers. Before these changes, we ha

### [isabelle-dev] Broken AFP

Hallo, sorry for the broken AFP – it's my fault, but I added a lot of new material about rings and prime factor decomposition. The projects that were affected by this the most are already fixed, and I will take care of the rest on Monday. Manuel

### Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

I've heard of negative thermal expansion in some materials, but I don't think RAM is subject to it. (scnr) In a more serious fashion: I don't see how ambient temperature could affect memory usage. I've run into "insufficient memory" and stack overflow problems in Isabelle several times

### Re: [isabelle-dev] The Great Picard Theorem

I'm not an expert in complex analysis either, but do remember that it was briefly mentioned – but not proved – in my introductory lecture on Complex Analysis when I was an undergratuate. My intuition tells me that this is a very beautiful result, but not one that you need a lot, but I could be

### Re: [isabelle-dev] not-exists problem

The desired multi-variable semantics of ∄ seem obvious enough to me and I think that this should be allowed. For ∃!, the implicit complexity introduced by the pairing seems too much to me, so I think this should be forbidden. On 13/09/16 10:41, Johannes Hölzl wrote: There is even a third

### Re: [isabelle-dev] Fisher–Yates in AFP

I've never used SourceTree, and it is, of course, very difficult to debug such things from afar. I could of course, with your permission, simply commit and push the entry myself. Cheers, Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de

### Re: [isabelle-dev] Fisher–Yates in AFP

Oh, that is quite possible. Sorry about that. I typically keep my prospective AFP entries in private HG repositories and then simply tarball and submit them when it's time. I don't think that ever was a problem before, but it sounds like the most reasonably explanation so far. Good catch!

### [isabelle-dev] Of lazy lists and friendly corecs

Hallo, I've been playing around with corec and friends in combination with the lazy lists from "$AFP/Coinductive/Coinductive_List" and encountered the following problem: Suppose I want a function that takes two (implicitly sorted) lazy lists and merges them in the following fashion:

### Re: [isabelle-dev] Jenkins maintenance

I have decided to add my own opinions to this debate. My knowledge of the old testing system is limited, but I hope my perspective will still hold some interest. First of all, a usable testing infrastructure does not grow overnight by itself. Someone has to put in a lot of time and effort to make

### Re: [isabelle-dev] Problem with factorial-ring in combination with containers

This is a problem that I have given quite some thought in the past. The problem is the following: You have a theory A providing certain operations on sets (in this case: Gcd) and a theory B providing implementations for sets (in this case: Containers). The problem is that the code equations for

### Re: [isabelle-dev] Problem with factorial-ring in combination with containers

are done at all at > the moment. > > Manuel's suggestion of code_abort is a bit cleaner than René's use > Code.abort, because Code.abort does not work with normalisation by > evaluation whereas code_abort does. > > Best, > Andreas > > > On 03/10/16 15:29

### Re: [isabelle-dev] Jenkins maintenance

This, too, is an industry standard. Of course, I am not the expert, but I'm pretty sure this is achievable with the system we have – if there is a consensus that this is what we want, that is. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de

### Re: [isabelle-dev] Problem with factorial-ring in combination with containers

lt value is that the > finiteness test remains inside the implementation library B whereas with > Finite_Set.fold, the finiteness test must be done whenever one wants to > use the combinator. So this might be an argument in favour of fold_default. > > Andreas > > On 03/1

### [isabelle-dev] Old_Number_Theory

I am glad to announce that as of261d42f0bfac, Old_Number_Theory is finally history. A lot of the proofs are still quite messy and don't take advantage of the new features we now have in Number_Theory (such as a uniform concept of ‘primes’ and ‘prime factorisations’ for both nat and int), but

### Re: [isabelle-dev] Old_Number_Theory

One remark on the diff: + src/HOL/Number_Theory/QuadraticReciprocity.thy + src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy This is a formal regression: a proper name has turned into CaMlCaSe. But that should be easy to correct. Ah indeed. Jaime probably didn't know about the naming

### Re: [isabelle-dev] Old_Number_Theory

with what we have for analysis. I blame John Harrison :-) Larry On 18 Oct 2016, at 12:11, Manuel Eberl <ebe...@in.tum.de <mailto:ebe...@in.tum.de>> wrote: I am glad to announce that as of261d42f0bfac, Old_Number_Theory is finally history. A lot of the proofs are still quite mes

### Re: [isabelle-dev] Towards the release

I for one am hoping to be able to get rid of the Old Number Theory before the release. All that is left to do is actually to adapt some theories of the ported theories to my recent changes concerning prime numbers, so I think I should be able to take care of that next week. Cheers, Manuel On

### [isabelle-dev] Changed theory merge behaviour

During a minor overhaul of some theories in the distribution, I discovered some problems with theory imports. Apparently, the theory merge behaviour changed in one of the most recent commits. I haven't been able to pin down which one it is exactly; I might do a bisection later if needed. In

### [isabelle-dev] SQLite-related error in testboard-afp job

There was an odd error in a testboard-afp job [1] before: 17:26:32 ### Ignoring bad database: "$ISABELLE_HOME/heaps/$ML_IDENTIFIER/log/HOL-Library.db" 17:26:32 ### [SQLITE_ERROR] SQL error or missing database (no such table: isabelle_session_info) […] 17:32:12 *** [SQLITE_ERROR] SQL error or

### Re: [isabelle-dev] The coming release of Isabelle2017

On 2017-07-05 22:09, Manuel Eberl wrote: > I still want to take care of two really tiny things: […] and the proper > printing > of "nat" values as numerals instead of successor notation. This is now done as of adf3155c57e2. I should note that I was somewhat imprecise, b

### Re: [isabelle-dev] Efficient code for Discrete.log

me reasonably large n. > > Cheers, > René > > PS: Unfortunately, Sqrt_Babylonian.log_floor and log_ceiling are not > connected to Discrete.log. > >> Am 29.06.2017 um 15:29 schrieb Manuel Eberl <ebe...@in.tum.de>: >> >> Hallo, >> >> I'm

### Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

omplex_Main think about that. Manuel On 2017-06-30 16:52, Tobias Nipkow wrote: > > On 30/06/2017 16:39, Manuel Eberl wrote: >> I do understand that argument, but I am not sure if >> Topological_Spaces.subseq is really used /that/ often. Actually, >> going one step furth

### Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

On 2017-06-30 20:33, Sebastien Gouezel wrote: > I used subseq quite heavily in my ergodic theory developments. From > a mathematician point of view, taking subsequences of sequences > from nat to nat is very common and very useful in analysis (much > more than taking subsequences of lists). So

### Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

ymbol. > It would be nice if non-quaified names could be found for this case. > > Tobias > > On 30/06/2017 16:14, Lawrence Paulson wrote: >> Indeed we do. >> Larry >> >>> On 28 Jun 2017, at 18:49, Manuel

### [isabelle-dev] Efficient code for Discrete.log

Hallo, I'm considering adding efficient code for Discrete.log (the dual logarithm on natural numbers). PolyML does provide an IntInf.log2 function that seems reasonably efficient so that one can set up code printing. However, I am struggling with one detail: Where would the code that does this

### Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

Yes, I noticed that as well. I decided to leave it that way since, well, we do have qualified names. If anybody has better suggestions, I am open to implementing them. Manuel On 2017-06-28 17:05, Andreas Lochbihler wrote: > Dear all, > > While porting some of my theories to the current

### Re: [isabelle-dev] The coming release of Isabelle2017

code_post rules to rewrite successor notation to numerals is a lot better than what we have at the moment. Manuel On 2017-07-05 21:45, Lawrence Paulson wrote: > What’s the idea here? > Larry > >> On 5 Jul 2017, at 21:09, Manuel Eberl <ebe...@in.tum.de> wrote: >> >

### Re: [isabelle-dev] The coming release of Isabelle2017

I still want to take care of two really tiny things: the "subseq" situation and the proper printing of "nat" values as numerals instead of successor notation. Just mentioning that for the sake of completeness. Manuel On 2017-07-05 21:04, Makarius wrote: > Dear all, > > we are now almost 7

### Re: [isabelle-dev] NEWS: GCD and Binomial in Main

Before I forget: I did that and it is as expected; everything still works. Manuel On 2017-04-25 11:12, Florian Haftmann wrote: Am 25.04.2017 um 11:06 schrieb Manuel Eberl: I think you actually solved that problem by now. If I recall correctly, it was one of the two dictionary-related

### [isabelle-dev] Sporadic build failure of HOL-Probability in 16a8991ab398

Hallo, I just had a strange build failure with HOL-Probability. I executed manuel@colosson ~/.i/etc> isabelle-dev build -d '$AFP' Random_BSTs Euler_MacLaurin Bertrands_Postulate and HOL-Probability failed to build: Building HOL-Probability ... HOL-Probability FAILED (see also

### Re: [isabelle-dev] NEWS: GCD and Binomial in Main

I think you actually solved that problem by now. If I recall correctly, it was one of the two dictionary-related problems I told you about a year ago or so, and then Lars and you solved that problem somehow. I can try putting in that code equation again and seeing what happens. >> (*TODO: This

### [isabelle-dev] [158c513a39f5] JVM crash

Hallo, on 158c513a39f5, I just had a JVM crash during "isabelle build" when it was building Isabelle/Scala. (Log attached). When I did "isabelle build" again, it proceeded to build the Pure session without problems. However, when I then tried to build HOL-Computational_Algebra, it stopped and

### Re: [isabelle-dev] [158c513a39f5] JVM crash

The following seems to be the most reliable way to trigger the problem: while true isabelle build -b -c Pure end I did that and about 6% of builds with Scala 2.12.3 failed with something like the attached log. I then tried the same thing with Scala 2.12.2 (double-checked "isabelle scala

### Re: [isabelle-dev] Build Problem in JinjaThreads

That was due to my reforms of the sublist/subseq stuff and should be repaired by this afternoon. Tomorrow's slow tests should run through fine again. Unfortunately, these slow sessions don't have the same rapid testing cycle as the normal sessions. Manuel On 2017-06-01 16:19, Florian

### Re: [isabelle-dev] Towards the Isabelle2017 release

On 2017-08-24 17:34, Florian Haftmann wrote: > I would still appreciate if someone would take the comment »Deviates > from the definition given in the library in number theory« as a starting > point to reconcile that definition with src/HOL/Number_Theory/Totient.thy. Oh actually I fixed that a

### Re: [isabelle-dev] Towards the Isabelle2017 release

Purely out of interest: Does this also hold for filters? Manuel On 2017-08-24 20:54, Viorel Preoteasa wrote: > I have now a file with the new class, and all necessary proofs > (both distributivity equalities, bool, set, fun interpretations, > proofs of the old distributivity properties). > > I

### Re: [isabelle-dev] [158c513a39f5] JVM crash

> If you still have that, can you send it to me? Sure. > Since the JVM crash happened during scalac compilation, I recommend to > enforce a fresh build, e.g. like this: That seems to have worked. The only output I got was this: ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ...

### Re: [isabelle-dev] [158c513a39f5] JVM crash

) So, all in all, my money would be on the JVM. Manuel On 19/08/17 21:04, Makarius wrote: > On 19/08/17 20:31, Manuel Eberl wrote: >>> If you still have that, can you send it to me? >> >> Sure. >> >>> Since the JVM crash happened during scalac compilation, I

### Re: [isabelle-dev] [158c513a39f5] JVM crash

Okay I have no idea what is going on anymore. I know have the following new data points: – 2500 iterations on my Intel Core i7 laptop. No failures. So it must be the Ryzen issue after all, I thought. I recalled that some people said the problem was less pronounced with SMT disabled, so I

### Re: [isabelle-dev] [158c513a39f5] JVM crash

that solved whatever issue I was having, and, of course, it took a reboot for it to kick in. On 20/08/17 14:14, Manuel Eberl wrote: > Okay I have no idea what is going on anymore. > > I know have the following new data points: > – 2500 iterations on my Intel Core i7 laptop. No failures. >

### Re: [isabelle-dev] [158c513a39f5] JVM crash

kernel within the last few > weeks that solved whatever issue I was having, and, of course, it took a > reboot for it to kick in. > > On 20/08/17 14:14, Manuel Eberl wrote: >> Okay I have no idea what is going on anymore. >> >> I know have the following new data poi

### [isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

Is it intentional that the "Computational_Algebra" theory does not import "Polynomial_Factorial"? Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

### Re: [isabelle-dev] [158c513a39f5] JVM crash

to make it considerably less frequent; however, only in Poly/ML 5.7.1 does it appear to not happen at all no matter how I run it. Does Poly/ML 5.7.1 contain any changes that could plausibly cause this bad behaviour to go away? Manuel On 2017-11-07 09:51, Manuel Eberl wrote: > It seems l

### Re: [isabelle-dev] [158c513a39f5] JVM crash

> If these crashes are happening at the end of the build process I would > suspect that it is something to do with either the data sharing or > writing out the heap image. Does writing out of the heap happen also when I just do "isabelle build Pure" as opposed to "isabelle build -b Pure"? Because

### Re: [isabelle-dev] Slow builds due to excessive heap images

If there are fixed-size integers in ML that raise an exception on overflow, it should be possible to just do appropriate code_printing setup similar to what Code_Target_Numeral does. We already have to somehow magically map Isabelle's "int" type to ML's "IntInf" type, so all we have to do is to

### Re: [isabelle-dev] [158c513a39f5] JVM crash

Is there an easy way to disable that for testing purposes? Some line I have to remove from a .scala file or something? Manuel On 2017-11-08 15:44, Makarius wrote: > On 08/11/17 15:39, Manuel Eberl wrote: >>> If these crashes are happening at the end of the build process I would