# 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.*