# HG changeset patch # User nipkow # Date 1730913039 -3600 # Node ID 21a493abde0f92350687408e4fa562b8e15151a6 # Parent 9c47740e974a47d8b1f286aaea7730ba5a7e5758 uniform name T_f for closed-form lemmas for function T_f diff -r 9c47740e974a -r 21a493abde0f src/HOL/Data_Structures/Array_Braun.thy --- a/src/HOL/Data_Structures/Array_Braun.thy Wed Nov 06 16:27:06 2024 +0100 +++ b/src/HOL/Data_Structures/Array_Braun.thy Wed Nov 06 18:10:39 2024 +0100 @@ -509,7 +509,7 @@ lemma T_brauns_simple: "T_brauns k xs = (if xs = [] then 0 else 3 * (min (2^k) (length xs) + 1) + (min (2^k) (length xs - 2^k) + 1) + T_brauns (k+1) (drop (2^k) xs)) + 1" -by(simp add: T_nodes T_take_eq T_drop_eq length_brauns min_def) +by(simp add: T_nodes T_take T_drop length_brauns min_def) theorem T_brauns_ub: "T_brauns k xs \ 9 * (length xs + 1)" diff -r 9c47740e974a -r 21a493abde0f src/HOL/Data_Structures/Selection.thy --- a/src/HOL/Data_Structures/Selection.thy Wed Nov 06 16:27:06 2024 +0100 +++ b/src/HOL/Data_Structures/Selection.thy Wed Nov 06 18:10:39 2024 +0100 @@ -639,7 +639,7 @@ time_fun partition3 equations partition3_code -lemma T_partition3_eq: "T_partition3 x xs = length xs + 1" +lemma T_partition3: "T_partition3 x xs = length xs + 1" by (induction x xs rule: T_partition3.induct) auto @@ -658,7 +658,7 @@ also have "T_insort xs \ (length xs + 1) ^ 2" by (rule T_insort_length) also have "T_nth (Sorting.insort xs) k = k + 1" - using assms by (subst T_nth_eq) (auto simp: length_insort) + using assms by (subst T_nth) (auto simp: length_insort) also have "k + 1 \ length xs" using assms by linarith also have "(length xs + 1) ^ 2 + length xs = length xs ^ 2 + 3 * length xs + 1" @@ -671,7 +671,7 @@ shows "T_slow_median xs \ length xs ^ 2 + 4 * length xs + 2" proof - have "T_slow_median xs = length xs + T_slow_select ((length xs - 1) div 2) xs + 1" - by (simp add: T_length_eq) + by (simp add: T_length) also from assms have "length xs > 0" by simp hence "(length xs - 1) div 2 < length xs" @@ -699,7 +699,7 @@ by (cases n; cases xs) (auto simp: T_chop.simps) lemma T_chop_le: "T_chop d xs \ 5 * length xs + 1" - by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take_eq T_drop_eq) + by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take T_drop) time_fun mom_select @@ -787,7 +787,7 @@ case True \ \base case\ hence "T_mom_select k xs \ (length xs)\<^sup>2 + 4 * length xs + 3" using T_slow_select_le[of k xs] \k < length xs\ - by (subst T_mom_select_simps(1)) (auto simp: T_length_eq) + by (subst T_mom_select_simps(1)) (auto simp: T_length) also have "\ \ 20\<^sup>2 + 4 * 20 + 3" using True by (intro add_mono power_mono) auto also have "\ = 483" @@ -812,7 +812,7 @@ have "T_ms \ 10 * n + 48" proof - have "T_ms = (\ys\chop 5 xs. T_slow_median ys) + length (chop 5 xs) + 1" - by (simp add: T_ms_def T_map_eq) + by (simp add: T_ms_def T_map) also have "(\ys\chop 5 xs. T_slow_median ys) \ (\ys\chop 5 xs. 47)" proof (intro sum_list_mono) fix ys assume "ys \ set (chop 5 xs)" @@ -902,8 +902,8 @@ unfold Let_def n_def [symmetric] x_def [symmetric] nl_def [symmetric] ne_def [symmetric] prod.case tw [symmetric]) simp_all also have "\ \ T_rec2 + T_rec1 + T_ms + 2 * n + nl + ne + T_chop 5 xs + 5" using False - by (auto simp add: T_rec1_def T_rec2_def T_partition3_eq - T_length_eq T_ms_def nl_def ne_def) + by (auto simp add: T_rec1_def T_rec2_def T_partition3 + T_length T_ms_def nl_def ne_def) also have "nl \ n" by (simp add: nl_def ls_def) also have "ne \ n" by (simp add: ne_def es_def) also note \T_ms \ 10 * n + 48\ diff -r 9c47740e974a -r 21a493abde0f src/HOL/Data_Structures/Time_Funs.thy --- a/src/HOL/Data_Structures/Time_Funs.thy Wed Nov 06 16:27:06 2024 +0100 +++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Nov 06 18:10:39 2024 +0100 @@ -29,7 +29,7 @@ abbreviation T_length :: "'a list \ nat" where "T_length \ T_size" -lemma T_length_eq: "T_length xs = length xs + 1" +lemma T_length: "T_length xs = length xs + 1" by (induction xs) auto lemmas [simp del] = T_size_list.simps @@ -41,7 +41,7 @@ "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_eq: "T_map T_f xs = (\x\xs. T_f x) + length xs + 1" +lemma T_map: "T_map T_f xs = (\x\xs. T_f x) + length xs + 1" by (induction xs) auto lemmas [simp del] = T_map_simps @@ -53,12 +53,12 @@ "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_eq: "T_filter T_P xs = (\x\xs. T_P x) + length xs + 1" +lemma T_filter: "T_filter T_P xs = (\x\xs. T_P x) + length xs + 1" by (induction xs) (auto simp: T_filter_simps) time_fun nth -lemma T_nth_eq: "n < length xs \ T_nth xs n = n + 1" +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.simps @@ -66,10 +66,10 @@ time_fun take time_fun drop -lemma T_take_eq: "T_take n xs = min n (length xs) + 1" +lemma T_take: "T_take n xs = min n (length xs) + 1" by (induction xs arbitrary: n) (auto split: nat.splits) -lemma T_drop_eq: "T_drop n xs = min n (length xs) + 1" +lemma T_drop: "T_drop n xs = min n (length xs) + 1" by (induction xs arbitrary: n) (auto split: nat.splits) time_fun rev