[isabelle] Locales and instances, again · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locales and instances, again

Email Gateway (Aug 22 2022 at 20:28):

From: "John F. Hughes" <jfh@cs.brown.edu>
My previous question about locales arose because I was trying to address a
more complicated question, and wanted a minimal case; apparently I
overshot. Here's the more complicated one. I've defined a locale, "affine
plane", with three axioms. (It has to include "affine_plane_data", because
I need the notions of parallelism and collinearity, which are defined
there; I confess that I don't understand the bit saying

locale affine_plane =
affine_plane_data meets
for meets :: "'point ⇒ 'line ⇒ bool" +
assumes ...

and wrote it because someone helpful earlier suggested it would let me tell
ISabelle that the "meets" functions in the two different locals were one
and the same, and would still be called "meets." The three axioms are
fairly straightforward: there's a unique line through any two distinct
points; if P does not lie on a line l, then there's a line through P that's
parallel to l; there are three noncollinear points.

I then build up the real affine plane (Cartesian 2-dimensional coordinate
space) by defining types for points and lines, and writing down the "meets"
function, which I've called "a2meets"; indeed, everything in this example
has "a2" as a preface, indicating "real affine 2-space".

I then state three theorems, whose proofs I've omitted by using "sorry" so
that I can get to the point, which is that I want to say that the function
"a2meets" constitutes the data needs for an affine plane, the final
theorem. The three little theorem match the axiom statements as closely as
I can make them. (I used cut-and-paste, and then added 'a2' in the relevant
places.) It seems completely obvious to me that theorem "a2_is_plane" is
true, but using "try" lead to no joy. Nor does

using a2_ax1 a2_ax2 a2_ax3 try

which I thought might guide "try" a little bit. Is there some way to guide
Isabelle to agree with this (obvious) conclusion? I'm going to have to show
various things are affine and projective planes over the next few weeks,
and I'd like to think that each proof need not require that I ask yet
another question of this mailing list.
========

theory Scratch3
imports Complex_Main

begin
locale affine_plane_data =
fixes meets :: "'point ⇒ 'line ⇒ bool"

begin
definition (in affine_plane_data) parallel:: "'line ⇒ 'line ⇒ bool"
(infix "||" 50)
where "l || m ⟷ (l = m ∨ ¬ (∃ P. meets P l ∧ meets P m))"

definition (in affine_plane_data) collinear :: "'point ⇒ 'point ⇒
'point ⇒ bool"
where "collinear A B C ⟷ (∃ l. meets A l ∧ meets B l ∧ meets C l)"
end

locale affine_plane =
affine_plane_data meets
for meets :: "'point ⇒ 'line ⇒ bool" +
assumes
ax1: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l" and
ax2: "¬ meets P l ⟹ ∃!m. l || m ∧ meets P m" and
ax3: "∃P Q R. P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R"

(* Now describe the real affine plane: Points are pairs (x,y); lines
are either ordinary (y = mx + b) or vertical (x = c). A point p meets
a line l if p lies on l. *)
datatype a2pt = A2Point "real" "real"

datatype a2ln = A2Ordinary "real" "real"
| A2Vertical "real"

fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where
"a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
"a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"

definition a2parallel:: "a2ln ⇒ a2ln ⇒ bool" (infix "a2||" 50)
where "l a2|| m ⟷ (l = m ∨ ¬ (∃ P. a2meets P l ∧ a2meets P m))"

definition a2collinear :: "a2pt ⇒ a2pt ⇒ a2pt ⇒ bool"
where "a2collinear A B C ⟷ (∃ l. a2meets A l ∧ a2meets B l ∧ a2meets
C l)"

theorem a2_ax1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
sorry

theorem a2_ax2: "¬ (a2meets P l) ⟹ ∃!m. l a2|| m ∧ a2meets P m"
sorry

theorem a2_ax3: "∃P Q R . P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ a2collinear P Q R"
sorry

theorem a2_is_plane: "affine_plane a2meets"
try

Email Gateway (Aug 22 2022 at 20:28):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
You need to create an interpretation of affine_plane_data in order to satisfy the
proof obligations of an an interpretation of affine_plane (cf. the "layered approach"
referred to somewhere that I remember reading in the tutorials on locales).

Your affine_plane_data locale has no assumptions, so the interpretation can
be made with a trivial proof (".", see below). Nevertheless, you need it because
"affine_plane_data a2meets" is an explicit condition of all the facts in "affine_plane".

=========================
theory Scratch3
imports Complex_Main

begin
locale affine_plane_data =
fixes meets :: "'point ⇒ 'line ⇒ bool"

begin
definition parallel:: "'line ⇒ 'line ⇒ bool" (infix "||" 50)
where "l || m ⟷ (l = m ∨ ¬ (∃ P. meets P l ∧ meets P m))"

definition collinear :: "'point ⇒ 'point ⇒ 'point ⇒ bool"
where "collinear A B C ⟷ (∃ l. meets A l ∧ meets B l ∧ meets C l)"
end