John Hughes (Feb 12 2025 at 17:37): John Hughes (Feb 12 2025 at 17:37):I'm trying to build two mutually recursive datatypes. The broad notion is that new "lines" are created by naming two points that are on them, and new "points" are created by naming two lines that should contain the new point (thus making the lines 'meet'). I have two versions of the code, simplified down to illustrate a particular problem. (The use of "real" here, for example, is to avoid talking about an 'a 'b fpoint, and similarly for fline.)
theory MWE4
imports Complex_Main
begin
(* Successful, but not what I wanted *)
datatype fpoint1 = BaseP "real" | NewP "fline1" "fline1"
and fline1 = BaseL "real" | NewL "fpoint1" "fpoint1"
(* Closer, but unsuccessful *)
datatype fpoint = BaseP "real" | NewP "fline set"
and fline = BaseL "real" | NewL "fpoint set"
end
The first says that a point can be either something we started with ('BaseP') or created from two existing lines, and similarly for lines. The problem with this is equality: I want the point NewP k n to be the same as NewP n k. So I thought "rather than separating the two points, I could put them in a set, because in general {n,k} = {k,n}. The second datatype description tries this, but produces an error: *
Unsupported recursive occurrence of type "fline" via
type constructor "Set.set" in type expression "fline set"
Use the "bnf" command to register "Set.set" as a bounded
natural functor to allow nested (co)recursion through it.
I tried to read about the bnf command, but the only example of its bd: argument comes after 47 pages of documentation, and I just couldn't make sense of it.
What I really want to use is a notion of an "unordered pair". That would be nice because it's of bounded complexity compared to an arbitrary set. And I even found that there was a notion of Upair ... but it's defined in ZF instead of HOL.
Is there some easy way to define an unordered pair type in Isabelle, in a way that won't make mutually recursive datatype definitions choke?
The key property is that
((a, b)) = ((c, d)) <--> (a = c /\ b = d) \/ (a = d /\ b = c)
where I'm using (( . )) as my imagined constructor for an unordered pair.
Jan van Brügge (Feb 13 2025 at 10:05):There is also a uprod type in HOL-Library.Uprod that will work. The reason why set does not work is that it is unbounded. Using e.g. fset (finite sets) from HOL-Library would work
John Hughes (Feb 13 2025 at 17:22):I'll try uprod; thanks. A google search only sent me to the ZF version. :(
Jan van Brügge (Feb 13 2025 at 18:51):I found it by grepping for quotient_type in the isabelle sources
Last updated: Mar 09 2025 at 12:28 UTC