Re: [isabelle] I need a meta-or
On 7/29/2013 3:23 PM, Makarius wrote:
If there's a &&&, then it seems there should be the complete suite of
basic meta operators
In principle you could define all the standard connectives of
Isabelle/HOL in Isabelle/Pure as well, but what is the point?
For myself, the point has become more general. Having meta-connectives
would now be a result of being able to define functions using "prop",
such as "prop => prop", "prop => prop => prop", etc., and have the
functions coexist nicely with Trueprop coercion just like
meta-implication does, that is, not having to annotate the variables
with PROP, and Trueprop not trying to coerce when it's not supposed to.
For me, the general point is to do formalizations about other logics
within HOL, and be able to keep those formalizations respectably
separate from the object-logic functions, definitions, axioms, etc.,
until I intentionally want to mix the (mostly) meta-logic with the
I don't know that it has to be about formalizing other logics. If you
had an Isar definition and Isar abbreviation command that allowed a
person to define functions using prop, and the functions behaved nicely
like ==>, then people would find a use for those commands.
I now have the perfect function to make my point, which is not the
meta-or I asked for at first. The meta-or I initially wanted sort of
fell under the "what is the point" category. Meta-or is "(!!R. (P ==> R)
==> (Q ==> R) ==> R)", so to make it practical to use, you would have to
start defining a bunch of simp rules, and then you'd end up asking, "And
why exactly am I duplicating all the simp rules that have been created
My function now is, "((P ==> False) ==> Q)", which requires absolutely
nothing additional to use. If I want to go total meta (other than bool
variables), then I can replace False with "(!!P Q. P == Q::bool)", which
would only require a simp rule to convert the meta-False back to False,
since meta-False by itself can make simplification slower.
The purpose of Isabelle/Pure is to provide a framework for
higher-order natural deduction, with declarative rule structure
indicated by the connectives !! and ==> (i.e. Minimal Higher-order
Logic). Anything beyond that is not really pure.
You're the authority, but my inclination is to say that a logic is
defined by its axioms, so I'm inclined to say that any logic that is
derived using only Pure is Pure. Even with a little bit of corruption,
like having to use bool variables, I'd say it can be considered Pure,
practically speaking. I'm just a novice here speaking.
You talk about Isabelle/Pure as a framework, but I don't see the problem
with taking the framework to its limits, though there would have to be
Isar commands to facilitate that, or ML templates that can be used to
define "prop" based functions that behave like ==>.
My interest in this evolved due to sequents. The LHS of a sequent is a
conjunction, which matches the use of ==> perfectly. The RHS of a
sequent is a disjunction, so for the RHS, ==> by itself ceases to work.
I created some notation to sync up the turnstile with ==>, and I used
\<or> to duplicate the RHS properties of the sequent.
I then plugged in a sequent derivation proof from Wikipedia with my
notation. It happened to be that the second line of the proof and the
conclusion of the proof were the same, because of the \<or>. Very
uninspiring. A "what's the point" moment.
If there's a mistake, it's that you make it too easy to use ==>. If I
know that ==> is of type (prop => prop => prop), and I can do:
theorem "A ==> (B ==> C)"
It's only natural that I think I should be able to do:
abbreviation imp2 :: "prop => prop => prop" (infixr "=+>" 15) where
"imp2 P Q == (P ==> Q)"
theorem "A =+> (B =+> C)"
But it doesn't work. I can finagle things to make it work, but it'll
never work like that.
The good news is that my finagling led to something that's acceptable
(with Lars' prior help).
I think there are lots of tangents to go off on for why a person might
want to intentionally stay within the meta-logic. Part of it is catching
the "meta-logic spirit". What other proof assistant has a meta-logic
that a person can use?
Part of it is trying to figure out what in Isabelle/HOL is optimized for
the meta-logic, and what's optimized for the object-logic. Overusing the
meta-logic should at least teach me how to use the meta-logic, and
formalizing something differently can sometimes help a person do old
I do this:
theorem "(A ==> False) ==> (~A)"
apply(auto simp only:)
The simp trace shows this:
SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
(A ==> False) ==> ~A
Adding rewrite rule "??.unknown":
A == True
I didn't give it any simp rules about True and False, but it knows how
to use them. That tells me the simplifier is optimized for the
object-logic, that and 15ms more for a proof if I use meta-False.
Consequently, I decide I should use "((P ==> False) ==> Q)" instead of
"((P ==> (!!P Q. P == Q::bool)) ==> Q)", because in this case, the
performance price for staying pure is probably too high, and False is
not too much to accept. It's some lambda calculus and the HOL refl axiom.
I know that the logic engine really likes statements like "P ==> Q", so
I'm trying to go through the exercise of seeing to what extent I can
stay in the "==>" world. I don't think the logic engine is fond of
things like "(!!R. (P ==> R) ==> (Q ==> R) ==> R)", but I'm pretty sure
that it doesn't consider "((P ==> False) ==> Q)" to be much more of a
burden than "P ==> Q". In fact, I think the logic engine loves "((P ==>
False) ==> Q)", because it's easy, and different.
In a more perfect world, my function "((P ==> False) ==> Q)" would be of
type "prop => prop => prop". It's okay that it's not. I'm happy to have
found something that's simple, and that fits in the "==>" paradigm.
After your email I put a little more effort into creating the
meta-versions of the standard connectives. I was trying to cut and paste
from the HOL versions, but the HOL versions use lambda calculus, which
wasn't working for me. Then I came up with the version for meta-False,
which gave me meta-not, and then I cut and pasted for the meta-exists.
If the performance cost is too high to stay pure, then I don't want to
use the meta-connectives. But my perfect example, "((P ==> False) ==>
Q)", which I've used to make my point, is not a standard connective.
It's also fast, and I need it, and I want it. I have it, too. Just not
in a one-operator form.
notation ==> (infixr "|-" 4)
abbreviation mFalse :: "prop" ("mFalse") where
"mFalse == (!!P Q. P == Q::bool)"
abbreviation (input) seqr :: "bool => bool => prop" (infixr "||" 9) where
"seqr P Q == ((P ==> mFalse) ==> Q)"
abbreviation (input) seql :: "bool => prop => prop" (infixr "|||" 9) where
"seql P Q == ((P ==> mFalse) ==> PROP Q)"
"mFalse == (Trueprop False)"
by(rule equal_intr_rule, metis, presburger)
(*3ms with False in abbreviation.
18ms with meta-False used in abbreviation and no mF_EQ_False simp rule.
3ms with meta-False used in abbreviation and simp rule mF_EQ_False.*)
" (A |- (~E ==> ~C ==> ~D ==> B))
==> (A |- (E ||| B ||| C || D))"
apply(auto simp only: mF_EQ_False)
"(P ==> (!!P Q. P == Q::bool)) == (Trueprop (~P))"
apply(simp only: mF_EQ_False not_def)
"(!!Q. (!!x. P x ==> Q) ==> Q) == (Trueprop (? x. P x))"
by(auto simp only:)
This archive was generated by a fusion of
Pipermail (Mailman edition) and