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

[Larry Paulson]

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 application to open.

It would certainly be nice to be able to open a theory file simply by 
double-clicking on it. A long time ago, I had this working by some low level 
hack, but I haven’t been able to reproduce it.

Larry

> On 13 Oct 2015, at 15:32, Makarius  wrote:
> 
> Apple has released OS X 10.11 (El Capitan) recently.
> 
> I have updated my test machine some days ago and made a few sanity checks. So 
> far the situation looks good concerning Isabelle. A test version is available 
> here: http://www4.in.tum.de/~wenzelm/test/Isabelle_07-Oct-2015
> 
> Are there further observations from full-time users of Mac OS X?
> 
> 
> We shall probably also shift our base-line of supported OS X versions from 
> 10.7 (Lion) to 10.8 (Mountain Lion).  See also 
> http://isabelle.in.tum.de/repos/isabelle/file/3c69ea85f8dd/Admin/PLATFORMS#l36
> 
> 
> Another note on the OS X "app": I've recently experimented with a current 
> fork of the JavaAppLauncher https://bitbucket.org/infinitekind/appbundler 
> that also supports file associations.  It somehow worked, but only after one 
> failed attempt to start the application for the very first time, probably due 
> to the lack of signed application.
> 
> In http://isabelle.in.tum.de/repos/isabelle/rev/9b4843250e1c I have reverted 
> this experiment -- users need to be able to start-up properly after a fresh 
> download of Isabelle.
> 
> If there is anybody who knows how to get this right, and maybe even has 
> official OS X developer credentials for signed application, we could try 
> again with the new launcher.
> 
> 
>   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] Broken AFP sessions

[Larry Paulson]

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) and three of 
the four ran perfectly. I fixed the fourth one by adding the obvious simp del: 
real_of_nat_Suc and that should have been that.

Now I’ve fixed these too.

Larry

> On 7 Oct 2015, at 08:33, Dmitriy Traytel  wrote:
> 
> Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is 
> now a simprule). Verified only for the Integral.thy failure.
> 
> Dmitriy
> 
> 
>> On 06 Oct 2015, at 23:19, Makarius  wrote:
>> 
>> Here are some more proof failures (Isabelle/5b5656a63bd6 and 
>> AFP/21bdf9fbf229):
>> 
>> Integration FAILED
>> *** At command "by" (line 1724 of 
>> "~/isabelle/afp-devel/thys/Integration/Integral.thy")
>> 
>> Markov_Models FAILED
>> *** At command "done" (line 1038 of 
>> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy")
>> *** At command "by" (line 1077 of 
>> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy")
>> 
>> Ordinary_Differential_Equations FAILED
>> *** At command "by" (line 804 of 
>> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
>> *** At command "by" (line 704 of 
>> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
>> 
>> 
>>  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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] real, of_nat and Suc

[Larry Paulson]

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 variety of different 
types and always yields a real; not all of these instances are even injections.

As a first step towards reconciling these, I looked into the problem that 
of_nat and real were not even simplified in the same way: of_nat (Suc n) was 
simplified by default whereas real (Suc n) was not. Under the impression that 
the latter behaviour was canonical, I tried removing the simprule status of 
of_nat_Suc. This turned out quite badly, and in particular, The function int 
(which seems to be analogous to real, but in fact is nothing but an 
abbreviation for of_nat) was then being simplified differently from before, and 
it’s quite difficult to justify why int (Suc n) should not be simplified in the 
obvious way.

So instead, real_of_nat_Suc is going to become a simprule. The only proofs 
where this caused a problem involved goals or even definitions that have been 
unwisely stated involving real (Suc n), rather than the obvious “real n + 1”.

Over the next week or two, I hope to get the chance to redefine real as an 
abbreviation for of_nat with the correct type, thereby putting it on exactly 
the same status as int.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 
>  wrote:
> 
> The »op •« is infamous. Whatever you wish instead (my personal favorite
> being no special syntax at all), problems include
> a) to detect unintended printing behaviour
> b) a suitable migration mechanisms
> 
> Concerning b), one you could imagine things like
> a) alternative declarations (infix(l/r)_new beside infix(l/r),
> infix(l/r) beside infix(l/r)_old)
> b) a flag to control the semantics of infix(l/r)
> c) a flag combined with a data slot to modify existing mixfix
> declarations afterwards also
> 
> Personally I would appreciate some move here, but this only makes sense
> if we agree what the goal is and whether it is worth the effort.
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> 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] Implicit eta-contraction during printing and product binders [was: NEWS]

[Larry Paulson]

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 
> important issues to work on.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] ML equality types

[Larry Paulson]

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 Haftmann 
>  wrote:
> 
> In src/Pure/library.ML, the signature still contains the discouraged and
> nowadays rarely used entries
>   
>   val equal: ''a -> ''a -> bool
>   val not_equal:  ''a -> ''a -> bool
> 
> Shall we attempt to get rid of them finally?
> 
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> 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] NEWS

[Larry Paulson]

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 welcome the simplified printing rules and your effort of
>> unifying case_prod/split, I am not sure if adding a third alternative name is
>> the way to go. The situation reminds me of the one depicted in [1].
>> 
>> Clearly, case_prod is the "right" name from the perspective of the 
>> (co)datatype
>> package.
> 
> Yes, we should return to that name in the end.
> 
> Tobias

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] status (AFP)

[Larry Paulson]

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 setsum_bounded_above, but I fixed it in 
afp/devel in the afternoon of 20 August. And committed and pushed my changes. 
Why this error still occurs, I have no idea.

Larry

 On 21 Aug 2015, at 12:31, Isabelle 
 isat...@macbroy2.informatik.tu-muenchen.de wrote:
 
 afp-test-devel-2015-08-21.log

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] testboard

[Larry Paulson]

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 repository 
somehow?

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 message, and it 
re-appears at least once more.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

Currently we have

definition
  of_real :: real ⇒ 'a::real_algebra_1 where
  of_real r = scaleR r 1

Maybe of_real could be done another way. 

And floats could be injected into the rationals.

Larry

 On 29 Jul 2015, at 16:34, Johannes Hölzl hoe...@in.tum.de wrote:
 
 Ah, I forgot about real 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.
 
 I now see that there is another case:
 
  real :: float = real
 
 This one is injective, and a properly generic function
 
  of_float :: real ⇒ 'a::real_algebra_1”
 
 looks easy to define.
 
 Larry
 
 On 29 Jul 2015, at 15:24, Johannes Hölzl hoe...@in.tum.de wrote:
 
 I'm fine with it. The only problem maight be that
 real :: ereal = real
 is overloaded in Extended_Real, which is quite often used in Probability
 theory. I can rename 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. If
 we are working more abstractly, only of_nat and of_int are general
 enough. It isn’t unusual to find both types of coercions in a single
 formula, and to make matters worse, their behaviour under
 simplification isn’t identical. But how can we fix this without
 breaking thousands of proofs?
 
 I have a suggestion based on the assumption that real :: int=real is
 almost never used. (I have previously removed overloading from other
 functions, and found essentially no uses of the integer version.) If
 this assumption is correct, we should be able to define real ::
 nat=real as an abbreviation for of_nat, so that the two functions are
 synonymous. Then we could eliminate the existing abbreviation
 real_of_nat. This should win all around: we keep the name “real”,
 which is more readable than “of_nat”, and get rid of the overloading.
 The effect on existing proofs should be modest, especially if we
 change things to ensure that of_nat is simplified exactly as real is
 now.
 
 Obviously, 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, 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 :: real \Rightarrow 'a::real_algebra_1
 
 With these functions, we can express practically all numeric conversions, 
 and they are based on algebraic principles. There is no need to introduce 
 quadratically many other functions for each possible combination of 
 source and target type. And yet we seem to done that. 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 real_of_int \equiv of_int
 
 abbreviation real_of_rat :: rat \Rightarrow real”
 where real_of_rat \equiv of_rat
 
 abbreviation complex_of_real :: real \Rightarrow complex
 where complex_of_real \equiv of_real
 
 And then why use overloading so that “real” redirects to one of those, 
 which in turn abbreviates one of the original four functions?  Note that 
 real x = of_nat x” is not an instance of reflexivity, but must be proved 
 using the definition real_of_nat_def. This definition is used 88 times in 
 our HOL development, and it’s also my direct experience of having two 
 different but equivalent coercions complicates proofs.
 
 We currently set up automatic coercions in Real.thy as follows:
 
 declare [[coercion of_nat :: nat \Rightarrow int]]
 declare [[coercion real   :: nat \Rightarrow real]]
 declare [[coercion real   :: int \Rightarrow real”]
 
 And then in Complex.thy as follows:
 
 declare [[coercion of_real :: real \Rightarrow complex]]
 declare [[coercion of_rat :: rat \Rightarrow complex]]
 declare [[coercion of_int :: int \Rightarrow complex]]
 declare [[coercion of_nat :: nat \Rightarrow complex”]]
 
 This latter version is the correct one, using just the primitive 
 coercions.
 
 I think that we should phase out all the derivative coercions in favour 
 of the primitive ones. I know that our complicated system arose by 
 accident, but it would not be that difficult to fix things.
 
 Larry
 
 On 3 Jun 2015, at 09:55, Fabian Immler imm...@in.tum.de wrote:
 
 I think I could live without real: coercions save a lot of the writing.
 Moreover, the real_of_foo abbreviations help

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

[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.

I now see that there is another case:

real :: float = real

This one is injective, and a properly generic function

of_float :: real ⇒ 'a::real_algebra_1”

looks easy to define.

Larry

 On 29 Jul 2015, at 15:24, Johannes Hölzl hoe...@in.tum.de wrote:
 
 I'm fine with it. The only problem maight be that
  real :: ereal = real
 is overloaded in Extended_Real, which is quite often used in Probability
 theory. I can rename 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. If
 we are working more abstractly, only of_nat and of_int are general
 enough. It isn’t unusual to find both types of coercions in a single
 formula, and to make matters worse, their behaviour under
 simplification isn’t identical. But how can we fix this without
 breaking thousands of proofs?
 
 I have a suggestion based on the assumption that real :: int=real is
 almost never used. (I have previously removed overloading from other
 functions, and found essentially no uses of the integer version.) If
 this assumption is correct, we should be able to define real ::
 nat=real as an abbreviation for of_nat, so that the two functions are
 synonymous. Then we could eliminate the existing abbreviation
 real_of_nat. This should win all around: we keep the name “real”,
 which is more readable than “of_nat”, and get rid of the overloading.
 The effect on existing proofs should be modest, especially if we
 change things to ensure that of_nat is simplified exactly as real is
 now.
 
 Obviously, 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, 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 :: real \Rightarrow 'a::real_algebra_1
 
 With these functions, we can express practically all numeric conversions, 
 and they are based on algebraic principles. There is no need to introduce 
 quadratically many other functions for each possible combination of source 
 and target type. And yet we seem to done that. 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 real_of_int \equiv of_int
 
 abbreviation real_of_rat :: rat \Rightarrow real”
 where real_of_rat \equiv of_rat
 
 abbreviation complex_of_real :: real \Rightarrow complex
 where complex_of_real \equiv of_real
 
 And then why use overloading so that “real” redirects to one of those, 
 which in turn abbreviates one of the original four functions?  Note that 
 real x = of_nat x” is not an instance of reflexivity, but must be proved 
 using the definition real_of_nat_def. This definition is used 88 times in 
 our HOL development, and it’s also my direct experience of having two 
 different but equivalent coercions complicates proofs.
 
 We currently set up automatic coercions in Real.thy as follows:
 
 declare [[coercion of_nat :: nat \Rightarrow int]]
 declare [[coercion real   :: nat \Rightarrow real]]
 declare [[coercion real   :: int \Rightarrow real”]
 
 And then in Complex.thy as follows:
 
 declare [[coercion of_real :: real \Rightarrow complex]]
 declare [[coercion of_rat :: rat \Rightarrow complex]]
 declare [[coercion of_int :: int \Rightarrow complex]]
 declare [[coercion of_nat :: nat \Rightarrow complex”]]
 
 This latter version is the correct one, using just the primitive coercions.
 
 I think that we should phase out all the derivative coercions in favour of 
 the primitive ones. I know that our complicated system arose by accident, 
 but it would not be that difficult to fix things.
 
 Larry
 
 On 3 Jun 2015, at 09:55, Fabian Immler imm...@in.tum.de wrote:
 
 I think I could live without real: coercions save a lot of the writing.
 Moreover, the real_of_foo abbreviations help to avoid type annotations:
 I suppose that all of the current occurrences of real could be replaced 
 with one particular real_of_foo.
 
 For reading (subgoals etc), one could perhaps think about less obstructive 
 abbreviations like e.g., real_N and real_Z, or real⇩N and real⇩Z.
 But I see that real_of_foo is much more uniform and you can immediately 
 read off the type foo.
 
 Fabian

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

[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. If we are working more 
abstractly, only of_nat and of_int are general enough. It isn’t unusual to find 
both types of coercions in a single formula, and to make matters worse, their 
behaviour under simplification isn’t identical. But how can we fix this without 
breaking thousands of proofs?

I have a suggestion based on the assumption that real :: int=real is almost 
never used. (I have previously removed overloading from other functions, and 
found essentially no uses of the integer version.) If this assumption is 
correct, we should be able to define real :: nat=real as an abbreviation for 
of_nat, so that the two functions are synonymous. Then we could eliminate the 
existing abbreviation real_of_nat. This should win all around: we keep the name 
“real”, which is more readable than “of_nat”, and get rid of the overloading. 
The effect on existing proofs should be modest, especially if we change things 
to ensure that of_nat is simplified exactly as real is now.

Obviously, 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, 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 :: real \Rightarrow 'a::real_algebra_1
 
 With these functions, we can express practically all numeric conversions, and 
 they are based on algebraic principles. There is no need to introduce 
 quadratically many other functions for each possible combination of source 
 and target type. And yet we seem to done that. 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 real_of_int \equiv of_int
 
 abbreviation real_of_rat :: rat \Rightarrow real”
  where real_of_rat \equiv of_rat
 
 abbreviation complex_of_real :: real \Rightarrow complex
  where complex_of_real \equiv of_real
 
 And then why use overloading so that “real” redirects to one of those, which 
 in turn abbreviates one of the original four functions?  Note that real x = 
 of_nat x” is not an instance of reflexivity, but must be proved using the 
 definition real_of_nat_def. This definition is used 88 times in our HOL 
 development, and it’s also my direct experience of having two different but 
 equivalent coercions complicates proofs.
 
 We currently set up automatic coercions in Real.thy as follows:
 
 declare [[coercion of_nat :: nat \Rightarrow int]]
 declare [[coercion real   :: nat \Rightarrow real]]
 declare [[coercion real   :: int \Rightarrow real”]
 
 And then in Complex.thy as follows:
 
 declare [[coercion of_real :: real \Rightarrow complex]]
 declare [[coercion of_rat :: rat \Rightarrow complex]]
 declare [[coercion of_int :: int \Rightarrow complex]]
 declare [[coercion of_nat :: nat \Rightarrow complex”]]
 
 This latter version is the correct one, using just the primitive coercions.
 
 I think that we should phase out all the derivative coercions in favour of 
 the primitive ones. I know that our complicated system arose by accident, but 
 it would not be that difficult to fix things.
 
 Larry
 
 On 3 Jun 2015, at 09:55, Fabian Immler imm...@in.tum.de wrote:
 
 I think I could live without real: coercions save a lot of the writing.
 Moreover, the real_of_foo abbreviations help to avoid type annotations:
 I suppose that all of the current occurrences of real could be replaced 
 with one particular real_of_foo.
 
 For reading (subgoals etc), one could perhaps think about less obstructive 
 abbreviations like e.g., real_N and real_Z, or real⇩N and real⇩Z.
 But I see that real_of_foo is much more uniform and you can immediately 
 read off the type foo.
 
 Fabian
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

I couldn’t possibly give a percentage. On the one hand, I would guess that most 
of Multivariate_Analysis comes from the HOL Light libraries. Maybe some of 
Probability as well, although originally it came from HOL4.

What I have just added is about the first 20% of the file cauchy.ml. The 
remaining 80% includes a development of winding numbers and quite a few other 
theorems. Probably most of them come from the famous list of 100 theorems. 
Other results, including the prime number theorem, are other files. None of 
these proofs are pretty. Puzzling them out is brain-bending.

Larry

 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 out of 
 energy!
 
 What is your estimate of the percentage of all material by John Harrison in 
 HOL-Light that has been ported to Isabelle/HOL already?
 
 
   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Fwd: isabelle dist build failed

[Larry Paulson]

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 2015 23:56:57 BST
 To: l...@cam.ac.uk
 
 Could not build isabelle distribution. Log file available at
 lxbroy10:/home/isatest/log/isatest-makedist-2015-07-23.log

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

It is interesting to look at competing systems and note that every one of them 
appears to be fully committed to a plain ASCII syntax as the only way of 
writing a formula. I think it may still be premature to abolish having ASCII 
even as an alternative syntax.

I wonder whether the appearance of HOL.thy is that important to a typical 
beginner. Although it sets out the basic logic, it is full of 
implementation-specific details. I don’t really see how having ∧ in place of  
would improve its legibility. Then allowing users to use the  symbol with some 
other meaning seems quite risky, 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 up
 this difficult-to-understand theory, would it be possible to directly
 introduce conjunction with the ∧ symbol? I see three advantages:
 
 1) It simplifies the axiomatizations (a very critical part).
 2) It may help in getting started with Isabelle since no confusing 
 symbol would appear anywhere. Currently, if a ctrl-click on a lemma
 sends me to HOL.thy, things look pretty scary.
 3) It would free up the symbol  for custom theories.
 
 This could also be done for %, --, ==, ~, and many more.
 
 I guess this would break a lot, that's why I'm posting on dev.
 
 Best,
  Cornelius
 ___
 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] NEWS: cases from goals

[Larry Paulson]

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.
 
 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.
 is marked as legacy, and will be removed eventually. Note that proof
 method goals achieves a similar effect within regular Isar.
 
 
 This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd proofs 
 are can be seen in changeset 7e741e22d7fc.
 
 
   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] Problem in AFP near 16e7d42ef7f4

[Larry Paulson]

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 
all traces and domains,
   and then can take long to be completed. *)
by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u,
 (((erule disjE)+)?, simp, blast?)+)

The comment doesn’t tell us whether to wait minutes or hours. Clearly this is a 
fragile step. Any sort of change could break this.

Larry

 On 25 Jun 2015, at 14:00, Florian Haftmann 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 isabelle: 19c277ea65ae tip
 afp: 16e7d42ef7f4 tip
 
 Running Noninterference_Generic_Unwinding ...
 *** Timeout
 Noninterference_Generic_Unwinding FAILED
 (see also
 /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
 
 val it = (): unit
 Loading theory GenericUnwinding
 Proofs for inductive predicate(s) rel_induct_auxp
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
 ### theory GenericUnwinding
 ### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
 
 Any hints what could have gone wrong?
 
   Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 ___
 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

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

[Larry Paulson]

Nobody has commented on this issue, and I would like to re-raise it, as it 
affects the development version.

It simply doesn’t make sense that fundamental axioms such as dist_norm are 
concealed from find_theorems. I imagine it would be very easy to change this 
behaviour.

Larry

 Begin 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
 
 I've stumbled across a related issue with find_theorems that certainly seems 
 wrong. I was searching for the theorem 
 Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type 
 class axiom here:
 
 class dist_norm = dist + norm + minus +
  assumes dist_norm: dist x y = norm (x - y)
 
 Calling find_theorems with suitable patterns, such as 
 
   dist norm (_-_)”
 
 does not return this theorem among the results, but clearly it should.
 
 Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 ∈ 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 
 all traces and domains,
   and then can take long to be completed. *)
by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u,
 (((erule disjE)+)?, simp, blast?)+)
 
 The comment doesn’t tell us whether to wait minutes or hours. Clearly this is 
 a fragile step. Any sort of change could break this.
 
 Larry
 
 On 25 Jun 2015, at 14:00, Florian Haftmann 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 isabelle: 19c277ea65ae tip
 afp: 16e7d42ef7f4 tip
 
 Running Noninterference_Generic_Unwinding ...
 *** Timeout
 Noninterference_Generic_Unwinding FAILED
 (see also
 /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
 
 val it = (): unit
 Loading theory GenericUnwinding
 Proofs for inductive predicate(s) rel_induct_auxp
 Proving monotonicity ...
 Proving the introduction rules ...
 Proving the elimination rules ...
 Proving the induction rule ...
 Proving the simplification rules ...
 ### theory GenericUnwinding
 ### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
 
 Any hints what could have gone wrong?
 
  Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 ___
 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 
introduced when the term has the matching type, and we would not want the 
pretty printer to insert [:real:] all over the place, but only when it is 
necessary.

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.

Larry

 On 23 Jun 2015, at 21:42, Makarius makar...@sketis.net wrote:
 
 On Sat, 6 Jun 2015, Florian Haftmann wrote:
 
 Conceivably we could introduce a prefix syntax for type constraints, e.g.
 
 [:real:]of_nat k
 
 I’d find such a thing useful from time to time.
 
 My personal favourite would be System-F-style type instantiation
 
  of_nat [real] k
 
 instead of type annotations but there are hardly any brackets left which
 could serve here.
 
 In theory we have an infinite store of Isabelle symbols, and many usable 
 Unicode points for rendering.  Here is a list of funny brackets to consider: 
 http://stackoverflow.com/questions/13535172/list-of-all-unicodes-open-close-brackets
 
 For example:
 
 U+2772 Ps LIGHT LEFT TORTOISE SHELL BRACKET ORNAMENT ❲
 U+2773 Pe LIGHT RIGHT TORTOISE SHELL BRACKET ORNAMENT ❳
 U+3014 Ps LEFT TORTOISE SHELL BRACKET 〔
 U+3015 Pe RIGHT TORTOISE SHELL BRACKET 〕
 
 
 In practice this also needs a LaTeX macro, and maybe some ASCII abbreviation 
 for input in the Prover IDE.
 
 
   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] Remaining uses of defer_recdef?

[Larry Paulson]

It looks like there is more work to do here then. Clearly the old package is 
doing something clever and we need to figure out what. Sadly, it probably isn’t 
worth a third Ph.D.
Larry

 On 11 Jun 2015, at 06:58, Tobias Nipkow nip...@in.tum.de wrote:
 
 Function and recdef work very differently. Function first disambiguates 
 the patterns, then it defines the graph of the function as an inductive 
 definition. Recdef turns the definitions into a single recursion equation 
 with case-expressions on the rhs.
 
 Concerning the minimum number of equations: neither definition facility finds 
 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 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.
 
 Tobias’ point about avoiding exponential blowup is important, though. Might 
 still be too early to retire recdef entirely if it is substantially better 
 for some kinds of definitions, esp if they are in use (I think the recdef 
 in Simpl is one of these).
 
 Cheers,
 Gerwin
 
 On 09.06.2015, at 11:27, Thomas Sewell thomas.sew...@nicta.com.au wrote:
 
 I've had a quick scan over the NICTA repositories. It doesn't look like
 there are any live original uses of recdef. There are recdefs in a copy
 of Simpl-AFP, and in some backups of historical papers.
 
 Short summary, NICTA doesn't have any stakes in recdef.
 
 Cheers,
   Thomas.
 
 On 08/06/15 06:13, Makarius wrote:
 On Sat, 6 Jun 2015, Gerwin Klein wrote:
 
 
 On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote:
 
 (2) 'defer_recdef' which is unused in the directly visible Isabelle
  universe.  So it could be deleted today.
 
 This mailing list thread is an opportunity to point out dark matter
 in the Isabelle universe, where 'defer_recdef' still occurs.
 Otherwise I will remove it soon, lets say within 1-2 weeks.
 
 Unused in our part of the dark matter universe as well.
 
 The thread has shifted over to actual 'recdef'. Are there remaining
 uses of 'recdef' in the NICTA dark matter?
 
 So far I always thought the remaining uses in HOL-Decision_Procs are
 only a reminder that there are other important applications.
 
 
   Makarius
 
 
 
 
 The information in this e-mail may be confidential and subject to legal 
 professional privilege and/or copyright. National ICT Australia Limited 
 accepts no liability for any damage caused by this email or its attachments.
 ___
 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
 
 
 ___
 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] Remaining uses of defer_recdef?

[Larry Paulson]

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 recursion and 
 partiality. That is worth taking on board.
 
 Tobias
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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.
 
 Tobias’ point about avoiding exponential blowup is important, though. Might 
 still be too early to retire recdef entirely if it is substantially better 
 for some kinds of definitions, esp if they are in use (I think the recdef in 
 Simpl is one of these).
 
 Cheers,
 Gerwin
 
 On 09.06.2015, at 11:27, Thomas Sewell thomas.sew...@nicta.com.au wrote:
 
 I've had a quick scan over the NICTA repositories. It doesn't look like
 there are any live original uses of recdef. There are recdefs in a copy
 of Simpl-AFP, and in some backups of historical papers.
 
 Short summary, NICTA doesn't have any stakes in recdef.
 
 Cheers,
   Thomas.
 
 On 08/06/15 06:13, Makarius wrote:
 On Sat, 6 Jun 2015, Gerwin Klein wrote:
 
 
 On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote:
 
 (2) 'defer_recdef' which is unused in the directly visible Isabelle
  universe.  So it could be deleted today.
 
 This mailing list thread is an opportunity to point out dark matter
 in the Isabelle universe, where 'defer_recdef' still occurs.
 Otherwise I will remove it soon, lets say within 1-2 weeks.
 
 Unused in our part of the dark matter universe as well.
 
 The thread has shifted over to actual 'recdef'. Are there remaining
 uses of 'recdef' in the NICTA dark matter?
 
 So far I always thought the remaining uses in HOL-Decision_Procs are
 only a reminder that there are other important applications.
 
 
   Makarius
 
 
 
 
 The information in this e-mail may be confidential and subject to legal 
 professional privilege and/or copyright. National ICT Australia Limited 
 accepts no liability for any damage caused by this email or its attachments.
 ___
 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] Remaining uses of defer_recdef?

[Larry Paulson]

 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 unconditional patterns only, 
while “recdef” allows conditional equations. But one could easily insert 
conditions manually in order to simplify the set of patterns. There are 14 
instances of recdef in Cooper.thy. Do any of them stand out as extra slow?

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 with simple guidelines for users might be tricky.

Larry

 On 7 Jun 2015, at 20:33, Florian Haftmann 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 As far as I know, this is due to layered architecture of the function
 package.  »recdef« does everything in one bunch and can hence optimize
 for sequential pattern matching.  Each layer of »function« must feed its
 result to its successor in a standardized form, and since there is no
 overall concept of sequential pattern matching, it has to be compiled
 away once and for all from the very beginning. (roughly spoken)
 
 An optimization would require a modified architecture.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 constraints, e.g.
 
  [:real:]of_nat k
 
 I’d find such a thing useful from time to time.
 
 My personal favourite would be System-F-style type instantiation
 
   of_nat [real] k
 
 instead of type annotations but there are hardly any brackets left which
 could serve here.
 
   Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 of recdef is that function can
 cause a combinatorial explosion the way it compiles pattern matches. I
 just tried Cooper.thy and changing one of the recdefs to function makes
 Isabelle go blue (purple) in the face until one gives up. Hardware alone
 will not solve that one.
 
 Now one could argue that since we need recdef, we should also keep the
 special variant defer_recdef, but if nobody speaks up for it, we don't
 have a proof that we really need it and it should go.
 
 At the time of their writing the recdef examples in (nowadays)
 src/HOL/Decision_Procs were the power applications of their times.
 
 Since then power applications have grown bigger and bigger and
 fun/function have been used widespread.  It seems strange to me that no
 application since then had never hit the same concrete wall again.
 
 So are there any experience reports that the combinatorial explosion in
 pattern matching in fun/function had to be worked around somehow?  Or do
 we have to conclude that the pattern complexity of the applications in
 src/HOL/Decision_Procs is indeed domain-specific?
 
   Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 ___
 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] Remaining uses of defer_recdef?

[Larry Paulson]

 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 talking about this definition?

recdef prep measure fmsize
  prep (E T) = T
  prep (E F) = F
  prep (E (Or p q)) = Or (prep (E p)) (prep (E q))
  prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))
  prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT 
q
  prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))
  prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))
  prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q (prep (E(And (NOT 
p) q)))
  prep (E p) = E (prep p)
  prep (A (And p q)) = And (prep (A p)) (prep (A q))
  prep (A p) = prep (NOT (E (NOT p)))
  prep (NOT (NOT p)) = prep p
  prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))
  prep (NOT (A p)) = prep (E (NOT p))
  prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))
  prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))
  prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))
  prep (NOT p) = NOT (prep p)
  prep (Or p q) = Or (prep p) (prep q)
  prep (And p q) = And (prep p) (prep q)
  prep (Imp p q) = prep (Or (NOT p) q)
  prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))
  prep p = p
  (hints simp add: fmsize_pos)

So what is recdef doing right that fun is doing wrong?

Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 real_of_int \equiv of_int
 
 abbreviation real_of_rat :: rat \Rightarrow real”
  where real_of_rat \equiv of_rat
 
 abbreviation complex_of_real :: real \Rightarrow complex
  where complex_of_real \equiv of_real
 
 The deeper reason why these have been introduced is that such
 conversions of type T = 'a::c can be difficult to write in presence of
 type ambiguities.  If you need more special types, you can do barely
 anything else than writing »(of_foo x :: T)« which clutters readability.

OK — but that’s no reason to introduce “real” as another way to write these 
coercions, while introducing precisely the sort of type ambiguity that is the 
root of such problems.

Conceivably we could introduce a prefix syntax for type constraints, e.g.

[:real:]of_nat k

I’d find such a thing useful from time to time.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 Cleaning up some obscure corners of the system, I've come across the old
 defer_recdef command.
 
 Are there any remaining uses of this historical relic?  I don't see any
 in the main Isabelle repository + AFP.
 
 Some years ago the idea was to let recdef stand as long as there are
 examples in the distribution.  The consequence would be to dismantle
 unused parts altogether.
 
 Further suggestios?
 
   Florian

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 :: real \Rightarrow 'a::real_algebra_1

With these functions, we can express practically all numeric conversions, and 
they are based on algebraic principles. There is no need to introduce 
quadratically many other functions for each possible combination of source and 
target type. And yet we seem to done that. 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 real_of_int \equiv of_int

abbreviation real_of_rat :: rat \Rightarrow real”
  where real_of_rat \equiv of_rat

abbreviation complex_of_real :: real \Rightarrow complex
  where complex_of_real \equiv of_real

And then why use overloading so that “real” redirects to one of those, which in 
turn abbreviates one of the original four functions?  Note that real x = 
of_nat x” is not an instance of reflexivity, but must be proved using the 
definition real_of_nat_def. This definition is used 88 times in our HOL 
development, and it’s also my direct experience of having two different but 
equivalent coercions complicates proofs.

We currently set up automatic coercions in Real.thy as follows:

declare [[coercion of_nat :: nat \Rightarrow int]]
declare [[coercion real   :: nat \Rightarrow real]]
declare [[coercion real   :: int \Rightarrow real”]

And then in Complex.thy as follows:

declare [[coercion of_real :: real \Rightarrow complex]]
declare [[coercion of_rat :: rat \Rightarrow complex]]
declare [[coercion of_int :: int \Rightarrow complex]]
declare [[coercion of_nat :: nat \Rightarrow complex”]]

This latter version is the correct one, using just the primitive coercions.

I think that we should phase out all the derivative coercions in favour of the 
primitive ones. I know that our complicated system arose by accident, but it 
would not be that difficult to fix things.

Larry

 On 3 Jun 2015, at 09:55, Fabian Immler imm...@in.tum.de wrote:
 
 I think I could live without real: coercions save a lot of the writing.
 Moreover, the real_of_foo abbreviations help to avoid type annotations:
 I suppose that all of the current occurrences of real could be replaced 
 with one particular real_of_foo.
 
 For reading (subgoals etc), one could perhaps think about less obstructive 
 abbreviations like e.g., real_N and real_Z, or real⇩N and real⇩Z.
 But I see that real_of_foo is much more uniform and you can immediately 
 read off the type foo.
 
 Fabian

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 Haftmann 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 For historic reasons, there is also the conversion real :: 'a ⇒ real
 which is overloaded and can be instantiated to arbitrary types. This
 (co)conversion works in the other direction without any algebraic
 foundation!
 
 My impression is that having this conversion is a bad idea.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] not working

[Larry Paulson]

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 =
   
[5:5:5:5:4:4.../4/:::.../:/:/4/::5:5.../5/::11
 0=179192 1=Nat.arity_type_nat.../11/:/5/:/5/::11 
0=370383 1=Int.arity_type_int:5:0 
0=HOL.type_class.../0/::0 
0=Pure.type.../0/:/5/::://:::/:/:0//:/:/11/:/5/::5:5:5:5.../5/::5.../5/:/5/::5:5.../5/::11
 0=370601 
1=Int.cr_int_def.../11/:/5/:/5/::5:5:5.../5/::5.../5/:/5/::5:5.../5/::5.../5/:/5/:/5/:/5/:/5/::5:5:5:5:5.../5/::5.../5/:/5/::5:5.../5/::11
 0=179192 
1=Nat.arity_type_nat.../11/:/5/:/5/::5:5:5.../5/::5.../5/:/5/::5:5.../5/::5.../5/:/5/:/5/:/5/::5:5:4:4.../4/:::.../:/:/4/::5:5.../5/::11
 0=179192 
1=Nat.arity_type_nat.../11/:/5/:/5/::5:5:4.../4/::5.../5/:/5/::5:5.../5/::5.../5/:/5/:/5/:/5/:/5/:/5]:
   Encode.body
val thm =
   Abs_Integ ?xa * Abs_Integ ?x =
Abs_Integ
 ((case ?xa of (x, y) = %(u, v). (x * u + y * v, x * v + y * u)) ?x):
   thm
### theory XML_Data
### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
*** exception Size raised (line 173 of ./basis/LibrarySupport.sml)
*** 
*** At command ML_val (line 59 of ~~/src/HOL/Proofs/ex/XML_Data.thy)
Unfinished session(s): HOL-Proofs-ex

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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
 
 Dear all,
 
 recently I started to formalize linear algebra results based on HOL-Algebra 
 (Matrices, Determinants, Eigenvalues, Gauss-Jordan-Elimination, …)
 
 while doing this I noticed a annoying difference between setprod and finprod 
 (or setsum and finsum):
 the set-based variants define the sum or product of an infinite set as the 
 neutral element, whereas finsum and finprod take „undefined“.
 
 To have more similarity between the two operators I propose to change the 
 definition of finprod from „undefined“ to 1 (which entails 0 for finsum).
 
 Then a lot of lemmas for finprod and finsum can be simplified where often the 
 assumption „finite A“ is now obsolete (and they more closely relate to 
 corresponding setprod and setsum lemmas).
 
 If this change is appreciated, then can someone please include the following 
 patch?
 It adapts all of HOL/Algebra to the change and also those entries of the AFP 
 which rely on HOL-Algebra still compile
 (Free-Groups Jordan_Hoelder Koenigsberg_Friendship Lehmer Matrix 
 Perfect-Number-Thm Secondary_Sylow Tarskis_Geometry VectorSpace)
 
 I tested everything with Isabelle 8614f8f0fb4b and AFP 7c57eabaad4b.
 
 Best regards,
 René
 


finprod.patch
Description: Binary data
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Larry Paulson]

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 
 old habits from the TTY age, and put the sledgehammer command into the text. 
 (Are there remaining uses of this ancient form? Or are there still pending 
 problems with the current Sledgehammer panel?)
 
 I don’t think such uses of essentially diagnostic commands should go away, 
 even if the corresponding panel works perfectly.
 
 I find typing in a diagnostic command usually much faster and less disruptive 
 of the workflow than finding a panel in a list of tabs, and using the mouse 
 to move focus there. Even though we have the very nice command-click for 
 theorems etc, I still find myself using the thm command semi-regularly, just 
 because I don’t want to pick up the mouse, or I want to leave in the command 
 to remind myself of something, or I want to see the theorem in the context of 
 where I’m trying to use it instead of were it is define.
 
 Sledgehammer is a slightly different case, because it often takes longer, but 
 even here I still sometimes prefer the text to the graphical interface when 
 I’m just using it to find a theorem.
 
 Panels are clearly better for beginners, and I do myself much appreciate them 
 for things I don’t do often, but I think we should continue to support both 
 modes of interaction so that people can do what suits their workflow best.
 
 Cheers,
 Gerwin
 
 
 
 
 The information in this e-mail may be confidential and subject to legal 
 professional privilege and/or copyright. National ICT Australia Limited 
 accepts no liability for any damage caused by this email or its attachments.
 ___
 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

[isabelle-dev] NEWS: powr

[Larry Paulson]

 * 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 thinks these are priorities for restoration, I guess we only 
have a few days. The problem with code generation has something to do with 
types.

Larry


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: powr

[Larry Paulson]

You should always have success by unfolding powr_def. And I’m told that the 
necessary changes to “approximation” are not difficult.

Larry

 On 12 Apr 2015, at 12:26, Manuel Eberl ebe...@in.tum.de wrote:
 
 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 not have to.
 
 The issue is, however, not terribly urgent since my project is still 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 = 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 thinks these are priorities for 
 restoration, I guess we only have a few days. The problem with code 
 generation has something to do with types.
 
 Larry
 
 
 ___
 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] NEWS: powr

[Larry Paulson]

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 Haftmann 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 from inspecting your diffs
 
   hg diff -c b785d6d06430 | grep code
   hg diff -c 065ecea354d0 | grep code
 
 I see that both hardly tinker with code declarations anyway.
 
 And previously the definitions of ln and powr have been the same on real
 as they are now.  So, there should hardly have been any working code
 setup before, and I can confirm that there is no such setup in Isabelle2014.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset insert

[Larry Paulson]

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 singleton), it would be 
 nicer to have only two constructors, like for finite sets: empty and insert. 
 In particular, this often avoids the use of ac_simps for union because 
 representations are more canonical. The singleton constructor would be 
 retained as an abbreviation for insert_mset _ {#} but M + {#x#} would be 
 simplified to insert_mset x M, like for sets.
 
 Any views?
 
 Tobias
 
 ___
 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] HOL-Probability broken

[Larry Paulson]

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 to that particular problem.
 
 That version f41a2f77ab1b looks fine.
 
 
 I’ve no time to verify that there are no further problems. Sorry again.
 
 New further problems emerge in 5b762cd73a8e: total existence failure due to 
 missing file Complex_Transcendental.thy.
 
 
   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Probability broken

[Larry Paulson]

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.
 ***
 *** Coercion inference failed:
 *** uncomparable types in type list
 ***
 *** Cannot fulfil subtype constraints:
 ***   ??'a  :  ereal   from function application
 *** \integral\^sup+ x. ereal (x ^ k * exp (- x)) *
 ***indicator {0::??'i..} x
 ***\partiallborel =
 *** fact k
 ***   ereal  :  ereal   from function application
 *** op =
 ***  (\integral\^sup+ x. ereal (x ^ k * exp (- x)) *
 ***  indicator {0::??'h..} x
 ***  \partiallborel)
 ***   nat = ??'a  :  ??'b = ??'c   from function application
 *** fact::??'b = ??'c
 *** At command lemma (line 116 of 
 ~~/src/HOL/Probability/Distributions.thy)
 
 The problem might be an untested merge by Larry, but I did not make more 
 detailed tests to prove that hypothesis.
 
 What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show 
 any activity nor results of testing.  Maybe the mira service is down?
 
 
   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] HOL-Probability broken

[Larry Paulson]

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:
 *** uncomparable types in type list
 ***
 *** Cannot fulfil subtype constraints:
 ***   ??'a  :  ereal   from function application
 *** \integral\^sup+ x. ereal (x ^ k * exp (- x)) *
 ***indicator {0::??'i..} x
 ***\partiallborel =
 *** fact k
 ***   ereal  :  ereal   from function application
 *** op =
 ***  (\integral\^sup+ x. ereal (x ^ k * exp (- x)) *
 ***  indicator {0::??'h..} x
 ***  \partiallborel)
 ***   nat = ??'a  :  ??'b = ??'c   from function application
 *** fact::??'b = ??'c
 *** At command lemma (line 116 of 
 ~~/src/HOL/Probability/Distributions.thy)
 
 The problem might be an untested merge by Larry, but I did not make more 
 detailed tests to prove that hypothesis.
 
 What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show 
 any activity nor results of testing.  Maybe the mira service is down?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] sign_simps

[Larry Paulson]

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 
 florian.haftm...@informatik.tu-muenchen.de wrote:
 
 I see two possibilities:
 * Discontinue sign_simps as an comparingly unfruitful attempt.
 * Turn sign_simps in a proper fact collection like algebra_simps and
 field_simps.  Maybe there are other candidates of splitting rewrite rules?
 
 Any suggestions on that topic?
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Mercurial failing as always

[Larry Paulson]

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