Email Gateway (Aug 22 2022 at 19:11): Email Gateway (Aug 22 2022 at 19:11):From: Makarius <makarius@sketis.net>
This is a side-branch of earlier threads about "user-space type systems"
or "soft-type systems" in the Isabelle framework (beyond the hardwired
type-discipline of HOL-like logics).
The general plan is indeed to provide further hooks for the "check" and
"declare" phases of terms within the proof context. I have had some
discussions in Jan-2019 with two other users of such a scenario. Proper
solutions might emerged eventually.
The abstract idea is to continue what is available in the Isabelle/ML
module "Variable" for proper logical judgements.
Makarius
Email Gateway (Aug 22 2022 at 19:13):From: Joshua Chen <josh@joshchen.io>
The general plan is indeed to provide further hooks for the "check"
and "declare" phases of terms within the proof context.
I assume that the "declare" phase is the point, after certification, at
which terms are made known to the surrounding context?
Beyond type-checking and type inference, another use for such
functionality in type theory object logics is the automatic export of
object-level proof terms. After proving some statement
my_prop: "t: T",
it would be nice for the logic to automatically define
my_prop_prf == t
so that users can use t in further proofs without having to explicitly
write it out again. It would be nice to be able to do this at the point
of "qed" in proofs.
Cheers,
Josh
Email Gateway (Aug 22 2022 at 19:13):From: Joshua Chen <josh@joshchen.io>
Dear all,
I am trying to add a particular functionality to a type theory object
logic. I have a single judgment
has_type :: "[t, t] ⇒ prop" (infix ":")
and to support object-level typechecking, I want to explicitly record
all theorems with head has_type that are introduced via "axiomatization"
or "qed".
To do this I would like to automatically declare such theorems to have
some attribute "typinfo" at the point in the theory at which they are
stated (for axioms) or proved (for theorems).
Is there a way to do this, other than defining my own outer syntax
keywords? Apparently hooking directly into the existing keywords is not
possible, but perhaps I can piggyback off some other function that is
called when the kernel checks/certifies the theorems?
Best,
Josh
Email Gateway (Aug 22 2022 at 19:13):From: Makarius <makarius@sketis.net>
On 21/02/2019 20:27, Joshua Chen wrote:
The general plan is indeed to provide further hooks for the "check"
and "declare" phases of terms within the proof context.
I assume that the "declare" phase is the point, after certification, at
which terms are made known to the surrounding context?
Not quite: "declare" refers to Variable.declare (and variations) in
Isabelle/ML. It is where a fully-typed term is added to the context,
e.g. to claim its freshly introduced type variables and other names, to
make implicit Hindley-Milner polymorphism work etc.
This preceeds the actual goal statement as a logical claim. When that is
proven, the resulting theorem is added to the context as a fact, not as
a term anymore.
Beyond type-checking and type inference, another use for such
functionality in type theory object logics is the automatic export of
object-level proof terms. After proving some statement
my_prop: "t: T",
it would be nice for the logic to automatically define
my_prop_prf == t
so that users can use t in further proofs without having to explicitly
write it out again. It would be nice to be able to do this at the point
of "qed" in proofs.
We have not spoken about this extra problem of type theories with proof
objects: the Isar context discipline and proof language provides no
special support for that. More than 20 years ago, I simply left it as
open problem for the future, but so far nobody has revisited it.
Makarius
Last updated: Apr 23 2024 at 08:19 UTC