# Theory Lem_list_extra

theory Lem_list_extra
imports Lem_list Lem_assert_extra
```chapter ‹Generated by Lem from ‹list_extra.lem›.›

theory "Lem_list_extra"

imports
Main
"Lem_bool"
"Lem_maybe"
"Lem_basic_classes"
"Lem_tuple"
"Lem_num"
"Lem_list"
"Lem_assert_extra"

begin

― ‹‹open import Bool Maybe Basic_classes Tuple Num List Assert_extra››

― ‹‹ ------------------------- ››
― ‹‹ head of non-empty list    ››
― ‹‹ ------------------------- ››
― ‹‹val head : forall 'a. list 'a -> 'a››
― ‹‹let head l=  match l with | x::xs -> x | [] -> failwith "List_extra.head of empty list" end››

― ‹‹ ------------------------- ››
― ‹‹ tail of non-empty list    ››
― ‹‹ ------------------------- ››
― ‹‹val tail : forall 'a. list 'a -> list 'a››
― ‹‹let tail l=  match l with | x::xs -> xs | [] -> failwith "List_extra.tail of empty list" end››

― ‹‹ ------------------------- ››
― ‹‹ last                      ››
― ‹‹ ------------------------- ››
― ‹‹val last : forall 'a. list 'a -> 'a››
― ‹‹let rec last l=  match l with | [x] -> x | x1::x2::xs -> last (x2 :: xs) | [] -> failwith "List_extra.last of empty list" end››

― ‹‹ ------------------------- ››
― ‹‹ init                      ››
― ‹‹ ------------------------- ››

― ‹‹ All elements of a non-empty list except the last one. ››
― ‹‹val init : forall 'a. list 'a -> list 'a››
― ‹‹let rec init l=  match l with | [x] -> [] | x1::x2::xs -> x1::(init (x2::xs)) | [] -> failwith "List_extra.init of empty list" end››

― ‹‹ ------------------------- ››
― ‹‹ foldl1 / foldr1           ››
― ‹‹ ------------------------- ››

― ‹‹ folding functions for non-empty lists,
which don`t take the base case ››
― ‹‹val foldl1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a››
fun foldl1  :: "('a ⇒ 'a ⇒ 'a)⇒ 'a list ⇒ 'a "  where
" foldl1 f (x # xs) = ( List.foldl f x xs )"
|" foldl1 f ([]) = ( failwith (''List_extra.foldl1 of empty list''))"

― ‹‹val foldr1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a››
fun foldr1  :: "('a ⇒ 'a ⇒ 'a)⇒ 'a list ⇒ 'a "  where
" foldr1 f (x # xs) = ( List.foldr f xs x )"
|" foldr1 f ([]) = ( failwith (''List_extra.foldr1 of empty list''))"

― ‹‹ ------------------------- ››
― ‹‹ nth element               ››
― ‹‹ ------------------------- ››

― ‹‹ get the nth element of a list ››
― ‹‹val nth : forall 'a. list 'a -> nat -> 'a››
― ‹‹let nth l n=  match index l n with Just e -> e | Nothing -> failwith "List_extra.nth" end››

― ‹‹ ------------------------- ››
― ‹‹ Find_non_pure             ››
― ‹‹ ------------------------- ››
― ‹‹val findNonPure : forall 'a. ('a -> bool) -> list 'a -> 'a››
definition findNonPure  :: "('a ⇒ bool)⇒ 'a list ⇒ 'a "  where
" findNonPure P l = ( (case  (List.find P l) of
Some e      => e
| None     => failwith (''List_extra.findNonPure'')
))"

― ‹‹ ------------------------- ››
― ‹‹ zip same length           ››
― ‹‹ ------------------------- ››

― ‹‹val zipSameLength : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)››
fun  zipSameLength  :: " 'a list ⇒ 'b list ⇒('a*'b)list "  where
" zipSameLength l1 l2 = ( (case  (l1, l2) of
(x # xs, y # ys) => (x, y) # zipSameLength xs ys
| ([], []) => []
| _ => failwith (''List_extra.zipSameLength of different length lists'')

))"

― ‹‹val     unfoldr: forall 'a 'b. ('a -> maybe ('b * 'a)) -> 'a -> list 'b››
function (sequential,domintros)  unfoldr  :: "('a ⇒('b*'a)option)⇒ 'a ⇒ 'b list "  where
" unfoldr f x = (
(case  f x of
Some (y, x') =>
y # unfoldr f x'
| None =>
[]
))"
by pat_completeness auto

end
```