(* File: Data_Structures/Time_Functions.thy Author: Manuel Eberl, TU München \<open>Time functions for various standard library operations. Also defines \<open>itrev\<close>.\<close> theory Time_Functionsimports Time_Commandsbegin "(@)" lemma T_append: "T_append xs ys = length xs + 1" by (induction xs) autoclass T_size =fixes T_size :: "'a \ nat" instantiation list :: (_) T_sizebegin instance ..end abbreviation T_length :: "'a list \ nat" where "T_length \ T_size" lemma T_length: "T_length xs = length xs + 1" by (induction xs) autolemmas [simp del] = T_size_list.simpslemma T_map_simps [simp,code]:"T_map T_f [] = 1" "T_map T_f (x # xs) = T_f x + T_map T_f xs + 1" by (simp_all add: T_map_def)lemma T_map: "T_map T_f xs = (\x\xs. T_f x) + length xs + 1" by (induction xs) autolemmas [simp del] = T_map_simpslemma T_filter_simps [code]:"T_filter T_P [] = 1" "T_filter T_P (x # xs) = T_P x + T_filter T_P xs + 1" by (simp_all add: T_filter_def)lemma T_filter: "T_filter T_P xs = (\x\xs. T_P x) + length xs + 1" by (induction xs) (auto simp: T_filter_simps)lemma T_nth: "n < length xs \ T_nth xs n = n + 1" by (induction xs n rule: T_nth.induct) (auto split: nat.splits)lemmas [simp del] = T_nth.simpslemma T_take: "T_take n xs = min n (length xs) + 1" by (induction xs arbitrary: n) (auto split: nat.splits)lemma T_drop: "T_drop n xs = min n (length xs) + 1" by (induction xs arbitrary: n) (auto split: nat.splits)lemma T_rev: "T_rev xs \ (length xs + 1)^2" by (induction xs) (auto simp: T_append power2_eq_square)fun itrev :: "'a list \ 'a list \ 'a list" where "itrev [] ys = ys" |"itrev (x#xs) ys = itrev xs (x # ys)" lemma itrev: "itrev xs ys = rev xs @ ys" by (induction xs arbitrary: ys) autolemma itrev_Nil: "itrev xs [] = rev xs" by (simp add: itrev)lemma T_itrev: "T_itrev xs ys = length xs + 1" by (induction xs arbitrary: ys) autolemma T_tl: "T_tl xs = 0" by (cases xs) simp_alldeclare T_tl.simps[simp del]end quality 97%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
