Email Gateway (Aug 22 2022 at 09:14): Email Gateway (Aug 22 2022 at 09:14):From: Makarius <makarius@sketis.net>
These slightly odd "atomize" and "rulify" things are mainly for internal
use of tools to make them work on regular rule statements given by the
user. When you write statements yourself, you normally do it the way it
works best for you from the start. Then you don't need to apply
atomize/rulify at all.
With a little bit of practice, it is easy to know what is best: usually an
open rule-format that can be applied readily later on.
This practice is a bit like currying in functional programming: looks odd
to totally new users, but is fairly natural after getting used to it.
Makarius
Email Gateway (Aug 22 2022 at 09:35):From: "W. Douglas Maurer" <maurer@gwu.edu>
(1) I am having trouble understanding why Isar permits both \forall
and \And, seeing that they appear to do exactly the same thing. I
understand that \And is for the statement of a theorem or lemma, and
is not supposed to be used in a proof. But what would happen if we
used \forall in the statement of a lemma, rather than \And? How would
this affect the rest of the proof?
(2) Am I to understand that, just as \And is the universal quantifier
at the meta-level, \Or is the existential quantifier at the
meta-level? Certainly \Or x. P(x) appears to do the same thing as
\exists x. P(x) . Further confusing me here is that a number of
example Isar proof statements do use \exists instead of \Or, such as
lemma assumes Pf: "\exists x. P(f x)" shows "\exists y. P y" (p. 10
of "A Tutorial Introduction To Structured Isar Proofs").
(3) In Whats In Main, under Orderings, under Syntax, there is given
some syntax for \forall and for \exists, such as \forall x \leq y. P
\equiv \forall x. x \leq y --> P . There are eight rules given here,
four for \forall and four for \exists . Do these rules also work for
\And and \Or ?
(4) Am I understanding correctly that \And applied to the null set is
True, while \Or applied to the null set is False?
Email Gateway (Aug 22 2022 at 09:35):From: Lars Noschinski <noschinl@in.tum.de>
On 07.04.2015 05:27, W. Douglas Maurer wrote:
(1) I am having trouble understanding why Isar permits both \forall and
\And, seeing that they appear to do exactly the same thing. I understand
that \And is for the statement of a theorem or lemma, and is not
supposed to be used in a proof. But what would happen if we used \forall
in the statement of a lemma, rather than \And? How would this affect the
rest of the proof?
The short answer is: Isabelle cannot reason about the HOL quantifiers
(and boolean connectives) directly, only by referring to their
characterisation in terms of the Pure (ore meta) counterparts <\And> and
\<Longrightarrow>.
So for lemmas you want to use into a proof (as opposed to maybe the
final theorem of a large development, which should just read nice),
you express it in terms of the meta operations as much as possible.
Otherwise, you can expect a lot of manual fiddling around, bringing the
theorem into a useful shape everytime you use it (although this depends
on the tools you use: metis for example doesn't care at all).
Some background:
In a way, \<And> is an artifact of Isabelle's Design. Isabelle was
designed as a generic theorem prover which one can use to formalise and
reason in various logics.
As such, Isabelle's kernel knows how to reason about a few primitive
constants, namely:
Pure.all :: ('a => prop) => prop (written as \<And>)
Pure.imp :: prop => prop => prop (written as \<Longrightarrow>)
We can use this logical framework (also refered to as Isabelle/Pure)
to formalise a logic (e.g. HOL) by declaring new constants and adding
rules (made from the primitive constants) as axioms (this is called an
"object logic" in Isabelle's notation). So implementing a new logic in
Isabelle does not involve writing code or changing the kernel, but just
writing a few rules in the logical framework.
Now, Isabelle/HOL has its own variants of the above operators,
HOL.All :: ('a => bool) => bool (written as \<forall>)
HOL.implies :: bool => bool => bool (written as \<longrightarrow>)
Note the different types and that bool and prop are not isomorphic (as
Isabelle/Pure does not have the law of the exluced middle).
(2) Am I to understand that, just as \And is the universal quantifier at
the meta-level, \Or is the existential quantifier at the meta-level?
There is no existential quantifier at the meta level. I'm not sure,
where \<Or> comes from (I don't have a current Isabelle at hand, at the
moment), but \<exists> is the common way to write an existential in
Isabell/HOL.
(3) In Whats In Main, under Orderings, under Syntax, there is given some
syntax for \forall and for \exists, such as \forall x \leq y. P \equiv
\forall x. x \leq y --> P . There are eight rules given here, four for
\forall and four for \exists . Do these rules also work for \And and \Or ?
There is no such syntax for \<And>.
(4) Am I understanding correctly that \And applied to the null set is
True, while \Or applied to the null set is False?
As HOL types are never empty, \<And> can never be applied "to the null
set". If you talk about "\<forall> x \<in> S. P x", yes, this is true if
S is empty.
-- Lars
Email Gateway (Aug 22 2022 at 09:35):From: Makarius <makarius@sketis.net>
You should not think of !! as the same as ALL, and ==> as the same as
--> etc.
Just a few notes on this, to overcome common misunderstandings.
Isabelle/Pure is minimal higher-order logic with connectives !! and ==>
used to describe natural deduction rules declaratively. The
Isabelle/Isar proof languages uses the same rule format to produce
structured proofs. These concepts are integral to Isabelle, and big
assets of its approach; schematic variables also belong here.
Isabelle/HOL is full higher-order logic with the whole zoo of
connectives (ALL, EX, -->, <-->, ~ etc.) and much more, to work with
applications. HOL statements may occur in Pure rules naturally.
The view of Pure as "meta-logic" and HOL as "object-logic" is OK in the
historical understanding of Isabelle as "logical framework" to declare
other logics, but it has little practical relevance today.
The view of Pure as "rule framework for structured reasoning" is very
relevant today. It is the canonical way how I usually explain that to
beginners.
Makarius
Email Gateway (Aug 22 2022 at 09:36):From: Andrew Gacek <andrew.gacek@gmail.com>
How do schematic variables relate to \And quantified variables? I know
that sometimes I need to use 'case' and sometimes 'case_tac' for
example, but it's not clear to me why I can't freely move a variable
from being \And quantified to being schematic and vice-versa.
-Andrew
Email Gateway (Aug 22 2022 at 09:36):From: Makarius <makarius@sketis.net>
On Tue, 7 Apr 2015, Andrew Gacek wrote:
How do schematic variables relate to \And quantified variables?
The Pure quantifier !!x. B x provides a local context to B x inside the
language of propositions. When you positively establish !!x. B x as a
fact, the system puts it into a standard form B ?x with schematic x. There
is normally no choice here: if facts with outermost !!x. B x persist,
something is usually wrong somewhere.
Negatively, on the assumption side, the !! quantier is not optional,
according to how the logic works.
but it's not clear to me why I can't freely move a variable
from being \And quantified to being schematic and vice-versa.
To develop an intuition about quantifier scoping rules, I recommend to
prove or disprove propositions involving ALL and --> in FOL or HOL (!) and
let "blast" or "iprover" or something else work on that. Then you
transfer the results mentally to !! and ==> in Pure.
I know that sometimes I need to use 'case' and sometimes 'case_tac' for
example
That is a slightly different situation. If you have a subgoal with local
!! quantification, these goal parameters are not part of the proof
context, so you can't refer to them directly.
Nonetheless case_tac and friends do that unofficially, and until
Isabelle2014 in a rather messy way. In Isabelle2015 this will be much
better, with extra colors to indicate the hidden goal scope that is
involved here.
As part of the Eisbach project, these old dark corners of the system have
become a bit lighter, and we might even get rid of rule_tac, case_tac etc.
eventually. They are stemming from very ancient times, before the proof
context was fully understood.
Makarius
Email Gateway (Aug 22 2022 at 09:36):From: "W. Douglas Maurer" <maurer@gwu.edu>
It looks as though you can always use lemma atomize_all to go back
and forth between !! (that is, \And) and ALL, so you can use
whichever one you need:
lemma atomize_all [atomize]: (!!x. P x) == Trueprop (ALL x. P x )
proof assume !!x. P x then show ALL x. P x ..
next assume ALL x. P x then show !!x. P x by (rule allE) qed
(section 2.2.17 of "Isabelle/HOL --- Higher-Order Logic")
-Douglas
Last updated: Nov 21 2024 at 12:39 UTC