[isabelle] flat function exists in Isabelle lib? · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] flat function exists in Isabelle lib?

Email Gateway (Aug 19 2022 at 17:28):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear all:
I need a flat function, which can be explained bya small example:
flat [[1,2],[2,3],[5,4]]=[1,2,3,5,4];

Its Intuitive meaning:
flaten a list of list into a list?

Is there such a function flat in Isabelle's library.

I have tried to find, but fail?

Need I define it by myself?

regards!

lyj238@ios.ac.cn

Email Gateway (Aug 19 2022 at 17:28):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear all:
I need a flat function, which can be explained bya small example:
flat [[1,2],[2,3],[5,4]]=[1,2,3,5,4];

Its Intuitive meaning:
flaten a list of list into a list?

Is there such a function flat in Isabelle's library.

I have tried to find, but fail?

Need I define it by myself?

regards!

lyj238@ios.ac.cn

Email Gateway (Aug 19 2022 at 17:29):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
find_consts "'a list list ⇒ 'a list"

found 4 constant(s):
List.product_lists :: "'a list list ⇒ 'a list list"
List.transpose :: "'a list list ⇒ 'a list list"
List.transpose_sumC :: "'a list list ⇒ 'a list list"
List.concat :: "'a list list ⇒ 'a list”

thm concat.simps

concat [] = []
concat (?x # ?xs) = ?x @ concat ?xs

List.concat is the one your want.

Cheers,
Gerwin