--- a/src/HOL/Data_Structures/Queue_2Lists.thy Tue Nov 05 23:51:44 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy Wed Nov 06 16:19:45 2024 +0100
@@ -5,7 +5,7 @@
theory Queue_2Lists
imports
Queue_Spec
- Reverse
+ Time_Funs
begin
text \<open>Definitions:\<close>
@@ -61,12 +61,8 @@
time_fun norm
time_fun enq
-time_fun tl
time_fun deq
-lemma T_tl_0: "T_tl xs = 0"
-by(cases xs)auto
-
text \<open>Amortized running times:\<close>
fun \<Phi> :: "'a queue \<Rightarrow> nat" where
@@ -76,6 +72,6 @@
by(auto simp: T_itrev)
lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 1"
-by(auto simp: T_itrev T_tl_0)
+by(auto simp: T_itrev T_tl)
end
--- a/src/HOL/Data_Structures/Reverse.thy Tue Nov 05 23:51:44 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-theory Reverse
-imports Define_Time_Function
-begin
-
-time_fun append
-time_fun rev
-
-lemma T_append: "T_append xs ys = length xs + 1"
-by(induction xs) auto
-
-lemma T_rev: "T_rev xs \<le> (length xs + 1)^2"
-by(induction xs) (auto simp: T_append power2_eq_square)
-
-fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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) auto
-
-lemma itrev_Nil: "itrev xs [] = rev xs"
-by(simp add: itrev)
-
-time_fun itrev
-
-lemma T_itrev: "T_itrev xs ys = length xs + 1"
-by(induction xs arbitrary: ys) auto
-
-end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Time_Funs.thy Tue Nov 05 23:51:44 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Nov 06 16:19:45 2024 +0100
@@ -2,7 +2,9 @@
File: Data_Structures/Time_Functions.thy
Author: Manuel Eberl, TU München
*)
-section \<open>Time functions for various standard library operations\<close>
+
+section \<open>Time functions for various standard library operations. Also defines \<open>itrev\<close>.\<close>
+
theory Time_Funs
imports Define_Time_Function
begin
@@ -69,5 +71,32 @@
lemma T_drop_eq: "T_drop n xs = min n (length xs) + 1"
by (induction xs arbitrary: n) (auto split: nat.splits)
-
+
+time_fun rev
+
+lemma T_rev: "T_rev xs \<le> (length xs + 1)^2"
+by(induction xs) (auto simp: T_append power2_eq_square)
+
+fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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) auto
+
+lemma itrev_Nil: "itrev xs [] = rev xs"
+by(simp add: itrev)
+
+time_fun itrev
+
+lemma T_itrev: "T_itrev xs ys = length xs + 1"
+by(induction xs arbitrary: ys) auto
+
+time_fun tl
+
+lemma T_tl: "T_tl xs = 0"
+by (cases xs) simp_all
+
+declare T_tl.simps[simp del]
+
end