Stream: Beginner Questions

Topic: Defining a function on a datatype


view this post on Zulip John Hughes (Jul 14 2025 at 00:56):

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.

view this post on Zulip Mathias Fleury (Jul 14 2025 at 05:14):

Definition does not allow pattern matching, you have to use fun (and [simp del]: to remove the simp rule)

view this post on Zulip Lukas Stevens (Jul 14 2025 at 08:45):

You can also match on the right-hand side using case or with a lambda (which gets translated to a case).

view this post on Zulip John Hughes (Jul 14 2025 at 13:02):

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

view this post on Zulip Mathias Fleury (Jul 14 2025 at 13:07):

fun rp2iso where
   [simp del]: "rp2iso (Ordinary P) = ... (x, y, 1)"

view this post on Zulip John Hughes (Jul 14 2025 at 13:25):

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.

view this post on Zulip Mathias Fleury (Jul 14 2025 at 13:28):

fun allows you to write arbitrary patterns

view this post on Zulip Mathias Fleury (Jul 14 2025 at 13:28):

including your "rp2iso (Ordinary (A2Point x y)) = (x, y, 1)"

view this post on Zulip John Hughes (Jul 14 2025 at 21:46):

Ah...thank you very much!


Last updated: Jul 19 2025 at 04:33 UTC