# HG changeset patch # User nipkow # Date 1711554503 -3600 # Node ID a594d22e69d6d6ef63a58d7e2fcbed7635ff28e7 # Parent c2cca97a57978a6b9579cc2070984cbb62ba34db updated time functions for Array_Braun diff -r c2cca97a5797 -r a594d22e69d6 src/HOL/Data_Structures/Array_Braun.thy --- a/src/HOL/Data_Structures/Array_Braun.thy Mon Mar 25 17:55:02 2024 +0100 +++ b/src/HOL/Data_Structures/Array_Braun.thy Wed Mar 27 16:48:23 2024 +0100 @@ -3,9 +3,10 @@ section "Arrays via Braun Trees" theory Array_Braun - imports - Array_Specs - Braun_Tree +imports + Time_Funs + Array_Specs + Braun_Tree begin subsection "Array" @@ -443,13 +444,6 @@ definition brauns1 :: "'a list \ 'a tree" where "brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)" -fun T_brauns :: "nat \ 'a list \ nat" where - "T_brauns k xs = (if xs = [] then 0 else - let ys = take (2^k) xs; - zs = drop (2^k) xs; - ts = brauns (k+1) zs - in 4 * min (2^k) (length xs) + T_brauns (k+1) zs)" - paragraph "Functional correctness" @@ -497,8 +491,28 @@ paragraph "Running Time Analysis" -theorem T_brauns: - "T_brauns k xs = 4 * length xs" +time_fun_0 "(^)" + +time_fun nodes + +lemma T_nodes: "T_nodes ls xs rs = length xs + 1" +by(induction ls xs rs rule: T_nodes.induct) auto + +time_fun brauns + +lemma T_brauns_pretty: "T_brauns k xs = (if xs = [] then 0 else + let ys = take (2^k) xs; + zs = drop (2^k) xs; + ts = brauns (k+1) zs + in T_take (2 ^ k) xs + T_drop (2 ^ k) xs + T_brauns (k + 1) zs + T_drop (2 ^ k) ts + T_nodes ts ys (drop (2 ^ k) ts)) + 1" +by(simp) + +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) + +theorem T_brauns_ub: + "T_brauns k xs \ 9 * (length xs + 1)" proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length]) case (less xs) show ?case @@ -507,15 +521,28 @@ thus ?thesis by(simp) next assume "xs \ []" - let ?zs = "drop (2^k) xs" - have "T_brauns k xs = T_brauns (k+1) ?zs + 4 * min (2^k) (length xs)" - using \xs \ []\ by(simp) - also have "\ = 4 * length ?zs + 4 * min (2^k) (length xs)" + let ?n = "length xs" let ?zs = "drop (2^k) xs" + have *: "?n - 2^k + 1 \ ?n" + using \xs \ []\ less_eq_Suc_le by fastforce + have "T_brauns k xs = + 3 * (min (2^k) ?n + 1) + (min (2^k) (?n - 2^k) + 1) + T_brauns (k+1) ?zs + 1" + unfolding T_brauns_simple[of k xs] using \xs \ []\ by(simp del: T_brauns.simps) + also have "\ \ 4 * min (2^k) ?n + T_brauns (k+1) ?zs + 5" + by(simp add: min_def) + also have "\ \ 4 * min (2^k) ?n + 9 * (length ?zs + 1) + 5" using less[of ?zs "k+1"] \xs \ []\ - by (simp) - also have "\ = 4 * length xs" + by (simp del: T_brauns.simps) + also have "\ = 4 * min (2^k) ?n + 9 * (?n - 2^k + 1) + 5" + by(simp) + also have "\ = 4 * min (2^k) ?n + 4 * (?n - 2^k) + 5 * (?n - 2^k + 1) + 9" by(simp) - finally show ?case . + also have "\ = 4 * ?n + 5 * (?n - 2^k + 1) + 9" + by(simp) + also have "\ \ 4 * ?n + 5 * ?n + 9" + using * by(simp) + also have "\ = 9 * (?n + 1)" + by (simp add: Suc_leI) + finally show ?thesis . qed qed @@ -551,17 +578,53 @@ definition list_fast :: "'a tree \ 'a list" where "list_fast t = list_fast_rec [t]" -function T_list_fast_rec :: "'a tree list \ nat" where +(* TODO: map and filter are a problem! +- The automatically generated T_map is slightly more complicated than needed. +- We cannot use the manually defined T_map directly because the automatic translation + assumes that T_map has a more complicated type and generates a "wrong" call. +Therefore we hide map/filter at the moment. +*) + +definition "filter_not_Leaf = filter (\t. t \ Leaf)" + +definition "map_left = map left" +definition "map_right = map right" +definition "map_value = map value" + +definition "T_filter_not_Leaf ts = length ts + 1" +definition "T_map_left ts = length ts + 1" +definition "T_map_right ts = length ts + 1" +definition "T_map_value ts = length ts + 1" +(* +time_fun "tree.value" +time_fun "left" +time_fun "right" +*) + +lemmas defs = filter_not_Leaf_def map_left_def map_right_def map_value_def + T_filter_not_Leaf_def T_map_value_def T_map_left_def T_map_right_def + +(* A variant w/o explicit map/filter; T_list_fast_rec is generated from it *) +lemma list_fast_rec_simp: +"list_fast_rec ts = (let us = filter_not_Leaf ts in + if us = [] then [] else + map_value us @ list_fast_rec (map_left us @ map_right us))" +unfolding defs list_fast_rec.simps[of ts] by(rule refl) + +time_function list_fast_rec equations list_fast_rec_simp +termination + by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term defs) + +lemma T_list_fast_rec_pretty: "T_list_fast_rec ts = (let us = filter (\t. t \ Leaf) ts - in length ts + (if us = [] then 0 else - 5 * length us + T_list_fast_rec (map left us @ map right us)))" - by (pat_completeness, auto) - -termination - by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term) + in length ts + 1 + (if us = [] then 0 else + 5 * (length us + 1) + T_list_fast_rec (map left us @ map right us))) + 1" +unfolding defs T_list_fast_rec.simps[of ts] +by(simp add: T_append) declare T_list_fast_rec.simps[simp del] + paragraph "Functional Correctness" lemma list_fast_rec_all_Leaf: @@ -624,6 +687,7 @@ "braun t \ list_fast t = list t" by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0]) + paragraph "Running Time Analysis" lemma sum_tree_list_children: "\t \ set ts. t \ Leaf \ @@ -631,7 +695,7 @@ by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps) theorem T_list_fast_rec_ub: - "T_list_fast_rec ts \ sum_list (map (\t. 7*size t + 1) ts)" + "T_list_fast_rec ts \ sum_list (map (\t. 14*size t + 1) ts) + 2" proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"]) case (less ts) let ?us = "filter (\t. t \ Leaf) ts" @@ -639,22 +703,26 @@ proof cases assume "?us = []" thus ?thesis using T_list_fast_rec.simps[of ts] - by(simp add: sum_list_Suc) + by(simp add: defs sum_list_Suc) next assume "?us \ []" let ?children = "map left ?us @ map right ?us" - have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts" - using \?us \ []\ T_list_fast_rec.simps[of ts] by(simp) - also have "\ \ (\t\?children. 7 * size t + 1) + 5 * length ?us + length ts" + have 1: "1 \ length ?us" + using \?us \ []\ linorder_not_less by auto + have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts + 7" + using \?us \ []\ T_list_fast_rec.simps[of ts] by(simp add: defs T_append) + also have "\ \ (\t\?children. 14 * size t + 1) + 5 * length ?us + length ts + 9" using less[of "?children"] list_fast_rec_term[of "?us"] \?us \ []\ by (simp) - also have "\ = (\t\?children. 7*size t) + 7 * length ?us + length ts" + also have "\ = (\t\?children. 14 * size t) + 7 * length ?us + length ts + 9" by(simp add: sum_list_Suc o_def) - also have "\ = (\t\?us. 7*size t) + length ts" + also have "\ \ (\t\?children. 14 * size t) + 14 * length ?us + length ts + 2" + using 1 by(simp add: sum_list_Suc o_def) + also have "\ = (\t\?us. 14 * size t) + length ts + 2" by(simp add: sum_tree_list_children) - also have "\ \ (\t\ts. 7*size t) + length ts" + also have "\ \ (\t\ts. 14 * size t) + length ts + 2" by(simp add: sum_list_filter_le_nat) - also have "\ = (\t\ts. 7 * size t + 1)" + also have "\ = (\t\ts. 14 * size t + 1) + 2" by(simp add: sum_list_Suc) finally show ?case . qed diff -r c2cca97a5797 -r a594d22e69d6 src/HOL/Data_Structures/Define_Time_Function.ML --- a/src/HOL/Data_Structures/Define_Time_Function.ML Mon Mar 25 17:55:02 2024 +0100 +++ b/src/HOL/Data_Structures/Define_Time_Function.ML Wed Mar 27 16:48:23 2024 +0100 @@ -353,7 +353,9 @@ (* The converter for timing functions given to the walker *) val converter : term option converter = { - constc = fn _ => fn _ => fn _ => fn _ => NONE, + constc = fn _ => fn _ => fn _ => fn t => + (case t of Const ("HOL.undefined", _) => SOME (Const ("HOL.undefined", @{typ "nat"})) + | _ => NONE), funcc = funcc, ifc = ifc, casec = casec, diff -r c2cca97a5797 -r a594d22e69d6 src/HOL/Data_Structures/Time_Funs.thy --- a/src/HOL/Data_Structures/Time_Funs.thy Mon Mar 25 17:55:02 2024 +0100 +++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Mar 27 16:48:23 2024 +0100 @@ -7,6 +7,11 @@ imports Define_Time_Function begin +time_fun "(@)" + +lemma T_append: "T_append xs ys = length xs + 1" +by(induction xs) auto + text \Automatic definition of \T_length\ is cumbersome because of the type class for \size\.\ fun T_length :: "'a list \ nat" where