blob: 123d8a78724619e01ab11be980ea8a582e6397e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
(*Generated by Lem from list_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_maybeTheory lem_basic_classesTheory lem_tupleTheory lem_numTheory lem_listTheory lem_assert_extraTheory;
val _ = numLib.prefer_num();
val _ = new_theory "lem_list_extra"
(*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*)
val _ = Define `
((foldl1:('a -> 'a -> 'a) -> 'a list -> 'a) f (x :: xs)= (FOLDL f x xs))
/\ ((foldl1:('a -> 'a -> 'a) -> 'a list -> 'a) f ([])= (failwith "List_extra.foldl1 of empty list"))`;
(*val foldr1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*)
val _ = Define `
((foldr1:('a -> 'a -> 'a) -> 'a list -> 'a) f (x :: xs)= (FOLDR f x xs))
/\ ((foldr1:('a -> 'a -> 'a) -> 'a list -> 'a) 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*)
val _ = Define `
((findNonPure:('a -> bool) -> 'a list -> 'a) P l= ((case (list_find_opt 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)*)
(*let rec zipSameLength l1 l2= match (l1, l2) with
| (x :: xs, y :: ys) -> (x, y) :: zipSameLength xs ys
| ([], []) -> []
| _ -> failwith "List_extra.zipSameLength of different length lists"
end*)
(*val unfoldr: forall 'a 'b. ('a -> maybe ('b * 'a)) -> 'a -> list 'b*)
val unfoldr_defn = Hol_defn "unfoldr" `
((unfoldr:('a ->('b#'a)option) -> 'a -> 'b list) f x=
((case f x of
SOME (y, x') =>
y :: unfoldr f x'
| NONE =>
[]
)))`;
val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn unfoldr_defn;
val _ = export_theory()
|
