Email Gateway (Aug 19 2022 at 11:35): Email Gateway (Aug 19 2022 at 11:35):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I put this up in case someone wants to add to what I've learned.
Attached is a THY and PDF of my exercise. The PDF shows my efforts to
make a printout self-contained. The numbered links take you to a theorem
summary, which has a bibliography link with a line number, which takes
you to the bibliography entry, which links to a Mercurial source file
with line numbers.
Being positively influenced by the concept of sequents, though only just
starting to dive into sequents, I saw that there is turnstile, which is
used as the meta-language symbol to give meaning to everything else.
There is then the meta-object symbol ==>, and wanting life to be simple,
I wanted to say that it is ==> that gives meaning to everything else.
However, willing for life to be more complex, I decided that at the
blackbox-in and blackbox-out levels, there is only prop, schematic
variables, and ==>.
The blackbox-in level is
theorem foo "..."
with Trueprop coercion unhidden, and the blackbox-out level is
thm foo
with Trueprop coercion unhidden, and you can't blame me for wanting only
prop, schematic variables, and ==>, when that's all I've seen for months
at the blackbox level.
In drule.ML, I stumbled on "equal_intr_rule", which expresses meta-logic
\<equiv> in terms of ==>. I also saw "triv_forall_equality", and in
logical haste, I decided that by proving a theorem that uses \<And> and
\<equiv>, and using only "equal_intr_rule", that would allow me to take
the perspective that at the blackbox level, it is ==> that gives
meaning, rather than \<And> and \<equiv>, where the function arrow
operator was far from my mind, though surely it's at a lower level anyway.
The theorem I chose was "atomize_all", but I hit a snag, which was
fortunate. I set up the assumptions correctly for "equal_intr_rule", but
"rule" didn't use them to prove "atomize_all" in one step, so I resorted
to "simp" to do parts of the proof.
The main value of the exercise was in seeing that the simplifier was
creating rewrite rules from the assumptions, so it gave new meaning to
those mysterious 'Adding rewrite rule "??.unknown"' statements.
What I was looking for was evidence that \<And> and \<equiv> operate
independently from ==>, so that they all have to be considered
fundamental. Looking at the simp trace kind of gave me that evidence,
but someone can correct me if I'm wrong.
Also, when "rule" didn't use the assumptions I gave it, it then made
goals based on "equal_intr_rule". But it didn't do an exact
instantiation. \<And> is used in the conclusion of "atomize_all", so
"rule" made some decisions, and did some rearranging of the use of
\<And> before it printed the goals, which indicates to me that it's
fundamental.
I'm a little closer to being able to eventually describe how ==>,
\<And>, and \<equiv> all fit in at the meta-logic level.
Regards,
GB
i130719_triv_forall_equality.thy
i130719_triv_forall_equality.pdf
Email Gateway (Aug 19 2022 at 11:35):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It's not exactly all there, but starting on page 27 of isar-ref.pdf,
there is section "2.1 The Pure Framework", in which a brief explanation
of the four meta-logic symbols is given, where the four symbols are =>,
\<And>, \<equiv>, and ==>. It pays to look at things 4 or 5 times, at least.
In particular, on page 28, it says, "Logical statements are composed via
\<And>x::alpha. B(x) and A ==> B." It then goes on to define some rules
for \<And> and ==> using sequents.
That's important because there is the section "Simulating sequents by
natural deduction" on page 203 which talks about expressing a form of
sequents using the ==> symbol.
You put those sections together, and you might be able to figure how to
use ==> to have a form of sequents in Isabelle/HOL where ==> is
considered the fundamental symbol for the sequents, and figure out how
to do it without abusing conventional standards too much.
You might call them isa-sequents. If you abuse things unintentionally,
an isa-sequent is whatever you define it be anyway.
Regards,
GB
Last updated: Apr 26 2024 at 04:17 UTC