Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Datatype + cardinality + polymorphismus?


view this post on Zulip Email Gateway (Aug 22 2022 at 10:23):

From: "Roger H." <s57076@hotmail.com>
Hello,

  1. If i have datatype color = red | blue
    how do i write smth like
    -"is c in color"...meaning "is c an instance of color?"
    -"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
    -length function..number of elements in the datatype .. so that it returns here length (color) = 2

  2. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
    f :: color -> ??red |-> {1,2}blue |-> {True}
    cause range f = UNIV isnt right.
    Many thanks!

view this post on Zulip Email Gateway (Aug 22 2022 at 10:23):

From: Larry Paulson <lp15@cam.ac.uk>
Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website http://isabelle.in.tum.de/documentation.html.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 10:23):

From: Peter Lammich <lammich@in.tum.de>
On Sa, 2015-06-27 at 13:06 +0200, Roger H. wrote:

Hi.

Hello,
1. If i have datatype color = red | blue
how do i write smth like
-"is c in color"...meaning "is c an instance of color?"
Exactly the c's of type color are in color.
The set of all colors is "UNIV :: color set".

-"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
Just "ALL c::color. P c". Here, the ::color is a type constraint,
which forces the bound variable "c" to have type color, but is not
explicitly visible in the parsed term.

-length function..number of elements in the datatype .. so that it returns here length (color) = 2
It's "card( UNIV :: color set)", provided color is a finite type.

  1. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
    f :: color -> ??red |-> {1,2}blue |-> {True}

This is not possible in HOL's type system. An approximation would be
f :: color => nat+bool

Here, nat+bool is the sum type, that has the
elements Inl (n::nat) and Inr (b::bool)

view this post on Zulip Email Gateway (Aug 22 2022 at 10:24):

From: "Roger H." <s57076@hotmail.com>

-"is c in color"...meaning "is c an instance of color?"
Exactly the c's of type color are in color. > The set of all colors is "UNIV :: color set".

  1. My question is how can i write this kind of predicate:
    (red \in color) .................which is of type bool
    I dont know it yet, since
    "red ∈ (UNIV :: color set)" doesnt seem the right way to write it, since for
    --datatype color = red | blue
    lemma "red ∈ (UNIV :: color set)" is proven true,--
    but also
    lemma "green ∈ (UNIV :: color set)" is also true..which should be false. ??

  2. Concerning the cardinality... how do i prove the following
    lemma "card( UNIV :: color set) = 2"
    Cause by simp, this just simplifies in : "card UNIV = 2"
    Thank you!

On Sa, 2015-06-27 at 13:06 +0200, Roger H. wrote: Hi.

Hello,
1. If i have datatype color = red | blue
how do i write smth like
-"is c in color"...meaning "is c an instance of color?"
Exactly the c's of type color are in color. The set of all colors is "UNIV :: color set".

-"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
Just "ALL c::color. P c". Here, the ::color is a type constraint, which forces the bound variable "c" to have type color, but is not explicitly visible in the parsed term.

-length function..number of elements in the datatype .. so that it returns here length (color) = 2
It's "card( UNIV :: color set)", provided color is a finite type.

  1. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
    f :: color -> ??red |-> {1,2}blue |-> {True}

This is not possible in HOL's type system. An approximation would be f :: color => nat+bool Here, nat+bool is the sum type, that has the elements Inl (n::nat) and Inr (b::bool) >

view this post on Zulip Email Gateway (Aug 22 2022 at 10:24):

From: "C. Diekmann" <diekmann@in.tum.de>
Probably you first want to define the type

datatype colors = Red | Blue | Green

The you want to reason about sets of this type

lemma "Red : {Blue, Red, Red}"

Otherwise, the manual provides good examples.
Cornelius

view this post on Zulip Email Gateway (Aug 22 2022 at 10:24):

From: Larry Paulson <lp15@cam.ac.uk>
I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 10:24):

From: Peter Lammich <lammich@in.tum.de>
You should check out (eg in the manual) how the type system in
Isabelle/HOL works.

Propositions like "x \<in> UNIV" are trivial, because x gets inferred
some type, and UNIV is the set of all elements of this type.

If you write "green", then green is just a variable (of type color).

view this post on Zulip Email Gateway (Aug 22 2022 at 10:24):

From: "Roger H." <s57076@hotmail.com>

I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Thank you Larry, this is a clear answer for one of my questions.
My other questions were:

  1. Assume I have
    datatype color = red |blue
    fun f:: color => nat setf red = {1}f blue = {2}
    definition M :: "nat set" whereM = the union...over all x in color...of f(x) //the result should be M = {1} union {2} = {1,2}
    I dont know how to write the implementation of M in isabelle syntax.

  2. card (color) = 2 ? or size (color) = 2 ? I am looking for the name of the function that gets a type and returns its number of constructors (for such simple finite non-recursive types)

Thank you!

Subject: Re: [isabelle] Datatype + cardinality + polymorphismus?
From: lp15@cam.ac.uk
Date: Sat, 27 Jun 2015 18:02:46 +0100
CC: isabelle-users@cl.cam.ac.uk
To: s57076@hotmail.com

I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Larry Paulson

On 27 Jun 2015, at 12:22, Larry Paulson <lp15@cam.ac.uk> wrote:

Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website http://isabelle.in.tum.de/documentation.html.

Larry Paulson

On 27 Jun 2015, at 12:06, Roger H. <s57076@hotmail.com> wrote:

Hello,
1. If i have datatype color = red | blue
how do i write smth like
-"is c in color"...meaning "is c an instance of color?"
-"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
-length function..number of elements in the datatype .. so that it returns here length (color) = 2
2. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
f :: color -> ??red |-> {1,2}blue |-> {True}
cause range f = UNIV isnt right.
Many thanks!

view this post on Zulip Email Gateway (Aug 22 2022 at 10:25):

From: "Roger H." <s57076@hotmail.com>
Or rather
1.datatype color = red |blue
fun f:: color => nat setf red = {1}f blue = {2}
how do i prove
lemma "(⋃x. f x) = {1,2}" ?
Thank you.
From: s57076@hotmail.com
To: isabelle-users@cl.cam.ac.uk
Subject: RE: [isabelle] Datatype + cardinality + polymorphismus?
Date: Sat, 27 Jun 2015 19:19:29 +0200

I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Thank you Larry, this is a clear answer for one of my questions.
My other questions were:

  1. Assume I have
    datatype color = red |blue
    fun f:: color => nat setf red = {1}f blue = {2}
    definition M :: "nat set" whereM = the union...over all x in color...of f(x) //the result should be M = {1} union {2} = {1,2}
    I dont know how to write the implementation of M in isabelle syntax.

  2. card (color) = 2 ? or size (color) = 2 ? I am looking for the name of the function that gets a type and returns its number of constructors (for such simple finite non-recursive types)

Thank you!

Subject: Re: [isabelle] Datatype + cardinality + polymorphismus?
From: lp15@cam.ac.uk
Date: Sat, 27 Jun 2015 18:02:46 +0100
CC: isabelle-users@cl.cam.ac.uk
To: s57076@hotmail.com

I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Larry Paulson

On 27 Jun 2015, at 12:22, Larry Paulson <lp15@cam.ac.uk> wrote:

Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website http://isabelle.in.tum.de/documentation.html.

Larry Paulson

On 27 Jun 2015, at 12:06, Roger H. <s57076@hotmail.com> wrote:

Hello,
1. If i have datatype color = red | blue
how do i write smth like
-"is c in color"...meaning "is c an instance of color?"
-"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
-length function..number of elements in the datatype .. so that it returns here length (color) = 2
2. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
f :: color -> ??red |-> {1,2}blue |-> {True}
cause range f = UNIV isnt right.
Many thanks!

view this post on Zulip Email Gateway (Aug 22 2022 at 10:25):

From: Larry Paulson <lp15@cam.ac.uk>
Sorry to repeat myself, but you really do need to read the documentation. Then you will be able to define f within Isabelle itself, and then you might find that Isabelle’s automation will make this example quite easy.

Larry Paulson


Last updated: Mar 28 2024 at 16:17 UTC