I've got a bunch of datatypes:
datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real" | A2Vertical "real"
definition A2Points::"a2pt set"
where "A2Points ≡ (UNIV::a2pt set)"
definition A2Lines::"a2ln set"
where "A2Lines ≡ (UNIV::a2ln set)"
datatype ('point, 'line) projPoint = OrdinaryP 'point | Ideal "'line set"
datatype ('point, 'line) projLine = OrdinaryL 'line | Infty
definition pPoints where
"pPoints ≡ {OrdinaryP P | P . (P ∈ A2Points)} ∪ {Ideal t | k t .
((k ∈ A2Lines) ∧ (t = affine_plane_data.line_pencil A2Points A2Lines (a2incid) k) )}"
definition pLines where
"pLines ≡ {OrdinaryL n | n . (n ∈ A2Lines)} ∪ {Infty}"
So there's really nothing subtle here -- just a bunch of nested constructors all boiling down to a pair of reals (or maybe something a little more complex in a couple of cases).
I'd really like to define a function from pPoints
to a triple of reals. I tried writing this:
definition rp2iso where
"rp2iso (Ordinary (A2Point x y)) = (x, y, 1)"
and got a Bad arguments on lhs
error, which didn't really surprise me.
But if I write
definition rp2iso where
"rp2iso (Ordinary P) = ... (x, y, 1)"
how do I fill in the "..." to extract the constructor arguments for the only possible constructor (A2Point
) for P
so that I can use them to write down the "result" that I want for the function?
BTW, I realize I also need to define the function on Ideal
points, but I suspect that this won't be so hard after I get the right syntax for Ordinary
points.
Definition does not allow pattern matching, you have to use fun
(and [simp del]:
to remove the simp rule)
You can also match on the right-hand side using case
or with a lambda (which gets translated to a case).
Thank you both, but I'm afraid that you both have overestimated my understanding of everything. In my example, I've got "..." in the midst of something that I think is "inner syntax", but each of you is proposing using various tokens that I think are "outer syntax" (e.g. case
and [simp del]:
). Is there a chance that one or both of you could actually type the line I need to replace
definition rp2iso where
"rp2iso (Ordinary P) = ... (x, y, 1)"
to make things work?
Also Mathias, should your [simp del]:
actually be [simp del: ...]
, where the ...
indicates some simp rule? If so, what simp-rule are you talking about? I've modifed the definition of pPoints
to make this code workable without reference to affine_plane_data
, and used find_theorems
to see if anything I've defined has generated any simp
rules, and I don't see any.
Here's the revised code for further discussion:
theory Construct
imports Complex_Main
begin
datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real" | A2Vertical "real"
definition A2Points::"a2pt set"
where "A2Points ≡ (UNIV::a2pt set)"
definition A2Lines::"a2ln set"
where "A2Lines ≡ (UNIV::a2ln set)"
datatype ('point, 'line) projPoint = OrdinaryP 'point | Ideal "'line set"
datatype ('point, 'line) projLine = OrdinaryL 'line | Infty
definition pPoints where
"pPoints ≡ {OrdinaryP P | P . (P ∈ A2Points)} ∪ {Ideal t | k t .
((k ∈ A2Lines) ∧ (t = {k}))}"
definition pLines where
"pLines ≡ {OrdinaryL n | n . (n ∈ A2Lines)} ∪ {Infty}"
find_theorems pPoints
end
fun rp2iso where
[simp del]: "rp2iso (Ordinary P) = ... (x, y, 1)"
I see...the [simp del]
is saying that Isabelle should not add this particular equality to its simp-set. I still don't understand how to extract x
and y
from the argument P
, but perhaps looking more at the documentation for fun
and datatypes will enlighten me.
fun
allows you to write arbitrary patterns
including your "rp2iso (Ordinary (A2Point x y)) = (x, y, 1)"
Ah...thank you very much!
Last updated: Jul 19 2025 at 04:33 UTC