summaryrefslogtreecommitdiff
path: root/snapshots/isabelle/lib/lem/Lem_list.thy
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_list.thy')
-rw-r--r--snapshots/isabelle/lib/lem/Lem_list.thy776
1 files changed, 776 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_list.thy b/snapshots/isabelle/lib/lem/Lem_list.thy
new file mode 100644
index 00000000..3bdef057
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_list.thy
@@ -0,0 +1,776 @@
+chapter \<open>Generated by Lem from list.lem.\<close>
+
+theory "Lem_list"
+
+imports
+ Main
+ "Lem_bool"
+ "Lem_maybe"
+ "Lem_basic_classes"
+ "Lem_function"
+ "Lem_tuple"
+ "Lem_num"
+ "Lem"
+
+begin
+
+
+
+(*open import Bool Maybe Basic_classes Function Tuple Num*)
+
+(*open import {coq} `Coq.Lists.List`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+(*open import {hol} `lemTheory` `listTheory` `rich_listTheory` `sortingTheory`*)
+
+(* ========================================================================== *)
+(* Basic list functions *)
+(* ========================================================================== *)
+
+(* The type of lists as well as list literals like [], [1;2], ... are hardcoded.
+ Thus, we can directly dive into derived definitions. *)
+
+
+(* ----------------------- *)
+(* cons *)
+(* ----------------------- *)
+
+(*val :: : forall 'a. 'a -> list 'a -> list 'a*)
+
+
+(* ----------------------- *)
+(* Emptyness check *)
+(* ----------------------- *)
+
+(*val null : forall 'a. list 'a -> bool*)
+(*let null l= match l with [] -> true | _ -> false end*)
+
+(* ----------------------- *)
+(* Length *)
+(* ----------------------- *)
+
+(*val length : forall 'a. list 'a -> nat*)
+(*let rec length l=
+ match l with
+ | [] -> 0
+ | x :: xs -> (Instance_Num_NumAdd_nat.+) (length xs) 1
+ end*)
+
+(* ----------------------- *)
+(* Equality *)
+(* ----------------------- *)
+
+(*val listEqual : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*val listEqualBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+
+fun listEqualBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool " where
+ " listEqualBy eq ([]) ([]) = ( True )"
+|" listEqualBy eq ([]) (_ # _) = ( False )"
+|" listEqualBy eq (_ # _) ([]) = ( False )"
+|" listEqualBy eq (x # xs) (y # ys) = ( (eq x y \<and> listEqualBy eq xs ys))"
+
+
+
+(* ----------------------- *)
+(* compare *)
+(* ----------------------- *)
+
+(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> ordering*)
+(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> ordering*)
+
+fun lexicographicCompareBy :: "('a \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> ordering " where
+ " lexicographicCompareBy cmp ([]) ([]) = ( EQ )"
+|" lexicographicCompareBy cmp ([]) (_ # _) = ( LT )"
+|" lexicographicCompareBy cmp (_ # _) ([]) = ( GT )"
+|" lexicographicCompareBy cmp (x # xs) (y # ys) = ( (
+ (case cmp x y of
+ LT => LT
+ | GT => GT
+ | EQ => lexicographicCompareBy cmp xs ys
+ )
+ ))"
+
+
+(*val lexicographicLess : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+fun lexicographicLessBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow>('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool " where
+ " lexicographicLessBy less1 less_eq1 ([]) ([]) = ( False )"
+|" lexicographicLessBy less1 less_eq1 ([]) (_ # _) = ( True )"
+|" lexicographicLessBy less1 less_eq1 (_ # _) ([]) = ( False )"
+|" lexicographicLessBy less1 less_eq1 (x # xs) (y # ys) = ( ((less1 x y) \<or> ((less_eq1 x y) \<and> (lexicographicLessBy less1 less_eq1 xs ys))))"
+
+
+(*val lexicographicLessEq : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessEqBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+fun lexicographicLessEqBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow>('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool " where
+ " lexicographicLessEqBy less1 less_eq1 ([]) ([]) = ( True )"
+|" lexicographicLessEqBy less1 less_eq1 ([]) (_ # _) = ( True )"
+|" lexicographicLessEqBy less1 less_eq1 (_ # _) ([]) = ( False )"
+|" lexicographicLessEqBy less1 less_eq1 (x # xs) (y # ys) = ( (less1 x y \<or> (less_eq1 x y \<and> lexicographicLessEqBy less1 less_eq1 xs ys)))"
+
+
+
+definition instance_Basic_classes_Ord_list_dict :: " 'a Ord_class \<Rightarrow>('a list)Ord_class " where
+ " instance_Basic_classes_Ord_list_dict dict_Basic_classes_Ord_a = ((|
+
+ compare_method = (lexicographicCompareBy
+ (compare_method dict_Basic_classes_Ord_a)),
+
+ isLess_method = (lexicographicLessBy
+ (isLess_method dict_Basic_classes_Ord_a) (isLessEqual_method dict_Basic_classes_Ord_a)),
+
+ isLessEqual_method = (lexicographicLessEqBy
+ (isLess_method dict_Basic_classes_Ord_a) (isLessEqual_method dict_Basic_classes_Ord_a)),
+
+ isGreater_method = (\<lambda> x y. (lexicographicLessBy
+ (isLess_method dict_Basic_classes_Ord_a) (isLessEqual_method dict_Basic_classes_Ord_a) y x)),
+
+ isGreaterEqual_method = (\<lambda> x y. (lexicographicLessEqBy
+ (isLess_method dict_Basic_classes_Ord_a) (isLessEqual_method dict_Basic_classes_Ord_a) y x))|) )"
+
+
+
+(* ----------------------- *)
+(* Append *)
+(* ----------------------- *)
+
+(*val ++ : forall 'a. list 'a -> list 'a -> list 'a*) (* originally append *)
+(*let rec ++ xs ys= match xs with
+ | [] -> ys
+ | x :: xs' -> x :: (xs' ++ ys)
+ end*)
+
+(* ----------------------- *)
+(* snoc *)
+(* ----------------------- *)
+
+(*val snoc : forall 'a. 'a -> list 'a -> list 'a*)
+(*let snoc e l= l ++ [e]*)
+
+
+(* ----------------------- *)
+(* Reverse *)
+(* ----------------------- *)
+
+(* First lets define the function [reverse_append], which is
+ closely related to reverse. [reverse_append l1 l2] appends the list [l2] to the reverse of [l1].
+ This can be implemented more efficienctly than appending and is
+ used to implement reverse. *)
+
+(*val reverseAppend : forall 'a. list 'a -> list 'a -> list 'a*) (* originally named rev_append *)
+(*let rec reverseAppend l1 l2= match l1 with
+ | [] -> l2
+ | x :: xs -> reverseAppend xs (x :: l2)
+ end*)
+
+(* Reversing a list *)
+(*val reverse : forall 'a. list 'a -> list 'a*) (* originally named rev *)
+(*let reverse l= reverseAppend l []*)
+
+(* ----------------------- *)
+(* Map *)
+(* ----------------------- *)
+
+(*val map_tr : forall 'a 'b. list 'b -> ('a -> 'b) -> list 'a -> list 'b*)
+function (sequential,domintros) map_tr :: " 'b list \<Rightarrow>('a \<Rightarrow> 'b)\<Rightarrow> 'a list \<Rightarrow> 'b list " where
+ " map_tr rev_acc f ([]) = ( List.rev rev_acc )"
+|" map_tr rev_acc f (x # xs) = ( map_tr ((f x) # rev_acc) f xs )"
+by pat_completeness auto
+
+
+(* taken from: https://blogs.janestreet.com/optimizing-list-map/ *)
+(*val count_map : forall 'a 'b. ('a -> 'b) -> list 'a -> nat -> list 'b*)
+function (sequential,domintros) count_map :: "('a \<Rightarrow> 'b)\<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'b list " where
+ " count_map f ([]) ctr = ( [])"
+|" count_map f (hd1 # tl1) ctr = ( f hd1 #
+ (if ctr <( 5000 :: nat) then count_map f tl1 (ctr +( 1 :: nat))
+ else map_tr [] f tl1))"
+by pat_completeness auto
+
+
+(*val map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+(*let map f l= count_map f l 0*)
+
+(* ----------------------- *)
+(* Reverse Map *)
+(* ----------------------- *)
+
+(*val reverseMap : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+
+
+(* ========================================================================== *)
+(* Folding *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* fold left *)
+(* ----------------------- *)
+
+(*val foldl : forall 'a 'b. ('a -> 'b -> 'a) -> 'a -> list 'b -> 'a*) (* originally foldl *)
+
+(*let rec foldl f b l= match l with
+ | [] -> b
+ | x :: xs -> foldl f (f b x) xs
+end*)
+
+
+(* ----------------------- *)
+(* fold right *)
+(* ----------------------- *)
+
+(*val foldr : forall 'a 'b. ('a -> 'b -> 'b) -> 'b -> list 'a -> 'b*) (* originally foldr with different argument order *)
+(*let rec foldr f b l= match l with
+ | [] -> b
+ | x :: xs -> f x (foldr f b xs)
+end*)
+
+
+(* ----------------------- *)
+(* concatenating lists *)
+(* ----------------------- *)
+
+(*val concat : forall 'a. list (list 'a) -> list 'a*) (* before also called flatten *)
+(*let concat= foldr (++) []*)
+
+
+(* -------------------------- *)
+(* concatenating with mapping *)
+(* -------------------------- *)
+
+(*val concatMap : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*)
+
+
+(* ------------------------- *)
+(* universal qualification *)
+(* ------------------------- *)
+
+(*val all : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally for_all *)
+(*let all P l= foldl (fun r e -> P e && r) true l*)
+
+
+
+(* ------------------------- *)
+(* existential qualification *)
+(* ------------------------- *)
+
+(*val any : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally exist *)
+(*let any P l= foldl (fun r e -> P e || r) false l*)
+
+
+(* ------------------------- *)
+(* dest_init *)
+(* ------------------------- *)
+
+(* get the initial part and the last element of the list in a safe way *)
+
+(*val dest_init : forall 'a. list 'a -> maybe (list 'a * 'a)*)
+
+fun dest_init_aux :: " 'a list \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list*'a " where
+ " dest_init_aux rev_init last_elem_seen ([]) = ( (List.rev rev_init, last_elem_seen))"
+|" dest_init_aux rev_init last_elem_seen (x # xs) = ( dest_init_aux (last_elem_seen # rev_init) x xs )"
+
+
+fun dest_init :: " 'a list \<Rightarrow>('a list*'a)option " where
+ " dest_init ([]) = ( None )"
+|" dest_init (x # xs) = ( Some (dest_init_aux [] x xs))"
+
+
+
+(* ========================================================================== *)
+(* Indexing lists *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* index / nth with maybe *)
+(* ------------------------- *)
+
+(*val index : forall 'a. list 'a -> nat -> maybe 'a*)
+
+(*let rec index l n= match l with
+ | [] -> Nothing
+ | x :: xs -> if (Instance_Basic_classes_Eq_nat.=) n 0 then Just x else index xs ((Instance_Num_NumMinus_nat.-)n 1)
+end*)
+
+(* ------------------------- *)
+(* findIndices *)
+(* ------------------------- *)
+
+(* [findIndices P l] returns the indices of all elements of list [l] that satisfy predicate [P].
+ Counting starts with 0, the result list is sorted ascendingly *)
+(*val findIndices : forall 'a. ('a -> bool) -> list 'a -> list nat*)
+
+fun findIndices_aux :: " nat \<Rightarrow>('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow>(nat)list " where
+ " findIndices_aux (i::nat) P ([]) = ( [])"
+|" findIndices_aux (i::nat) P (x # xs) = ( if P x then i # findIndices_aux (i +( 1 :: nat)) P xs else findIndices_aux (i +( 1 :: nat)) P xs )"
+
+(*let findIndices P l= findIndices_aux 0 P l*)
+
+
+
+(* ------------------------- *)
+(* findIndex *)
+(* ------------------------- *)
+
+(* findIndex returns the first index of a list that satisfies a given predicate. *)
+(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> maybe nat*)
+(*let findIndex P l= match findIndices P l with
+ | [] -> Nothing
+ | x :: _ -> Just x
+end*)
+
+(* ------------------------- *)
+(* elemIndices *)
+(* ------------------------- *)
+
+(*val elemIndices : forall 'a. Eq 'a => 'a -> list 'a -> list nat*)
+
+(* ------------------------- *)
+(* elemIndex *)
+(* ------------------------- *)
+
+(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> maybe nat*)
+
+
+(* ========================================================================== *)
+(* Creating lists *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* genlist *)
+(* ------------------------- *)
+
+(* [genlist f n] generates the list [f 0; f 1; ... (f (n-1))] *)
+(*val genlist : forall 'a. (nat -> 'a) -> nat -> list 'a*)
+
+
+(*let rec genlist f n=
+ match n with
+ | 0 -> []
+ | n' + 1 -> snoc (f n') (genlist f n')
+ end*)
+
+
+(* ------------------------- *)
+(* replicate *)
+(* ------------------------- *)
+
+(*val replicate : forall 'a. nat -> 'a -> list 'a*)
+(*let rec replicate n x=
+ match n with
+ | 0 -> []
+ | n' + 1 -> x :: replicate n' x
+ end*)
+
+
+(* ========================================================================== *)
+(* Sublists *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* splitAt *)
+(* ------------------------- *)
+
+(* [splitAt n xs] returns a tuple (xs1, xs2), with append xs1 xs2 = xs and
+ length xs1 = n. If there are not enough elements
+ in [xs], the original list and the empty one are returned. *)
+(*val splitAtAcc : forall 'a. list 'a -> nat -> list 'a -> (list 'a * list 'a)*)
+function (sequential,domintros) splitAtAcc :: " 'a list \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list*'a list " where
+ " splitAtAcc revAcc n l = (
+ (case l of
+ [] => (List.rev revAcc, [])
+ | x # xs => if n \<le>( 0 :: nat) then (List.rev revAcc, l) else splitAtAcc (x # revAcc) (n-( 1 :: nat)) xs
+ ))"
+by pat_completeness auto
+
+
+(*val splitAt : forall 'a. nat -> list 'a -> (list 'a * list 'a)*)
+(*let rec splitAt n l=
+ splitAtAcc [] n l*)
+
+
+(* ------------------------- *)
+(* take *)
+(* ------------------------- *)
+
+(* take n xs returns the prefix of xs of length n, or xs itself if n > length xs *)
+(*val take : forall 'a. nat -> list 'a -> list 'a*)
+(*let take n l= fst (splitAt n l)*)
+
+(* ------------------------- *)
+(* drop *)
+(* ------------------------- *)
+
+(* [drop n xs] drops the first [n] elements of [xs]. It returns the empty list, if [n] > [length xs]. *)
+(*val drop : forall 'a. nat -> list 'a -> list 'a*)
+(*let drop n l= snd (splitAt n l)*)
+
+(* ------------------------------------ *)
+(* splitWhile, takeWhile, and dropWhile *)
+(* ------------------------------------ *)
+
+(*val splitWhile_tr : forall 'a. ('a -> bool) -> list 'a -> list 'a -> (list 'a * list 'a)*)
+fun splitWhile_tr :: "('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list*'a list " where
+ " splitWhile_tr p ([]) acc1 = (
+ (List.rev acc1, []))"
+|" splitWhile_tr p (x # xs) acc1 = (
+ if p x then
+ splitWhile_tr p xs (x # acc1)
+ else
+ (List.rev acc1, (x # xs)))"
+
+
+(*val splitWhile : forall 'a. ('a -> bool) -> list 'a -> (list 'a * list 'a)*)
+definition splitWhile :: "('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list*'a list " where
+ " splitWhile p xs = ( splitWhile_tr p xs [])"
+
+
+(* [takeWhile p xs] takes the first elements of [xs] that satisfy [p]. *)
+(*val takeWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+definition takeWhile :: "('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list " where
+ " takeWhile p l = ( fst (splitWhile p l))"
+
+
+(* [dropWhile p xs] drops the first elements of [xs] that satisfy [p]. *)
+(*val dropWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+definition dropWhile :: "('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list " where
+ " dropWhile p l = ( snd (splitWhile p l))"
+
+
+(* ------------------------- *)
+(* isPrefixOf *)
+(* ------------------------- *)
+
+(*val isPrefixOf : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+fun isPrefixOf :: " 'a list \<Rightarrow> 'a list \<Rightarrow> bool " where
+ " isPrefixOf ([]) _ = ( True )"
+|" isPrefixOf (_ # _) ([]) = ( False )"
+|" isPrefixOf (x # xs) (y # ys) = ( (x = y) \<and> isPrefixOf xs ys )"
+
+
+(* ------------------------- *)
+(* update *)
+(* ------------------------- *)
+(*val update : forall 'a. list 'a -> nat -> 'a -> list 'a*)
+(*let rec update l n e=
+ match l with
+ | [] -> []
+ | x :: xs -> if (Instance_Basic_classes_Eq_nat.=) n 0 then e :: xs else x :: (update xs ((Instance_Num_NumMinus_nat.-) n 1) e)
+end*)
+
+
+
+(* ========================================================================== *)
+(* Searching lists *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* Membership test *)
+(* ------------------------- *)
+
+(* The membership test, one of the basic list functions, is actually tricky for
+ Lem, because it is tricky, which equality to use. From Lem`s point of
+ perspective, we want to use the equality provided by the equality type - class.
+ This allows for example to check whether a set is in a list of sets.
+
+ However, in order to use the equality type class, elem essentially becomes
+ existential quantification over lists. For types, which implement semantic
+ equality (=) with syntactic equality, this is overly complicated. In
+ our theorem prover backend, we would end up with overly complicated, harder
+ to read definitions and some of the automation would be harder to apply.
+ Moreover, nearly all the old Lem generated code would change and require
+ (hopefully minor) adaptions of proofs.
+
+ For now, we ignore this problem and just demand, that all instances of
+ the equality type class do the right thing for the theorem prover backends.
+*)
+
+(*val elem : forall 'a. Eq 'a => 'a -> list 'a -> bool*)
+(*val elemBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> bool*)
+
+definition elemBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool " where
+ " elemBy eq e l = ( ((\<exists> x \<in> (set l). (eq e) x)))"
+
+(*let elem= elemBy (=)*)
+
+(* ------------------------- *)
+(* Find *)
+(* ------------------------- *)
+(*val find : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) (* previously not of maybe type *)
+(*let rec find P l= match l with
+ | [] -> Nothing
+ | x :: xs -> if P x then Just x else find P xs
+end*)
+
+
+(* ----------------------------- *)
+(* Lookup in an associative list *)
+(* ----------------------------- *)
+(*val lookup : forall 'a 'b. Eq 'a => 'a -> list ('a * 'b) -> maybe 'b*)
+(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> maybe 'b*)
+
+(* DPM: eta-expansion for Coq backend type-inference. *)
+definition lookupBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a \<Rightarrow>('a*'b)list \<Rightarrow> 'b option " where
+ " lookupBy eq k m = ( map_option (\<lambda> x . snd x) (List.find ( \<lambda>x .
+ (case x of (k', _) => eq k k' )) m))"
+
+
+(* ------------------------- *)
+(* filter *)
+(* ------------------------- *)
+(*val filter : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+(*let rec filter P l= match l with
+ | [] -> []
+ | x :: xs -> if (P x) then x :: (filter P xs) else filter P xs
+ end*)
+
+
+(* ------------------------- *)
+(* partition *)
+(* ------------------------- *)
+(*val partition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+(*let partition P l= (filter P l, filter (fun x -> not (P x)) l)*)
+
+(*val reversePartition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+definition reversePartition :: "('a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list*'a list " where
+ " reversePartition P l = ( List.partition P (List.rev l))"
+
+
+
+(* ------------------------- *)
+(* delete first element *)
+(* with certain property *)
+(* ------------------------- *)
+
+(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> maybe (list 'a)*)
+(*let rec deleteFirst P l= match l with
+ | [] -> Nothing
+ | x :: xs -> if (P x) then Just xs else Maybe.map (fun xs' -> x :: xs') (deleteFirst P xs)
+ end*)
+
+
+(*val delete : forall 'a. Eq 'a => 'a -> list 'a -> list 'a*)
+(*val deleteBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
+
+definition deleteBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list " where
+ " deleteBy eq x l = ( case_option l id (delete_first (eq x) l))"
+
+
+
+(* ========================================================================== *)
+(* Zipping and unzipping lists *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* zip *)
+(* ------------------------- *)
+
+(* zip takes two lists and returns a list of corresponding pairs. If one input list is short, excess elements of the longer list are discarded. *)
+(*val zip : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) (* before combine *)
+(*let rec zip l1 l2= match (l1, l2) with
+ | (x :: xs, y :: ys) -> (x, y) :: zip xs ys
+ | _ -> []
+end*)
+
+(* ------------------------- *)
+(* unzip *)
+(* ------------------------- *)
+
+(*val unzip: forall 'a 'b. list ('a * 'b) -> (list 'a * list 'b)*)
+(*let rec unzip l= match l with
+ | [] -> ([], [])
+ | (x, y) :: xys -> let (xs, ys) = unzip xys in (x :: xs, y :: ys)
+end*)
+
+(* ------------------------- *)
+(* distinct elements *)
+(* ------------------------- *)
+
+(*val allDistinct : forall 'a. Eq 'a => list 'a -> bool*)
+fun allDistinct :: " 'a list \<Rightarrow> bool " where
+ " allDistinct ([]) = ( True )"
+|" allDistinct (x # l') = ( \<not> (Set.member x (set l')) \<and> allDistinct l' )"
+
+
+(* some more useful functions *)
+(*val mapMaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*)
+function (sequential,domintros) mapMaybe :: "('a \<Rightarrow> 'b option)\<Rightarrow> 'a list \<Rightarrow> 'b list " where
+ " mapMaybe f ([]) = ( [])"
+|" mapMaybe f (x # xs) = (
+ (case f x of
+ None => mapMaybe f xs
+ | Some y => y # (mapMaybe f xs)
+ ))"
+by pat_completeness auto
+
+
+(*val mapi : forall 'a 'b. (nat -> 'a -> 'b) -> list 'a -> list 'b*)
+function (sequential,domintros) mapiAux :: "(nat \<Rightarrow> 'b \<Rightarrow> 'a)\<Rightarrow> nat \<Rightarrow> 'b list \<Rightarrow> 'a list " where
+ " mapiAux f (n :: nat) ([]) = ( [])"
+|" mapiAux f (n :: nat) (x # xs) = ( (f n x) # mapiAux f (n +( 1 :: nat)) xs )"
+by pat_completeness auto
+
+definition mapi :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b)\<Rightarrow> 'a list \<Rightarrow> 'b list " where
+ " mapi f l = ( mapiAux f(( 0 :: nat)) l )"
+
+
+(*val deletes: forall 'a. Eq 'a => list 'a -> list 'a -> list 'a*)
+definition deletes :: " 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list " where
+ " deletes xs ys = (
+ List.foldl ((\<lambda> x y. remove1 y x)) xs ys )"
+
+
+(* ========================================================================== *)
+(* Comments (not clean yet, please ignore the rest of the file) *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* skipped from Haskell Lib*)
+(* -----------------------
+
+intersperse :: a -> [a] -> [a]
+intercalate :: [a] -> [[a]] -> [a]
+transpose :: [[a]] -> [[a]]
+subsequences :: [a] -> [[a]]
+permutations :: [a] -> [[a]]
+foldl` :: (a -> b -> a) -> a -> [b] -> aSource
+foldl1` :: (a -> a -> a) -> [a] -> aSource
+
+and
+or
+sum
+product
+maximum
+minimum
+scanl
+scanr
+scanl1
+scanr1
+Accumulating maps
+
+mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+
+iterate :: (a -> a) -> a -> [a]
+repeat :: a -> [a]
+cycle :: [a] -> [a]
+unfoldr
+
+
+takeWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhileEnd :: (a -> Bool) -> [a] -> [a]Source
+span :: (a -> Bool) -> [a] -> ([a], [a])Source
+break :: (a -> Bool) -> [a] -> ([a], [a])Source
+break p is equivalent to span (not . p).
+stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]Source
+group :: Eq a => [a] -> [[a]]Source
+inits :: [a] -> [[a]]Source
+tails :: [a] -> [[a]]Source
+
+
+isPrefixOf :: Eq a => [a] -> [a] -> BoolSource
+isSuffixOf :: Eq a => [a] -> [a] -> BoolSource
+isInfixOf :: Eq a => [a] -> [a] -> BoolSource
+
+
+
+notElem :: Eq a => a -> [a] -> BoolSource
+
+zip3 :: [a] -> [b] -> [c] -> [(a, b, c)]Source
+zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]Source
+zip5 :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]Source
+zip6 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [(a, b, c, d, e, f)]Source
+zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]Source
+
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]Source
+zipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]Source
+zipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]Source
+zipWith5 :: (a -> b -> c -> d -> e -> f) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f]Source
+zipWith6 :: (a -> b -> c -> d -> e -> f -> g) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]Source
+zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]Source
+
+
+unzip3 :: [(a, b, c)] -> ([a], [b], [c])Source
+unzip4 :: [(a, b, c, d)] -> ([a], [b], [c], [d])Source
+unzip5 :: [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])Source
+unzip6 :: [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])Source
+unzip7 :: [(a, b, c, d, e, f, g)] -> ([a], [b], [c], [d], [e], [f], [g])Source
+
+
+lines :: String -> [String]Source
+words :: String -> [String]Source
+unlines :: [String] -> StringSource
+unwords :: [String] -> StringSource
+nub :: Eq a => [a] -> [a]Source
+delete :: Eq a => a -> [a] -> [a]Source
+
+() :: Eq a => [a] -> [a] -> [a]Source
+union :: Eq a => [a] -> [a] -> [a]Source
+intersect :: Eq a => [a] -> [a] -> [a]Source
+sort :: Ord a => [a] -> [a]Source
+insert :: Ord a => a -> [a] -> [a]Source
+
+
+nubBy :: (a -> a -> Bool) -> [a] -> [a]Source
+deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]Source
+deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+groupBy :: (a -> a -> Bool) -> [a] -> [[a]]Source
+sortBy :: (a -> a -> Ordering) -> [a] -> [a]Source
+insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]Source
+maximumBy :: (a -> a -> Ordering) -> [a] -> aSource
+minimumBy :: (a -> a -> Ordering) -> [a] -> aSource
+genericLength :: Num i => [b] -> iSource
+genericTake :: Integral i => i -> [a] -> [a]Source
+genericDrop :: Integral i => i -> [a] -> [a]Source
+genericSplitAt :: Integral i => i -> [b] -> ([b], [b])Source
+genericIndex :: Integral a => [b] -> a -> bSource
+genericReplicate :: Integral i => i -> a -> [a]Source
+
+
+*)
+
+
+(* ----------------------- *)
+(* skipped from Lem Lib *)
+(* -----------------------
+
+
+val for_all2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val exists2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c
+val rev_map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c
+val fold_left2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'a) -> 'a -> list 'b -> list 'c -> 'a
+val fold_right2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'c) -> list 'a -> list 'b -> 'c -> 'c
+
+
+(* now maybe result and called lookup *)
+val assoc : forall 'a 'b. 'a -> list ('a * 'b) -> 'b
+let inline {ocaml} assoc = Ocaml.List.assoc
+
+
+val mem_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> bool
+val remove_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> list ('a * 'b)
+
+
+
+val stable_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+val fast_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+
+val merge : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a -> list 'a
+val intersect : forall 'a. list 'a -> list 'a -> list 'a
+
+
+*)
+
+(*val catMaybes : forall 'a. list (maybe 'a) -> list 'a*)
+function (sequential,domintros) catMaybes :: "('a option)list \<Rightarrow> 'a list " where
+ " catMaybes ([]) = (
+ [])"
+|" catMaybes (None # xs') = (
+ catMaybes xs' )"
+|" catMaybes (Some x # xs') = (
+ x # catMaybes xs' )"
+by pat_completeness auto
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:00:47 +0000