Email Gateway (Aug 23 2022 at 08:13): Email Gateway (Aug 23 2022 at 08:13):From: "John F. Hughes" <jfh@cs.brown.edu>
I'm trying to use locales to represent projective planes in synthetic
projective geometry. So to me, a "projective geometry" Is a function
"meets" that has a few properties (the "axioms" of the projective geometry,
like "every two distinct lines intersect at a single point"). So "meets P
k" is my version of "the point P lies on the line k".
For reasons I don't understand, I need to describe the existence of "meets"
first, and then combine it with the axioms (or so I was advised by someone
far more expert with locales than I am) so building a simple starting case,
I get this:
=============
theory Example
imports Complex_Main
begin
locale projective_plane_data =
fixes meets :: "'point ⇒ 'line ⇒ bool"
begin
end
(* Things look OK here; not clear what ":: 'a" is all about *)
value projective_plane_data
locale projective_plane =
projective_plane_data meets
for meets :: "'point ⇒ 'line ⇒ bool" +
assumes
p1: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l"
(A)
begin
end
(* What's the problem here? *)
value projective_plane
==============
I expect, at that last line, to get some response like "projective_plane"
is a value that looks like <something or other>
But instead, I get:
Wellsortedness error:
Type 'b ⇒ 'a ⇒ bool not of sort typerep
Cannot derive subsort relation {} < typerep
I'd really like to be able to use the automatically-generated predicate
"projective_plane(...)" both in hypotheses and conclusions of theorems
(Example: the dual of a projective plane is also a projective plane.), but
right now, replacing that last line with
fun u :: "nat ⇒ nat ⇒ bool" where
"u (x) (y) = ((x+y) = 0)"
value "projective_plane(u)"
produces not "true" or "false" but an error:
No code equations for projective_plane.
Can someone help me understand what's going on here?
Email Gateway (Aug 23 2022 at 08:13):From: Peter Zeller <p_zeller@cs.uni-kl.de>
The "value" command can only be used with executable definitions. It is
possible to define your own code equations, but that is not needed to
use the predicate in proofs.
For example, you can write a Lemma and show that the predicate does not
hold for "u":
lemma "¬projective_plane u"
unfolding projective_plane_def by auto
-- Peter
Email Gateway (Aug 23 2022 at 08:14):From: "John F. Hughes" <jfh@cs.brown.edu>
Thank you. Onward and upward!
Last updated: Nov 21 2024 at 12:39 UTC