Re: [isabelle-dev] Distro broken

[Johannes Hölzl]

My bad, should be fixed now.

 - Jo

Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
> > 
> > isabelle: fb5c74a58796 tip
> > afp: c03838321f2a tip
> > *** No such file:
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
> > ential_Supremum.thy"
> > *** The error(s) above occurred for theory "Essential_Supremum"
> > *** (required by "Probability") (line 15 of
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Pro
> > bability.thy")
> > *** The error(s) above occurred in session "HOL-Probability" (line
> > 716 of "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/ROOT")
>   Florian
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Johannes Hölzl]

You may want to use

  hg archive ~/Fishe-Yates.tar.gz

in the future.

  - Johannes

Am Dienstag, den 04.10.2016, 13:18 +0200 schrieb Manuel Eberl:
> Oh, that is quite possible. Sorry about that. I typically keep my
> prospective AFP entries in private HG repositories and then simply
> tarball and submit them when it's time. I don't think that ever was a
> problem before, but it sounds like the most reasonably explanation so
> far.
> Good catch!
> Manuel
> 
> On 04/10/16 13:16, Lars Hupel wrote:
> > > It isn’t only about SourceTree. As I mentioned, manually adding
> > > Fisher_Yates had no effect, and even now "hg diff” shows nothing,
> > > even though Fisher_Yates should appear as “added” or untracked
> > > (given that it’s on my machine and nowhere else). I’ve also
> > > checked every .hgignore file.
> > > 
> > > Possibly my copy of the AFP has got corrupted somehow.
> > I just checked the submission Manuel uploaded to the submission
> > system
> > and there seems to be an extra ".hg" folder in there. So possibly
> > Mercurial ignores that directory. It might get fixed by "rm -rf"ing
> > that
> > extra folder.
> > 
> > Cheers
> > Lars
>  
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] More HOL-Analysis

[Johannes Hölzl]

I just pushed the foundations to merge your measure theory port. Now
the absolutely integrable functions are an abbreviation for Lebesgue
integrable functions. 

Absolute integrability was only used to prove that bounded variance
implies them (I kept this proof) and for dominated convergence. Now the
last one is proved by using the relation with the Lebesgue (i.e.
Bochner) integral. For this I finally proved that all HK-integrable
functions are Lebesgue-measurable.

 - Johannes

changeset:   63941:f353674c2528
tag: tip
user:hoelzl
date:Fri Sep 23 18:34:34 2016 +0200
summary: move absolutely_integrable_on to 
Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral

changeset:   63940:0d82c4c94014
user:hoelzl
date:Fri Sep 23 10:26:04 2016 +0200
summary: prove HK-integrable implies Lebesgue measurable; prove HK-integral 
equals Lebesgue integral for nonneg functions



Am Mittwoch, den 21.09.2016, 15:29 +0100 schrieb Lawrence Paulson:
> Convex_Euclidean_Space is the largest file in Analysis, more than
> half a megabyte, so rather than combining the files it would be good
> to split them up even more.
> 
> I admit, I have been putting in a lot of new material and trying to
> put things in sensible places, but with no global overview of the
> development.
> 
> Larry
> 
> > 
> > On 16 Sep 2016, at 16:20, Johannes Hölzl  wrote:
> > 
> > Also Brian's theories are still in HOL-Library (i.e. Inner_Product
> > and
> > Product_Vector). I would also move Convex back. It was split of
> > Convex_Euclidean_Space to be usable in Probability. Which is not
> > necessary anymore as Probability is based on Analysis.
> > 
> > I will move these files.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] More HOL-Analysis

[Johannes Hölzl]

I'm still working on integrating your HOL Light measure theory with
HOL-Analysis. Showing that HK-integrable implies measurable is more
involved as I though.

When this is finished I will move the theories. I'm not sure yet what
to do with Convex and Convex_Euclidean_Spaces.

 - Johannes

Am Mittwoch, den 21.09.2016, 17:03 +0100 schrieb Lawrence Paulson:
> Please let me know when you move the file
> Continuum_Not_Denumerable.thy. I have quite a few theorems connected
> with cardinality and topological concepts. Possibly they should not
> be added to that theory and it should simply be included at some
> point in the development.
> 
> Larry
> 
> > 
> > On 16 Sep 2016, at 15:23, Makarius  wrote:
> > 
> > There seems to be an ongoing consolidation of HOL-Analysis
> > (although the
> > NEWS are relatively terse about it).
> > 
> > How about moving src/HOL/Library/Continuum_Not_Denumerable.thy
> > there,
> > too? The recent change b746b19197bd appears to supports this.
> > 
> > There might be more Analysis material in HOL-Library that is worth
> > moving.
> > 
> > 
> > Makarius
> > ___
> > isabelle-dev mailing list
> > isabelle-...@in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] More HOL-Analysis

[Johannes Hölzl]

Also Brian's theories are still in HOL-Library (i.e. Inner_Product and
Product_Vector). I would also move Convex back. It was split of
Convex_Euclidean_Space to be usable in Probability. Which is not
necessary anymore as Probability is based on Analysis.

I will move these files.

 - Johannes

Am Freitag, den 16.09.2016, 15:43 +0100 schrieb Lawrence Paulson:
> I’m continuing to port a lot of material from HOL Light, and indeed
> I’m going to need that exact theory very soon.
> Larry
> 
> > 
> > On 16 Sep 2016, at 15:23, Makarius  wrote:
> > 
> > There seems to be an ongoing consolidation of HOL-Analysis
> > (although the
> > NEWS are relatively terse about it).
> > 
> > How about moving src/HOL/Library/Continuum_Not_Denumerable.thy
> > there,
> > too? The recent change b746b19197bd appears to supports this.
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Johannes Hölzl]

There is even a third one: ∄!

I would vote to forbid the multiple variable case. At least for the
next release. Is it possible to restrict this by a mixfix syntax or
does it require to write a ML parse translations.

 - Johannes

Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow:
> There is a method to this madness: if B is a binder, "B x y. t" is
> short for "B 
> x. B y. t". However, I agree that for ∄ and ∃! this is confusing and
> one of the 
> solutions proposed should be adopted.
> 
> Tobias
> 
> On 13/09/2016 09:45, Peter Lammich wrote:
> > 
> > On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:
> > > 
> > > We have a problem with the ∄ operator, when existential
> > > quantifiers
> > > are nested:
> > > 
> > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
> > >   by (rule refl)
> > I do not see a particular problem with this, however, not-exists
> > and
> > also exists-one have funny semantics when used with multiple
> > variables:
> > 
> > lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
> > by (rule refl)
> > 
> > lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
> > by (rule refl)
> > 
> > this leads to funny lemmas like:
> > 
> > lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
> >   by presburger
> > 
> > lemma also_strange: "∃!x y. x = abs (y::int)"
> >   by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
> > equal_neg_zero)
> > 
> > 
> > I would have expected:
> > (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> > and
> > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
> > 
> > 
> > 
> > We should either forbid multiple variables on those quantifiers, or
> > try
> > to figure out whether there is a widely-accepted consensus on their
> > meaning.
> > 
> > --
> >   Peter
> > 
> > 
> > > 
> > > 
> > > Note that ∄x y. P x y would be fine.
> > > 
> > > Larry
> > > 
> > > ~/isabelle/Repos/src/HOL: hg id
> > > dca6fabd8060 tip
> > > 
> > > ___
> > > isabelle-dev mailing list
> > > isabelle-...@in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abel
> > > le-dev
> > ___
> > isabelle-dev mailing list
> > isabelle-...@in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> > 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Johannes Hölzl]

Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson:
> Thank you for making this change!
> 
> > 
> > My idea would be to rename both integrals into something like:
> >   has_bc_integral, bc_integrable, bc_integral,
> >   has_hk_integral, hk_integrable, hk_integral
> > and consequently rename the integral theorems.
> I would greatly prefer renaming the relevant theories instead so that
> we have Bochner.has_integral versus Gauge.has_integral, etc. That is
> the point of having compound names. I would go so far as to suggest
> that equivalent theorems with slightly different names should be
> rationalised.

I would prefer this too,  but has_integral is not a name. It is special
syntax, one writes:   (f has_integral x) s

Either we remove the syntax (and add it to a locale to be interpreted
locally) or rename it. Unfortunately the first option is still
problematic. For example, one needs to setup a context to use it, and
then one is not allowed to enter a locale context.

Another problem is that the theory which gets loaded later is always
slightly preferred as it does not need the theory prefix. Only way to
avoid this would be to hide the theorem names. Or put it in a context
and add the "qualified" command prefix.

Unifying the different names (i.e. integral_minus, sub, diff, uminus,
cmult, mult_left, ...) is also on my TODO list.

 - Johannes






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

[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Johannes Hölzl]

* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.

* Moved measure theory from HOL-Probability to HOL-Analysis. When importing
HOL-Analysis some theorems need additional name spaces prefixes due to name
clashes.
INCOMPATIBILITY.




The incompatibility is obviously due to the renaming, but we also have
currently two integrals which share now some theorem names. The problem
is that one integral does not subsume the other:

* The /Bochner/ integral is defined on arbitrary measures, but 
  restricted to be absolutely integrable, i.e. when a function is 
  integrable than also its norm is integrable. 

* The /Henstock-Kurzweil/ integral is restricted to Euclidean spaces 
  (and the Lebesgue measure on it), but it is not restricted to 
  absolutely integrable functions.
My idea would be to rename both integrals into something like:
  has_bc_integral, bc_integrable, bc_integral,
  has_hk_integral, hk_integrable, hk_integral
and consequently rename the integral theorems.

Currently the measure theory is based on the stuff in the former
Multivariate_Analysis. My plan is to integrate it further down and then
replace some old stuff by more generic definitions/proofs from measure
theory.

There are currently further restrictions where we are not sure how to
solve them:

* Dominated convergence is very general on the Bochner integral it
  works for integrals into Banach spaces, while for the HK integral 
  it is currently only proven for Euclidean spaces.

* We require dominated convergence to prove that both integrals are 
  equal. Hence currently equality is only proven for Euclidean spaces.

* FTC for the Bochner integral is derived from FTC for the HK integral.
  Hence FTC for the Bochner integral is only available for Euclidean 
  spaces.

 - Johannes

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

Re: [isabelle-dev] multiplicity and prime numbers

[Johannes Hölzl]

I also would vote for option 3.

But is it possible to adapt all lemmas accordingly?  I could imagine
that some statements use the fact that the support of multiplicity are
the prime numbers.

 - Johannes

Am Dienstag, den 19.07.2016, 12:09 +0100 schrieb Lawrence Paulson:
> This is what I would do 
> 
> Larry Paulson
> 
> > 
> > On 19 Jul 2016, at 11:03, Manuel Eberl  wrote:
> > 
> > 3. replace the old multilicity with the new one and adapt all
> > lemmas accordingly
> > 
> > Currently, I tend towards the last options. Are there any other
> > opinions on this?

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

Re: [isabelle-dev] \nexists

[Johannes Hölzl]

Am Freitag, den 15.07.2016, 11:30 +0200 schrieb Makarius:
> On 14/07/16 17:50, Lawrence Paulson wrote:
> 
> > 
> > What’s unfortunate is that the “negated exists” quantifier is
> > available
> > both for input and output in Isabelle, just not as a TeX macro.
> The macro is available here (nipkow 2005-05-30):
> http://isabelle.in.tum.de/repos/isabelle/annotate/d51a0a772094/lib/te
> xinputs/isabellesym.sty#l224
> 
> It only needs the amssymb package.
> 

Added amssymb to HOL-MV_A. And reintroduced \nexists in ef794d2e3754.

 - Johannes


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

Re: [isabelle-dev] \nexists

[Johannes Hölzl]

Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow:
> LaTeX build problems are not infrequent and could be avoided easily
> if "build" 
> produced the document by default.
> 
> Tobias

+1

 - Johannes

> On 14/07/2016 17:50, Lawrence Paulson wrote:
> > 
> > The recent failure in Multivariable_Analysis was caused by the
> > \nexists macro,
> > which is not defined:
> > 
> > ! Undefined control sequence.
> >  \nexists
> > 
> > The corresponding source line is here:
> > 
> > Multivariate_Analysis/Brouwer_Fixpoint.thy:have nog:
> > "\g.
> > continuous_on (S \ connected_component_set (- S) a) g \
> > 
> > What’s unfortunate is that the “negated exists” quantifier is
> > available both for
> > input and output in Isabelle, just not as a TeX macro.
> > 
> > I’ve pushed a fix. However, ideally this macro should be defined
> > somehow and my
> > change reverted.
> > 
> > Larry
> > 
> > 
> > This body part will be downloaded on demand.
> > 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[Johannes Hölzl]

Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:
> Dear AFP developers,
> 
> some of you may have noticed that the "AFP devel" pages have not been
> updated since April. This is partly my fault because I migrated the
> infrastructure and partly not my fault because the scripts to produce
> these pages make a lot of assumptions about the infrastructure :-)
> 
> Anyway, there's now a reboot of these pages available at:
> 
>   
> 
> Note that this is a preview: The status is still [skipped] everywhere
> and most download links don't work. This will be fixed some time this
> week.
> 
> As soon as that's done, the old links ("/devel-entries" and the like)
> will go offline.

Can't we just let the /devel-entries redirect to http://devel. ?  I'm
sure there are quite some papers which reference the /devel entries.

> Cheers
> Lars

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

Re: [isabelle-dev] Permutations

[Johannes Hölzl]

Am Dienstag, den 05.07.2016, 20:02 +0200 schrieb Florian Haftmann:
> 
> > 
> > 
> > What about adding it to the ab_group_add typeclass? I know this is
> > not
> > the usual mathematical syntax for permutations, but at least we can
> > reuse a lot of theorems from this type class.
> There *is* reuse since there is a separate interpretation of the
> abstract ab_group locale.
I meant of course group_add, not ab_group_add. I still think that the
type class interpretation gives us more theorems. Not everything is
expressible in the class-locale.

> 
> I once met an algebraist who preferred + for abelian groups and *
> otherwise, and this makes sense.
And I agree that * is much nicer, but not as practicable in our
concrete Isabelle setting.

> 
> Cheers,
>   Florian
> 
> 
> > 
> > 
> > 
> >  - Johannes
> > 
> > Am Dienstag, den 05.07.2016, 19:40 +0200 schrieb Florian Haftmann:
> > > 
> > > 
> > > > 
> > > > 
> > > > 
> > > > One question: why did you only set it up for monoid_mult and
> > > > inverse,
> > > > and not as a ab_group_mult?
> > > The answer is simple: there is no type class
> > > ab_group_mult.  Why?  Since
> > > our multiplicative structures are tailored towards rings where 0
> > > is
> > > no
> > > part of the multiplicative group.
> > > 
> > > Cheers,
> > >   Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Permutations

[Johannes Hölzl]

What about adding it to the ab_group_add typeclass? I know this is not
the usual mathematical syntax for permutations, but at least we can
reuse a lot of theorems from this type class.

 - Johannes

Am Dienstag, den 05.07.2016, 19:40 +0200 schrieb Florian Haftmann:
> > 
> > One question: why did you only set it up for monoid_mult and
> > inverse,
> > and not as a ab_group_mult?
> The answer is simple: there is no type class
> ab_group_mult.  Why?  Since
> our multiplicative structures are tailored towards rings where 0 is
> no
> part of the multiplicative group.
> 
> Cheers,
>   Florian
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Permutations

[Johannes Hölzl]

Ah sorry, my previous email should have been a response here.

Very nice!

One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?

 - Johannes

Am Montag, den 04.07.2016, 21:25 +0200 schrieb Florian Haftmann:
> Hi all,
>   
> see 59803048b0e8 for some basic facts about almost everywhere
> bijections
> aka permutations. Maybe this will become a convenient coagulation
> point
> for various scattered material in the future.
>   
> It turned out quite ambitious to formulate basic properties, e.g.
> circularity. I did not search for any literature because I thought
> that
> things covered in introductory courses should be straightforward to
> formalize ;-).
>   
> My original interest had been cycles, but I realized that this needs
> more work than I am willing to spend here, even more since I further
> realized that the combinatorial interpretation of first Stirling
> numbers
> can work just on cycles without need of their interpretation as
> permutations.
>   
> If anybody wants to push that work further, the agenda is roughly as
> follows:
> * Consolidate scattered material on permutations (functions) into
> Library/Perm.thy (see my post
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-June/msg0009
> 1.html
> for further details).
> * Gradually abandon Library/Permutation with its equivalence relation
> ‹perm› – it is much easier to reason about equality on multisets
> ‹mset
> xs = mset ys›. There is also no equivalence relation ‹same_elems ::
> 'a
> list ⇒ 'a list ⇒ bool›, but we write just ‹set xs = set ys›, for the
> same and good reason.
> 
> I still have some work regarding cycles and combinatorial functions
> in
> the drawer which I hope to finish gradually over time.
>   
> Cheers,
>   Florian
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Bijections

[Johannes Hölzl]

Very nice!

One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?

 - Johannes

Am Montag, den 04.07.2016, 21:13 +0200 schrieb Florian Haftmann:
> Hi all,
>   
> in 1a474286f315 I have introduced a locale for (total) bijections,
> allowing to obtain typical facts like ‹inv f ∘ f = id› by
> interpretation.
> 
> The motivation was that most of these facts have not ‹bij› but ‹inj›
> or
> ‹surj› as premise, which makes proof complicated due to two lifting
> steps, especially if you need the same facts over and over.
> 
> Of course there could also be a locale for partial bijections, and
> also
> a whole hierarchy spanning injections etc., but this would result in
> a
> lot of duplication.
> 
> The idea to turn all those predicates into locales sounds too radical
> for me, since lifting arguments referring to terms like ‹bij (f ∘ g)›
> are tedious to express within the module system. But maybe others
> with
> more experience than me in that area have already made some thoughts
> about that matter.
>   
> Cheers,
>   Florian

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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Johannes Hölzl]

Hi Mathias,

there is at least the type class 'canonically_ordered_monoid' which has
the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
Are the multisets already in this typeclass?

 - Johannes


Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
> Dear type-classes and simplifier experts,
> 
> in the plan of instantiating multisets with the multiset ordering, I
> am trying to instantiate the multisets with additional typeclasses to
> get specific simplification theorems. The aim is to mimic the
> simplifier’s behaviour of other types like natural numbers. One of my
> problems can be nicely illustrated by the following lemma: “M <= M +
> N <-> 0 <= N”. 
> 
> 
> Analog simplification rules already exist for rings (e.g., natural
> numbers*) and ordered groups too:
>   thm
> Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze
> ro
>   thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
> Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as
> [simp].
> 
> 
> However, the multisets are neither a group (no inverse for the law
> “+”) nor a ring (no multiplication). I could duplicate the theorems,
> but I noticed that the proofs of the theorems do only rely on the
> fact it is a monoid_add (for the zero element) and an
> ordered_ab_semigroup_add_imp_le (for the order). The following
> theorem would work too and is general enough to include the multiset
> case:
> 
> lemma le_add_same_cancel1 [simp]:
>   “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b
> ⟷ 0 ≤ b”
>   using add_le_cancel_left [of a 0] by simp
> 
> 
> Are there any obvious differences between this more general version
> with explicit type class annotations
> and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,
> would it make sense to use this version in Isabelle?
> 
> 
> 
> Thanks in advance,
> Mathias Fleury
> 
> 
> 
> 
> * for natural numbers, the simproc
> Numeral_Simprocs.natle_cancel_numerals is able to do it too.
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Considered harmful: surj

[Johannes Hölzl]

Yes I second that. It surely is a good idea to just use it only as a
input translation.

 - Johannes

Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann:
> Hi all,
>   
> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
> UNIV›. This is a little bit unfortunate since an ordinary equation is
> just hidden in output that way, resulting in lots of casual
> confusion. I
> would suggest to turn ‹surj› into a mere input abbreviation, similar
> to
> ‹trivial_limit› which also covers an equality. This may also open the
> possibility to re-introduce ‹surj_on f A› as in input abbreviation
> for
> ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange
> assymmetry wrt. inj(_on), bij(_betw).
>   
> Cheers,
>   Florian
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP/MFMC_Countable still failing

[Johannes Hölzl]

Unfortunately it is not easily upgraded, as I did a semantic change in
HOL-Probability (i.e. ereal -> ennreal).

My local version of MFMC is currently 25% ported, and I hope to be
finished in a couple of days. (I didn't work on it over the long
weekend)

 - Johannes

On Mo, 2016-05-30 at 23:28 +0200, Makarius wrote:
> As of Isabelle/dd6cd88cebd9 + AFP/8186added238, MFMC_Countable is
> still
> failing.
> 
> As a new entry it might be actually easy to upgrade.
> 
> Afterwards we might be back to the rare situation where Isabelle +
> AFP
> fully work.
> 
> 
>   Makarius

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

Re: [isabelle-dev] Nonterminating AFP build

[Johannes Hölzl]

I will take care of it next week.

  - Johannes

On Do, 2016-05-12 at 11:58 +0100, Lawrence Paulson wrote:
> There are multiple failures in PMF_OF_List. It looks like the
> behaviour of simplification has changed concerning the functions
> ennreal and ereal.
> Larry
> 
> > 
> > On 12 May 2016, at 11:39, Lawrence Paulson  wrote:
> > 
> > It has no timeout, sorry, that was my fault. Now set to 300
> > seconds.
> > 
> > We don’t need a global timeout, but why not a default timeout? We
> > could set up to the median runtime. Actually I think our typical
> > value of 600 seconds is much too high, considering that a loop in a
> > common library could make dozens of entries run forever.
> > Larry
> > 
> > > 
> > > On 11 May 2016, at 23:58, Gerwin Klein  > > > wrote:
> > > 
> > > If it doesn’t have a timeout set, then that’s a mistake and
> > > should be fixed. It’d be good to have protection for all builds,
> > > not only through Jenkins.
> > > 
> > > We’ve avoided a global timeout so far, because it’d have to be
> > > fairly long, i.e. if you have a few entries that don’t terminate
> > > because of a change in Isabelle for instance, you might very
> > > quickly be looking at multiple days.
> > > 
> > > Might still be a good idea to add one anyway as an additional
> > > safety net.
> > > 
> > > Cheers,
> > > Gerwin
> > > 
> > > 
> > > 
> > > > 
> > > > On 12.05.2016, at 06:58, Lars Hupel  wrote:
> > > > 
> > > > Isabelle/8326aa594273
> > > > AFP/ffea2c11f257
> > > > 
> > > > We appear to have an issue with nonterminating builds. See
> > > > here:
> > > >  > > > leFull>.
> > > > I had to manually kill the running poly process. I'm not quite
> > > > sure
> > > > which session causes it, but it's possibly
> > > > Randomised_Social_Choice. I
> > > > was under the assumption that all AFP sessions had timeouts set
> > > > –
> > > > apparently this is not the case.
> > > > 
> > > > In order to avoid these problems in the future, I'll implement
> > > > job
> > > > timeouts in Jenkins.
> > > > 
> > > > Cheers
> > > > Lars
> > > > ___
> > > > isabelle-dev mailing list
> > > > isabelle-...@in.tum.de
> > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/
> > > > isabelle-dev
> > > 
> > > 
> > > 
> > > 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/is
> > > abelle-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: HOL-Probability -- type of emeasure and nn_integral was changed from ereal to ennreal

[Johannes Hölzl]

Argh, the change to the AFP broke the entire build by accidentally
removing `Ergodic_Theory/document/root.tex`. I don't know how this
happened. It is fixed now. Sorry for the inconvenience.

 - Johannes



Am Donnerstag, den 14.04.2016, 15:57 +0200 schrieb Johannes Hölzl:
> In HOL-Probability the type of emeasure and nn_integral was changed
> from ereal to ennreal:
>   emeasure :: 'a measure => 'a set => ennreal
>   nn_integral :: 'a measure => ('a => ennreal) => ennreal
> INCOMPATIBILITY.
> 
> 
> This is a major incompatibility for most users of HOL-Probability. I
> changed the Isabelle repository and the AFP. I hope there are not too
> many external theories.
> 
>  - Johannes

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

[isabelle-dev] NEWS: HOL-Probability -- type of emeasure and nn_integral was changed from ereal to ennreal

[Johannes Hölzl]

In HOL-Probability the type of emeasure and nn_integral was changed
from ereal to ennreal:
  emeasure :: 'a measure => 'a set => ennreal
  nn_integral :: 'a measure => ('a => ennreal) => ennreal
INCOMPATIBILITY.


This is a major incompatibility for most users of HOL-Probability. I
changed the Isabelle repository and the AFP. I hope there are not too
many external theories.

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

Re: [isabelle-dev] Syntax for lattice operations?

[Johannes Hölzl]

Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann:
> Hi all,
>   

> 
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
> 
> Meanwhile however all those operations to which that syntax is attached
> to are members of syntactic type classes.  It could be worth to attempt
> to make that syntax standard, using funny subscripts or similar for the
> more exotic cases.
> 
> Cheers,
>   > Florian

Yes absolutely. I recently added by accident Lattice_Syntax somewhere
in the Library and a lot of AFP theories (and HOLCF) broke down at
unexpected places.

Alternatively: Would a lattice_syntax locale work nowadays? I remember
I tried it once and for some reason it didn't work. Either notations
aren't supported in locales or they are exported after the context
-block.

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

Re: [isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.

Your suggestion would be great, to completely disable code generation
for "open" and "uniformity". It would avoid a lot of [code del]
annotations at class instantiations, and some strange constructions for
filter ;-)


 - Johannes


Am Donnerstag, den 14.01.2016, 11:47 +0100 schrieb Florian Haftmann:
> Hi Johannes, hi Andreas,
> 
> the core of the problem is that dictionaries are always generated for
> type class instances, even if the operations therein are never
> referred
> to.  Is this the first time that we have such a situation, or are
> there
> more examples (e.g. in the AFP)?  If yes, the code generator could be
> equipped to treat particular constants *not* as class parameters.
> 
> Cheers,
>   Florian
> 
> Am 11.01.2016 um 12:00 schrieb Johannes Hölzl:
> > 
> > 
> > Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> > > Ho Johannes.
> > > 
> > > > > >  Then the dictionary construction for type constructors
> > > > > > does
> > > > > > not
> > > > > >  work in ML! The type signature would be the following:
> > > > > > 
> > > > > >val test_prod : ('a * 'b) filter
> > > > > > 
> > > > > >  Which apparently is not allow in ML.
> > > > > This is the famous value restriction (which I also regularly
> > > > > run
> > > > > into). The standard 
> > > > > solution is to add a unit closure, because functions may be 
> > > > > polymorphic in ML.
> > > 
> > > Nothing to add about that.
> > > 
> > > In the examples there is also the problem that constructing a
> > > dictionary
> > > provokes an exception already.  Here the general solution is to
> > > hide
> > > the
> > > problematic terms beneath an abstraction beneath a constructor.
> > > 
> > > Applying that to your examples, I had a look at the sources and
> > > came
> > > to
> > > the conclusion that it is a bad idea have Abs_filter and
> > > Rep_filter
> > > in
> > > generated code at all.
> > > 
> > > For the simple examples, it is much better to use »principal« as
> > > a
> > > formal constructor, which maps nicely to sets and provides some
> > > executability for a considerable class of filters.
> > > 
> > > I did not have an idea in which algebraic framework »uniformity«
> > > could
> > > fit.  Hence I provided a constructor which is a variant of
> > > identity
> > > and
> > > used that, which makes also the examples involving uniformity
> > > compileable (but of course not evaluable).
> > > 
> > > Maybe you have an idea how this could be improved.
> > 
> > Well filters are mostly non-computable. Actually I would prefer to
> > tell
> > the code-generator to not generate code for topologies and uniform
> > spaces at all, as these type classes are carry only non-computable
> > data.
> > 
> > But of course your implementation looks cleaner, so I changed in
> > Isabelle df65f5c27c15.
> > 
> >  - Johannes
> > 
> > 
> > > Cheers,
> > >   Florian
> > > 
> > > > 
> > > > Ah thanks! This explains it.
> > > > 
> > > > Unfortunately, in my case the type is fixed in HOL to:
> > > > 
> > > >   uniformity :: ('a * 'a) filter  (where 'a :: uniform_space)
> > > > 
> > > > And I do not want to change the type signature for code
> > > > generation.
> > > > So
> > > > I will stick to Solution 3.
> > > > 
> > > >  - Johannes
> > > > 
> > > > 
> > > > > > 2.  If your type class contains non-computable data, i.e.
> > > > > > 
> > > > > >instantiation bool :: test_class
> > > > > >begin
> > > > > > 
> > > > > >definition "test = if P = NP then top else bot"
> > > > > > 
> > > > > >instance proof qed
> > > > > >  

Re: [isabelle-dev] Impossible_Geometry

[Johannes Hölzl]

Am Dienstag, den 12.01.2016, 13:48 + schrieb Lawrence Paulson:
> This AFP entry no longer works. I think that the culprit is recent
> changes affecting the metric_space type class. See attachment.
> 
> Larry


Ah, sorry I overlooked this. I will fix it.

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

Re: [isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> Ho Johannes.
> 
> > > >  Then the dictionary construction for type constructors
> > > > does
> > > > not
> > > >  work in ML! The type signature would be the following:
> > > > 
> > > >val test_prod : ('a * 'b) filter
> > > > 
> > > >  Which apparently is not allow in ML.
> > > This is the famous value restriction (which I also regularly run
> > > into). The standard 
> > > solution is to add a unit closure, because functions may be 
> > > polymorphic in ML.
> 
> Nothing to add about that.
> 
> In the examples there is also the problem that constructing a
> dictionary
> provokes an exception already.  Here the general solution is to hide
> the
> problematic terms beneath an abstraction beneath a constructor.
> 
> Applying that to your examples, I had a look at the sources and came
> to
> the conclusion that it is a bad idea have Abs_filter and Rep_filter
> in
> generated code at all.
> 
> For the simple examples, it is much better to use »principal« as a
> formal constructor, which maps nicely to sets and provides some
> executability for a considerable class of filters.
> 
> I did not have an idea in which algebraic framework »uniformity«
> could
> fit.  Hence I provided a constructor which is a variant of identity
> and
> used that, which makes also the examples involving uniformity
> compileable (but of course not evaluable).
> 
> Maybe you have an idea how this could be improved.

Well filters are mostly non-computable. Actually I would prefer to tell
the code-generator to not generate code for topologies and uniform
spaces at all, as these type classes are carry only non-computable
data.

But of course your implementation looks cleaner, so I changed in
Isabelle df65f5c27c15.

 - Johannes


> Cheers,
>   Florian
> 
> > 
> > Ah thanks! This explains it.
> > 
> > Unfortunately, in my case the type is fixed in HOL to:
> > 
> >   uniformity :: ('a * 'a) filter  (where 'a :: uniform_space)
> > 
> > And I do not want to change the type signature for code generation.
> > So
> > I will stick to Solution 3.
> > 
> >  - Johannes
> > 
> > 
> > > > 2.  If your type class contains non-computable data, i.e.
> > > > 
> > > >instantiation bool :: test_class
> > > >begin
> > > > 
> > > >definition "test = if P = NP then top else bot"
> > > > 
> > > >instance proof qed
> > > >end
> > > > 
> > > >  You get a non-terminating program at the time point when
> > > > the
> > > >  dictionary for bool :: test_class is constructed. When the
> > > >  code equation is hidden with [code del] one gets a
> > > > exception!
> > > > 
> > > > 3.  Our current solution is to introduce code_datatype
> > > > Abs_filter
> > > >  Rep_filter [code del] and define for each uniformity:
> > > > 
> > > >uniformity = Abs_filter (%P. Code.abort (STR''FAILED'')
> > > > (Rep_filter test P))
> > > > 
> > > >  @Florian: is the an alternative solution?
> > > > 
> > > > 
> > > > - Johannes
> > > > 
> > > > PS: Here is a short, concrete example:
> > > > 
> > > > theory Scratch
> > > >imports Complex_Main
> > > > begin
> > > > 
> > > > class test_class =
> > > >fixes test :: "'a filter"
> > > > 
> > > > instantiation prod :: (test_class, test_class) test_class
> > > > begin
> > > > 
> > > > definition [code del]: "test = (test ×⇩F test :: ('a × 'b)
> > > > filter)"
> > > > 
> > > > instance proof qed
> > > > end
> > > > 
> > > > instantiation unit :: test_class
> > > > begin
> > > > 
> > > > definition [code del]:
> > > >"(test :: unit filter) = bot"
> > > > 
> > > > instance proof qed
> > > > end
> > > > 
> > > > definition "test2 (x::'a::test_class) = (Suc 0)"
> > > > definition "test3 = test2 ((), ())"
> > > > 
> > > > value [code] "test3"
> 

Re: [isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

Am Freitag, den 08.01.2016, 15:48 +0100 schrieb Andreas Lochbihler:
> Hi Johannes,
> 
> >  Then the dictionary construction for type constructors does
> > not
> >  work in ML! The type signature would be the following:
> > 
> >val test_prod : ('a * 'b) filter
> > 
> >  Which apparently is not allow in ML.
> This is the famous value restriction (which I also regularly run
> into). The standard 
> solution is to add a unit closure, because functions may be 
> polymorphic in ML.

Ah thanks! This explains it.

Unfortunately, in my case the type is fixed in HOL to:

  uniformity :: ('a * 'a) filter  (where 'a :: uniform_space)

And I do not want to change the type signature for code generation. So
I will stick to Solution 3.

 - Johannes


> > 2.  If your type class contains non-computable data, i.e.
> > 
> >instantiation bool :: test_class
> >begin
> > 
> >definition "test = if P = NP then top else bot"
> > 
> >instance proof qed
> >end
> > 
> >  You get a non-terminating program at the time point when the
> >  dictionary for bool :: test_class is constructed. When the
> >  code equation is hidden with [code del] one gets a exception!
> > 
> > 3.  Our current solution is to introduce code_datatype Abs_filter
> >  Rep_filter [code del] and define for each uniformity:
> > 
> >uniformity = Abs_filter (%P. Code.abort (STR''FAILED'')
> > (Rep_filter test P))
> > 
> >  @Florian: is the an alternative solution?
> > 
> > 
> > - Johannes
> > 
> > PS: Here is a short, concrete example:
> > 
> > theory Scratch
> >imports Complex_Main
> > begin
> > 
> > class test_class =
> >fixes test :: "'a filter"
> > 
> > instantiation prod :: (test_class, test_class) test_class
> > begin
> > 
> > definition [code del]: "test = (test ×⇩F test :: ('a × 'b) filter)"
> > 
> > instance proof qed
> > end
> > 
> > instantiation unit :: test_class
> > begin
> > 
> > definition [code del]:
> >"(test :: unit filter) = bot"
> > 
> > instance proof qed
> > end
> > 
> > definition "test2 (x::'a::test_class) = (Suc 0)"
> > definition "test3 = test2 ((), ())"
> > 
> > value [code] "test3"
> > 
> > section ‹Solution›
> > 
> > code_datatype Abs_filter
> > declare [[code abort: Rep_filter]]
> > 
> > lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR ''test'')
> > (λx. Rep_filter test P))"
> >unfolding Code.abort_def Rep_filter_inverse ..
> > 
> > declare test_Abort[where 'a="'a::test_class * 'b :: test_class",
> > code]
> > declare test_Abort[where 'a=unit, code]
> > 
> > end
> > 
> > 
> > 
> > 
> > 
> > 
> > Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
> > > Hi,
> > > 
> > > I want to introduce uniform spaces in HOL, for this I need to
> > > introduce
> > > a type class of the form (see the attached bundle):
> > > 
> > >class uniformity =
> > >  fixes uniformity :: "('a × 'a) filter"
> > > 
> > > Note that uniformity is a filter and not a function.
> > > 
> > > which sits between topological spaces and metric spaces, i.e.
> > > every
> > > metric type is also in the following type classes:
> > > 
> > >class open_uniformity = "open" + uniformity +
> > >  assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U. eventually
> > > (λ(x',
> > > y). x' = x ⟶ y ∈ U) uniformity)"
> > > 
> > >class uniformity_dist = dist + uniformity +
> > >  assumes uniformity_dist: "uniformity = (INF e:{0 <..}.
> > > principal
> > > {(x, y). dist x y < e})"
> > > 
> > > Everything works fine until Affinite_Arithmetic, there in
> > > Intersection.thy the code generation fails with the following ML
> > > error:
> > > 
> > >Error: Type mismatch in type constraint.
> > >   Value: {uniformity = uniformity_proda} : {uniformity: 'a}
> > >   Constraint: ('a * 'b) uniformity
> > >   Reason:
> > >  Can't unify 'a to

Re: [isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

Okay Fabian and I discovered the following problems when one defines a
type class which contains a constant which is not a function:

1.  If there is a type class which contains data depending on the type
classes variable, i.e. 

  class test_class =
fixes test :: "'a filter"

Then the dictionary construction for type constructors does not 
work in ML! The type signature would be the following:
 
  val test_prod : ('a * 'b) filter
 
Which apparently is not allow in ML.

2.  If your type class contains non-computable data, i.e.

  instantiation bool :: test_class
  begin

  definition "test = if P = NP then top else bot"

  instance proof qed
  end

You get a non-terminating program at the time point when the 
dictionary for bool :: test_class is constructed. When the
code equation is hidden with [code del] one gets a exception!

3.  Our current solution is to introduce code_datatype Abs_filter
Rep_filter [code del] and define for each uniformity: 

  uniformity = Abs_filter (%P. Code.abort (STR''FAILED'') (Rep_filter test 
P))

@Florian: is the an alternative solution? 


- Johannes

PS: Here is a short, concrete example:

theory Scratch
  imports Complex_Main
begin

class test_class =
  fixes test :: "'a filter"

instantiation prod :: (test_class, test_class) test_class
begin

definition [code del]: "test = (test ×⇩F test :: ('a × 'b) filter)"

instance proof qed
end

instantiation unit :: test_class
begin

definition [code del]:
  "(test :: unit filter) = bot"

instance proof qed
end

definition "test2 (x::'a::test_class) = (Suc 0)"
definition "test3 = test2 ((), ())"

value [code] "test3"

section ‹Solution›

code_datatype Abs_filter
declare [[code abort: Rep_filter]]

lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR ''test'')
(λx. Rep_filter test P))"
  unfolding Code.abort_def Rep_filter_inverse ..

declare test_Abort[where 'a="'a::test_class * 'b :: test_class", code]
declare test_Abort[where 'a=unit, code]

end






Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
> Hi,
> 
> I want to introduce uniform spaces in HOL, for this I need to
> introduce
> a type class of the form (see the attached bundle):
> 
>   class uniformity = 
> fixes uniformity :: "('a × 'a) filter"
> 
> Note that uniformity is a filter and not a function.
> 
> which sits between topological spaces and metric spaces, i.e. every
> metric type is also in the following type classes:
> 
>   class open_uniformity = "open" + uniformity +
> assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U. eventually (λ(x',
> y). x' = x ⟶ y ∈ U) uniformity)"
> 
>   class uniformity_dist = dist + uniformity +
> assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal
> {(x, y). dist x y < e})"
> 
> Everything works fine until Affinite_Arithmetic, there in
> Intersection.thy the code generation fails with the following ML
> error:
> 
>   Error: Type mismatch in type constraint.
>  Value: {uniformity = uniformity_proda} : {uniformity: 'a}
>  Constraint: ('a * 'b) uniformity
>  Reason:
> Can't unify 'a to (('a * 'b) * ('a * 'b)) filter
>(Type variable is free in surrounding scope)
>   {uniformity = uniformity_proda} : ('a * 'b) uniformity
>   At (line 1619 of "generated code")
>   Exception- Fail "Static Errors" raised
> 
> I assume this is a strange interaction btw code_abort and the fact
> that
> uniformity is a filter (datatype 'a filter = _EMPTY) and not a
> function.
> 
> Does anybody know how to avoid such kind of errors? Do I need to
> sprinkle more [code del] or code_abort annotations?
> 
>  - Johannes
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

Hi,

I want to introduce uniform spaces in HOL, for this I need to introduce
a type class of the form (see the attached bundle):

  class uniformity = 
fixes uniformity :: "('a × 'a) filter"

Note that uniformity is a filter and not a function.

which sits between topological spaces and metric spaces, i.e. every
metric type is also in the following type classes:

  class open_uniformity = "open" + uniformity +
assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U. eventually (λ(x', y). x' = x 
⟶ y ∈ U) uniformity)"

  class uniformity_dist = dist + uniformity +
assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). 
dist x y < e})"

Everything works fine until Affinite_Arithmetic, there in
Intersection.thy the code generation fails with the following ML error:

  Error: Type mismatch in type constraint.
 Value: {uniformity = uniformity_proda} : {uniformity: 'a}
 Constraint: ('a * 'b) uniformity
 Reason:
Can't unify 'a to (('a * 'b) * ('a * 'b)) filter
   (Type variable is free in surrounding scope)
  {uniformity = uniformity_proda} : ('a * 'b) uniformity
  At (line 1619 of "generated code")
  Exception- Fail "Static Errors" raised

I assume this is a strange interaction btw code_abort and the fact that
uniformity is a filter (datatype 'a filter = _EMPTY) and not a
function.

Does anybody know how to avoid such kind of errors? Do I need to
sprinkle more [code del] or code_abort annotations?

 - Johannes



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

[isabelle-dev] CONTRIBUTIONS: The central limit theorem is now in Isabelle

[Johannes Hölzl]

The central limit theorem is now in the Isabelle repository:

* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
  Proof of the central limit theorem: includes weak convergence, characteristic
  functions, and Levy's uniqueness and continuity theorem.

http://isabelle.in.tum.de/repos/isabelle/rev/7582b39f51ed


Besides this I do not have any further contributions for the Isabelle 2016 
release.

 - Johannes

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

Re: [isabelle-dev] Towards the release

[Johannes Hölzl]

I'm currently cleaning up the Central Limit Theorem, and I want to it
entirely to HOL-Probability. 

I hope to finish this in 1 week, to get it into Isabelle 2016.

 - Johannes

Am Freitag, den 01.01.2016, 20:24 +0100 schrieb Makarius:
> Isabelle2016-RC0 is published, but we are still in normal incremental
> change mode on the isabelle-dev repository.
> 
> This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS,
> and the 
> website.
> 
> 
> Are there bigger changes still in the pipeline?  Larry are you
> finished 
> with the ports from HOL Light, as far as Isabelle2016 is concerned?
> 
> Depending on that, the fork point for the release will be a bit
> sooner or 
> later.  Lets say in about 2 weeks. Hopefully, Oracle manages to
> deliver 
> the next Java 8 update in 3 weeks, as scheduled.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Johannes Hölzl]

Ah, after I read Gerwin's email, I thought it was really a problem with
find_theorems. But now you reminded me that it was the setup of
dist_norm.

As far as I remember the reason is that you want to have the syntactic
type classes when you instantiate a type to have dist and norm. But
later when you prove you always want to have metric_space or
real_normed_vector.

Why is the instantiation easier? You only need to define dist as
dist_norm governs, and otherwise you do not show anything about dist.
You only proof real_normed_vector axioms for norm, and then you know
that metric_space is a subclass of real_normed_vector.

The other options I can think of are:

  1) you have special type classes like: 
 * toplogical_metric_space (open is defined with dist)
 * metric_real_normed_vector (dist_norm holds)

  2) you repeat always the proof that your dist defined with norm is 
 actually a metric space...

A solution for the dist_norm (and also open_dist) problem would be to
just add a theorem:

lemma dist_norm:
  fixes x y :: "'a :: real_normed_vector"
  shows "dist x y = norm (x - y)" by (rule dist_norm)
 
(and of course rename the original one to something like
dist_norm_syntactical) Then at least that one gets found...

 - Johannes



Am Donnerstag, den 26.11.2015, 15:07 +0100 schrieb Andreas Lochbihler:
> Hi Larry,
> 
> Type inferences assigns to "dist" the type "'a => 'a => real" where
> 'a :: metric_space, 
> and to "norm" the type "'b => real" where 'b :: real_normed_vector
> (due to the type 
> constraint manipulations in Real_Vector_Spaces.thy. The theorem
> dist_norm uses dist and 
> norm with the sort dist_norm. Consequently, it can find this theorem
> only if metric_space 
> and real_normed_vector are both subclasses of dist_norm, but they are
> not. Thus, it is not 
> found.
> 
> In your concrete application, you can nevertheless apply the theorem
> dist_norm, because 
> you have a concrete type (e.g. real) which instantiates both
> real_normed_vector and 
> metric_space.
> 
> As Florian said, the problem here is really the manipulation of the
> type for dist and 
> norm. Maybe Johannes can remember why Brian introduced this.
> 
> Best,
> Andreas
> 
> On 26/11/15 14:34, Lawrence Paulson wrote:
> > > On 26 Nov 2015, at 11:58, Florian Haftmann <
> > > florian.haftm...@informatik.tu-muenchen.de> wrote:
> > > 
> > > The sort constraints of constants play *no* role for
> > > searching theorems.  The sort constraints of terms to be searched
> > > *do*,
> > > and in my view this is the desired behaviour:  if I formulate a
> > > property
> > > on partial orders, I do not want to be bothered by facts which
> > > only
> > > apply to linear orders.
> > 
> > I’m not sure that I understand this statement. At what point do
> > constants become terms anyway? Consider the following search:
> > 
> > "_<=_" "_=_”
> > 
> > There are two terms, but they are nothing but constants. No theory
> > is implied (I’m not sure how one could express a search that was
> > specifically about partial orders that were not linear), and there
> > are more than 2000 hits. They include statements involving natural
> > numbers, integers and sets. In fact it would be good to find a way
> > of excluding some of those.
> > 
> > Meanwhile, the search
> > 
> > norm dist
> > 
> > contains only constants, and nevertheless it fails to pick up
> > dist_norm: "dist x y = norm (x - y)”.
> > 
> > Larry
> > 
> > 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Johannes Hölzl]

Am Sonntag, den 15.11.2015, 11:43 +0100 schrieb Andreas Lochbihler:
> Vickey_Clarke_Groves looks related to the changes to "real", but I
> have not tried to fix this.

This should be fixed now in AFP e6d87060e398.

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

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

[Johannes Hölzl]

It looks like the setup for blast changed, in the following entries is a
non-terminating blast call. They do not seam to be related to the change
at all:

  Graph_Theory
  ShortestPath
  Rank_Nullity_Theorem
  Echelon_Form
  Gauss_Jordan

Interestingly in 
  Jordan_Normal_Form
  QR_Decomposition
a real :: 'a => real is required! Both introduce a type class with
group/vector-space homomorphism.

I did _not_ look yet into:
  JinjaThreads
  Ordinary_Differential_Equations
  Affine_Arithmetic
  Akra_Bazzi

 - Johannes

Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl:
> Okay, I look at the AFP entries.
> 
> I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow
> if this is unusual.
> 
>  - Johannes
> 
> Am Mittwoch, den 11.11.2015, 17:19 + schrieb Lawrence Paulson:
> > It would be great if you could help. I have just committed some
> > corrections to a number of AFP theories, including that one I think.
> > Affine_Arithmetic comes with some examples that run extremely slowly;
> > I’m not sure whether there is a problem or whether it is always like
> > that. If you want to take over with those, I can do some more tidying
> > up with the main libraries.
> > 
> > Larry
> > 
> > > On 11 Nov 2015, at 17:17, Johannes Hölzl  wrote:
> > > 
> > > Hi Larry,
> > > 
> > > this is a huge change and after I adapted Markov_Models I see that it
> > > simplifies some proofs.
> > > 
> > > If you want I can adapt all AFP entries for which I'm the maintainer, or
> > > which are related to Probability theory:
> > > 
> > >  Density_Compiler
> > >  Integration
> > >  Lower_Semicontinuous
> > >  Markov_Models
> > >  Ordinary_Differential_Equations
> > >  Possibilistic_Noninterference
> > >  Probabilistic_Noninterference
> > >  UpDown_Scheme
> > >  Girth_Chromatic
> > >  Probabilistic_System_Zoo
> > >  Random_Graph_Subgraph_Threshold
> > >  pGCL
> > > 
> > > Just tell me which of these you are already working on, so we can merge
> > > without conflicts.
> > > 
> > > - Johannes
> > > 
> > > 
> > > Am Mittwoch, den 11.11.2015, 12:28 + schrieb Lawrence Paulson:
> > >> I’m glad to have your support. It’s just possible that I might ask your 
> > >> help in getting some things working in the AFP.
> > >> 
> > >> Larry
> > >> 
> > >>> On 10 Nov 2015, at 17:53, Manuel Eberl  wrote:
> > >>> 
> > >>> This is very nice to hear. ‘real’ has plagued me for some time now and 
> > >>> I am glad to see it gone.
> > >>> 
> > >>> Thanks for the good work!
> > >>> 
> > >>> 
> > >>> On 10/11/15 17:45, Lawrence Paulson wrote:
> > >>>> The first phase of this project is finished: the function “real” now 
> > >>>> has the monomorphic type nat => real and is simply an abbreviation for 
> > >>>> the generic function, of_nat. In addition, the function “real_of_int” 
> > >>>> abbreviates the generic function of_int.
> > >>>> 
> > >>>> It took about a week to convert all the theories in the main 
> > >>>> Isabelle/HOL directory. Most of them needed little or no attention, 
> > >>>> the big exceptions being Probability (which frequently used “real” 
> > >>>> with the type ereal => real) and Decision_Procs, which contained many 
> > >>>> thousands of instances of “real” on integers and floats.
> > >>>> 
> > >>>> The main priority at the moment is to fix the decision procedure mir, 
> > >>>> which isn’t working but appears to be entirely unused. Then there is 
> > >>>> still a lot of cleaning up to do, especially in Real.thy and its 
> > >>>> ancestors. Two or three dozen theorems existed in duplicate forms, 
> > >>>> with versions for “real” separate from versions for the other 
> > >>>> coercions; occasionally these variants were named systematically, but 
> > >>>> often their names were unrelated from the originals, and the names of 
> > >>>> variables in the theorems were almost always different. The 
> > >>>> simplification status of the two variants generally differed as well. 
> > >>>> Thus the behaviour of the simplifier on a formula depended on which 
> > >>>> coercion had

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

[Johannes Hölzl]

Okay, I look at the AFP entries.

I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow
if this is unusual.

 - Johannes

Am Mittwoch, den 11.11.2015, 17:19 + schrieb Lawrence Paulson:
> It would be great if you could help. I have just committed some
> corrections to a number of AFP theories, including that one I think.
> Affine_Arithmetic comes with some examples that run extremely slowly;
> I’m not sure whether there is a problem or whether it is always like
> that. If you want to take over with those, I can do some more tidying
> up with the main libraries.
> 
> Larry
> 
> > On 11 Nov 2015, at 17:17, Johannes Hölzl  wrote:
> > 
> > Hi Larry,
> > 
> > this is a huge change and after I adapted Markov_Models I see that it
> > simplifies some proofs.
> > 
> > If you want I can adapt all AFP entries for which I'm the maintainer, or
> > which are related to Probability theory:
> > 
> >  Density_Compiler
> >  Integration
> >  Lower_Semicontinuous
> >  Markov_Models
> >  Ordinary_Differential_Equations
> >  Possibilistic_Noninterference
> >  Probabilistic_Noninterference
> >  UpDown_Scheme
> >  Girth_Chromatic
> >  Probabilistic_System_Zoo
> >  Random_Graph_Subgraph_Threshold
> >  pGCL
> > 
> > Just tell me which of these you are already working on, so we can merge
> > without conflicts.
> > 
> > - Johannes
> > 
> > 
> > Am Mittwoch, den 11.11.2015, 12:28 + schrieb Lawrence Paulson:
> >> I’m glad to have your support. It’s just possible that I might ask your 
> >> help in getting some things working in the AFP.
> >> 
> >> Larry
> >> 
> >>> On 10 Nov 2015, at 17:53, Manuel Eberl  wrote:
> >>> 
> >>> This is very nice to hear. ‘real’ has plagued me for some time now and I 
> >>> am glad to see it gone.
> >>> 
> >>> Thanks for the good work!
> >>> 
> >>> 
> >>> On 10/11/15 17:45, Lawrence Paulson wrote:
> >>>> The first phase of this project is finished: the function “real” now has 
> >>>> the monomorphic type nat => real and is simply an abbreviation for the 
> >>>> generic function, of_nat. In addition, the function “real_of_int” 
> >>>> abbreviates the generic function of_int.
> >>>> 
> >>>> It took about a week to convert all the theories in the main 
> >>>> Isabelle/HOL directory. Most of them needed little or no attention, the 
> >>>> big exceptions being Probability (which frequently used “real” with the 
> >>>> type ereal => real) and Decision_Procs, which contained many thousands 
> >>>> of instances of “real” on integers and floats.
> >>>> 
> >>>> The main priority at the moment is to fix the decision procedure mir, 
> >>>> which isn’t working but appears to be entirely unused. Then there is 
> >>>> still a lot of cleaning up to do, especially in Real.thy and its 
> >>>> ancestors. Two or three dozen theorems existed in duplicate forms, with 
> >>>> versions for “real” separate from versions for the other coercions; 
> >>>> occasionally these variants were named systematically, but often their 
> >>>> names were unrelated from the originals, and the names of variables in 
> >>>> the theorems were almost always different. The simplification status of 
> >>>> the two variants generally differed as well. Thus the behaviour of the 
> >>>> simplifier on a formula depended on which coercion had been used, and in 
> >>>> 150 cases, the simplification itself included the mapping of one 
> >>>> coercion to another (there were two equivalent theorems for doing this).
> >>>> 
> >>>> Innumerable type constraints have now become redundant (things such as 
> >>>> real_of_int (i::int)), but I intend to leave them as they are. I have a 
> >>>> lot of AFP entries to fix.
> >>>> 
> >>>> 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] the function "real"

[Johannes Hölzl]

Hi Larry,

this is a huge change and after I adapted Markov_Models I see that it
simplifies some proofs.

If you want I can adapt all AFP entries for which I'm the maintainer, or
which are related to Probability theory:

  Density_Compiler
  Integration
  Lower_Semicontinuous
  Markov_Models
  Ordinary_Differential_Equations
  Possibilistic_Noninterference
  Probabilistic_Noninterference
  UpDown_Scheme
  Girth_Chromatic
  Probabilistic_System_Zoo
  Random_Graph_Subgraph_Threshold
  pGCL

Just tell me which of these you are already working on, so we can merge
without conflicts.

 - Johannes


Am Mittwoch, den 11.11.2015, 12:28 + schrieb Lawrence Paulson:
> I’m glad to have your support. It’s just possible that I might ask your help 
> in getting some things working in the AFP.
> 
> Larry
> 
> > On 10 Nov 2015, at 17:53, Manuel Eberl  wrote:
> > 
> > This is very nice to hear. ‘real’ has plagued me for some time now and I am 
> > glad to see it gone.
> > 
> > Thanks for the good work!
> > 
> > 
> > On 10/11/15 17:45, Lawrence Paulson wrote:
> >> The first phase of this project is finished: the function “real” now has 
> >> the monomorphic type nat => real and is simply an abbreviation for the 
> >> generic function, of_nat. In addition, the function “real_of_int” 
> >> abbreviates the generic function of_int.
> >> 
> >> It took about a week to convert all the theories in the main Isabelle/HOL 
> >> directory. Most of them needed little or no attention, the big exceptions 
> >> being Probability (which frequently used “real” with the type ereal => 
> >> real) and Decision_Procs, which contained many thousands of instances of 
> >> “real” on integers and floats.
> >> 
> >> The main priority at the moment is to fix the decision procedure mir, 
> >> which isn’t working but appears to be entirely unused. Then there is still 
> >> a lot of cleaning up to do, especially in Real.thy and its ancestors. Two 
> >> or three dozen theorems existed in duplicate forms, with versions for 
> >> “real” separate from versions for the other coercions; occasionally these 
> >> variants were named systematically, but often their names were unrelated 
> >> from the originals, and the names of variables in the theorems were almost 
> >> always different. The simplification status of the two variants generally 
> >> differed as well. Thus the behaviour of the simplifier on a formula 
> >> depended on which coercion had been used, and in 150 cases, the 
> >> simplification itself included the mapping of one coercion to another 
> >> (there were two equivalent theorems for doing this).
> >> 
> >> Innumerable type constraints have now become redundant (things such as 
> >> real_of_int (i::int)), but I intend to leave them as they are. I have a 
> >> lot of AFP entries to fix.
> >> 
> >> 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

[Johannes Hölzl]

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  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  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 \ ‘a::semiring_1
> >>>   of_int :: int \ ‘a::ring_1
> >>>   of_rat :: rat \ ‘a:: field_char_0
> >>>   of_real :: real \ '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 \ real”
> >>> where "real_of_nat \ of_nat"
> >>> 
> >>> abbreviation real_of_int :: "int \ real”
> >>> where "real_of_int \ of_int"
> >>> 
> >>> abbreviation real_of_rat :: "rat \ real”
> >>> where "real_of_rat \ of_rat"
> >>> 
> >>> abbreviation complex_of_real :: "real \ complex"
> >>> where "complex_of_real \ 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:

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

[Johannes Hölzl]

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  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 \ ‘a::semiring_1
> > of_int :: int \ ‘a::ring_1
> > of_rat :: rat \ ‘a:: field_char_0
> > of_real :: real \ '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 \ real”
> >  where "real_of_nat \ of_nat"
> > 
> > abbreviation real_of_int :: "int \ real”
> >  where "real_of_int \ of_int"
> > 
> > abbreviation real_of_rat :: "rat \ real”
> >  where "real_of_rat \ of_rat"
> > 
> > abbreviation complex_of_real :: "real \ complex"
> >  where "complex_of_real \ 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 \ int"]]
> > declare [[coercion "real   :: nat \ real"]]
> > declare [[coercion "real   :: int \ real”]
> > 
> > And then in Complex.thy as follows:
> > 
> > declare [[coercion "of_real :: real \ complex"]]
> > declare [[coercion "of_rat :: rat \ complex"]]
> > declare [[coercion "of_int :: int \ complex"]]
> > declare [[coercion "of_nat :: nat \ 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  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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: structured Isar goal statements

[Johannes Hölzl]

Am Montag, den 15.06.2015, 20:30 +0200 schrieb Makarius:
> On Mon, 15 Jun 2015, Lars Noschinski wrote:
>* What is the meaning of this anyway?
> 
>assume "B x" if "A x" for x
> 
>  Is it:
> 
>assume "!!x. A x ==> B x"
> 
>  or is it:
> 
>fix x assume "A x" assume "B x"
> 
>  Since if/for in have/show is explicit notation for the eigen-context,
>  the second one is conceptually more obvious, but probably not to the
>  user.

Hm, maybe with parenthesis:
  assume ("integrable (M i) (f i)" if "i : I" for i)
But yeah, this does not look very canonical...

>* What are convicing applications where spelling out !! and ==>
>  connectives in assumptions, or extra fix/assume context elements is
>  too awkward?

At least if premises share sub-premises, for example:

lemma nn_integral_setsum:
  assumes "finite I"
  assumes ("!!x. 0 <= f i x" and "f i : borel_measurable M"
 if "i : I" for i)
  show "(INT x. SUM i : I. f i x d M) = (SUM i : I. INT x. f i x d M)"
...

E.g. in measure theory I often have the case to assume that for a
indexed-familiy all elements are non-negative & measurable or similar.

>* Implementation complexity: if/for for assume and presume would demand
>  the same for "theorem fixes / assumes / shows / obtains", probably
>  also for 'obtain' and 'consider' etc.
> 
> 
>   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] »real« considered harmful

[Johannes Hölzl]

The syntax is nice, but I would interpret "_⇩ℕ" not as of_nat but as
into nat, or more specifically I would read: _⇩ℝ  == real _.

 - Johannes

Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann:
> Hi again,
> 
> after I first iteration of discussion I see a list of three requirements:
> 
> 1. Conversions can be written succinctly.
> 2. Conversions are printed succinctly.
> 3. Conversions are unique, there are no accidental equivalences which
> require explicit conversions.
> 
> Concerning (1), my guess indeed is the implicit conversions should do
> the job.  There is the borderline case with required explicit type
> annotations (»of_nat n :: rat«) which is currently handled by distinct
> abbreviations, but these could be dropped.
> 
> (2) is not so trivial if you want to make sure that the printed terms
> are compact but still complete in the sense that they are invariant
> under copy-and-paste. I think of_nat/of_int/of_rat is fine, but
> real_of_int etc. is definitely not.  Anyway, like in (1) these
> abbreviations might be entirely superfluous.  The disadvantage of the
> algebraic conversions is that the do not tell what the result type is --
> which is usually the more important information, since the argument
> type's is usually easily inferred.  Maybe suitable symbol syntax can
> help here.
> 
> Below I made some experiments how fancy symbol syntax could look like,
> but I am still lacking a conclusive idea.
> 
> (3) Everything has been said about this already.
> 
> So, I would suggest we spend thoughts how *printing* of
> of_foo-Conversions can be improved with reasonable means (2).  We are
> still at the beginngin…
> 
> Cheers,
>   Florian
> 
> > notation of_nat ("_⇩ℕ" [999])
> > notation of_int ("_⇩ℤ" [999])
> > notation of_rat ("_⇩ℚ" [999])
> > 
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> > 
> > notation real_of_nat ("of'_nat⇩ℝ")
> > notation real_of_int ("of'_int⇩ℝ")
> > notation real_of_rat ("of'_int⇩ℚ")
> > 
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> > 
> > notation of_nat ("of'_ℕ")
> > notation of_int ("of'_ℤ")
> > notation of_rat ("of'_ℚ")
> > 
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> > 
> > notation real_of_nat ("ℝ'_of'_ℕ")
> > notation real_of_int ("ℝ'_of'_ℤ")
> > notation real_of_rat ("ℝ'_of'_ℚ")
> 
> 
> 
> 
> ___
> 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

[Johannes Hölzl]

Maybe we should resurrect the idea of using adhoc overloading for the
"real" abbreviation.

Florian, does your rework of the generic machinery for syntactic
abbreviations include moving more of the adhoc overloading into HOL?
Then we could setup real as an adhoc overloaded constant and the proof
machinery only sees of_nat, of_int, while the user has still the ability
to write "real".

 - Johannes

Am Mittwoch, den 03.06.2015, 11:20 +0200 schrieb Tobias Nipkow:
> Thank you for reminding me of the "reading" part. My ability to read formulas 
> decreases quadratically with their length. Trading in "real_of_int" for 
> "real" 
> makes things definitely worse.
> 
> I would want to see a concrete figures how much duplication is avoided in the 
> current theories and how much additional annotation is needed. Note also that 
> if 
> some device helps to make the foundations elegant but complicates the 
> applications it can be detrimental if the foundations remain fixed but the 
> applications keep growing.
> 
> Tobias
> 
> On 03/06/2015 10:55, Fabian Immler 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
> >
> >> Am 03.06.2015 um 10:11 schrieb Tobias Nipkow :
> >>
> >> For me the main point of "real" is the ease of writing. If we get rid of 
> >> some lemma duplications but trade that in for many type annotations, I am 
> >> not in favour.
> >>
> >> Tobias
> >>
> >> On 02/06/2015 20:18, Florian Haftmann wrote:
> >>> Dear all,
> >>>
> >>> recently, I stumbled (once again) over the matter of the »real« 
> >>> conversion.
> >>>
> >>> There is an inclusion hierarchy (⊆) of numerical types
> >>>
> >>>   (num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex
> >>>
> >>> We can embed »smaller« into »bigger« types using conversions
> >>>
> >>>   (numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real
> >>>
> >>> These conversions have solid generic algebraic definitions!
> >>>
> >>> 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. For
> >>> illustration have a look at
> >>> http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
> >>> which gives a wonderful generic lemma relating fraction division and
> >>> integer division:
> >>>
> >>>   »floor (of_int k / of_int l) = k div l«
> >>>
> >>> Note that the result type of the of_int conversion is polymorphic and
> >>> can be instantiated to rat and real likewise!
> >>>
> >>> In the presence of the »real« conversion, there is a second variant
> >>>
> >>>   »floor (real k / real l) = k div l«
> >>>
> >>> which must be given separately!
> >>>
> >>> For uniformity it would be much better to have »real« disappear in the
> >>> middle run. I see two potential inconveniences at the moment:
> >>> * Writing »of_foo« might demand a type annotation on its result in many
> >>> cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
> >>> explicit type annotations must be given in terms rather than at »fixes«).
> >>> * We have the existing abbreviations »real_of_foo« which have no type
> >>> ambiguity, but might seem a little bit verbose.
> >>> Anyway, the duplication seems more grivious to me than such syntax issues.
> >>>
> >>> Any comments?
> >>>   Florian
> >>>
> >>>
> >>>
> >>> ___
> >>> 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] Isabelle repository broken

[Johannes Hölzl]

Sorry this was my fault.

"isabelle build -a" does not guarantee that the current changes are
actually committed...

BTW, can the predicate_compiler setup s.t. typedefs are ignored
automatically?

 - Johannes


Am Montag, den 13.04.2015, 11:28 +0200 schrieb Makarius:
> In current 7ff7fdfbb9a0 there is this breakdown:
> 
> HOL-Quickcheck_Examples FAILED
> *** No specification for Abs_filter
> *** At command "quickcheck" (line 150 of 
> "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
> *** No specification for Abs_filter
> *** At command "quickcheck" (line 145 of 
> "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
> 
> 
> Since there is no way around a full "isabelle build -a" before pushing 
> anything, such incidents can't happen, at least in theory.
> 
> 
>   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] [isabelle] Semirings in HOL/Algebra/Ring

[Johannes Hölzl]

Merged & pushed with 5fd0b3c8a355.

  - Johannes

Am Montag, den 30.03.2015, 06:39 + schrieb Thiemann, Rene:
> Dear all,
> 
> can someone please integrate the attached patch which introduces a
> locale for semirings.
> 
> I tested the patch by running all sessions of the AFP though without
> ISABELLE_FULL_TEST:
> there have been no problems.
> 
> Isabelle: db0b87085c16
> AFP:  55e04ff27c52
> 
> Thanks,
> René
> 
> 
> 
> 
> > 
> >> Looks like a good idea to me. Are there any drawbacks?
> > 
> > None of which I'm aware of. I just tested my changes against three
> AFP-entries which are based on HOL-Algebra 
> > and they all compile without problems. (Jordan_Hoelder
> Secondary_Sylow VectorSpace)
> > 
> > However, I really just adapted Ring.thy by adding semiring as
> intermediate locale. I did not make further 
> > changes at this point, e.g., by also having commutative semirings,
> homomorphisms on semirings, etc.
> 
> 
> ___
> 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] Isabelle gets stuck when imported theory is not found

[Johannes Hölzl]

In rev 304ee0a475d1 I fixed a problem that only appears when one loads
~~/src/HOL/Probability interactively based on the HOL image. 
In Measure_Space the theory "Multivariate_Analysis" was imported without
the correct path. When started with "-l HOL-Multivariate_Analysis" it
worked.

Unfortunately there is no error message, it just looks like
Isabelle/jEdit gets stuck at this point.

Is there a way to show an error message at the position of the import
header? 

 - Johannes

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

Re: [isabelle-dev] Unfinished session(s): Abstract_Completeness, Probabilistic_Noninterference

[Johannes Hölzl]

Fixed with 1bcf0828d38c and 7a2b867fa843.

Am Montag, den 17.11.2014, 09:13 +0100 schrieb Florian Haftmann:
> > isabelle: 059ba950a657 tip
> > afp: 0fdf8f639bb4 tip
> > Building HOL-Multivariate_Analysis ...
> > Running Sturm_Tarski ...
> > Running Abstract_Completeness ...
> > Finished Sturm_Tarski (0:00:28 elapsed time, 0:01:21 cpu time, factor 2.89)
> > 
> > Abstract_Completeness FAILED
> > (see also 
> > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Abstract_Completeness)
> > 
> > 
> > [20] [21] [22] [23] [24] [25]) (./Abstract_Completeness.tex)
> > (./Propositional_Logic.tex [26] [27])) [28] (./root.aux) )
> > (see the transcript file for additional 
> > information) > s/type1/public/amsfonts/cm/cmbx10.pfb> > /amsfonts/cm/cmbx12.pfb> > mex10.pfb> > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb> > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb> > /public/amsfonts/cm/cmr17.pfb> > s/cm/cmr7.pfb>
> >  > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb>
> > Output written on root.pdf (28 pages, 198420 bytes).
> > Transcript written on root.log.
> > 
> > *** Failed to apply terminal proof method (line 128 of 
> > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy"):
> > *** goal (1 subgoal):
> > ***  1. ev (holds (op = r)) (rs @- flat (smap (%n. stake n rules) (fromN 
> > n)))
> > *** At command "qed" (line 128 of 
> > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy")
> > Finished HOL-Multivariate_Analysis (0:03:18 elapsed time, 0:10:58 cpu time, 
> > factor 3.32)
> > Building HOL-Probability ...
> > Finished HOL-Probability (0:03:20 elapsed time, 0:11:32 cpu time, factor 
> > 3.46)
> > Running Probabilistic_Noninterference ...
> > 
> > Probabilistic_Noninterference FAILED
> > (see also 
> > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Probabilistic_Noninterference)
> > 
> > mr/m/n/10 )$ \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 c1 $\OMS/cmsy/m/n/10 
> > ^^Y$\
> > OT1/cmr/m/it/10 01 c2 $\OMS/cmsy/m/n/10 ^^Q$ $\OT1/cmr/m/n/10 
> > ($\OT1/cmr/m/it/1
> > 0 c1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 c2$\OT1/cmr/m/n/10 )$ 
> > $\OMS/cmsy/m/n/1
> > 0 2$ \OT1/cmr/m/it/10 Example[]PL$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 
> > ZObis[] 
> > [69])) (./root.bbl) [70] (./root.aux) )
> > (see the transcript file for additional 
> > information) > s/type1/public/amsfonts/cm/cmbx10.pfb> > /amsfonts/cm/cmbx12.pfb> > mex10.pfb> > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb> > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb> > /public/amsfonts/cm/cmr17.pfb> > s/cm/cmr6.pfb>
> >  > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb>
> > Output written on root.pdf (70 pages, 254440 bytes).
> > Transcript written on root.log.
> > 
> > *** Undefined constant: "T.hitting_time" (line 235 of 
> > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy")
> > *** At command "abbreviation" (line 235 of 
> > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy")
> > Unfinished session(s): Abstract_Completeness, Probabilistic_Noninterference
> > 0:08:36 elapsed time, 0:33:24 cpu time, factor 3.88
> 
> 
> 
> ___
> 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] JinjaThreads FAILED

[Johannes Hölzl]

Sorry was my mistake, should be fixed with d5a3dbc9da17 now.

 - Johannes

Am Sonntag, den 16.11.2014, 19:48 +0100 schrieb Florian Haftmann:
> > isabelle: 059ba950a657 tip
> > afp: 0fdf8f639bb4 tip
> > Running JinjaThreads ...
> > 
> > 
> > JinjaThreads FAILED
> > (see also 
> > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/JinjaThreads)
> > 
> > *** At command "inductive" (line 413 of 
> > "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> > *** Type unification failed: No type arity prod :: floor_ceiling
> > *** 
> > *** Type error in application: incompatible operand type
> > *** 
> > *** Operator:  floor :: ??'a => int
> > *** Operand:   (x, ln) :: ??'b * (real => real)
> > *** 
> > *** Coercion Inference:
> > *** 
> > *** Local coercion insertion on the operand failed:
> > *** No type arity prod :: floor_ceiling
> > *** 
> > *** Now trying to infer coercions globally.
> > *** 
> > *** Coercion inference failed:
> > *** weak unification of subtype constraints fails
> > *** Clash of types "_ option" and "int"
> > *** 
> > *** At command "inductive" (line 413 of 
> > "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy")
> > Unfinished session(s): JinjaThreads
> > 0:13:06 elapsed time, 1:00:51 cpu time, factor 4.64
> ___
> 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: uniform document heading commands

[Johannes Hölzl]

Am Montag, den 03.11.2014, 10:30 +0100 schrieb Makarius:
> On Mon, 3 Nov 2014, Timothy Bourke wrote:

> > Would it also be reasonable to allow 'text' before an initial 'theory' ?
> 
> I have asked myself that yesterday, when updating some AFP entries in that 
> respect.
> 
> The canonical question: Is such a feature really needed?
> 
> So far the standard way is to say 'theory' first, before writing longer 
> paragraphs of text.  The concept of Isabelle document preparation is to 
> write in a formal context (which is required for antiquotations), but 
> before the theory start it is undefined.

In most cases I want to write a small (informal) introduction. But then
the "theory ... imports ... begin" command looks out of place in the
generated document and I hide it using (*<*) (*>*).

So having a way to write an abstract / or an informal introduction would
be nice.

 - Johannes

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

Re: [isabelle-dev] natfloor_div_nat not general enough

[Johannes Hölzl]

This is now generalized in the repository:

This generalizes to floor, and removes the assumption 0 <= y
  http://isabelle.in.tum.de/repos/isabelle/rev/d17b3844b726

This finally removes the assumption 0 <= x
  http://isabelle.in.tum.de/repos/isabelle/rev/387f65e69dd5


 - Johannes

Am Montag, den 27.10.2014, 09:42 +0100 schrieb Johannes Hölzl:
> I will fix it.
> 
>   - Johannes
> 
> Am Sonntag, den 26.10.2014, 17:25 + schrieb Lawrence Paulson:
> > FYI: the lemma is used only once, in Real.thy, and not at all in the AFP.
> > 
> > Still worth fixing though. Any volunteers?
> > 
> > Larry
> > 
> > > Begin forwarded message:
> > > 
> > > From: Joachim Breitner 
> > > To: isabelle-us...@cl.cam.ac.uk
> > > Date: 26 October 2014 14:15:40 GMT
> > > Subject: [isabelle] natfloor_div_nat not general enough
> > > 
> > > Hi,
> > > 
> > > Real.thy contains the lemma
> > > 
> > > lemma natfloor_div_nat:
> > >  assumes "1 <= x" and "y > 0"
> > >  shows "natfloor (x / real y) = natfloor x div y"
> > > 
> > > but the first assumption is redundant:
> > > 
> > > 
> > > lemma natfloor_div_nat:
> > >  assumes "y > 0"
> > >  shows "natfloor (x / real y) = natfloor x div y"
> > > proof-
> > >  have "x ≤ 0 ∨ x ≥ 0 ∧ x < 1 ∨ 1 ≤ x" by arith
> > >  thus ?thesis
> > >  proof(elim conjE disjE)
> > >assume *: "1 ≤ x"
> > >show ?thesis by (rule Real.natfloor_div_nat[OF * assms])
> > >  next
> > >assume *: "x ≤ 0"
> > >moreover
> > >from * assms have "x / y ≤ 0" by (simp add: field_simps)
> > >ultimately
> > >show ?thesis by (simp add: natfloor_neg)
> > >  next
> > >assume *: "x ≥ 0" "x < 1"
> > >hence "natfloor x = 0" by (auto intro: natfloor_eq)
> > >moreover
> > >from * assms have "x / y ≥ 0" and "x / y < 1" by (auto simp add: 
> > > field_simps)
> > >hence "natfloor (x/y) = 0" by (auto intro: natfloor_eq)
> > >ultimately
> > >show ?thesis by simp
> > >  qed
> > > qed
> > > 
> > > Greetings,
> > > Joachim
> > > 
> > > -- 
> > > Dipl.-Math. Dipl.-Inform. Joachim Breitner
> > > Wissenschaftlicher Mitarbeiter
> > > http://pp.ipd.kit.edu/~breitner
> > 
> > ___
> > 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] Fwd: [isabelle] natfloor_div_nat not general enough

[Johannes Hölzl]

I will fix it.

  - Johannes

Am Sonntag, den 26.10.2014, 17:25 + schrieb Lawrence Paulson:
> FYI: the lemma is used only once, in Real.thy, and not at all in the AFP.
> 
> Still worth fixing though. Any volunteers?
> 
> Larry
> 
> > Begin forwarded message:
> > 
> > From: Joachim Breitner 
> > To: isabelle-us...@cl.cam.ac.uk
> > Date: 26 October 2014 14:15:40 GMT
> > Subject: [isabelle] natfloor_div_nat not general enough
> > 
> > Hi,
> > 
> > Real.thy contains the lemma
> > 
> > lemma natfloor_div_nat:
> >  assumes "1 <= x" and "y > 0"
> >  shows "natfloor (x / real y) = natfloor x div y"
> > 
> > but the first assumption is redundant:
> > 
> > 
> > lemma natfloor_div_nat:
> >  assumes "y > 0"
> >  shows "natfloor (x / real y) = natfloor x div y"
> > proof-
> >  have "x ≤ 0 ∨ x ≥ 0 ∧ x < 1 ∨ 1 ≤ x" by arith
> >  thus ?thesis
> >  proof(elim conjE disjE)
> >assume *: "1 ≤ x"
> >show ?thesis by (rule Real.natfloor_div_nat[OF * assms])
> >  next
> >assume *: "x ≤ 0"
> >moreover
> >from * assms have "x / y ≤ 0" by (simp add: field_simps)
> >ultimately
> >show ?thesis by (simp add: natfloor_neg)
> >  next
> >assume *: "x ≥ 0" "x < 1"
> >hence "natfloor x = 0" by (auto intro: natfloor_eq)
> >moreover
> >from * assms have "x / y ≥ 0" and "x / y < 1" by (auto simp add: 
> > field_simps)
> >hence "natfloor (x/y) = 0" by (auto intro: natfloor_eq)
> >ultimately
> >show ?thesis by simp
> >  qed
> > qed
> > 
> > Greetings,
> > Joachim
> > 
> > -- 
> > Dipl.-Math. Dipl.-Inform. Joachim Breitner
> > Wissenschaftlicher Mitarbeiter
> > http://pp.ipd.kit.edu/~breitner
> 
> ___
> 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] @ML antiquotation in generated code

[Johannes Hölzl]

In 3094b0edd6b5 I needed to change a document comment {* ..*} to a
source comment (* .. *). Looks like using the @{ML ..} antiquotation in
a document comment does not work. Latex does not allow \verb inside
commands-parameters.

Is it possible to change \verb to \texttt, with the necessary _ -> \_
and maybe more conversions?

 - Johannes



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

Re: [isabelle-dev] Products over lists – naming convention for big sums and products.

[Johannes Hölzl]

Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann:
> Changeset #fe083c681ed8 introduces products over lists.  There has been
> some private discussion whether there could be a serious attempt to
> establish a new consistent naming scheme for summation and products over
> collections.
> 
> a) for lists: sum_list (← listsum), prod_list (← listprod)
> b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod)
> c) for finite sets: Sum (← setsum), Prod (← setprod)

I assume a) means Sum_list and Prod_list?!

Why Sum and not Sum_set in c)? Is the intention that the canonical type
always gets the short name? Like map instead of map_list.

And why upper case Sum instead of sum?

 - Johannes

PS: Maybe c) could be tackled in the future when we have a hypothetical
constant/lemma renaming tool.

> As far as can be forseen, 58 theories would be affected by a switch as
> suggested by a). b) is no big issue. c) is maybe beyond what should be
> reasonably attempted (218 affected theories).
>   
> Suggestions welcome.
>   
> Cheers,
>   Florian
> 
> ___
> 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] Methods that fail with stack-overflow

[Johannes Hölzl]

However this happened at the Scala level. Nitpick produced a huge number
in Suc representation, which the output panel was only possible to
display when the Java stack size was 16MB. 

 - Johannes

Am Donnerstag, den 03.07.2014, 14:16 +0200 schrieb Tobias Nipkow:
> Funnily enough I had the same problem yesterday and was at a loss what 
> happened
> until Johannes pointed out to me that there is a "stack overflow" message in 
> the
> shell window. Of course you need to scroll through all those messages to find 
> it.
> 
> Tobias
> 
> On 03/07/2014 13:57, Peter Lammich wrote:
> > Hi,
> > 
> > I recently ran into a method that produced a stack-overflow.
> > 
> > The good thing is: In the current jedit version, it is properly
> > highlighted and you immediately see that there is some error. (This was
> > not always the case in the past)
> > 
> > The bad thing: The only way how to get a clue what is going wrong is to
> > open the "raw output panel". This writes "stack-overflow" then, without
> > any location or trace. How to enable tracing for those exceptions, in
> > particular as Toplevel.debug seems to have gone away?
> > 
> > --
> >   Peter
> > 
> > ___
> > 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] Build problems in AFP with current tips

[Johannes Hölzl]

Fixed in AFP 833ddc4860dd.

 - Johannes

Am Mittwoch, den 18.06.2014, 22:32 +0200 schrieb Florian Haftmann:
> The two other failures are also reproducible interactively and seem to
> result from recent changes in HOL-Probability.  Johannes, I guess this
> is your part.
> 
>   Florian
> 
> On 18.06.2014 21:39, Lawrence Paulson wrote:
> > Strange — I took a look (with the latest versions, same ids as quoted) and 
> > it was fine.
> > 
> > 
> > On 18 Jun 2014, at 18:47, Florian Haftmann 
> >  wrote:
> > 
> >> isabelle: 88263522c31e tip
> >> afp: b514f0bac50e tip
> >>
> >> Completeness FAILED
> >> *** Failed to load theory "Soundness" (unresolved "Completeness")
> >> *** Extra variables on rhs: "founded", "bounded"
> >> *** The error(s) above occurred in definition:
> >> *** "proofTree A == bounded A & founded subs (SATAxiom o sequent) A"
> >> *** At command "definition" (line 70 of
> >> "/mnt/home/haftmann/data/afp/master/thys/Completeness/Completeness.thy")
> > 
> 


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

Re: [isabelle-dev] Testboard problem

[Johannes Hölzl]

We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it
works...

I don't know why mira is accessing this file, it actually sets up the
settings file to _not_ look into the users heaps-directory. But it looks
like there is a problem with this setup.

 - Johannes



Am Mittwoch, den 04.06.2014, 10:18 +0200 schrieb Johannes Hölzl:
> Hi,
> 
> a change of mine leads to a failure of the testboard,
> HOL-Proofs-Extraction can not be build anymore.
> 
> For example see:
> 
> http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28
> 
> But when I run on this very changeset the commands
> 
>   isabelle build -b HOL-Proofs-Extraction
> 
> or
> 
>   isabelle build -a
> 
> on my machine, everything runs fine.
> 
> Is there a special setup for the testboard when it runs Isabelle
> makeall?
> 
>  - Johannes
> 
> ___
> 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] Testboard problem

[Johannes Hölzl]

Hi,

a change of mine leads to a failure of the testboard,
HOL-Proofs-Extraction can not be build anymore.

For example see:

http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28

But when I run on this very changeset the commands

  isabelle build -b HOL-Proofs-Extraction

or

  isabelle build -a

on my machine, everything runs fine.

Is there a special setup for the testboard when it runs Isabelle
makeall?

 - Johannes

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

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

[Johannes Hölzl]

Am Sonntag, den 11.05.2014, 04:55 -0700 schrieb Andrei Popescu:
> > Johannes wrote:
> > Theorems about complex numbers are now stated only using Re and Im,
> the Complex
> >  constructor is not used anymore. It is possible to use primcorec to
> defined the behaviour of a complex-valued function.
> 
> >> Makarius wrote:
> >> That is indeed very nice.  Is that a new invention or an old trick
> that every category theorist knows?

I do not count myself a category theorist (I don't know what a functor
adjunction is). As Manuel pointed out, the change was mostly a
bureaucratic one.
It boils down to the fact that the Re/Im rules should match more often.

For example assume one wants to proof:

  "Complex a b + cis x + Complex c d = cis x + Complex (c + a) (b + d)"

(where "cis x = cos x + i * sin x")

With complex_eq_iff and the Re/Im rules this can be proved by
field_simps, even without giving Re/Im rules for cis. When we only have
the Complex rules, this does not work, we need either to do a case-split
on "cis x", or unfold cis_def. 

 - Johannes


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

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

[Johannes Hölzl]

* Theorems about complex numbers are now stated only using Re and Im, the 
Complex
  constructor is not used anymore. It is possible to use primcorec to defined 
the
  behaviour of a complex-valued function.

  Removed theorems about the Complex constructor from the simpset, they are
  available as the lemma collection legacy_Complex_simps. This especially
  removes
i_complex_of_real: "ii * complex_of_real r = Complex 0 r".

  Instead the reverse direction is supported with
Complex_eq: "Complex a b = a + \ * b"

  Moved csqrt from Fundamental_Algebra_Theorem to Complex.

  Renamings:
Re/Im  ~>  complex.sel
complex_Re/Im_zero ~>  zero_complex.sel
complex_Re/Im_add  ~>  plus_complex.sel
complex_Re/Im_minus~>  uminus_complex.sel
complex_Re/Im_diff ~>  minus_complex.sel
complex_Re/Im_one  ~>  one_complex.sel
complex_Re/Im_mult ~>  times_complex.sel
complex_Re/Im_inverse  ~>  inverse_complex.sel
complex_Re/Im_scaleR   ~>  scaleR_complex.sel
complex_Re/Im_i~>  ii.sel
complex_Re/Im_cnj  ~>  cnj.sel
Re/Im_cis  ~>  cis.sel

complex_divide_def   ~>  divide_complex_def
complex_norm_def ~>  norm_complex_def
cmod_def ~>  norm_complex_de

  Removed theorems:
complex_zero_def
complex_add_def
complex_minus_def
complex_diff_def
complex_one_def
complex_mult_def
complex_inverse_def
complex_scaleR_def

-

This is also a surprising application of primcorec!

 - Johannes



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

Re: [isabelle-dev] status (AFP)

[Johannes Hölzl]

I use "isabelle afp_build Probabilistic_Noninterference" to build it,
which includes the document generation. So it is possible that the
document generation on the macbroy2 is different from my setup.

Looking into the reports attached to the status email, I also see that
the log for Probabilistic_Noninterference is missing!


 - Johannes


Am Montag, den 05.05.2014, 11:18 +0200 schrieb Dmitriy Traytel:
> Could it be the document preparation?
> 
> Dmitriy
> 
> Am 05.05.2014 11:17, schrieb Johannes Hölzl:
> > Has anybody an idea why the AFP test for Probabilistic_Noninterference
> > fails?
> >
> > When I build it on my machine with either the combination in the email
> > (i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a recent hg version
> > (AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems.
> >
> >   - Johannes
> >
> > Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle :
> >> The status of the following AFP entries changed or remains FAIL:
> >> [Selection_Heap_Sort] is still on FAIL.
> >> [Native_Word] is still on FAIL.
> >> [HyperCTL] is still on FAIL.
> >> [Launchbury] is still on FAIL.
> >> [Probabilistic_Noninterference] is still on FAIL.
> >>
> >> Full entry status at http://afp.sourceforge.net/status.shtml
> >>
> >> AFP version: development -- hg id acd2cc051b4f
> >> Isabelle version: devel -- hg id 52e5bf245b2a
> >> Test ended on: macbroy2, Mon May  5 07:50:12 CEST 2014.
> >>
> >> Have a nice day,
> >>isatest
> >>
> >
> > ___
> > 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] status (AFP)

[Johannes Hölzl]

Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?

When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a recent hg version
(AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems.

 - Johannes

Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle :
> The status of the following AFP entries changed or remains FAIL: 
> [Selection_Heap_Sort] is still on FAIL.
> [Native_Word] is still on FAIL.
> [HyperCTL] is still on FAIL.
> [Launchbury] is still on FAIL.
> [Probabilistic_Noninterference] is still on FAIL.
> 
> Full entry status at http://afp.sourceforge.net/status.shtml
> 
> AFP version: development -- hg id acd2cc051b4f
> Isabelle version: devel -- hg id 52e5bf245b2a
> Test ended on: macbroy2, Mon May  5 07:50:12 CEST 2014.
> 
> Have a nice day,
>   isatest
> 


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

[isabelle-dev] Unresponsive Isabelle/jEdit

[Johannes Hölzl]

Currently I have the problem that when opening a file in
Multivariate_Analysis it can take quite some time until the theories it
depends on are loaded. In this time I/jEdit does not respond to mouse or
keyboard input.

For example:
 1) I'm opening
~~/src/HOL/Multivaraiate_Analysis/Complex_Analysis_Basic.thy
 2) I/jEdit loads around 10 theories
 3) I/jEdit stops at the end of Topology_Euclidean_Space
 4) now I/jEdit is for a couple of minutes not responsible,
   and uses a lot of cpu resources (top says java, but maybe also poly)
 5) this continuous with Cartesian_Euclidean_Space, and so on

Before I/jEdit did always react to mouse or keyboard input, even when
loading the theries.

I tried to bisect the recent changes, and the problem seams to be appear
with the changeset

  0fc032898b05: back to cumulative treatment of command status, which is
important for total accounting (amending
8201790fdeb9);).


 - Johannes

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

Re: [isabelle-dev] Consolidation of manual naming

[Johannes Hölzl]

+1

Fortunately, nowadays the list of manuals shown in jEdit is very helpful
here.

Am Mittwoch, den 26.03.2014, 22:07 +0100 schrieb Florian Haftmann:
> Hi,
> 
> since ancient times there is a glitch in the naming of manuals vs. their
> originating sessions, e.g. isar-ref vs. IsarRef.
> 
> Would it be worth an effort to consolidate this?  I regularly get
> confused about that.
> 
> Cheers,
>   Florian


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

[isabelle-dev] NEWS: clean up Series and Deriv in Complex_Main

[Johannes Hölzl]

* Removed and renamed theorems in Series:
  summable_le ~>  suminf_le
  suminf_le   ~>  suminf_le_const
  series_pos_le   ~>  setsum_le_suminf
  series_pos_less ~>  setsum_less_suminf
  suminf_ge_zero  ~>  suminf_nonneg
  suminf_gt_zero  ~>  suminf_pos
  suminf_gt_zero_iff  ~>  suminf_pos_iff
  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  suminf_0_le ~>  suminf_nonneg [rotate]
  pos_summable~>  summableI_nonneg_bounded
  ratio_test  ~>  summable_ratio_test

  removed series_zero, replaced by sums_finite

  removed auxiliary lemmas:
sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
real_setsum_nat_ivl_bounded,
summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
sumr_one_lb_realpow_zero, summable_convergent_sumr_iff,
sumr_diff_mult_const
INCOMPATIBILITY.

* Replace (F)DERIV syntax by has_derivative:
  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s :
f'"

  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x :
s : f'"

  - "f differentiable at x within s" replaces "_ differentiable _ in _"
syntax

  - removed constant isDiff

  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
input
syntax.

  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed

  - Renamed FDERIV_... lemmas to has_derivative_...

  - Other renamings:
differentiable_def~>  real_differentiable_def
differentiableE   ~>  real_differentiableE
fderiv_def~>  has_derivative_at
field_fderiv_def  ~>  field_has_derivative_at
isDiff_der~>  differentiable_def
deriv_fderiv  ~>  has_field_derivative_def
INCOMPATIBILITY.


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

Re: [isabelle-dev] HOL-Decision_Procs FAILED

[Johannes Hölzl]

Sorry for the inconvenience introduced by my changeset.
And thanks Brian for fixing it so fast!

 - Johannes

Am Dienstag, den 18.03.2014, 12:10 -0700 schrieb Brian Huffman:
> Revision c7dfd924a165 should now take care of it.
> 
> - Brian
> 
> On Tue, Mar 18, 2014 at 11:47 AM, Makarius  wrote:
> > On Tue, 18 Mar 2014, Florian Haftmann wrote:
> >
> >> hg id 9ffbb4004c81
> >
> >
> > I've noticed this as well, when preparing a push.  The broken state means I
> > have to roll back and wait until tomorrow.
> >
> > Everything comes to a grinding halt, just because a routine "build -a" (with
> > usual -j options) of maybe 20min was forgotten.
> >
> >
> > Makarius


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

Re: [isabelle-dev] 'specification' and 'ax_specification'

[Johannes Hölzl]

Yes, the same here. I would like to use specification sometimes, but
without supporting contexts it not as helpful as it could. I also do not
need ax_specification.

So my preference is option (b).

 - Johannes

Am Freitag, den 14.03.2014, 15:10 +0100 schrieb Andreas Lochbihler:
> I myself found specification quite convenient and use it occasionally, e.g., 
> in 
> AFP/Containers/Set_Linorder and a number of my private developments. It's a 
> useful 
> shortcut to a definition with SOME and deriving the properties later with 
> someI. It would 
> be good if it works with contexts. I have never used ax_specification, though.
> 
> Andreas
> 
> On 14/03/14 14:44, Makarius wrote:
> > On Fri, 14 Mar 2014, Jasmin Blanchette wrote:
> >
> >>>  * HOL/Tools/choice_specification.ML which is loaded into
> >>>HOL/Hilbert_Choice.thy -- really old stuff that would require serious
> >>>renovation if actually used: 'ax_specification' with its unchecked
> >>>axiomatization is actually unsed, and 'specification' only by
> >>>HOL-Auth (and its many clones).
> >>>
> >>>A candidate for HOL-Library, after removing the axiomatic part?
> >>>Nitpick seems to have special tricks to cope with it, though.
> >>
> >> These special tricks could be taken out. They're not vital in any way.
> >
> > (This deserves its own mail thread.)
> >
> > Motivated by the surprise about ``"code_pred" introduces axioms?'' from 
> > last October
> > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00228.html
> > I've checked the situation more systematically some weeks ago.
> >
> > Spurious axiomatizations can lead to unpleasant surprises to users that are 
> > unaware of the
> > danger.  We probably can't do anything about code_pred now, but check the 
> > general
> > situations about further such trapdoors.
> >
> >
> > So how about 'ax_specification'?  It is an alternate personality of 
> > 'specification' that
> > would make it very hard to renovate the latter, if that is desirable at all:
> > 'ax_specification' is unused and 'specification' only used in HOL-Auth and 
> > its
> > derivatives, which appears to have been a demo for that.
> >
> > There are various possibilities:
> >
> >(a) Do nothing and let this old stuff collect more dust.
> >
> >(b) Remove 'ax_specification' and brush-up 'specification' a little
> >(proper local contexts, PIDE markup etc.).
> >
> >(c) Remove both 'ax_specification' and 'specification', and do the
> >HOL-Auth applications with a hypothetical context, potentially
> >with a proven interpretation of the assumptions.
> >
> >
> >  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

Re: [isabelle-dev] AFP failures

[Johannes Hölzl]

Am Dienstag, den 26.11.2013, 13:12 +0100 schrieb Makarius:
[..]
> > I added now Zorn to HOL-Library (isa# acb41098607a), at least
> > Coinductive works now.
> 
> I don't understand this at all, neither the above explanation nor the 
> formal changeset (with its vacuous log message).
> 
> How does the inclusion or non-inclusion of some theory affect the latex 
> macro environment?

When Zorn is not in HOL-Library its tex-output is included in the
document for AFP-Coinductive. The root.tex for AFP-Coinductive does not
include the setup for \sqsubset, so its pdf-generation fails. By adding
Zorn back to HOL-Library, the output for Zorn is not included in the pdf
for AFP-Coinductive.

 - Johannes



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

Re: [isabelle-dev] AFP failures

[Johannes Hölzl]

Am Dienstag, den 26.11.2013, 11:52 +0100 schrieb Jasmin Christian
Blanchette:
> The AFP tests are finally back, and this revealed a series of failures
> related to my refactorings last week. Looking more closely at the
> falures, I found they were all in the LaTeX generation, which I hadn't
> tested locally before pushing. In most of the theories, it's the LaTeX
> symbol \sqsubset that causes problem, because the necessary package is
> not included.
> 
> Does anybody have any idea of why this suddenly pops up as an issue
> just because I moved a few theories around?

Looks like Zorn's lemma is not included in HOL-Library anymore. When
Coinductive loads Zorn it is also included in the Latex document. (Zorn
uses \sqsubset in a local)

I added now Zorn to HOL-Library (isa# acb41098607a), at least
Coinductive works now.

 - Johannes


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

Re: [isabelle-dev] Problem in AFP/Ordinary_Differential_Equations

[Johannes Hölzl]

solved in afp id 03689082b646

Am Dienstag, den 05.11.2013, 19:09 +0100 schrieb Florian Haftmann:
> isabelle id 9d623cada37f
> afp id 68e8895167cc



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

[isabelle-dev] NEWS: updated conditionally complete lattices

[Johannes Hölzl]

*** HOL ***

* SUP and INF generalized to conditionally_complete_lattice

* Theory Lubs moved from HOL image to HOL-Library. It is replaced by
Conditionally_Complete_Lattices.   INCOMPATIBILITY.

* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
instead of explicitly stating boundedness of sets.


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

[isabelle-dev] Should code_abort remove the corresponding code equations?

[Johannes Hölzl]

Hi *,

code_abort does not remove the corresponding code equations
(in Isabelle 19764bef2730)

  definition "test = True"
  code_abort test
  value [code] test -- "outputs True"

  definition [code del]: "test2 = True"
  code_abort test2
  value [code] test2 -- "raises 'test' exception"

Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.

Greetings,
 - Johannes



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

Re: [isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)

[Johannes Hölzl]

Hi Stephen,

Am Dienstag, den 25.06.2013, 17:37 -0500 schrieb Stephen Nuchia:
> Just joined the list, still very much a beginner but I think the attached
> change is valid and desirable.  The theorem trace_mul_sym in
> HOL/Multivariate_Analysis/Determinants.thy is not stated in full
> generality; relaxing the restriction that the factor matrices be
> individually square is valid.  In fact, the original proof script succeeds
> unmodified.

I pushed your bundle to the Isabelle repository!
  http://isabelle.in.tum.de/repos/isabelle/rev/e64c1344f21b

Are you working on a formalization using the linear algebra in
Determinants?


 - Johannes

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

Re: [isabelle-dev] Isabelle takes more time to be built on testboard

[Johannes Hölzl]

Hi,

My changes Ondřej mentions are between
  Old: http://isabelle.in.tum.de/repos/isabelle/rev/7957d26c3334
and
  New: http://isabelle.in.tum.de/repos/isabelle/rev/f415febf4234

Where I were mostly moving stuff around in HOL. This should be only visible
in Complex_Main and not in Main. But the HOL-Proof and especially the
ZF images also take more time. 

 - Johannes


Am Montag, den 13.05.2013, 15:01 +0200 schrieb Ondřej Kunčar:
> Hi!
> Recently I noticed that it takes considerably more time to build 
> Isabelle (makeall) on testboard than it used to take before. I did a 
> small inspection and something must have happened between 25.3.2013 and 
> 26.3.2013 because this build from 25.3. took 27 minutes
> https://isabelle.in.tum.de/testboard/Isabelle/report/91ed3c78c39c44a8a0f1c3e241973bb7
> and this build from 26.3.2008 took 42 minutes.
> https://isabelle.in.tum.de/testboard/Isabelle/report/da1a4b7e64ee47fc9ce315741bb78ecc
> 
> I talked to Johannes and this slowdown doesn't seem to be related to his 
> changes from 26.3.
> One can also see here that almost all sessions started to take more time 
> to be built around that time:
> http://isabelle.in.tum.de/devel/stats/at-poly.html
> 
> Any ideas?
> 
> Ondrej
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



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

[isabelle-dev] linear_continuum_topology (was: NEWS)

[Johannes Hölzl]

Am Donnerstag, den 25.04.2013, 10:56 +0200 schrieb Johannes Hölzl:
> I also renamed the type class linear_continuum_topology to
> connected_linorder_topology as they are not compact spaces. If somebody
> knows a better name for these spaces I'm also happy to rename them. 

Okay, forget this.

"linear_continuum_topology" is actually the right name. But we need the
additional axiom that the type has more than one element.


  - Johannes



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

Re: [isabelle-dev] NEWS

[Johannes Hölzl]

Am Mittwoch, den 24.04.2013, 11:45 +0200 schrieb Tjark Weber:
> Johannes,
> 
> On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote:
> > * Introduce type class "conditional_complete_lattice": Like a complete
> >   lattice but does not assume the existence of the top and bottom elements.
> 
> The name "conditional complete lattice" suggests a special kind of
> complete lattice. However, without top and bottom elements, this
> structure is not a complete lattice at all. In the literature, it is
> therefore more aptly called "conditionally complete lattice." I propose
> to retain the "-ly" suffix in the name of the type class.

Thanks for noticing this! I changed it now in Isabelle #9328c6681f3c .

I also renamed the type class linear_continuum_topology to
connected_linorder_topology as they are not compact spaces. If somebody
knows a better name for these spaces I'm also happy to rename them. 

 - Johannes

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

[isabelle-dev] NEWS

[Johannes Hölzl]

This sums up the cleanup / generalizations / unifications I did on
HOL-Complex_Main and HOL-Multivariate_Analysis in the last four month. 

 9< --

* Introduce type class "conditional_complete_lattice": Like a complete
  lattice but does not assume the existence of the top and bottom elements.
  Allows to generalize some lemmas about reals and extended reals.
  Removed SupInf and replaced it by the instantiation of
  conditional_complete_lattice for real. Renamed lemmas about conditional
  complete lattice from Sup_... to cSup_... and from Inf_... to
  cInf_... to avoid hidding of similar complete lattice lemmas.
INCOMPATIBILITY.

* Introduce type classes "no_top" and "no_bot" for orderings without top
  and bottom elements.

* Split dense_linorder into inner_dense_order and no_top, no_bot.

* Complex_Main: Unify and move various concepts from
  HOL-Multivariate_Analysis to HOL-Complex_Main.

 - Introduce type class (lin)order_topology. Allows to generalize theorems
   about limits and order. Instances are reals and extended reals.

 - continuous and continuos_on from Multivariate_Analysis:
   "continuous" is the continuity of a function at a filter.
   "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f".

   Generalized continuity lemmas from isCont to continuous on an arbitrary
   filter.

 - compact from Multivariate_Analysis. Use Bolzano's lemma
   to prove compactness of closed intervals on reals. Continuous functions
   attain infimum and supremum on compact sets. The inverse of a continuous
   function is continuous, when the function is continuous on a compact set.

 - connected from Multivariate_Analysis. Use it to prove the
   intermediate value theorem. Show connectedness of intervals on order
   topologies which are a inner dense, conditional complete linorder.

 - first_countable_topology from Multivariate_Analysis. Is used to
   show equivalence of properties on the neighbourhood filter of x and on
   all sequences converging to x.

 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems
   from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on
   FDERIV. Add variants of DERIV and FDERIV which are restricted to sets,
   i.e. to represent derivatives from left or right.

 - Removed the within-filter. It is replaced by the principal filter:

 F within X = inf F (principal X)

 - Introduce "at x within U" as a single constant, "at x" is now an
   abbreviation for "at x within UNIV"

 - Introduce named theorem collections tendsto_intros, continuous_intros,
   continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or
   FDERIV_intros) are also available as tendsto_eq_intros (or
   FDERIV_eq_intros) where the right-hand side is replaced by a congruence
   rule. This allows to apply them as intro rules and then proving
   equivalence by the simplifier.

 - Restructured theories in HOL-Complex_Main:

   + Moved RealDef and RComplete into Real

   + Introduced Topological_Spaces and moved theorems about
 topological spaces, filters, limits and continuity to it

   + Renamed RealVector to Real_Vector_Spaces

   + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and
 Limits

   + Moved Ln and Log to Transcendental

   + Moved theorems about continuity from Deriv to Topological_Spaces

 - Remove various auxiliary lemmas.

INCOMPATIBILITY.


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

Re: [isabelle-dev] auto raises a TYPE exception

[Johannes Hölzl]

Am Freitag, den 05.04.2013, 14:16 +0200 schrieb Makarius:
> On Fri, 5 Apr 2013, Johannes Hölzl wrote:
> 
> > It looks like the problem is somewhere in the call to 
> > Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
> >
> >   clasimp.ML  
> >
> > fun nodup_depth_tac ctxt m i st =
> >  SELECT_GOAL
> >(Classical.safe_steps_tac ctxt 1 THEN_ELSE
> >  (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
> >Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
> >  (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 
> > 1) 1 i st;
> >
> > ---
> >
> > Dmitriy and I tried to simplify the testcase by replicating the goal on
> > which inst0_step_tac is called but could not replicated the failure.
> 
> > * How can I activate backtraces in ML to get an better understand of the
> > problem? I tried declare [[ML_trace = true]] but I didn't get a
> > backtrace.
> 
> ML_trace is only for the static phase, to say what is the actual ML source 
> after expanding antiquotations.
> 
> In principle ML "Toplevel.debug := true" gives you an exception trace 
> (only visible on "Raw Output"), but it is hidden behind lazy sequence 
> evaluation here.  So you should try the exception_trace combinator in the 
> deeper parts of the ML code, where you suspect a problem.

Ah that's good to know!

Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions
which call Envir.var_clash is not shown.

I checked Isabelle2012 and Isabelle2011, the exception happens also
there, so it is not special to Isabelle2013 or the development
repository.

 - Johannes


 8< 

theory Scratch
  imports Main
begin

consts P :: "'a set => bool"
lemma P_Int [intro]:  "P A ==> P B ==> P (A Int B)" sorry
lemma P_UNIV [intro]: "P UNIV" sorry
lemma P_INT [intro]: "ALL x : A. P (B x) ==> P (INT x : A. B x)" sorry
lemma P_UNION [intro]: "ALL x : A. P (B x) ==> P (UN x : A. B x)" sorry

lemma 
  fixes x :: "'a" and Q :: "'b => bool" and f :: "'a => 'b"
  shows "EX S. P S & x : S & (ALL xa : S. Q (f xa))"
  apply (auto simp only: )


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

[isabelle-dev] auto raises a TYPE exception

[Johannes Hölzl]

Hi,

In Isabelle2013 as well as the current development revision (#0a7b4e0384d0)
the following call to "auto" raises a TYPE exception in envir.ML

 8< 
theory Scratch
  imports Main
begin

class test =
  fixes P :: "'a set ⇒ bool"

lemma
  shows P_UNIV [intro]: "P UNIV"
and P_Int [intro]: "P S ⟹ P T ⟹ P (S ∩ T)"
and P_Union [intro]: "∀S∈K. P S ⟹ P (⋃ K)"
and P_INT [intro]: "finite A ⟹ ∀x∈A. P (B x) ⟹ P (⋂x∈A. B x)"
sorry

lemma
  fixes Q :: "'b ⇒ bool" and f :: "'a::test ⇒ 'b"
  shows "(∃S. P S ∧ x ∈ S ∧ (∀xa∈S. Q (f xa)))"
  apply (auto simp only:)
  oops



It looks like the problem is somewhere in the call to Classical.inst0_step_tac 
in nodup_depth_tac (clasimp.ML):

  clasimp.ML  

fun nodup_depth_tac ctxt m i st =
  SELECT_GOAL
(Classical.safe_steps_tac ctxt 1 THEN_ELSE
  (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
  (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 
1 i st;

---

Dmitriy and I tried to simplify the testcase by replicating the goal on
which inst0_step_tac is called but could not replicated the failure.

* Has anybody a idea what is causing this exception?

* Any helpful tips how to continue to debug this bug?

* How can I activate backtraces in ML to get an better understand of the
problem? I tried declare [[ML_trace = true]] but I didn't get a
backtrace.


Greetings,
  Johannes

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

Re: [isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

Hi Thomas _Sewell_,

no no don't worry, the report was from Thomas _Tuerk_! And the change
was not too hard to produce.

What were your problems with the let-simproc? Did it to much or not
enough unfolding?

 - Johannes

Am Donnerstag, den 07.02.2013, 11:34 +1100 schrieb Thomas Sewell:
> I'd forgotten I'd ever reported this to you.
> 
> My problems with let_simproc run a little deeper anyway, and I've moved 
> to a different approach in the meanwhile. Sorry if I've left you 
> labouring on my behalf.
> 
> Yours,
>      Thomas.
> 
> On 07/02/13 02:38, Johannes Hölzl wrote:
> > Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius:
> >> On Tue, 5 Feb 2013, Johannes Hölzl wrote:
> >>
> >>> there is a bugproblem with the let-simproc, resulting in a non
> >>> terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
> >>> isabelle-release):
> >>>
> >>>   theory Scratch imports Complex_Main begin
> >>>
> >>>   lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
> >>> using [[simp_trace]]
> >>> apply simp
> >>>
> >>> The attached hg-bundle changes this behaviour to a terminating simproc.
> >>> (The bundle can be applied to a repo containing #58e2d0cd81ae by
> >>> "hg pull let_simp_betaeta.bundle")
> >>>
> >>> It currently runs in the testboard:
> >>>   http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c
> >>>
> >>> @Makarius: Is it possible to include this patch in Isabelle2013, when
> >>> the testboard run is green?
> >> Testboard does not test very much, compared to what has been tested
> >> manually and semi-automatically in the past 2 weeks for the release.  AFP
> >> would also have to be covered.
> >>
> >> Anyway, this behaviour of let_simproc seems to have been there from its
> >> beginning, or at least back until Isabelle2011 (what is what I have
> >> tried). Nobody has noticed a problem in several years, so this change is
> >> for the next release, unless there are really strong reasons to revisit it
> >> now.
> >>
> >>
> >>Makarius
> > Thomas reported the problem to me. For me it is okay to fix it after
> > Isabelle2013.
> >
> > @Thomas: Is it important for you to fix it in Isabelle2013? I hope the
> > workaround with adding Let_def to the simplifier should work fine. Then
> > I will add it just to the development version of Isabelle.
> >
> >   - Johannes
> >
> >
> >
> >
> >
> > ___
> > 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 with let-simproc

[Johannes Hölzl]

Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius:
> On Tue, 5 Feb 2013, Johannes Hölzl wrote:
> 
> > there is a bugproblem with the let-simproc, resulting in a non
> > terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
> > isabelle-release):
> >
> >  theory Scratch imports Complex_Main begin
> >
> >  lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
> >using [[simp_trace]]
> >apply simp
> >
> > The attached hg-bundle changes this behaviour to a terminating simproc.
> > (The bundle can be applied to a repo containing #58e2d0cd81ae by
> > "hg pull let_simp_betaeta.bundle")
> >
> > It currently runs in the testboard:
> >  http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c
> >
> > @Makarius: Is it possible to include this patch in Isabelle2013, when
> > the testboard run is green?
> 
> Testboard does not test very much, compared to what has been tested 
> manually and semi-automatically in the past 2 weeks for the release.  AFP 
> would also have to be covered.
> 
> Anyway, this behaviour of let_simproc seems to have been there from its 
> beginning, or at least back until Isabelle2011 (what is what I have 
> tried). Nobody has noticed a problem in several years, so this change is 
> for the next release, unless there are really strong reasons to revisit it 
> now.
> 
> 
>   Makarius

Thomas reported the problem to me. For me it is okay to fix it after
Isabelle2013.

@Thomas: Is it important for you to fix it in Isabelle2013? I hope the
workaround with adding Let_def to the simplifier should work fine. Then
I will add it just to the development version of Isabelle.

 - Johannes





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

Re: [isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

Okay, this fails in HOL-IMP.

The check I introduced is to strong. I relaxed the check now and it
should check if f =beta-eta-alpha= g, where g is the simplified version
of f.

The testboard changeset is:
 http://isabelle.in.tum.de/testboard/Isabelle/rev/e9827a6f934e

 - Johannes

Am Dienstag, den 05.02.2013, 14:48 +0100 schrieb Johannes Hölzl:
> Hi Isabelle-dev,
> 
> there is a bugproblem with the let-simproc, resulting in a non
> terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
> isabelle-release):
> 
>   theory Scratch imports Complex_Main begin
> 
>   lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
> using [[simp_trace]]
> apply simp
> 
> The attached hg-bundle changes this behaviour to a terminating simproc. 
> (The bundle can be applied to a repo containing #58e2d0cd81ae by
> "hg pull let_simp_betaeta.bundle")
> 
> It currently runs in the testboard:
>   http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c
> 
> @Makarius: Is it possible to include this patch in Isabelle2013, when
> the testboard run is green?
> 
> == Analysis ==
> 
> The let-simproc produces:
>   (let x = Collect P in R x x ∧ (Ball s P)) ==
>   (let x = Collect P in R x x ∧ (ALL t : s. P t))
> 
> So it looks like the simproc forgets a eta-conversion step.
> 
> == Solution ==
> 
> The problematic part is (in HOL.thy, let_simp):
> 
>   if (Term.betapply (f, x)) aconv g then NONE (*avoid identity conversion*)
> 
> I would apply Envir.beta_eta_contract on both sides:
> 
>   if (Envir.beta_eta_contract (Term.betapply (f, x))) aconv 
> (Envir.beta_eta_contract g) then NONE (*avoid identity conversion*)
> 
> Or is there a better way to do this?
> 
> Greetings,
>   Johannes
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



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

[isabelle-dev] Problem with let-simproc

[Johannes Hölzl]

Hi Isabelle-dev,

there is a bugproblem with the let-simproc, resulting in a non
terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
isabelle-release):

  theory Scratch imports Complex_Main begin

  lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X"
using [[simp_trace]]
apply simp

The attached hg-bundle changes this behaviour to a terminating simproc. 
(The bundle can be applied to a repo containing #58e2d0cd81ae by
"hg pull let_simp_betaeta.bundle")

It currently runs in the testboard:
  http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c

@Makarius: Is it possible to include this patch in Isabelle2013, when
the testboard run is green?

== Analysis ==

The let-simproc produces:
  (let x = Collect P in R x x ∧ (Ball s P)) ==
  (let x = Collect P in R x x ∧ (ALL t : s. P t))

So it looks like the simproc forgets a eta-conversion step.

== Solution ==

The problematic part is (in HOL.thy, let_simp):

  if (Term.betapply (f, x)) aconv g then NONE (*avoid identity conversion*)

I would apply Envir.beta_eta_contract on both sides:

  if (Envir.beta_eta_contract (Term.betapply (f, x))) aconv 
(Envir.beta_eta_contract g) then NONE (*avoid identity conversion*)

Or is there a better way to do this?

Greetings,
  Johannes



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

[isabelle-dev] NEWS: removed indexed basis

[Johannes Hölzl]

* HOL/Multivariate_Analysis:
  Replaced "basis :: 'a::euclidean_space => nat => real" and
  "\\ :: (nat => real) => 'a::euclidean_space" on euclidean spaces by
  using the inner product "_ \ _" with vectors from the Basis set.
  "\\ i. f i" is replaced by "SUM i : Basis. f i *r i".

  With this change the following constants are also chanegd or removed:

DIM('a) :: nat   ~>   card (Basis :: 'a set)   (is an abbreviation)
a $$ i~>inner a i  (where i : Basis)
cart_base i removed
\, \'   removed

  Theorems about these constants where removed.

  Renamed lemmas:

component_le_norm   ~>   Basis_le_norm
euclidean_eq   ~>   euclidean_eq_iff
differential_zero_maxmin_component   ~>   differential_zero_maxmin_cart
euclidean_simps   ~>   inner_simps
independent_basis   ~>   independent_Basis
span_basis   ~>   span_Basis
in_span_basis   ~>   in_span_Basis
norm_bound_component_le   ~>   norm_boound_Basis_le
norm_bound_component_lt   ~>   norm_boound_Basis_lt
component_le_infnorm   ~>   Basis_le_infnorm

  INCOMPATIBILITY.


This change was suggested by Brian Huffman and it finished his introduction of 
the Basis set.

 - Johannes

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

[isabelle-dev] NEWS: filterlim

[Johannes Hölzl]

* Further generalized the definition of limits:

  - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that
when the input values x converge to F then the output f x converges to G.

  - Added filters for convergence to positive (at_top) and negative infinity 
(at_bot).
Moved infinity in the norm (at_infinity) from Multivariate_Analysis to 
Complex_Main.

  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
INCOMPATIBILITY

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

Re: [isabelle-dev] push request (Sublist.thy)

[Johannes Hölzl]

Am Freitag, den 14.12.2012, 13:47 +0100 schrieb Makarius:
> On Fri, 14 Dec 2012, Makarius wrote:
> 
> > When I did the re-cloning last time, I documented it explicitly in 
> > http://isabelle.in.tum.de/repos/isabelle/rev/71136069089d see also 
> > http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02978.html
> 
> I have compared the wiki advice with the authentic version above.  Since 
> Mediawiki lacks good version control, I copy the content here for 
> reference:
> 
>   When this does not work another solution is:
> 
>   Clone the revisions up to the faulty one:
> 
>   hg clone --config=format.dotenode=0 --pull -U -r  isabelle 
> isabelle-new
> 
>   cd isabelle-new
>   cp ../isabelle/Mercurial .
>   cd .hgrc
>   cp ../../isabelle/.hgrc/hgrc .
>   cp ../../isabelle/.hgrc/shamap .
>   chgrp -R isabelle .
>   chmod -R g+rwX .
>   find . -type d -exec chmod g+s "{}" \;
> 
> 
> Instead of "cd .hgrc" you probably meant "cd .hg".  What was also missing 
> is the "mkdir .hg/strip-backup", which is important for the next one doing 
> a strip, otherwise nobody else can strip with backup the afterwards -- I 
> have done that now.
> 
> I sincerely hope that the rest is equivalent with what I wrote in 
> 71136069089d 4 months ago, where I spent extra care in getting the order 
> of permission changes right, and fine-tune the sequence of shell commands.

I see two differences:

 * I used "find" to update the g+s flag in all sub-directories of .hg
   (there are some in .hg/store) I don't know how important this is.

 * I also copied shamap. It is related to the convert extension hence I
   assume it contains informations how the hg repository was generated
   from the CVS repo.

> And I am not asking to update the wiki, but to remove that page from it.

It now only mentions Admin/Mercurial/Central .

> Anythying that needs to be added to Admin/Mercurial/Central/README can be 
> discussed here (or privately).

I think we should add the trick by Alex to use strip. 


 * When the Isabelle repository is corrupted "hg verify" can be used to
   find the corrupt revision:

 * With "hg strip -r " this revision can be removed. Then
   try to push your changes again

 * If this is not possibly try to clone the repository:
   ...


I know its a bad idea to perform a non-monotonic change like strip to
the repository. But I think it is less error prone than cloning the
repository with all these steps.

> The Admin/ area within the Isabelle 
> repository remains the one place for administrative information, not some 
> odd wiki where I am not participating. (Hopefully it will attract a 
> genuine Isabelle user community at some point, when hints on funny 
> technical incidents at TUM have disappeared.)


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

Re: [isabelle-dev] push request (Sublist.thy)

[Johannes Hölzl]

Am Freitag, den 14.12.2012, 13:25 +0100 schrieb Makarius:
> On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
> 
> > Stripping did not work (even on lxbroy10 with some older Mercurial). 
> > However, Johannes managed to apparently fix everything by doing a fresh 
> > clone, copying some files (such as hgrc) and adjusting permissions (cf. 
> > https://isabelle.in.tum.de/community/Reconstructing_the_Isabelle_repository).
> 
> This is a serious problem, not just in a technical sense.
> 
> Why is there again this diverging clone of important administrative 
> information?  So the community wiki is not about Isabelle community at 
> all, but to make administration harder by putting unreliable information 
> snippets on a virtual whiteboard.  It actually causes dis-unity not 
> com-unity.

Most informations in the community wiki are from the former
community.html of the Isabelle website (which is maintained in
http://isabelle.in.tum.de/repos/website/). So the wiki contains mostly:

 * links where to find help for beginners (additional courses etc.)

 * informations about additional Isabelle theories (AFP, IsarMathLib etc ...)

 * lists for bigger cleanup tasks (like introducing 'a set back).

When we put this informations back into the website repository should we
also add the people who are now editors of the wiki as administrators
to the website repository? What alternatives have we for the wiki?

> When I did the re-cloning last time, I documented it explicitly in 
> http://isabelle.in.tum.de/repos/isabelle/rev/71136069089d see also 
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02978.html
> 
> Our main tools for Isabelle development are the repistory and the 
> isabelel-dev mailing list.  I am not even a user of the Isabelle community 
> wiki, and will not maintain all this divergence of clones.

I only was aware of Alex's email about the repository corruption. I did
not find Admin/Mercurial/Central. Now I replaced the wiki page by a link
to it.

> We probably also need to rethink the hosting problem of the conventional 
> push-area for the central clone of the Isabelle reposity.  A single 
> dropout every 2 years would be acceptable, but not several times in 1 
> year.  Maybe there is a chance to discuss it with Franz Huber next week, 
> and a solution without home-made servers.  Otherwise we need an external 
> hosting service, which is relatively easy.  It will be reletively hard to 
> sort out the administrative structure, though, since we are still stuck in 
> the "everybody is root" paradigm stemming from CVS 1.0.
> 
> 
>   Makarius


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

Re: [isabelle-dev] Permission denied

[Johannes Hölzl]

Am Montag, den 10.12.2012, 16:39 +0100 schrieb Jasmin Blanchette:
> Am 10.12.2012 um 16:33 schrieb Makarius:
> 
> > After the update these machines have very new Mercurial 2.4, so it could be 
> > a communication problem with your local Mercurial and the version that it 
> > runs via ssh.
> > 
> > How is the situation with lxbroy10 or simular (which can only be accessed 
> > locally).
> 
> It looks like the issue is that we were kicked out of the "isabelle" group. 
> On "macbroy24":
> 
> groups
> 
> prints
> 
> tumuser
> 
> for me (same for Johannes).
> 
> But on "lxbroy10", I am correctly a member of the "isabelle" group, and 
> pushing works. Thanks for the tip! :)
> 
> Johannes is now gone to talk to the system administrators to ask them "was 
> los ist".
> 
> Jasmin

A administrator forgot to set the correct LDAP settings after he updated
the macbroys. Florian Bichmaier fixed it and using the macbroys should
work again since yesterday afternoon.

 - Johannes


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

Re: [isabelle-dev] Repository Trouble

[Johannes Hölzl]

Am Montag, den 10.12.2012, 15:27 +0100 schrieb Makarius:
> On Tue, 27 Nov 2012, Johannes Hölzl wrote:
> 
> > We had again a problem with the repository. We fixed it by using again
> >
> >  hg verify
> >  hg strip 
> >
> > now it works again (at least on my machine and on the web server)
> >
> > I used Mercurial 2.0.2 (installed with Ubuntu 12.04).
> > I updated now to Mercurial 2.4 and hope that it does not happen again.
> 
> Since Jasmin reported push problems on the other thread, I did some 
> peeking of the physical repository as well.  This reveals the following:
> 
>-rw-rw-r-- 1 hoelzl isabelle 0 Nov 27 15:15 .hg/bookmarks
> 
> I vaguely remember that when the first breakdown happened this summer (due 
> to a push by Alex Krauss) the very same odd file was left over, with owner 
> krauss.
> 
> Bookmarks are a version of "branches" in Mercurial, but we don't use them 
> in the Isabelle repository.  Do you use them locally for yourself?

No I do not use them at all. The file is also empty on my local
repository. I only use rebase and Mercurial queues but I don't think
this is related. I assume it is created by the new Mercurial version?

 - Johannes





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

Re: [isabelle-dev] AFP devel broken

[Johannes Hölzl]

Am Mittwoch, den 05.12.2012, 21:50 + schrieb Gerwin Klein:
> On 05/12/2012, at 6:31 PM, Tobias Nipkow  wrote:
> 
> > Can anybody still build the AFP on some machine?
> 
> I have been able to build everything on a linux machine late last
> night.
> 
> The only entry that comes up with an error is Girth_Cromatic
> (something with filter_lim that looks related to a recent change).

This is fixed in changeset AFP/7d05a06f8793. I did the commit 2 days
ago, but maybe I forgot to push it.

 - Johannes

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

Re: [isabelle-dev] Status of HOL/SMT

[Johannes Hölzl]

Am Dienstag, den 04.12.2012, 15:13 +0100 schrieb Jasmin Blanchette:
> Am 04.12.2012 um 15:06 schrieb Makarius:
> 
> > If you provide a state where the SMT_Examples session can reproduce its 
> > proofs,
> 
> I'll try to. Last time I regenerated the certificate, there were a couple of 
> cases where I was not successful with 3.2 (on my Mac) and had to use 4.0. But 
> I need to dig down into this again. It's on my radar, but probably not before 
> February.
> 
> In general, we should try to reduce our exposure to SMT proofs in Isabelle 
> (and keep it to 0 in the AFP). That "SMT_Examples" use them is fine, but any 
> "smt" call that can be replaced by something else in other places, e.g. 
> "Multivariate_Analysis", should be done in the long term. It's something 
> where the Sledgehammer Isar proof generation framework should help at some 
> point (e.g. in one year from now) -- once we're done with the ATP side we'll 
> see what can be done with SMT proofs.

I remove the SMT certificates in HOL-Multivariate_Analysis in
Isabelle/4b4fe0d5ee22.

> > I should be able to wire up some alternative session run with 
> > [condition=ISABELLE_FULL_TEST].
> 
> Be aware that
> 
> declare [[smt_read_only_certificates = true]]
> 
> is hard-coded in those files, and this flags basically says: "use the 
> certificates, and if they're not there, fail". (You're free, of course, to 
> rethink the entire mechanism.)
> 
> Jasmin
> 
> ___
> 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] Exception TERM in method arith

[Johannes Hölzl]

Fabian and I found the missing check in Cooper's algorithm
(src/HOL/Tools/Qelim). The fix can be found in the testboard
52e97a5f5e25. If it works I will push it to the Isabelle repository.

 - Johannes 


Am Samstag, den 01.12.2012, 22:01 +0100 schrieb Florian Haftmann:
> In rev. 544764f4324d
> 
> theory Foo
> imports Main
> begin
> 
> lemma less_dvd_minus:
>   fixes m n :: nat
>   assumes "m < n"
>   shows "m dvd n ⟷ m dvd (n - m)"
>   using assms apply arith oops
> 
>   Florian


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

[isabelle-dev] Repository Trouble

[Johannes Hölzl]

We had again a problem with the repository. We fixed it by using again

  hg verify
  hg strip 

now it works again (at least on my machine and on the web server)

I used Mercurial 2.0.2 (installed with Ubuntu 12.04).
I updated now to Mercurial 2.4 and hope that it does not happen again.

Sorry for the inconvenience,
  Johannes

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

[isabelle-dev] NEWS

[Johannes Hölzl]

* HOL/Probability:
  - Add simproc "measurable" to automatically prove measurability

  - Add induction rules for sigma sets with disjoint union 
(sigma_sets_induct_disjoint)
and for Borel-measurable functions (borel_measurable_induct).

  - The Daniell-Kolmogorov theorem (the existence the limit of a projective 
family)

* Library/FuncSet.thy: Extended support for Pi and extensional and introduce the
extensional dependent function space "PiE". Replaces extensional_funcset by an
abbreviation, rename a couple of lemmas from extensional_funcset to PiE:

  extensional_empty ~> PiE_empty
  extensional_funcset_empty_domain ~> PiE_empty_domain
  extensional_funcset_empty_range ~> PiE_empty_range
  extensional_funcset_arb ~> PiE_arb
  extensional_funcset_mem > PiE_mem
  extensional_funcset_extend_domainI ~> PiE_fun_upd
  extensional_funcset_restrict_domain ~> fun_upd_in_PiE
  extensional_funcset_extend_domain_eq ~> PiE_insert_eq
  card_extensional_funcset ~> card_PiE
  finite_extensional_funcset ~> finite_PiE

* Library/Countable_Set.thy: Theory of countable sets.


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

Re: [isabelle-dev] AFP: Session AVL-Trees broken

[Johannes Hölzl]

Am Donnerstag, den 08.11.2012, 09:40 +1100 schrieb Gerwin Klein:
[..]
> The solution may be to just increase timeouts. On the other hand, this
> whole thing used to work just fine and started to go haywire
> 2012-10-19, then the log files are cut off in the middle at
> HOL-Probability (probably nonterminating, I guess these sessions
> should get a timeout too, the old setup was cumulative), HOL-Probality
> worked on 2012-10-26 (but then timeouts), then again stuck at
> HOL-Probability, and since 2012-10-28 mostly timeouts.

Just as another data point: I regularly build the HOL-Probability image
from the repository on my machine (32-bit linux, Core 2 Duo, 4GB ram)
and I never had a problem in the last months.

 - Johannes


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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Johannes Hölzl]

HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
patch.

A surprising change is found in Markov_Models:

  We get an error when an assumption has the same name as a fact in the
  locale:

locale loc
begin
  lemma X: "True" ..

  lemma assumes X: "X" shows "True"
^- raises "Duplicate fact declaration "local.X" vs. 
"local.X""
 
Is this easily avoidable? I think this might confuse people and add a
maintenance burden when one adds a fact to a locale with a popular name.

 - Johannes



Am Mittwoch, den 10.10.2012, 16:51 +0200 schrieb Makarius:
> On Tue, 9 Oct 2012, Makarius wrote:
> 
> > On Sun, 7 Oct 2012, Florian Haftmann wrote:
> >
> >> After some pondering I would argue that this should be forbidden:
> >> * (Complete) shadowing is a constant source of confusion.
> >> * Global interpretations are impossible then, since they would result in
> >> two global theorems with the same name.
> >
> > I've started some experiments with this idea and will report the empirical 
> > results soon ...
> 
> After some detours I am now back on Isabelle/28e37eab4e6f.
> 
> In principle, the last big reform of locale + interpretation name space 
> prefixes has addressed the situation already, where each locale scope is 
> locally strict, but composing several of them in locale expressions etc. 
> works by mandatory or non-mandatory prefixes.
> 
> Actual strictness checking is part of the underlying name space policy, 
> when bindings are applied and react with some naming. The "local" context 
> of the locale construction is particularly important here.  It was merely 
> a historical left-over that fact bindings were not checked strictly:
> 
>(1) in distant past facts were never strict and totally un-authentic
> 
>(2) the Isar proof "body" mode allows to override 'notes' as it does for
>'fixes'.
> 
> So with the "ch-strict" changeset applied to the critical spot of local 
> notes, the namespace policy enforces the concentual locale scopes.
> 
> Applying this in practice leads to many surprises about situations found 
> in existing theory libraries, though.  Some of the changsets leading up to 
> Isabelle/28e37eab4e6f already sort this out.  Some other ad-hoc changes 
> are attached as ch-test here.
> 
> 
> With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1
> the following sessions fail:
> 
> BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, 
> HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, 
> Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, 
> PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, 
> Transitive-Closure-II, Valuation
> 
> So the question if ch-strict can be activated soon is mainly a matter of 
> library space.  It is up to emerging volunteers to sort it out further.
> 
> (For me it was interesting to see how Isabell/jEdit works on the 
> JinjaThreads monster session.  See also AFP/77f79b2076f1 of the result of 
> investing 3GB for poly, 4GB for java, and quite a bit of CPU time and 
> elapsed time.)
> 
> 
>   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] AFP entry Grith_Chromatic fails with "THM 0"

[Johannes Hölzl]

Hi,

I tried to build AFP/Grith_Chormatic, but the simplifier fails in

  Ugraphs.thy line 168:

using card_left_less_pair assms by simp


with the following exception:

  exception THM 0 raised (line 790 of "drule.ML"):
  Ill-typed instantiation:
  Type
  ?'a ⇒ ?'b
  of variable ?f
  cannot be unified with type
  (?'a × ?'a) set ⇒ bool of
  term finite
  ?x = ?y ⟹ ?f ?x = ?f ?y

There is no instantiation happening in the Isar text.

Isabelle hg: 9a2a53be24a2, afp hg: 2b6348e4bda7, near the current tips.

It seems to happen somewhere internal when instantiating
card_left_less_pair.

When I write 

  using card_left_less_pair[of A] assms by simp

it works.

 - Johannes


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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Johannes Hölzl]

Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski:
> On 07.10.2012 09:37, Florian Haftmann wrote:
> > Hi all,
> >
> > currently, theorem names in locales can be shadowed (given that
> > declarations are in different theories, otherwise the foundation level
> > would reject the declaration since the two foundation theorems would
> > have the same name).
> >
> > After some pondering I would argue that this should be forbidden:
> > * (Complete) shadowing is a constant source of confusion.
> > * Global interpretations are impossible then, since they would result in
> > two global theorems with the same name.
> >
> > Any comments?
> 
> How would this interact with sublocale? If two (unrelated) locales 
> contain a lemma with the same name, can I still establish a sublocale 
> relation?
> 
>-- Lars

You are forced to give a name to the subplocale interpretation:

  sublocale L1 < NAME!: L2

but then it should work.

 - Johannes



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

Re: [isabelle-dev] isabelle build

[Johannes Hölzl]

Am Dienstag, den 07.08.2012, 09:03 +0200 schrieb Tobias Nipkow:
> Am 07/08/2012 09:00, schrieb Jasmin Christian Blanchette:
> > Am 07.08.2012 um 00:15 schrieb Johannes Hölzl:
> > 
> >> And I would suggest that isabelle mkroot tells the user to use version
> >> control:
> >>
> >> * Use Mercurial to manage your project
> >>   hg init Project_X
> >>   hg add Project_X
> >>   hg commit Project_X -m "initial commit"
> > 
> > Isn't that condescending?
> 
> Worse, it has nothing to do with "build".
> 
> Tobias


isabelle mkroot shouldn't be about build only.
I think it is a good idea to propose some best practices, like

  * you can use a ROOT file to check your theories with isabelle build

  * you can use LaTex to document your theories (document/root.tex)

  * you can use version control the same way as with regular source code

Of course, it shouldn't be condescending. But why shouldn't we give a
beginner some kind of guidelines?

  - Johannes




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

Re: [isabelle-dev] isabelle build

[Johannes Hölzl]

Hi Makarius,

For the mkroot tool I would suggest that the layout looks more like a
AFP submission. The resulting directory should contain everything:

$ isabelle mkroot Project_X

Results in:
   
  Project_X/ROOT
  Project_X/Project_X.thy
  Project_X/document/root.tex

Also instead of calling the theory file "Ex.thy" I would call it like
the directory. This is quiet likely the name of the theory the user
wants for formalize. So if the user just has one theory file he does not
need to modify the ROOT file. And it allows the user to just pack the
directory Project_X and submit it as an AFP entry.

And I would suggest that isabelle mkroot tells the user to use version
control:

 * Use Mercurial to manage your project
   hg init Project_X
   hg add Project_X
   hg commit Project_X -m "initial commit"


- Johannes



Am Montag, den 06.08.2012, 19:24 +0200 schrieb Makarius:
> On Mon, 6 Aug 2012, Makarius wrote:
> 
> > In Isabelle/doc-src/ROOT there are some examples with document_dump and 
> > document_dump_mode that are leading into the direction to make typical 
> > configurations for papers based on regular sessions.
> >
> > I have my own traditional idioms here, but did not try to express them 
> > in the new way yet.  It will practially require some ./build script to 
> > wrap up the whole process as used to be done by several IsaMakefile 
> > command lines, but shell scripting is no longer built into the build 
> > tool.
> 
> I would like to encourage early adopters to post their favourite session 
> layout for individual documents (papers etc.).  So far there is a first 
> version of isabelle mkroot in eeb4480b5877, but it is still a bit awkward 
> -- too much influenced by the bounds of isabelle usedir.
> 
> The abstract specification for the result is like this:
> 
>isabelle mkroot && ./build
> 
> It remains to figure out what mkroot generates in the directory, and what 
> the local build script looks like (based on isabelle build + isabelle 
> document etc.).
> 
> 
>   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] Isabelle release test website

[Johannes Hölzl]

The current state of the Download-button can be seen here:

  http://www21.in.tum.de/~hoelzl/test/


 * If the detection does not work all platforms are shown as button

 * If the detection works then the suggested platforms are shown as
   buttons, and the other ones as normal links

- Johannes


Am Donnerstag, den 26.04.2012, 14:09 +0200 schrieb Makarius:
> The website itself is starting to take shape.  Thanks to Johannes Hölzl 
> we now have nice download buttons that detect the platform of the web 
> browser: Linux, Linux 64 bit, Mac OS X, Windows.  All 4 buttons are shown 
> if the platform cannot be detected.
> 
> Please report any problems with your exotic browser and exotic operating 
> system.

> The idea is that the user can get through with a few standard clicks most 
> of the time, and can ignore the detailed Installation instructions by 
> default.
> 
> 
>   Makarius


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

Re: [isabelle-dev] Isabelle release test website

[Johannes Hölzl]

Am Montag, den 23.04.2012, 17:22 +0200 schrieb Makarius:
> Here is an update of the test website for warming up a bit more 
> http://www4.in.tum.de/~wenzelm/test/website/
> 
> I've spent this cold and wet weekend to produce a monolitic Windows 
> application, which bundles both JDK and Cygwin 1.7.9, see the Download 
> page.  (Cygwin 1.7.9 is important here, because in the later version from 
> this year Poly/ML multithreading is a bit unstable.)

The JDK in Isabelle_23-Apr-2012_bundle_x86-linux.tar.gz seams to be the
64-bit version:

Isabelle_23-Apr-2012/contrib/jdk-7u3_x86-linux/jdk1.7.0_03/bin/java:
ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses 
shared libs), for GNU/Linux 2.6.9, not stripped

> Is there anybody who could lend me a hand to produce a quick download link 
> in JavaScript, like the one on http://mercurial.selenic.com/ that already 
> knows the platform of the user's browser?
> 
> This could be put prominently on the main index.html, so that 
> download.html only needs to be visited for further details. Last time 
> there was also a surprising number of seasoned Linux users who could not 
> tell if they are running x86 or x86_64; the js magic would help here as 
> well.  (For Linux the platform distinction is relevant due common problems 
> caused by C/C++ library dependencies.)
> 
> 
>   Makarius

I already have a download button, I hope it is still on my laptop. I
will sent it to you when I'm at home.

 - Johannes






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

[isabelle-dev] NEWS

[Johannes Hölzl]

Session HOL-Probability: Introduced the type "'a measure" to represent
measures, this replaces the records 'a algebra and 'a measure_space. The
locales based on subset_class now have two locale-parameters the space
\ and the set of measurables sets M. The product of probability spaces
uses now the same constant as the finite product of sigma-finite measure
spaces "PiM :: ('i => 'a) measure". Most constants are defined now
outside of locales and gain an additional parameter, like null_sets,
almost_eventually or \'. Measure space constructions for distributions
and densities now got their own constants distr and density. Instead of
using locales to describe measure spaces with a finite space, the
measure count_space and point_measure is introduced. INCOMPATIBILITY.

  Renamed constants:
  measure -> emeasure
  finite_measure.\' -> measure
  product_algebra_generator -> prod_algebra
  product_prob_space.emb -> prod_emb
  product_prob_space.infprod_algebra -> PiM

  Removed locales:
  completeable_measure_space
  finite_measure_space
  finite_prob_space
  finite_product_finite_prob_space
  finite_product_sigma_algebra
  finite_sigma_algebra
  measure_space
  pair_finite_prob_space
  pair_finite_sigma_algebra
  pair_finite_space
  pair_sigma_algebra
  product_sigma_algebra

  Removed constants:
  distribution -> use distr measure, or distributed predicate
  joint_distribution -> use distr measure, or distributed predicate
  product_prob_space.infprod_algebra -> use PiM
  subvimage
  image_space
  conditional_space
  pair_measure_generator

  Replacement theorems:
  sigma_algebra.measurable_sigma -> measurable_measure_of
  measure_space.additive -> emeasure_additive
  measure_space.measure_additive -> plus_emeasure
  measure_space.measure_mono -> emeasure_mono
  measure_space.measure_top -> emeasure_space
  measure_space.measure_compl -> emeasure_compl
  measure_space.measure_Diff -> emeasure_Diff
  measure_space.measure_countable_increasing -> emeasure_countable_increasing
  measure_space.continuity_from_below -> SUP_emeasure_incseq
  measure_space.measure_incseq -> incseq_emeasure
  measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
  measure_space.measure_decseq -> decseq_emeasure
  measure_space.continuity_from_above -> INF_emeasure_decseq
  measure_space.measure_insert -> emeasure_insert
  measure_space.measure_setsum -> setsum_emeasure
  measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
  finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite
  measure_space.measure_setsum_split -> setsum_emeasure_cover
  measure_space.measure_subadditive -> subadditive
  measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
  measure_space.measure_eq_0 -> emeasure_eq_0
  measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite
  measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
  measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
  measure_unique_Int_stable -> measure_eqI_generator_eq
  measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
  measure_space.measure_Un_null_set -> emeasure_Un_null_set
  measure_space.almost_everywhere_def -> eventually_ae_filter
  measure_space.almost_everywhere_vimage -> AE_distrD
  measure_space.measure_space_vimage -> emeasure_distr
  measure_space.AE_iff_null_set -> AE_iff_null
  measure_space.real_measure_Union -> measure_Union
  measure_space.real_measure_finite_Union -> measure_finite_Union
  measure_space.real_measure_Diff -> measure_Diff
  measure_space.real_measure_UNION -> measure_UNION
  measure_space.real_measure_subadditive -> measure_subadditive
  measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
  measure_space.real_continuity_from_below -> Lim_measure_incseq
  measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
  measure_space.real_continuity_from_above -> Lim_measure_decseq
  measure_space.real_measure_countably_subadditive -> 
measure_subadditive_countably
  finite_measure.finite_measure -> finite_measure.emeasure_finite
  finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
  finite_measure.positive_measure' -> measure_nonneg
  finite_measure.real_measure -> finite_measure.emeasure_real
  finite_measure.empty_measure -> measure_empty
  finite_measure.finite_measure_countably_subadditive -> 
finite_measure.finite_measure_subadditive_countably
  finite_measure.finite_measure_finite_singleton -> 
finite_measure.finite_measure_eq_setsum_singleton
  finite_measure.finite_continuity_from_below -> 
finite_measure.finite_Lim_measure_incseq
  finite_measure.finite_continuity_from_above -> 
finite_measure.finite_Lim_measure_decseq
  measure_space.simple_integral_vimage -> simple_integral_distr
  measure_space.integrable_vimage -> integrable_distr
  measure_space.positive_integral_translated_density -> 
positive_integral_density
  measure_space.integral_translated_density -> integral_density
  measure_space.in