Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)

I have also upgraded and I find that everything still works the same as before. The only restriction on an unsigned application is that the first time you open it, you need to select the “open” menu item rather than simply double-clicking on some file. Then you need to confirm that you want the

Re: [isabelle-dev] Broken AFP sessions

It’s a bit mysterious. On Monday I got a failure message from the AFP and checked the status page. Four entries were shown as not working. I’ve tried them on my own machine (no matter precisely which version of the sources I had, it certainly had that simprule change, which I had made myself)

[isabelle-dev] real, of_nat and Suc

As has been discussed previously, our setup of injections among numeric types is chaotic. In particular, we have the function of_nat, which maps 0 and Suc to their equivalents on types that are supersets of the natural numbers. We have another function called real, which is overloaded from a

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

Is there a consensus that there is a problem with this notation? Having no special syntax might work, especially with jEdit, where one can click on an unexpected constant to see what it refers to. Larry > On 22 Sep 2015, at 15:21, Florian Haftmann >

Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]

Like, next week I do want to try to unify of_nat and real. Larry > On 22 Sep 2015, at 15:39, Tobias Nipkow wrote: > > I would prefer to leave things as they are now. That print translation is ok > and you would be moving the complications elsewhere. We really have more >

Re: [isabelle-dev] ML equality types

I can't see any specific benefit of doing this. I still think that the next big project of this kind should be to sort out the real/of_nat mess. I’ve proposed an approach to doing it, but haven’t yet found a sufficient block of time in which executed. Larry > On 10 Sep 2015, at 11:31, Florian

Re: [isabelle-dev] NEWS

Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory. Larry > On 10 Sep 2015, at 12:34, Tobias Nipkow wrote: > > > On 10/09/2015 12:19, Dmitriy Traytel wrote: >> Hi Florian, >> >> while I very much

Re: [isabelle-dev] status (AFP)

The error is as follows: *** Undefined fact: setsum_bounded (line 286 of /mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy) *** At command using (line 286 of /mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy”) Yes, I renamed this theorem to

[isabelle-dev] testboard

I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main

[isabelle-dev] The following files are required to resolve theory imports

I frequently look at finished theories when looking for useful theorems. But I’ve noticed a new and undesirable behaviour: I get the message The following files are required to resolve theory imports” even though the theory is finished, and presumably has already been imported. Dismiss the

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

of float. I assume you meant: of_float :: float = 'a::field - Johannes Am Mittwoch, den 29.07.2015, 16:07 +0100 schrieb Larry Paulson: This is an unusual case, because this function is not even injective. I would prefer to reserve of_XXX for generic functions, like the existing ones

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

it to of_ereal. - Johannes Am Mittwoch, den 29.07.2015, 15:02 +0100 schrieb Larry Paulson: In recent work, I’ve seen again how tricky things are with coercions. We need “real” because it is already used in thousands of places and in many basic lemmas, but it can only do nat=real and int=real

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

, the biggest obstacle is likely to be occurrences of real :: int=real. Any explicit occurrences will immediately be flagged, and can be replaced by of_int. Views? Larry On 3 Jun 2015, at 12:23, Larry Paulson l...@cam.ac.uk wrote: The situation regarding coercions has become extremely untidy

[isabelle-dev] NEWS: Cauchy's integral theorem

Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem, ported from HOL Light There is much more that could be added here, assuming I don’t run out of energy! Larry ___ isabelle-dev mailing list

Re: [isabelle-dev] NEWS: Cauchy's integral theorem

On 28 Jul 2015, at 16:40, Makarius makar...@sketis.net wrote: On Tue, 28 Jul 2015, Larry Paulson wrote: Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem, ported from HOL Light There is much more that could be added here, assuming I don’t run

[isabelle-dev] Fwd: isabelle dist build failed

I pushed some changes on Monday, and although they seemed to go okay, I was looking out for problems. But I don’t know what this one signifies. Larry Begin forwarded message: From: Account Isatest isat...@lxbroy10.informatik.tu-muenchen.de Subject: isabelle dist build failed Date: 22 July

Re: [isabelle-dev] Deprecating legacy ASCII symbols?

, at least in the short term. Larry Paulson On 29 Jun 2015, at 23:23, C. Diekmann diekm...@in.tum.de wrote: Dear list, the following mail may contain a stupid idea. In HOL.thy, the conjunction (conj) is first introduced with the symbol. Later, the notation ∧ is introduced. In order to clean

Re: [isabelle-dev] NEWS: cases from goals

Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while. Larry On 26 Jun 2015, at 23:46, Makarius makar...@sketis.net wrote: * Proof method goals turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case.

Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

I took a look, and it all runs perfectly well, except here: show xs ∈ T⇩c ∧ ys ∈ T⇩c ∧ ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶ {x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c} (* The following proof step performs an exhaustive case distinction over

[isabelle-dev] Fwd: [isabelle] find_theorems and locales

forwarded message: From: Larry Paulson l...@cam.ac.uk Subject: Re: [isabelle] find_theorems and locales Date: 19 June 2015 16:22:53 BST To: Florian Haftmann florian.haftm...@informatik.tu-muenchen.de Cc: Bertram Felgenhauer bertram.felgenha...@googlemail.com, cl-isabelle-us...@lists.cam.ac.uk

Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

This does it nicely (20s): apply (simp add: T⇩c_def I⇩c_def) apply clarify apply (cases u; elim disjE; simp; blast) Larry On 25 Jun 2015, at 14:52, Larry Paulson l...@cam.ac.uk wrote: I took a look, and it all runs perfectly well, except here: show xs ∈ T⇩c ∧ ys

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

The first question is, do we need a prefix syntax for type constraints? My point was that the ability to write [:real:]of_nat k might be better than having to introduce and abbreviations such as real_of_nat, but this is not clear. The latter has the advantage that it is automatically

Re: [isabelle-dev] Remaining uses of defer_recdef?

a minimum, it is too hard: Alexander Krauss. Pattern minimization problems over recursive data types. ICFP 2008. Tobias On 10/06/2015 23:19, Larry Paulson wrote: We need to figure out how recdef does it. The minimum number of equations is mathematically fixed, so recdef must be using

Re: [isabelle-dev] Remaining uses of defer_recdef?

Absolutely, totally. We must go forward and not back. Larry On 11 Jun 2015, at 13:27, Tobias Nipkow nip...@in.tum.de wrote: On 11/06/2015 14:00, Makarius wrote: Is that just a question of which side of the river has greener grass? Function does a number of things very nicely, eg nested

Re: [isabelle-dev] Remaining uses of defer_recdef?

We need to figure out how recdef does it. The minimum number of equations is mathematically fixed, so recdef must be using conditional expressions or other tricks. Larry On 9 Jun 2015, at 23:07, Gerwin Klein gerwin.kl...@nicta.com.au wrote: I can confirm that, at least that side is simple.

Re: [isabelle-dev] Remaining uses of defer_recdef?

On 7 Jun 2015, at 07:38, Dmitriy Traytel tray...@in.tum.de wrote: I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: Thanks for investigating. But how do we explain this? Possibly “fun” insists on converting on creating

Re: [isabelle-dev] Remaining uses of defer_recdef?

I suggest looking for ways for users to avoid exponential blowup. Presumably this means avoiding deeply nested patterns in favour of conditional expressions in some cases. Such a formalisation might be easier to reason with too, who wants an induction rule with hundreds of cases? But coming up

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

My proposal of [: :] is suggestive of typing and should be good enough, considering that such “type casts” would seldom be necessary. Larry On 6 Jun 2015, at 16:06, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Conceivably we could introduce a prefix syntax for type

Re: [isabelle-dev] Remaining uses of defer_recdef?

Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy? Larry On 6 Jun 2015, at 16:11, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The reason for the continued existence

Re: [isabelle-dev] Remaining uses of defer_recdef?

On 6 Jun 2015, at 19:37, Tobias Nipkow nip...@in.tum.de wrote: You can always turn all patterns of the lhs into cases on the rhs and derive the individual equations as lemmas. You also need to derive an induction principle. I would rather keep recdef than do all that by hand. Are we

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

On 5 Jun 2015, at 22:22, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Why do we need abbreviations such as these? abbreviation real_of_nat :: nat \Rightarrow real” where real_of_nat \equiv of_nat abbreviation real_of_int :: int \Rightarrow real” where

Re: [isabelle-dev] Remaining uses of defer_recdef?

I’d be happy to see the complete phasing out of TFL. It’s had its day. It was always a tricky thing to maintain. I’m amazed that it still works despite all of the many fundamental changes to system APIs. Larry On 5 Jun 2015, at 21:42, Florian Haftmann

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

The situation regarding coercions has become extremely untidy, and I think it should be cleared up. We have four generic functions: of_nat :: nat \Rightarrow ‘a::semiring_1 of_int :: int \Rightarrow ‘a::ring_1 of_rat :: rat \Rightarrow ‘a:: field_char_0 of_real ::

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

Agree. And now real (fact k)” must never be used, now that “fact” is also generic. This reminds me of a current IDE limitation: there’s currently no way (as far as I know) to get the type of a nonvariable expression, such as fact k” above. Larry Paulson On 2 Jun 2015, at 19:18, Florian

[isabelle-dev] not working

Today I added some material about complex transcendental functions, and then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the latter. ~/isabelle/Repos/src/HOL: hg id bd773c47ad0b tip Larry val xml =

[isabelle-dev] Fwd: [isabelle] Changing definition of finprod

This sounds like a good proposal to me. Do we have time before the fork? Larry Begin forwarded message: From: Thiemann, Rene rene.thiem...@uibk.ac.at Subject: [isabelle] Changing definition of finprod Date: 17 April 2015 10:55:32 BST To: Cl-isabelle Users cl-isabelle-us...@lists.cam.ac.uk

Re: [isabelle-dev] NEWS: Z3 open source

I use “thm” all the time, especially to inspect theorems that are pre-built and therefore not open to inspection via hover-click directly. Larry On 15 Apr 2015, at 09:02, Gerwin Klein gerwin.kl...@nicta.com.au wrote: Despite such routine improvements, many users will probably just stick to

[isabelle-dev] NEWS: powr

* Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y = 0 by definition. INCOMPATIBILITY: type constraints may be necessary. But I had to remove support for powr in code generation and the approximation method. If anybody

Re: [isabelle-dev] NEWS: powr

several weeks from being finished, and I only need approximation for a small part that is independent from everything else. Manuel Larry Paulson l...@cam.ac.uk wrote: * Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y

Re: [isabelle-dev] NEWS: powr

All I know is that HOL-Codegenerator_Test failed because of some (?) type-related ambiguity connected with powr, with no indication of where this instance of powr actually was. Adding [code del] to its definition eliminated the error, God knows why. Larry On 12 Apr 2015, at 20:03, Florian

Re: [isabelle-dev] Multiset insert

Sounds logical to me. Larry On 8 Apr 2015, at 08:13, Tobias Nipkow nip...@in.tum.de wrote: Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and union. Although induction already has only two cases (empty and union with

Re: [isabelle-dev] HOL-Probability broken

Sorry, I overlooked this due to the many untracked files of the form *.prv. Wouldn’t it make sense to add this pattern to our .hgignore file? Larry On 18 Mar 2015, at 14:52, Makarius makar...@sketis.net wrote: On Tue, 17 Mar 2015, Larry Paulson wrote: I’ve pushed a correction

Re: [isabelle-dev] HOL-Probability broken

I’ve pushed a correction to that particular problem. I’ve no time to verify that there are no further problems. Sorry again. Larry On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote: In Isabelle/cd945dc13bec HOL-Probability is broken: *** Now trying to infer coercions globally.

Re: [isabelle-dev] HOL-Probability broken

Sorry, I don’t know how that one slipped through. I test on my own machine. Larry On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote: In Isabelle/cd945dc13bec HOL-Probability is broken: *** Now trying to infer coercions globally. *** *** Coercion inference failed: ***

Re: [isabelle-dev] sign_simps

I really don’t see the gain from getting rid of sign_simps, even if it is unsuccessful. Except for the occurrence linordered_field_class.sign_simps(41) in Multivariate_Analysis/Derivative.thy. Larry On 14 Feb 2015, at 10:32, Florian Haftmann

Re: [isabelle-dev] Mercurial failing as always

I see that the secret lies in the difference between .hgrc and .hg/hgrc (how silly of me) Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev