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.