Theory Lem_list_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