-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathLem_list_extra.thy
executable file
·120 lines (86 loc) · 3.63 KB
/
Lem_list_extra.thy
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
111
112
113
114
115
116
117
118
119
120
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 \<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''))"
declare foldl1.simps [simp del]
(*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''))"
declare foldr1.simps [simp del]
(* ------------------------- *)
(* 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'')
))"
declare zipSameLength.simps [simp del]
(*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