# HG changeset patch
# User nipkow
# Date 1708327403 -3600
# Node ID 65223730d7e1a704c81fbb86e667446a911daae5
# Parent  0a152b2f73aebde32a06d9a7247046875506c871
use define_time_fun

diff -r 0a152b2f73ae -r 65223730d7e1 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sun Feb 18 21:35:03 2024 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Mon Feb 19 08:23:23 2024 +0100
@@ -9,6 +9,7 @@
   "HOL-Library.Pattern_Aliases"
   Complex_Main
   Priority_Queue_Specs
+  Define_Time_Function
 begin
 
 text \<open>
@@ -471,21 +472,19 @@
 
 subsubsection \<open>Timing Functions\<close>
 
-text \<open>
-  We define timing functions for each operation, and provide
-  estimations of their complexity.
-\<close>
-definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
-[simp]: "T_link _ _ = 0"
+define_time_fun link
+
+lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0"
+by(cases t\<^sub>1; cases t\<^sub>2, auto)
+
+define_time_fun rank
 
-fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a trees \<Rightarrow> nat" where
-  "T_ins_tree t [] = 1"
-| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = 1 +
-    (if rank t\<^sub>1 < rank t\<^sub>2 then 0
-     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
+lemma T_rank[simp]: "T_rank t = 0"
+by(cases t, auto)
 
-definition T_insert :: "'a::linorder \<Rightarrow> 'a trees \<Rightarrow> nat" where
-"T_insert x ts = T_ins_tree (Node 0 x []) ts"
+define_time_fun ins_tree
+
+define_time_fun insert
 
 lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
 by (induction t ts rule: T_ins_tree.induct) auto
@@ -497,7 +496,7 @@
   shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 1"
 proof -
   have "real (T_insert x ts) \<le> real (length ts) + 1"
-    unfolding T_insert_def using T_ins_tree_simple_bound
+    unfolding T_insert.simps using T_ins_tree_simple_bound
     by (metis of_nat_1 of_nat_add of_nat_mono) 
   also note size_mset_trees[OF \<open>invar ts\<close>]
   finally show ?thesis by simp
@@ -505,20 +504,11 @@
 
 subsubsection \<open>\<open>T_merge\<close>\<close>
 
-context
-includes pattern_aliases
-begin
+define_time_fun merge
 
-fun T_merge :: "'a::linorder trees \<Rightarrow> 'a trees \<Rightarrow> nat" where
-  "T_merge ts\<^sub>1 [] = 1"
-| "T_merge [] ts\<^sub>2 = 1"
-| "T_merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + (
-    if rank t\<^sub>1 < rank t\<^sub>2 then T_merge ts\<^sub>1 h\<^sub>2
-    else if rank t\<^sub>2 < rank t\<^sub>1 then T_merge h\<^sub>1 ts\<^sub>2
-    else T_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2
-  )"
-
-end
+(* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>,
+apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated.
+*)
 
 text \<open>A crucial idea is to estimate the time in correlation with the
   result length, as each carry reduces the length of the result.\<close>
@@ -529,7 +519,7 @@
 
 lemma T_merge_length:
   "T_merge ts\<^sub>1 ts\<^sub>2 + length (merge ts\<^sub>1 ts\<^sub>2) \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
-by (induction ts\<^sub>1 ts\<^sub>2 rule: T_merge.induct)
+by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
    (auto simp: T_ins_tree_length algebra_simps)
 
 text \<open>Finally, we get the desired logarithmic bound\<close>
@@ -557,9 +547,14 @@
 
 subsubsection \<open>\<open>T_get_min\<close>\<close>
 
-fun T_get_min :: "'a::linorder trees \<Rightarrow> nat" where
-  "T_get_min [t] = 1"
-| "T_get_min (t#ts) = 1 + T_get_min ts"
+define_time_fun root
+
+lemma T_root[simp]: "T_root t = 0"
+by(cases t)(simp_all)
+
+define_time_fun min
+
+define_time_fun get_min
 
 lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
 by (induction ts rule: T_get_min.induct) auto
@@ -576,9 +571,10 @@
 
 subsubsection \<open>\<open>T_del_min\<close>\<close>
 
-fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
+define_time_fun get_min_rest
+(*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
   "T_get_min_rest [t] = 1"
-| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"
+| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*)
 
 lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
   by (induction ts rule: T_get_min_rest.induct) auto
@@ -599,9 +595,7 @@
 
 definition "T_rev xs = length xs + 1"
 
-definition T_del_min :: "'a::linorder trees \<Rightarrow> nat" where
-  "T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
-                    \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2)"
+define_time_fun del_min
 
 lemma T_del_min_bound:
   fixes ts
@@ -624,7 +618,7 @@
     by (auto simp: mset_trees_def)
 
   have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
-    unfolding T_del_min_def GM
+    unfolding T_del_min.simps GM
     by simp
   also have "T_get_min_rest ts \<le> log 2 (n+1)" 
     using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp