Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sort hypotheses in proof

Email Gateway (Aug 22 2022 at 11:33):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 11:47):

From: Lars Hupel <hupel@in.tum.de>
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
Hyps.thy

Last updated: Apr 24 2024 at 04:17 UTC