src/HOL/Data_Structures/Binomial_Heap.thy
 changeset 66550 b8a6f9337229 parent 66549 253880668a43 child 66564 ff561d9cb661
equal 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"`