Email Gateway (Aug 23 2022 at 08:41): Email Gateway (Aug 23 2022 at 08:41):From: Georgy Dunaev <georgedunaev@gmail.com>
Hello!
What are the types of PROP and P in the following theorem from Pure/Pure.ml
?
I mean this lemma:
lemma meta_spec:
assumes "⋀x. PROP P x"
shows "PROP P x"
by (rule ‹⋀x. PROP P x›)
I used ctrl+click and command Isabelle2019/src/Pure$ grep -rIn "PROP" but i
didn't find the definition.
What are the types of P and PROP here?
If PROP has type (prop=>prop) (as It told in implementation pdf) then why I
can't remove it and assume "!!x. P x"? (Where it "was told to" Isabelle
something like this "from this moment PROP s not necessary to write", if it
was, of course.)
What is the type of the term "type"?
It looks like " 'a itself ", but what does it mean exactly?
Does it have several types, for example, both " (prop=>prop) itself " and
"prop itself"?
Kind regards,
Georgy Dunaev
Email Gateway (Aug 23 2022 at 08:41):From: Lawrence Paulson <lp15@cam.ac.uk>
PROP doesn’t have any type at all: it is a keyword. Its purpose is to disable the implicit coercion from bool to prop whereby (for example)
shows “P”
is interpreted as
shows “Trueprop P”
thereby giving P type bool.
If instead you write
shows “PROP P”
then P will be assigned type prop.
And what is prop? It is the type of truth values in the meta level proof calculus. The purpose of Trueprop (which has type bool => prop) is to map the object level truth values (bool) to their meta level equivalents.
Larry
Email Gateway (Aug 23 2022 at 08:42):From: Makarius <makarius@sketis.net>
On 17/03/2020 11:59, Georgy Dunaev wrote:
What are the types of PROP and P in the following theorem from Pure/Pure.ml
?
I mean this lemma:lemma meta_spec:
assumes "⋀x. PROP P x"
shows "PROP P x"
by (rule ‹⋀x. PROP P x›)I used ctrl+click and command Isabelle2019/src/Pure$ grep -rIn "PROP" but i
didn't find the definition.What are the types of P and PROP here?
You should always use the Prover IDE (Isabelle/jEdit) for exploring Isabelle.
Note that for the ML files of Pure, you need to have src/Pure/ROOT.ML open, as
given in the Documentation panel.
For "P" above you can use normal C-hover with the mouse to see its type: 'a ⇒
prop and you can use the same techniques on the popup window to explore the
provenience of "prop" (but it is hardwired in Pure).
For PROP the visual clue tells you that it is a syntax keyword. Since it is
free-form mixfix syntax, there is no hyperlink on it (an omission of the
Prover IDE). You can use other means to find it in the implementation: use the
regular jEdit search dialog to make a "hypersearch" on the subdirectory
$ISABELLE_HOME/src/Pure --- probably also as a single word. This will give you
further clues how the Pure bootstrap works.
In the context of Isabelle/jEdit it makes sense to learn the builtin
hypersearch facility works --- grep is very clumsy compared to that.
What is the type of the term "type"?
It looks like " 'a itself ", but what does it mean exactly?
Does it have several types, for example, both " (prop=>prop) itself " and
"prop itself"?
See "implementation" manual section 2.3.2
"Auxiliary connectives".
Makarius
Last updated: Apr 25 2024 at 16:19 UTC