Stream: Beginner Questions

Topic: "infix" notation in a definition

John Hughes (May 24 2025 at 10:10):

I've written theorems of the form "if $g$ is a function with certain properties, then ..."; a typical one starts like this:

lemma AB:
  fixes Points::"'p set"
  fixes Lines::"'l set"
  fixes incid :: "'p ⇒ 'l ⇒ bool"  (infix "⊲" 60)
  fixes join::"'p ⇒ 'p ⇒ 'l"
  assumes ... various things...
  shows ...something...

where I typically show something about the functions incid and join.

I not want to state a theorem in the form "If we define $g$ to be the function [details], then $g$ has the following properties..." A typical theorem statement is this:

lemma Ap2:
  assumes ap: "affine_plane Points Lines incid join find_parallel"
  defines pPdef: "pPoints ≡ {OrdinaryP P | P . (P ∈ Points)} ∪ {Ideal t | k t .
                  ((k ∈ Lines) ∧ (t = affine_plane_data.line_pencil Points Lines (incid) k) )}"
  defines pLdef: "pLines ≡ {OrdinaryL n | n . (n ∈ Lines)} ∪ {Infty}"
  defines ‹pincid ≡  mprojectivize (incid) (infix "⊲" 60)›
  shows "⟦k ∈ pLines; n ∈ pLines⟧ ⟹ ∃ P . (P ∈ pPoints ∧ P ⊲ k ∧ P ⊲ n)"

Here, in the definition of pincid, I've used cartouches rather than double-quotes, but I've also tried

  defines "pincid ≡  mprojectivize (incid) (infix "⊲" 60)"

which fails because the double-quotes starting the 'infix' expression terminate the opening double-quotes. And I've tried

  defines ‹pincid ≡  mprojectivize (incid) (infix ‹⊲› 60)›

in hope that matching of open- and close- cartouches might help Isabelle parse this, but without any luck.
As you can see, the "shows" line uses the ⊲; so does the rather long proof. I could get rid of this and use prefix notation throughout, but it's certainly less readable. Is there any way to do what I'm trying to do, or is this a limitation of the fixes-assumes-defines-shows notation?

Mathias Fleury (May 24 2025 at 11:32):

Use a context. In the context you can define notations…

Mathias Fleury (May 24 2025 at 11:35):

context
  fixes l :: nat
begin
qualified definition x where ‹x a b = (l + a > b)›

notation x (infix "TT" 70)


lemma H:
  shows ‹a TT 4›
  sorry
end

thm H

Mathias Fleury (May 24 2025 at 11:36):

and if the definitions are not interesting enough to be named in the theorem, there is no reason to have them in a theorem either…

John Hughes (May 24 2025 at 12:55):

Thanks for the tip on 'context' -- I hadn't seen that before.

I've also found a workaround in the theorem statement, replacing the last defines with

  fixes pincid (infix "p⊲" 60)
  assumes ‹pincid =  mprojectivize (incid)›

which seems to achieve the same thing.

Mathias Fleury (May 25 2025 at 05:28):

I thought that you did not want that:

I not want to state a theorem in the form "If we define $g$ to be the function [details], then $g$ has the following properties..."

John Hughes (May 28 2025 at 12:00):

You are (sort of) correct. I just tried to re-read what I wrote and it made no sense to me, either.

The key problem is this: I wrote "I not want to ...", but I intended to write "I now want to..." My apologies for the confusion.

Last updated: May 31 2025 at 04:25 UTC