src/HOL/Data_Structures/Binomial_Heap.thy
changeset 73295 2138a4a9031a
parent 73182 8b92a2ab5370
equal deleted inserted replaced
73294:c03a148110cc 73295:2138a4a9031a
   481 text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
   481 text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
   482   to keep the following analysis simpler and more to the point.
   482   to keep the following analysis simpler and more to the point.
   483 \<close>
   483 \<close>
   484 fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
   484 fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
   485   "T_ins_tree t [] = 1"
   485   "T_ins_tree t [] = 1"
   486 | "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
   486 | "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = (
   487     (if rank t\<^sub>1 < rank t\<^sub>2 then 1
   487     (if rank t\<^sub>1 < rank t\<^sub>2 then 1
   488      else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
   488      else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)
   489   )"
   489   )"
   490 
   490 
   491 definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
   491 definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
   492 "T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
   492 "T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
   493 
   493