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

[Florian Haftmann]

For the record:

> Running on host lxbroy10
> isabelle: fc53fbf9fe01 tip
> afp: 835c7e115feb tip
> Running ConcurrentGC ...
> Finished ConcurrentGC (1:08:48 elapsed time, 5:15:14 cpu time, factor 4.58)
> 1:21:59 elapsed time, 5:53:13 cpu time, factor 4.30

This seems to be fine now.

Florian

Am 16.11.2015 um 17:17 schrieb Peter Gammie:
> For:
> 
> isabelle: e6784939d645
> afp: e6d87060e398
> 
> the attached patch makes ConcurrentGC go through under Isabelle/JEdit. I 
> waited ~ 4 CPU hours for the batch build before killing it. I cannot read the 
> log files that Isabelle generates now, so I do not know what proof I 
> interrupted. Sorry about that. I’ve attached the log in case it has value to 
> someone. The log from isatest also does not have enough useful context.
> 
> It seems that the simplifier got smarter about the option datatype.
> 
> cheers,
> peter
> 
> 
> 
> 
> 
>> On 15 Nov 2015, at 16:38, Florian Haftmann 
>>  wrote:
>>
>> isabelle: f1b257607981 tip
>> afp: 1a688183b05a tip
>>
>> Any idea what is going on here?
>>
>>  Florian
>>
>> -- 
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] popup in ce6320b9ef9b

[Florian Haftmann]

>> Here is a minimal example, but I am at loss to explain what is going on
>> here.
> 
> The usual reason for a term being annotated twice is that it is (type)
> checked twice.

Good to know.  Maybe a double-check somewhere in the interpretation
machinery.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
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

[Florian Haftmann]

Hi all,

> I had no idea that sort constraints played any role in the finding of 
> theorems, or why they should play a role. Whatever function they have in a 
> search doesn’t prevent the very similar query
> 
>   dist norm "op=“
> 
> from picking up quite a few things. To my mind it’s quite unintuitive and 
> maybe should be looked at again.

just to make sure.  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 do not think find_theorems is to be blamed for the confusion
concerning dist_norm.  Instead, somebody a little bit familiar with the
topic has to find out why the sort constraints of norm are manipulated
in the way they are and whether there is room for improvement here.

Cheers,
Florian

> 
> Larry
> 
>> On 19 Nov 2015, at 09:21, Andreas Lochbihler 
>>  wrote:
>>
>> Hi Larry and Florian,
>>
>> the sort constraints for open, dist, and norm are changed in
>>
>> http://isabelle.in.tum.de/repos/isabelle/file/e89cfc004f18/src/HOL/Real_Vector_Spaces.thy#l1218
>>
>> These constraints were introduced by Brian Huffman in 2d91b2416de8 while he 
>> was reworking the type class hierarchy for topological spaces in 2009. I do 
>> not know his reasons for this, but I guess that they are meant to save type 
>> annotations.
>>
>> Best,
>> Andreas
>>
>>
>> On 19/11/15 10:10, Florian Haftmann wrote:
>>> Hi Larry,
>>>
 Andreas’s message reminds me that axioms of type classes are still not
>>> picked up:

 class dist_norm = dist + norm + minus +
   assumes dist_norm: "dist x y = norm (x - y)”

 This item has the status of a theorem. However, the query

dist "norm(_-_)”

 doesn’t find it. Surely it should?
>>>
>>> my mail from this summer still applies:
>>>
 There is nothing wrong with type classes here:

 class involutory =
   fixes f :: "'a ⇒ 'a"
   assumes involutory: "f (f x) = x"
 begin

 lemma involutory3:
   "f (f (f x)) = f x"
   by (fact involutory)

 end

 find_theorems "f"

 It seems to be a constraint issue:

 find_theorems "_ = norm (_ - _)"
~> 'a::real_normed_vector is inferred
 find_theorems "_ = norm ((_::'a::dist_norm) - _)"
~> typing error

 Maybe some naughty tweaking of sort constraints or an unforseen
 behaviour of coercions, but these are mere guesses.  I do not understand
 these parts of the type class hierarchy.
>>>
>>> I do not know why and how the default constraints of »dist« are changed,
>>> but this is the basic cause for the behaviour you experience.
>>>
>>> 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
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
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

[Lawrence Paulson]

> On 26 Nov 2015, at 11:58, Florian Haftmann 
>  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/isabelle-dev

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

[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 
 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/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] find_theorems and type class axioms

[Lawrence Paulson]

I still have no idea why find_theorems should refuse to find a theorem 
containing two named constants, no matter what the sorts say. Are there 
examples of searches that would deliver crazy results if this constraint were 
lifted? 

Larry

> On 26 Nov 2015, at 14:41, Johannes Hölzl  wrote:
> 
> 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...

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