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
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) an
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 var
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. Whateve
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 wo
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 pr
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
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 s
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 reposi
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 mess
Yes, except you won’t be able to find an injection
»of_float :: float => 'a::field«
since there are finite fields. Maybe field_char_0 will be sufficient.
Who wants to actually do this?
Larry
> On 6 Aug 2015, at 11:05, Florian Haftmann
> wrote:
>
> A conclusion of what I have unders
; 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
>>
ed 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 th
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 wrote:
>
> The situation regarding coercions has beco
On 28 Jul 2015, at 16:40, Makarius 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 c
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-..
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"
> Subject: isabelle dist build failed
> Date: 22 July 2015 23:56:57 BST
> To: l...@cam.ac.
I’ve seen this error consistently in the past week or so. Updating today didn’t
help.
"remote_vampire": Internal error:
exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML”)
~/isabelle/Repos/src/HOL: hg id
4050b243fc60 tip
Larry
__
isky, at least in the short term.
Larry Paulson
> On 29 Jun 2015, at 23:23, C. Diekmann 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 no
Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a
while.
Larry
> On 26 Jun 2015, at 23:46, Makarius wrote:
>
> * Proof method "goals" turns the current subgoals into cases within the
> context; the conclusion is bound to variable ?case in each case.
>
> * The und
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 wrote:
>
> I took a look, and it all runs perfectly well, except here:
>
>show "
gin forwarded message:
>
> From: Larry Paulson
> Subject: Re: [isabelle] find_theorems and locales
> Date: 19 June 2015 16:22:53 BST
> To: Florian Haftmann
> Cc: Bertram Felgenhauer ,
> cl-isabelle-us...@lists.cam.ac.uk
>
> I've stumbled across a related issue with
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
a
This may be the problem. I don’t remember exactly what I was trying to do, only
that it was very difficult. Of course nobody uses show_types any more.
Larry
> On 24 Jun 2015, at 15:13, Dmitriy Traytel wrote:
>
> You can hover in the output panel, but you won't see types of constants there.
___
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
i
Absolutely, totally. We must go forward and not back.
Larry
> On 11 Jun 2015, at 13:27, Tobias Nipkow 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 recursi
imum 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
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 wrote:
>
> I can confirm that, at least that side is simple.
>
> Tobias’ point abou
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
> On 7 Jun 2015, at 07:38, Dmitriy Traytel 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 patter
> On 6 Jun 2015, at 19:37, Tobias Nipkow 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 thi
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
> wrote:
>
>> Conceivably we could introduce a prefix syntax for type constraints, e.g.
>>
>> [:real:]o
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
> wrote:
>
>> The reason for the continued existence of recdef is that function can
>> caus
On 5 Jun 2015, at 22:22, Florian Haftmann
wrote:
>
>> Why do we need abbreviations such as these?
>>
>> abbreviation real_of_nat :: "nat \ real”
>> where "real_of_nat \ of_nat"
>>
>> abbreviation real_of_int :: "int \ real”
>> where "real_of_int \ of_int"
>>
>> abbreviation real_of_rat :: "
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
> wrote:
>
>> Cleaning up some obscure
The situation regarding coercions has become extremely untidy, and I think it
should be cleared up. We have four generic functions:
of_nat :: nat \ ‘a::semiring_1
of_int :: int \ ‘a::ring_1
of_rat :: rat \ ‘a:: field_char_0
of_real :: real \ 'a::real_algebra_1
Wit
I would be OK with / for integer division, but there would be a lot of
compatibility issues.
Larry
> On 2 Jun 2015, at 19:17, Florian Haftmann
> wrote:
>
> a) The radical solution: there is only »_ / _« for both field division
> and euclidean division. How natural is notation like »a / b * b +
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 1
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
Maybe I don’t understand how this works. I was under the impression that both
the main repository and the AFP had been forked in preparation for the release,
allowing people to add new material to the repository (with appropriate
corrections to the AFP) that would be independent of the current r
This sounds like a good proposal to me. Do we have time before the fork?
Larry
> Begin forwarded message:
>
> From: "Thiemann, Rene"
> Subject: [isabelle] Changing definition of finprod
> Date: 17 April 2015 10:55:32 BST
> To: Cl-isabelle Users
>
> Dear all,
>
> recently I started to formaliz
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 wrote:
>
>
>> Despite such routine improvements, many users will probably just stick to
>> old habits from
I don’t intend any more changes. Fans of “approximation” may have to get used
to doing “simp add: powr_def” first.
Larry
> On 14 Apr 2015, at 15:35, Makarius wrote:
>
> Does that mean there will be further changes, to make it fully work in the
> coming release?
>
> It would be nice to see th
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 Ha
ce 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 wrote:
>
>>> * Complex powers and square roots. The functions "ln" and &quo
> * 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 anybod
Sounds logical to me.
Larry
> On 8 Apr 2015, at 08:13, Tobias Nipkow 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
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 wrote:
>
> On Tue, 17 Mar 2015, Larry Paulson wrote:
>
>> I’ve pushed a correction
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 wrote:
>
> In Isabelle/cd945dc13bec HOL-Probability is broken:
>
> *** Now trying to infer coercions globally.
> ***
> *** Co
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 wrote:
>
> In Isabelle/cd945dc13bec HOL-Probability is broken:
>
> *** Now trying to infer coercions globally.
> ***
> *** Coercion inference failed:
> *** uncomparable types
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
> wrote:
>
> I see two possibilities
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
52 matches
Mail list logo
