Re: [isabelle] Sort hypotheses in proof
On Tue, 20 Oct 2015, Lars Hupel wrote:
today I noticed a funny suffix in my goal state:
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
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"
assume "rules rs"
thm ârules rsâ
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and