# Re: [isabelle] Sort hypotheses in proof

```On Tue, 20 Oct 2015, Lars Hupel wrote:

```
```today I noticed a funny suffix in my goal state:

using this:
wellformed 0 t'
rs â t â* t'  [evaluate]

Peter informed me that "[evaluate]" is a (pending?) sort hypothesis.
```
```
```
There are a fewmore explanations in the "implementation" manual section "2.3.3 Sort hypotheses".
```

```
However, I've seen some inconsistent behaviour in which cases exactly those are printed. Consider the following minimal theory (see also attachment):
```
typedecl rules
consts rules :: "rules â bool"

class evaluate =
fixes eval :: "'a â bool"
assumes eval_valid: "rules rs â eval a"

definition scoped_eval_fun where
"scoped_eval_fun rs f â (âx. eval x â eval (f x))"

lemma "rules rs â scoped_eval_fun rs a"
proof -
fix rs
assume "rules rs"
thm this
thm ârules rsâ
oops

In the proof, I expected that either both "thm" statements print the
sort hypothesis, or both don't.
```
```
```
As explained in the "isar-ref" manual section 6.3.3, the following is equivalent:
```
note `prop`

have "prop" by fact

```
So the alt-string notation for literal facts is not just a reference to an existing fact, but a proven statement (possibly a genuine instance of an existing fact).
```
```
That is the technical reason for the difference: a proof always imposes all sort hypotheses from the context on the result, for reasons of modularity (proof irrelevance).
```

```
The print operations of theorems should take that into account, but until Isabelle2015 it is still not fully "localized" in that respect. I will change that for the next release.
```

```
This confuses me tremendously, especially given that the fact "rules rs" doesn't stem from the class.
```
```
Normally the situation does not occur in practice, because classes have some standard instances in the library context. Sort hypotheses for inhabited classes are always stripped.
```
So maybe you can imitate such a situation in your application.

Makarius```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.