# HG changeset patch
# User nipkow
# Date 1730906385 -3600
# Node ID 8070e4578ecec4ff326b7627145f54805987d36d
# Parent  a1567e05f7fda969895c7069af4c5b804369b4fb
merged Reverse into Time_Funs

diff -r a1567e05f7fd -r 8070e4578ece src/HOL/Data_Structures/Queue_2Lists.thy
--- 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
diff -r a1567e05f7fd -r 8070e4578ece src/HOL/Data_Structures/Reverse.thy
--- 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
diff -r a1567e05f7fd -r 8070e4578ece src/HOL/Data_Structures/Time_Funs.thy
--- 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