author | nipkow |
Tue, 31 May 2022 20:55:51 +0200 | |
changeset 75501 | 426afab39a55 |
parent 73108 | 981a383610df |
child 79495 | 8a2511062609 |
permissions | -rw-r--r-- |
73108
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
File: Data_Structures/Time_Functions.thy |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Manuel Eberl, TU München |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
*) |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
section \<open>Time functions for various standard library operations\<close> |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
theory Time_Funs |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
imports Main |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
begin |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
fun T_length :: "'a list \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
"T_length [] = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
| "T_length (x # xs) = T_length xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
lemma T_length_eq: "T_length xs = length xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
by (induction xs) auto |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
lemmas [simp del] = T_length.simps |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
fun T_map :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
"T_map T_f [] = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
| "T_map T_f (x # xs) = T_f x + T_map T_f xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
lemma T_map_eq: "T_map T_f xs = (\<Sum>x\<leftarrow>xs. T_f x) + length xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
by (induction xs) auto |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
lemmas [simp del] = T_map.simps |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
fun T_filter :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
"T_filter T_p [] = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
| "T_filter T_p (x # xs) = T_p x + T_filter T_p xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
lemma T_filter_eq: "T_filter T_p xs = (\<Sum>x\<leftarrow>xs. T_p x) + length xs + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
by (induction xs) auto |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
lemmas [simp del] = T_filter.simps |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
fun T_nth :: "'a list \<Rightarrow> nat \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
"T_nth [] n = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
| "T_nth (x # xs) n = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_nth xs n' + 1)" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
lemma T_nth_eq: "T_nth xs n = min n (length xs) + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
by (induction xs n rule: T_nth.induct) (auto split: nat.splits) |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
lemmas [simp del] = T_nth.simps |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
fun T_take :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
"T_take n [] = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
| "T_take n (x # xs) = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_take n' xs + 1)" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
lemma T_take_eq: "T_take n xs = min n (length xs) + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
by (induction xs arbitrary: n) (auto split: nat.splits) |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
fun T_drop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
"T_drop n [] = 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
| "T_drop n (x # xs) = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_drop n' xs + 1)" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
lemma T_drop_eq: "T_drop n xs = min n (length xs) + 1" |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
by (induction xs arbitrary: n) (auto split: nat.splits) |
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
|
981a383610df
HOL-Data_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
end |