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 matching/unification plays out, but we’ll see what we can do. Cheers, Gerwin > On 19 Nov 2015, at 10:57 pm, Manuel Eberl <ebe...@in.tum.de> wrote: > > 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 I would very much like to see > this resolved in some way if it is possible. > > > On 19/11/15 12:49, Lawrence Paulson wrote: >> 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. >> >> Larry >> >>> On 19 Nov 2015, at 09:21, Andreas Lochbihler >>> <andreas.lochbih...@inf.ethz.ch> 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 > > _______________________________________________ > 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/isabelle-dev
