Email Gateway (Aug 22 2022 at 18:52): Email Gateway (Aug 22 2022 at 18:52):From: "John F. Hughes" <jfh@cs.brown.edu>
Again, I'm trying to work with affine geometries. It seemed that proving
things about general affine geometries might be like proving things about
general groups, or modules, or other things like that...but because I seem
to have two type-parameters, the "class" approach used in
section ‹Basic affine geometries›
theory Affine1
imports Main
begin
locale affine_plane_basics =
fixes
meets :: "'point ⇒ 'line ⇒ bool"
locale affine_plane = affine_plane_basics +
assumes
a1a: "⟦ (P::'a) ≠ Q ⟧ ⟹ (∃! (l::'b). meets P l ∧ meets Q l)"
(* This version fails:
a1b: "⟦ (P::'point) ≠ Q ⟧ ⟹ (∃! (l::'line). meets P l ∧ meets Q l)"
*)
Last updated: Nov 21 2024 at 12:39 UTC