[isabelle] How to define parametric finite set of natural... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to define parametric finite set of natural...

Email Gateway (Mar 03 2025 at 22:03):

From: Kangfeng Ye <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I would like to define a new data type for a finite set of natural numbers,
and it is also parametric in its size.

Something like below.

abbreviation "max_agents ≡ 2"
typedef snat = "{0..<max_agents}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

There is one problem here because max_agents is not a parameter for snat. So
it couldn't be instantiated to types with different sizes.

I have tried the finite type variable below.

typedef ('s, 'n::finite) snat = "{0..<CARD('n)}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

But there are two problems:

I cannot use "derive linorder" to instantiate linorder for the type (I want
to use the sort for the type)
an error in code generation "Finite_Set.hs:21:1-52: Non-exhaustive patterns
in function card"

Then I tried locale as well like below.

locale T1 =
fixes max_agents :: "nat"
begin
typedef snat = "{0..<max_agents}"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)
end

This also caused an error:

Illegal variables in representing set: "max_agents"

It seems related to "closed term" as mentioned in
https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf

By the way, I am using Isabelle2023 now.

Any suggestions?

Thanks,
Kangfeng

Email Gateway (Mar 04 2025 at 11:28):

From: Fabian Huch <huch@in.tum.de>
In HOL (and Isabelle/HOL in particular), types cannot depend on terms,
so #1 and #3 are not possible -- you can only do #2, commonly called the
'Harrison Trick' [1].

Why the Haskell code-gen isn't set up for CARD is a different question
(that I can't answer).

Fabian

[1]: Kunčar, O., Popescu, A. (2016). From Types to Sets by Local Type
Definitions in Higher-Order Logic. In: Blanchette, J., Merz, S. (eds)
Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer
Science(), vol 9807. Springer, Cham.
https://doi.org/10.1007/978-3-319-43144-4_13

On 3/3/25 23:03, Kangfeng Ye (via cl-isabelle-users Mailing List) wrote:

Dear all,

I would like to define a new data type for a finite set of natural numbers,
and it is also parametric in its size.

Something like below.

abbreviation "max_agents ≡ 2"
typedef snat = "{0..<max_agents}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

There is one problem here because max_agents is not a parameter for snat. So
it couldn't be instantiated to types with different sizes.

I have tried the finite type variable below.

typedef ('s, 'n::finite) snat = "{0..<CARD('n)}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

But there are two problems:
- I cannot use "derive linorder" to instantiate linorder for the type (I want
to use the sort for the type)
- an error in code generation "Finite_Set.hs:21:1-52: Non-exhaustive patterns
in function card"

Then I tried locale as well like below.

locale T1 =
fixes max_agents :: "nat"
begin
typedef snat = "{0..<max_agents}"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)
end

This also caused an error:
- Illegal variables in representing set: "max_agents"

It seems related to "closed term" as mentioned in
https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf

By the way, I am using Isabelle2023 now.

Any suggestions?

Thanks,
Kangfeng

Email Gateway (Mar 04 2025 at 12:28):

From: Kangfeng Ye <cl-isabelle-users@lists.cam.ac.uk>
Fabian,

That's what I thought. Thanks for confirming it and I will focus on #2 and
try to figure out the problem with the code generation.

Cheers,
Kangfeng

On Tue, 4 Mar 2025, 12:28 Fabian Huch, <huch@in.tum.de> wrote:

In HOL (and Isabelle/HOL in particular), types cannot depend on terms,
so #1 and #3 are not possible -- you can only do #2, commonly called the
'Harrison Trick' [1].

Why the Haskell code-gen isn't set up for CARD is a different question
(that I can't answer).

Fabian

[1]: Kunčar, O., Popescu, A. (2016). From Types to Sets by Local Type
Definitions in Higher-Order Logic. In: Blanchette, J., Merz, S. (eds)
Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer
Science(), vol 9807. Springer, Cham.
https://doi.org/10.1007/978-3-319-43144-4_13

On 3/3/25 23:03, Kangfeng Ye (via cl-isabelle-users Mailing List) wrote:

Dear all,

I would like to define a new data type for a finite set of natural
numbers,
and it is also parametric in its size.

Something like below.

abbreviation "max_agents ≡ 2"
typedef snat = "{0..<max_agents}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

There is one problem here because max_agents is not a parameter for
snat. So
it couldn't be instantiated to types with different sizes.

I have tried the finite type variable below.

typedef ('s, 'n::finite) snat = "{0..<CARD('n)}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

But there are two problems:
- I cannot use "derive linorder" to instantiate linorder for the type (I
want
to use the sort for the type)
- an error in code generation "Finite_Set.hs:21:1-52: Non-exhaustive
patterns
in function card"

Then I tried locale as well like below.

locale T1 =
fixes max_agents :: "nat"
begin
typedef snat = "{0..<max_agents}"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)
end

This also caused an error:
- Illegal variables in representing set: "max_agents"

It seems related to "closed term" as mentioned in
https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf

By the way, I am using Isabelle2023 now.

Any suggestions?

Thanks,
Kangfeng

Email Gateway (Mar 04 2025 at 21:59):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
I would recommend looking at HOL/Library/Numeral_Type.thy -- it implements types with n elements. These types are then just called "n".

I.e. you can write "x :: 10" and x will be a variable that can take on values 0..9. They support a decent amount of arithmetic modulo the type size, e.g. "5 + 5 = (0::10)".

There is a bit of additional library for it in https://github.com/seL4/l4v/blob/master/lib/More_Numeral_Type.thy

Cheers,
Gerwin

On 4 Mar 2025, at 23:28, Kangfeng Ye <cl-isabelle-users@lists.cam.ac.uk> wrote:

Fabian,

That's what I thought. Thanks for confirming it and I will focus on #2 and try to figure out the problem with the code generation.

Cheers,
Kangfeng

On Tue, 4 Mar 2025, 12:28 Fabian Huch, <huch@in.tum.de<mailto:huch@in.tum.de>> wrote:
In HOL (and Isabelle/HOL in particular), types cannot depend on terms,
so #1 and #3 are not possible -- you can only do #2, commonly called the
'Harrison Trick' [1].

Why the Haskell code-gen isn't set up for CARD is a different question
(that I can't answer).

Fabian

On 3/3/25 23:03, Kangfeng Ye (via cl-isabelle-users Mailing List) wrote:

Dear all,

I would like to define a new data type for a finite set of natural numbers,
and it is also parametric in its size.

Something like below.

abbreviation "max_agents ≡ 2"
typedef snat = "{0..<max_agents}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

There is one problem here because max_agents is not a parameter for snat. So
it couldn't be instantiated to types with different sizes.

I have tried the finite type variable below.

typedef ('s, 'n::finite) snat = "{0..<CARD('n)}::nat set"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)

But there are two problems:
- I cannot use "derive linorder" to instantiate linorder for the type (I want
to use the sort for the type)
- an error in code generation "Finite_Set.hs:21:1-52: Non-exhaustive patterns
in function card"

Then I tried locale as well like below.

locale T1 =
fixes max_agents :: "nat"
begin
typedef snat = "{0..<max_agents}"
morphisms nat_of_snat snat_of_nat
by (rule_tac x="0" in exI, auto)
end

This also caused an error:
- Illegal variables in representing set: "max_agents"

It seems related to "closed term" as mentioned in
https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf

By the way, I am using Isabelle2023 now.

Any suggestions?

Thanks,
Kangfeng

Email Gateway (Mar 05 2025 at 00:29):

From: Kangfeng Ye <cl-isabelle-users@lists.cam.ac.uk>
Gerwin,

I would recommend looking at HOL/Library/Numeral_Type.thy -- it implements

types with n elements. These types are then just called "n".

I.e. you can write "x :: 10" and x will be a variable that can take on

values 0..9. They support a decent amount of arithmetic modulo the type
size, e.g. "5 + 5 = (0::10)".

I did use the Numeral_Type.thy for the 'a::finite and I usually instantiate
the type "('s, 'a::finite) snat" as "(T, 2) snat". Then I got the error in
code generation "Finite_Set.hs:21:1-52: Non-exhaustive patterns".
At the moment, I have received suggestions from other people about using
Type_Length (as used in Saturated.thy or Word.thy). I am trying this
approach.

There is a bit of additional library for it in

https://github.com/seL4/l4v/blob/master/lib/More_Numeral_Type.thy

Glad to know this additional library.

Cheers,
Kangfeng

Email Gateway (Mar 07 2025 at 01:08):

From: Kangfeng Ye <cl-isabelle-users@lists.cam.ac.uk>
Based on Peter Gammie, Fabian, and others' suggestions, I have found a
workable solution using #2. I have attached the theory for your reference.

A little bit of information about the scenario. I would like to use the
finite set of natural numbers to define finite agents, finite messages and
channels.

For example,

datatype ('a::len) dagent = Agent (ag: "'a ssnat")

datatype ('k::len,'s::len) dkey = Kp (kp: "ssnat['k]") | Ks (ks:

"ssnat['s]")

Then for each protocol, they are instantiated to specific finite types.

type_synonym max_agents = 4

type_synonym max_pks = 4
type_synonym max_sks = 4
type_synonym dagent = "max_agents dagent"

type_synonym dkey = "(max_pks, max_sks) dkey"

This is what I want to have: it is parametric in sizes and can generate
right Haskell code.

Thanks for all your help.

Cheers,
Kangfeng

On Wed, 5 Mar 2025 at 01:28, Kangfeng Ye <kangfeng.ye@york.ac.uk> wrote:

Gerwin,

I would recommend looking at HOL/Library/Numeral_Type.thy -- it implements

types with n elements. These types are then just called "n".

I.e. you can write "x :: 10" and x will be a variable that can take on

values 0..9. They support a decent amount of arithmetic modulo the type
size, e.g. "5 + 5 = (0::10)".

I did use the Numeral_Type.thy for the 'a::finite and I usually
instantiate the type "('s, 'a::finite) snat" as "(T, 2) snat". Then I got
the error in code generation "Finite_Set.hs:21:1-52: Non-exhaustive
patterns".
At the moment, I have received suggestions from other people about using
Type_Length (as used in Saturated.thy or Word.thy). I am trying this
approach.

There is a bit of additional library for it in

https://github.com/seL4/l4v/blob/master/lib/More_Numeral_Type.thy

Glad to know this additional library.

Cheers,
Kangfeng

FSNat.thy

Last updated: Mar 09 2025 at 12:28 UTC