From: "Roger H." <s57076@hotmail.com>
Hello,
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
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!
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
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.
- 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)
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".
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. ??
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.
- 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) >
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
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
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).
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:
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.
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.comI 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!
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:
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.
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.comI 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!
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