src/HOL/Data_Structures/Leftist_Heap.thy
changeset 70363 6d96ee03b62e
parent 68600 bdd6536bd57c
child 70450 7c2724cefcb8
equal deleted inserted replaced
70362:421727c19b23 70363:6d96ee03b62e
    44 fun get_min :: "'a lheap \<Rightarrow> 'a" where
    44 fun get_min :: "'a lheap \<Rightarrow> 'a" where
    45 "get_min(Node l a n r) = a"
    45 "get_min(Node l a n r) = a"
    46 
    46 
    47 text \<open>For function \<open>merge\<close>:\<close>
    47 text \<open>For function \<open>merge\<close>:\<close>
    48 unbundle pattern_aliases
    48 unbundle pattern_aliases
    49 declare size_prod_measure[measure_function]
       
    50 
    49 
    51 fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    50 fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    52 "merge Leaf t2 = t2" |
    51 "merge Leaf t2 = t2" |
    53 "merge t1 Leaf = t1" |
    52 "merge t1 Leaf = t1" |
    54 "merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
    53 "merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =