Email Gateway (Aug 19 2022 at 11:22): Email Gateway (Aug 19 2022 at 11:22):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
There's the meta-and, &&&, but I need a meta-or, so I don't have to
define two meta-or operators to keep from using PROP. After giving a
summary, I show what I found in pure_thy.ML, but I don't know how to
make it work.
As it is, I have to define two meta-or operators to not have to use PROP:
definition orbb :: "bool ⇒ bool ⇒ prop" (infixr "||" 15) where
"orbb P Q == (!!R. (P ==> R) ==> (Q ==> R) ==> R)"
definition orbp :: "bool ⇒ prop ⇒ prop" (infixr "|||" 15) where
"orbp P Q == (!!R. (P ==> R) ==> (PROP Q ==> R) ==> R)"
(Life is messy with two operators.)
theorem
"(A ||| (B || C)) ==> (A | (B | C))"
apply(simp add: orbb_def orbp_def)
by(smt)
(Life is clean with &&&.)
theorem
"(A &&& (B &&& C)) ==> (A & (B & C))"
by(linarith)
If there's a &&&, then it seems there should be the complete suite of
basic meta operators, along the lines of lines 175 to 183 in HOL.thy.
In pure_thy.ML, I found these lines for &&&:
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
val const = Lexicon.mark_const;
Sign.add_syntax_i [(const "Pure.conjunction", typ "prop => prop =>
prop", Infixr ("&&&", 2))];
Sign.add_consts_i [(Binding.name "conjunction", typ "prop => prop =>
prop", NoSyn)];
(Global_Theory.add_defs false o map Thm.no_attributes)
[(Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==>
B ==> C) ==> C)")];
Sign.hide_const false "Pure.conjunction";
I tried to modify them like this to get my meta-or, but I can't make it
work:
ML{*
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
val const = Lexicon.mark_const;
Sign.add_syntax_i [(const "MFZ.meta_or", typ "prop => prop => prop",
Infixr ("|||", 2))];
Sign.add_consts_i [(Binding.name "meta_or", typ "prop => prop => prop",
NoSyn)];
(Global_Theory.add_defs false o map Thm.no_attributes)
[(Binding.name "meta_or_def", prop "(A ||| B) == (!!R::prop. (P ==> R)
==> (Q ==> R) ==> R)")];
Sign.hide_const false "MFZ.meta_or";
*}
If anyone can do a quick edit to make that work, I would appreciate it.
Thanks,
GB
Email Gateway (Aug 19 2022 at 11:22):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I found a faster solution, so I don't know if I need what I asked for.
However, it shows that a person might want to define a function using
type prop, and not have to annotate everything with PROP, and need not
to have to fight the automatic Trueprop coercion.
But I'm trying to duplicate the functionality of the right-hand side of
a sequent without resorting to the object-logic operators.
According to pg.203 of isar-ref.pdf, if you have a sequent "A |- E, B,
C, D", then you can negate all the right-hand side members except for
one of them, and make a big implication out of it, with the non-negated
member put to the far right, like "A ==> ~E ==> ~C ==> ~D ==> B".
So rather than implement the right-hand side as a meta-disjunction, I
stay closer to what's in isar-ref.pdf. It's faster and acceptably meta.
I have to use variables of type bool, along with False, which equals
(!P. P), but the rest is ==>.
The simplifier seems to like working directly with True and False,
rather than lower-level definitions.
I still have to use two operators:
notation ==> (infixr "|-" 4)
definition seqr :: "bool => bool => prop" (infixr "||" 15) where
"seqr P Q == ((P ==> False) ==> Q)"
thm seqr_def
definition seql :: "bool => prop => prop" (infixr "|||" 15) where
"seql P Q == ((P ==> False) ==> PROP Q)"
thm seql_def
theorem
" (A |- (~E ==> ~C ==> ~D ==> B))
==> (A |- (E ||| B ||| C || D))"
apply(auto simp only: seqr_def seql_def)
done
theorem
" (A |- (E ||| B ||| C || D))
==> (A |- (~E ==> ~C ==> ~D ==> B))"
apply(auto simp only: seqr_def seql_def)
done
It seems right.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:23):From: Makarius <makarius@sketis.net>
In principle you could define all the standard connectives of Isabelle/HOL
in Isabelle/Pure as well, but what is the point?
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.
Note that &&& is merely used internally as auxilary device -- it should
hardly ever occur in applications of Isabelle/Pure (or HOL). You just use
multiple propositions directly in Isar like this:
lemma A and B and C
proof -
show A sorry
show B sorry
show C sorry
qed
You better chose to ignore that the internal system state somewhere
involves "A &&& B &&& C" -- it is never encountered in a regular proof.
Makarius
Email Gateway (Aug 19 2022 at 11:24):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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 operatorsIn principle you could define all the standard connectives of
Isabelle/HOL in Isabelle/Pure as well, but what is the point?
Makarius,
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
object-logic.
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
for \<or>?"
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
things better.
I do this:
theorem "(A ==> False) ==> (~A)"
using[[simp_trace]]
apply(auto simp only:)
done
The simp trace shows this:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
(A ==> False) ==> ~A
[1]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.
Regards,
GB
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)"
theorem mF_EQ_False:
"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.*)
theorem
" (A |- (~E ==> ~C ==> ~D ==> B))
==> (A |- (E ||| B ||| C || D))"
apply(auto simp only: mF_EQ_False)
done
theorem meta_not_EQ_not:
"(P ==> (!!P Q. P == Q::bool)) == (Trueprop (~P))"
apply(simp only: mF_EQ_False not_def)
apply(rule equal_intr_rule)
by(auto)
theorem meta_exists_EQ_exists:
"(!!Q. (!!x. P x ==> Q) ==> Q) == (Trueprop (? x. P x))"
apply(rule equal_intr_rule)
by(auto simp only:)
Email Gateway (Aug 19 2022 at 11:25):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It's a syntax priority problem.
Trueprop priority is 5, so dealing with the syntax of functions of type
"prop => prop" and "prop => prop => prop" is tricky:
Trueprop :: "bool => prop" ("(_)" 5)
I haven't figured out the rules completely, but it seems I have what I need.
However, the rules don't make complete sense. For this meta_not_abbr,
the function form "meta_not_abbr P" gets a coercion error, but notation
with a priority of 40 works, or even 4:
abbreviation (input) meta_not_abbr :: "prop => prop" where
"meta_not_abbr P == (PROP P ==> False)"
notation meta_not_abbr ("~~~ _" 40)
theorem
"meta_not_abbr P" (* coercion error *)
theorem
"(~~~ (~~~ P)) == Trueprop (P)"
by(rule equal_intr_rule, auto simp only:)
I then have my meta_or_abbr. The function form "meta_or_abbr P Q" also
gets a coercion error, but infixr notation with priority less than 5
works, and notation ("mOr _ _") also works:
abbreviation (input) meta_or_abbr :: "prop => prop => prop" where
"meta_or_abbr P Q == ((PROP P ==> False) ==> PROP Q)"
notation
meta_or_abbr (infixr "+++" 4) and
meta_or_abbr ("mOr _ _")
theorem
"(P +++ Q +++ R) == Trueprop (P | Q | R)"
by(rule equal_intr_rule, auto simp only:)
theorem
"(mOr P Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)
theorem
"meta_or_abbr P Q" (* coercion error *)
Here are the four connective hybrids. I know why I need one of them:
theorem meta_not:
"(P ==> False) == Trueprop (~P)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_or:
"((P ==> False) ==> Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_and:
"((P ==> (Q ==> False)) ==> False) == Trueprop (P & Q)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_exists:
"((!!x. P x ==> False) ==> False) == Trueprop (? x. P x)"
by(rule equal_intr_rule, auto simp only:)
Email Gateway (Aug 19 2022 at 11:25):From: Makarius <makarius@sketis.net>
If you want to play with syntax, you can always use 'notation' and
'no_notation' to specify things in any way you like, but don't ask me
about suitable priorities -- this is a black art and better not changed
fundamentally.
Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic to
reason about other logics. It is just a logical framework, for
higher-order natural deduction based on !! and ==>.
If you really want to reason about some other logic, better do it in
Isabelle/HOL, and define you syntax as datatype, semantics as function,
inference system as inductive predicate in the usual way. AFP has
examples for that.
Makarius
Email Gateway (Aug 19 2022 at 11:35):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 7/31/2013 3:29 PM, Makarius wrote:
Trueprop priority is 5, so dealing with the syntax of functions of
type "prop => prop" and "prop => prop => prop" is tricky:Trueprop :: "bool => prop" ("(_)" 5)
If you want to play with syntax, you can always use 'notation' and
'no_notation' to specify things in any way you like, but don't ask me
about suitable priorities -- this is a black art and better not
changed fundamentally.
Reminder to self. Add the following to the official GB list of HOL
cardinal rules: "Never change the default settings of Trueprop priority.
Live within the limits of Trueprop priority being at 5, lest you cause
yourself or others great logical harm in the future."
Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic to
reason about other logics. It is just a logical framework, for
higher-order natural deduction based on !! and ==>.If you really want to reason about some other logic, better do it in
Isabelle/HOL, and define you syntax as datatype, semantics as
function, inference system as inductive predicate in the usual way.
AFP has examples for that.
In these technical matters, I'm a practical purist. I'm only interested
in logics other than HOL to the extent they help me understand
isar-ref.pdf, and other Isabelle documentation. I also want there to be
the possibility that I can use anything I do as part of HOL. I'm just a
user who delves into foundations because I never found the book "Set
Theory, Real Analysis, Algebra, Combinatorics, and Number Theory for
Maple, Mathematica, and Even Isabelle2013".
I decided to take a step back and finally study natural deduction.
However, natural deduction inevitably leads to sequents, so I have
wanted to create a psuedo-sequent to use with exercises and, in some
manner, really be using a metalanguage.
With the pseudo-sequent I have now, there is the possibility that it
will all end up being academic, where I end up only using the standard
natural deduction rules. There is also the possibility that I will
eventually find a use for the pseudo-sequent, or at least for the notation.
I have no idea at this point why the RHS of a sequent needs to behave as
a disjunction, or why a person needs more than what the natural
deduction rules provide. But, it could be that I find a practical use
for stating a theorem using a meta-or along with !! and ==>. Sometimes,
we do that kind of thing as a preliminary step, because it helps us sort
out foggy concepts.
Thanks for the help, and thanks to Lars for the info about PROP.
I got my meta-False down to "(!!P. P::bool)". If I could roam the halls
of CMU, I'd stop by Avigad's office, make sure I called him professor,
and ask him if I can get a meta-False without using !!.
Regards,
GB
notation ==> (infixr "|-" 4) (* ==> and |-, they're close relatives. *)
notation ==> (infixr ",," 4) (* Fake sequent comma. It's all ==> on the
LHS. *)
(Warning!! What's below could all be bogus.)
(*Meta False. Trying to use "PROP P" instead of "P::bool" causes some
looping
below. It's no loss. If automatic Trueprop coercion is used, there's
no extra
purity obtained from using "PROP P".
It looks like I'm only tied into the object-logic because of these
statements:
typedecl bool
judgment Trueprop :: "bool => prop",
though probably also to the arities statements right above them.*)
abbreviation MFalse :: "prop" ("MFalse") where
"MFalse == (!!P. P::bool)"
theorem meta_False:
"MFalse == (Trueprop False)"
by(rule equal_intr_rule, auto simp only:)
(Meta not.)
abbreviation (input) meta_not_abbr :: "prop => prop" ("([~]_)" 40) where
"meta_not_abbr P == (PROP P ==> MFalse)"
theorem meta_not:
"([~]P) == Trueprop (~P)"
by(rule equal_intr_rule, auto simp only:)
(Meta or.)
abbreviation (input) meta_or_abbr :: "prop => prop => prop" (infixr
"([|])" 4) where
"meta_or_abbr P Q == ((PROP P ==> MFalse) ==> PROP Q)"
theorem meta_or:
"(P [|] Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)
(Meta and.)
abbreviation (input) meta_and_abbr :: "prop => prop => prop" (infixr
"([&])" 4) where
"meta_and_abbr P Q == ((PROP P ==> (PROP Q ==> MFalse)) ==> MFalse)"
theorem meta_and:
"(P [&] Q) == Trueprop (P & Q)"
by(rule equal_intr_rule, auto simp only:)
(*Meta exists. I don't feel like looking up how to do the binder
notation right
now. The presence of implicit meta-quantification always leaves one
paranoid.
You do the pencil and paper scratch work 15 times, but because you cannot
stop by Avigad's office to get confirmation of the obvious, and
because you
have used up your bi-monthly mailing list quota for asking questions,
you never
rest easy.*)
theorem meta_exists:
"((!!x. P x ==> MFalse) ==> MFalse) == Trueprop (? x. P x)"
by(rule equal_intr_rule, auto simp only:)
(*Finally, the pseudo-sequent. The order of the arguments on both the
LHS and
RHS don't matter, and there's actually a meta-language operator being
used
that's not HOL disjunction.
The priorities of the commas, |-, and [|] are all at 4, so they nest
to the
right, which means I don't have to use parentheses for the turnstile
statement.
The ==> is at priority 1 so the parentheses have to be used as shown.*)
theorem
" (P,, Q |- (~E ==> ~C ==> ~D ==> B))
== (Q,, P |- E [|] B [|] C [|] D)"
by(rule equal_intr_rule, auto simp only:)
theorem
" (P,, Q |- (~E ==> ~C ==> ~D ==> B))
== (Q,, P |- D [|] E [|] B [|] C)"
by(rule equal_intr_rule, auto simp only:)
Email Gateway (Aug 19 2022 at 11:36):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Wanting to be a helpful, altruistic individual, I give you now a way to
create some priority space, for that day when selfish indiviuals
complain, moan, and groan about there not being enough space between the
priorities of =>, !!, ==>, ==, and Trueprop, which are at 0, 0, 1, 2,
and 5, you being well aware of such things.
For priorities 5 and above, you add 95 to them. This puts Trueprop at a
nice 100. For priorities 0 to 4, you put them at 10, 20, 30, 40, and 50.
That would be one way to do it, unless there's something I'm not
considering.
Regards,
GB
Last updated: Nov 21 2024 at 12:39 UTC