Lem_list_extra.thy

chapter \<open>Generated by Lem from \<open>list_extra.lem\<close>.\<close>

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 \<Rightarrow> 'a \<Rightarrow> 'a)\<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> 'a)\<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'b list \<Rightarrow>('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 \<Rightarrow>('b*'a)option)\<Rightarrow> 'a \<Rightarrow> 'b list "  where 
     " unfoldr f x = (
  (case  f x of
      Some (y, x') =>
        y # unfoldr f x'
    | None =>
        []
  ))" 
by pat_completeness auto


end