[isabelle-dev] find_theorems and type class axioms

[Lawrence Paulson]

> On 26 Nov 2015, at 11:58, Florian Haftmann <florian.haftmann at 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