src/HOL/Data_Structures/Leftist_Heap.thy
 changeset 73875 0c8d6bec6491 parent 72773 8eabaf951e6b
equal inserted replaced
73874:4b413b78cd94 73875:0c8d6bec6491
`    35 definition empty :: "'a lheap" where`
`    35 definition empty :: "'a lheap" where`
`    36 "empty = Leaf"`
`    36 "empty = Leaf"`
`    37 `
`    37 `
`    38 definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where`
`    38 definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where`
`    39 "node l a r =`
`    39 "node l a r =`
`    40  (let rl = mht l; rr = mht r`
`    40  (let mhl = mht l; mhr = mht r`
`    41   in if rl \<ge> rr then Node l (a,rr+1) r else Node r (a,rl+1) l)"`
`    41   in if mhl \<ge> mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)"`
`    42 `
`    42 `
`    43 fun get_min :: "'a lheap \<Rightarrow> 'a" where`
`    43 fun get_min :: "'a lheap \<Rightarrow> 'a" where`
`    44 "get_min(Node l (a, n) r) = a"`
`    44 "get_min(Node l (a, n) r) = a"`
`    45 `
`    45 `
`    46 text \<open>For function \<open>merge\<close>:\<close>`
`    46 text \<open>For function \<open>merge\<close>:\<close>`