src/HOL/Data_Structures/Binomial_Heap.thy
 changeset 73295 2138a4a9031a parent 73182 8b92a2ab5370 child 76184 33177228aa69
equal 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 `