Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Defining things; checking instances

Email Gateway (Aug 22 2022 at 18:51):

From: "John F. Hughes" <jfh@cs.brown.edu>
I'm trying to use Isabelle to play with synthetic projective geometry.
I've managed to prove things in the first couple of pages of the
textbook I'm using, which is great. But in doing so, I've stumbled on
several items. I hope it's OK to ask multiple questions at once here.

1. As a starting point, I'm working with affine planes. Those consist
   of a set of points (an abstract type) and lines, a line being a subset
   of the set of points. Two lines are parallel if their intersection is
   empty, or if they're identical. So I've got this:

theory Geometry2_jfh
imports Main
begin
locale affine_plane_syntax =
fixes
Points :: "'a set" and
Lines :: "'a set set"
begin
definition parallel (infix "||" 50)
where "⟦ l ∈ Lines; m ∈ Lines ⟧ ⟹ l || m ⟷ l = m ∨ ¬ (∃ P∈
Points. P∈ l ∧ P ∈ m)"
end

There are a few axioms for an affine plane, and then I try to prove
that parallelism is an equivalence relation...but nitpick shows that
it's not...by giving me an example in which s is parallel to t, and t
is parallel to u, but s is not parallel to u. This is not because of
a failure in the foundations of affine geometry, but a failure in my
Isabelle formulation: the sets s, t, u that "nitpick" discovers are
not actually lines in my geometry. They're subsets of the set of
points, but are not among those particular subsets that are declared
to be "lines". The definition above says that IF l and m are lines,
then parallelism means this particular thing. But if they're NOT
lines, it also has a meaning. Is there a way for me to say "parallel"
is a predicate that operates on pairs of elements of the set "Lines",
and not on pairs of arbitrary subsets of the set of Points?

[For now I've added two "axioms" that say that if m is not in "Lines",
then a || m is false, and that m || a is false, but that seems bogus.]

2. My current work has all been about a single affine plane, but at
   some point I need to say things where A and A' are both affine planes,
   and f is an isomorphism between them, etc. For that, I probably want
   to use the "class" construction as was done for groups (in the
   abstract algebra sense) here:
   http://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/Group.html

I have a question about this, however: suppose that, in that "groups"
document, I'd wanted to prove that $Z/3Z$, i.e., a three element set
with an operation defined in analogy with modular addition, is a
group. I don't see how to do this. I basically want to build a
constant (my three-element set together with its addition operation)
and assert that this is an element of the class "group". Any thoughts?

3. Even within my current work, I'd like to say "The 4-point affine
   plane is an affine plane," or at least "the 4-point affine plane
   satisfies my first axiom, namely that for any two distinct points,
   there's a line containing them". I tried writing this:

theorem (in affine_plane) four_point_plane : " (Points = {P,Q,R,S}) ∧
(Lines = {{P,Q},{P,R},{P,S},{Q,R},{Q,S},{R,S}}) →
(((E ∈ Points) ∧ (F ∈ Points) ∧ (E ≠ F)) → (∃! l∈ Lines. E ∈ l ∧ F ∈ l))

but got a "failed to parse prop" error.

I tried reducing this to a minimal non-working example, and arrived at this:

theory test_jfh
imports Main
begin
theorem silly : "(Points = {P}) → (P ∈ Points)"
end

for which I got the same "failed to parse prop" error.

I'd sure appreciate any suggestions.

Email Gateway (Aug 22 2022 at 18:51):

From: Mark Wassell <mpwassell@gmail.com>
Hi,

Regarding your last question: The problem here is that your implication
arrow is too short. Trying entering --> (two dashes and then greater than).
Alternatively \longrightarrow.

Cheers

Mark

Email Gateway (Aug 22 2022 at 18:51):

From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks! I've begun resolving some of the other bits as well, but definitely
feel as if there are a lot of arrows, and they all mean "this leads to
that" , some being in Isabelle, some being in HOL, and the distinction
being baffling. And then there's the choice to use int => int to mean an
int-to-int function, rather than int -> int, which seems just weird. Does
the "->" arrow mean ANYthing at all? Or is it just a vestigial thing left
around to tease newcomers? :)

Just when I think I might be beginning to sort something out, I come to
this in "Programming and Proving":
===
The implication ⇒ is part of the Isabelle framework. It structures theorems
and proof states, separating assumptions from conclusions. The implication
→ is part of the logic HOL and can occur inside the formulas that make up
the assumptions and conclusion. Theorems should be of the form [[ A1; . .
.; An ]] ⇒ A, not A1 ∧ . . . ∧ An → A. Both are logically equivalent but
the first one works better when using the theorem in further proofs.
===
It'd be nice if this oh-so-cryptic paragraph gave a hint about WHY one of
two logically equivalent things "works better." Otherwise I'm just being
told "do this because it's what the master does," and doesn't help me
achieve my own mastery. Sigh.

--John

Email Gateway (Aug 22 2022 at 18:52):

From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is a logical framework. Inference rules are expressed in this framework using the symbols (in ASCII) !! and ==>. It’s a higher-order framework, so it has function types, written using =>. All built-in inference mechanisms work on the level of this framework. Variables of the form ?x also express universal quantification.

Note that a logic defined in Isabelle doesn’t need to have its own implication symbol, quantifiers or any concept of function space. But if it does, symbols such as !, --> and -> are available to denote them.

In Isabelle/ZF, A -> B denotes the set of functions between the sets A and B. And it has the same meaning in Isabelle/HOL.

If you write a theorem as A ==> B, then it can immediately be used for forward or backward chaining. If instead you write it as A --> B, then you’ll need to involve implication rules in order to do anything with it. No surprise then that proofs in certain other systems are dominated by the use of implication rules.

Larry

Email Gateway (Aug 22 2022 at 18:54):

From: Thomas Sewell <sewell@chalmers.se>
I'll add some observations, which might or might not be helpful.

There are indeed a lot of arrows. In addition, like every functional language I've used, Isabelle seems to make some non-orthodox decisions about about the symbol/arrow for various basic operators.

I think that you are right, and the short-single arrow is always parsed as a symbol but is not (by default) part of any particular syntax.

Here's the more substantial question. Given that they're logically equivalent, why would "P ==> Q ==> R" be described as more useful than "P & Q --> R"?

To a beginner, they may in fact be equivalent. Most of the complex/smart tools, like metis or the simplifier, will use rules of either form in essentially the same way.

However the basic Isabelle rule calculus can also be quite useful. The basic calculus takes its cues on how to use a rule from its shape, and only looks at the pure Isabelle operators "_ ==> _" and "!!_. _". Used as an introduction rule, "P & Q --> R" can solve goals of exactly the same form, but "P ==> Q ==> R" will replace goals of the form "R" with a pair of goals "P" and "Q". "P ==> Q ==> R" can also be used as a destruction rule or elimination rule, which "P & Q --> R" can't.

Or, in short, if you know how to use the resolution calculus, "P ==> Q ==> R" allows you to specify three different kinds of single step, whereas "P & Q --> R" is only useful in a situation you're unlikely to be in.

Cheers,
Thomas.

Email Gateway (Aug 22 2022 at 18:55):

From: Makarius <makarius@sketis.net>
It is better to have clearly designated threads for each topic, to
increase chances that all problems are eventually sorted out.

Makarius

Last updated: May 06 2024 at 12:29 UTC