Defining a quotient in a locale · Beginner Questions

I have a locale for representing something called an affine plane; it's defined using a different locale (affine_plane_data) which is just a hack for allowing me to define the word "parallel", so that I can use it in defining an affine plane.

Within an affine plane, "parallel" is an equivalence relation on lines, as one might expect by analogy with Euclidean geometry. I'd like to define something called (in geometry books) a 'pencil of parallel lines', which is an equivalence class of parallel lines within my plane. In euclidean geometry, the collection of all vertical lines is a pencil; the collection of all horizontal lines is a pencil; the collection of all lines of slope 13 is a pencil, and so on.

When I try to do this, I get into trouble because my notion of "parallel" depends on the 'parameters' of my affine plane, namely the types for the sets Points and Lines and a function called meets, and quotient_type fails me.

The problem is shown below, where I've replaced the proofs with sorry so as to show the key problem. The failure is in the quotient_type just a few lines before the end.

theory Affine_BasicsMWE
  imports Complex_Main HOL.Equiv_Relations
begin

locale affine_plane_data =
  fixes Points :: "'p set" and Lines :: "'l set" and meets :: "'p ⇒ 'l ⇒ bool"
  fixes join:: "'p ⇒ 'p ⇒ 'l"
  fixes find_parallel:: "'l ⇒ 'p ⇒ 'l"
begin

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

definition collinear :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
    where "collinear A B C = (if A ∈ Points ∧ B ∈ Points ∧ C ∈ Points
  then (∃ l. l ∈ Lines ∧ meets A l ∧ meets B l ∧ meets C l) else undefined)"
end

locale affine_plane =
    affine_plane_data  +
    assumes
    a1a: "⟦P ≠ Q; P ∈ Points; Q ∈ Points⟧ ⟹ join P Q ∈ Lines ∧ meets P (join P Q)  ∧ meets Q (join P Q)" and
    a1b: "⟦P ≠ Q; P ∈ Points; Q ∈ Points; meets P m; meets Q m⟧ ⟹ m = join P Q" and
    a2a: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹ find_parallel l P ∈ Lines" and
    a2b: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹  ( find_parallel l P) || l" and
    a2c: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹  meets P (find_parallel l P)" and
    a2d: "⟦ P ∈ Points; l ∈ Lines; m ∈ Lines; m || l; meets P m⟧ ⟹ m = find_parallel l P" and
    a3: "∃P Q R. P ∈ Points ∧ Q ∈ Points ∧ R ∈ Points ∧ P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ (collinear P Q R)"
begin

lemma parr_refl:
  shows "reflp parallel"
  sorry

lemma parr_sym:
  shows "symp parallel"
  sorry

lemma parr_trans:
  shows "transp parallel"
  sorry

lemma parallel_equivalence:
  shows "Equiv_Relations.equivp parallel"
proof -
  show ?thesis using parr_refl parr_sym parr_trans equivpI by auto
qed

quotient_type  pencil = "'l" / "parallel::'l ⇒ 'l⇒ bool"
  morphisms Rep_Pencil Abs_Pencil

find_consts name: "parallel"
(* gives  Affine_Basics.affine_plane_data.parallel :: "'p set ⇒ 'l set ⇒ ('p ⇒ 'l ⇒ bool) ⇒ 'l ⇒ 'l ⇒ bool" *)

end

Stream: Beginner Questions

Topic: Defining a quotient in a locale

John Hughes (Feb 10 2025 at 11:18):