src/HOL/Data_Structures/Binomial_Heap.thy
changeset 66550 b8a6f9337229
parent 66549 253880668a43
child 66564 ff561d9cb661
equal deleted inserted replaced
66549:253880668a43 66550:b8a6f9337229
    95 context
    95 context
    96 includes pattern_aliases
    96 includes pattern_aliases
    97 begin
    97 begin
    98 
    98 
    99 fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    99 fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   100   "link (Node r x\<^sub>1 c\<^sub>1 =: t\<^sub>1) (Node _ x\<^sub>2 c\<^sub>2 =: t\<^sub>2) = 
   100   "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) = 
   101     (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2))"
   101     (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))"
   102 
   102 
   103 end
   103 end
   104 
   104 
   105 lemma invar_btree_link:
   105 lemma invar_btree_link:
   106   assumes "invar_btree t\<^sub>1"
   106   assumes "invar_btree t\<^sub>1"