Email Gateway (Aug 18 2022 at 20:17): Email Gateway (Aug 18 2022 at 20:17):From: Makarius <makarius@sketis.net>
There two different things here:
(1) Outermost quantifiers are circumvented, by writing things with fixed
variables instead ("eigen context") and then make them arbitrary in
the result.
If you do write explicit quantifiers, which are escpecially required
for things nested on the LHS (e.g. in assumptions), there is an
explicit core inference that removes the quantifiers and expresses the
generality in terms of schematic variables.
Examples:
theorem "x = y ==> y = z ==> x = z" by (rule trans)
theorem "⋀x y z. x = y ==> y = z ==> x = z" by (rule trans)
Note that this stripping of outermost quantifiers looses some
information, but it is convenient, and quite essential for the
implicit rule composition scheme of Isabelle.
(2) [.] is notation in the cited paper for Trueprop. Here is a
copy-paste from an explanation that I have given in some Isabelle
course at some point:
text {*
The object-logic is embedded into the Pure framework via an implicit
derivability judgment @{term "Trueprop :: bool ⇒ prop"}.
Thus any HOL formulae appears atomic to the Pure framework, while
the rule structure outlines the corresponding proof pattern.
This can be made explicit as follows:
*}
notepad
begin
write Trueprop ("Tr")
thm conjI
thm impI
thm nat.induct
end
Above you can also use a global 'notation' command, but making everything
local is more fun.
Makarius
Email Gateway (Aug 18 2022 at 20:17):From: Makarius <makarius@sketis.net>
The FOL and HOL-Proofs images have proof terms already included. You can
say something like "Isabelle2012/build FOL" or "Isabelle2012/build -m
HOL-Proofs" in the terminal; the latter takes quite long.
Once your session is up and running with one of these images, you need to
enable proof terms again for your interactive session, e.g. like this:
ML {* proofs := 2 *}
Unfortunately, the manuals and the system are not in best shape for proof
terms, because they are so rarely used.
Some examples are in src/HOL/Proofs/.
Makarius
Email Gateway (Aug 18 2022 at 20:22):From: gottfried.barrow@gmx.com
In Krauss & Schropp's "A Mechanized Translation from Higher-Order Logic
to Set Theory", page 5, <http://home.in.tum.de/~schropp/>, they say:
In Isabelle, outermost quanti
ers and the [.]-embedding are not
printed...
QUESTION 1: Is there a command to show these hidden meta-logic
quantifiers, or any other such hidden meta-logic? I suppose not.
In looking for such a command, I was looking at the "prf" command on
page 141 of isar-ref.pdf. It says:
Note that this requires proof terms to be switched on for the
current object logic (see the "Proof terms" section of the
Isabelle reference manual for information on how to do this).
I did searches, looked around, and looked in the index of isar-ref.pdf,
but I never found any "Proof terms" section that gave such information.
QUESTION 2: Where does it tell me how to switch on proof terms for the
current object logic?
Thanks
GB
Email Gateway (Aug 19 2022 at 08:06):From: Makarius <makarius@sketis.net>
On Fri, 29 Jun 2012, Gottfried Barrow wrote:
Examples:
theorem "x = y ==> y = z ==> x = z" by (rule trans)
theorem "⋀x y z. x = y ==> y = z ==> x = z" by (rule trans)Note that this stripping of outermost quantifiers looses some
information, but it is convenient, and quite essential for the
implicit rule composition scheme of Isabelle.But I typed in your 2 theorems above. For the first, in the output of step 0,
it shows x, y, and z as variables. For the second theorem, no variables are
shown in the step 0 output.
That is because the second statement has all variables bound, so the goal
formula is closed and there are no free variables to display here.
I have declare[[show_consts=true]], and this discussion is making some
sense of the constants that show up, which I talk about below in
relation to Trueprop.Okay, all of this helps make sense of the mystery constants that show up in
the output window:prop :: prop => prop, and
HOL.Trueprop :: HOL.bool => prop.They're being used, but it doesn't show explicitly how they're being used.
Well, if the constant quantifier \<And> is really being used, but not
explicitly, then I'm guessing it should show up in the output, like
Trueprop.
This is a misunderstanding inherited from the holzf.pdf that was cited
earlier on this thread. The Pure "all" quantifier is always explicitly
visible by the !! or \<And> notation when it is there. The system
explicitly strips outermost quantifiers from result theorems, not by
suppression in the syntax, but by changing the theorem via some
inferences.
I tried
notation prop ("Pr")
to see how prop is being used, but that gives an error.
You need to quote the "prop" above, to prevent its interpretation as
command keyword (as highlighted by Isabelle/jEdit).
The "prop" constant is a bit more esoteric than Trueprop. It normally
does not show up in user applications at all. See section 2.3.2 of
http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf for
some bits of explanations on it.
I naively thought that every bool gets mapped to prop, but no, it's not
that simple, as shown by "P x" above;
Then there would be no reason to have Trueprop at all. The purpose of it
is to indicate the boundary between the Pure framework (with its native
language of natural deduction rules over \<And> and ==>) and the
object-logic with its diversity of connectives.
Makarius
Last updated: May 01 2024 at 20:18 UTC