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

Perhaps the question relates to how polymorphism is interpreted in these searches. I’m getting the idea that the search for “dist” and “norm” somehow produces a combination of type classes that doesn’t precisely match the instances in the axiom “dist_norm”, where they are too specific to be

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

Hi Larry, > 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? I think the misunderstanding is that

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

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

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

> 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

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

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

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

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

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

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

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

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.

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

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

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

I agree, we should do something about it. All relevant people on our side currently are pretty busy with a project deliverable for 1st Dec, but we should be able to give find_theorems some of the TLC it deserves after that. This may not be easy to solve - it probably is just how

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

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

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

This particular issue has, in fact, annoyed me a great deal. I needed the ‘dist_norm’ lemma a lot lately and was never able to find it with ‘find_theorems’, which was very frustrating. I eventually found it by reading a proof that used it somewhere. I did not think much of it at the time, but

[isabelle-dev] find_theorems and type class axioms

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? Larry