[isabelle] Sort hypotheses in proof



Dear list,

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.
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. In reality, if I reference a fact by
name, it won't show up; only, if I reference it by a literal. This
confuses me tremendously, especially given that the fact "rules rs"
doesn't stem from the class.

Cheers
Lars

Attachment: Hyps.thy
Description: application/extension-thy



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