52 |
52 |
53 datatype ('a, 'b) searchtree = |
53 datatype ('a, 'b) searchtree = |
54 Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | |
54 Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | |
55 Leaf of 'a * 'b; |
55 Leaf of 'a * 'b; |
56 |
56 |
57 fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) = |
57 fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = |
58 (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_) |
58 (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) A2_) |
59 it key |
59 it key |
60 then Branch (update (C1_, C2_) (it, entry) t1, key, t2) |
60 then Branch (update (A1_, A2_) (it, entry) t1, key, t2) |
61 else Branch (t1, key, update (C1_, C2_) (it, entry) t2)) |
61 else Branch (t1, key, update (A1_, A2_) (it, entry) t2)) |
62 | update (C1_, C2_) (it, entry) (Leaf (key, vala)) = |
62 | update (A1_, A2_) (it, entry) (Leaf (key, vala)) = |
63 (if HOL.eqop C1_ it key then Leaf (key, entry) |
63 (if HOL.eqop A1_ it key then Leaf (key, entry) |
64 else (if HOL.less_eq |
64 else (if HOL.less_eq |
65 ((Orderings.ord_order o Orderings.order_linorder) C2_) it |
65 ((Orderings.ord_order o Orderings.order_linorder) A2_) it |
66 key |
66 key |
67 then Branch (Leaf (it, entry), it, Leaf (key, vala)) |
67 then Branch (Leaf (it, entry), it, Leaf (key, vala)) |
68 else Branch (Leaf (key, vala), it, Leaf (it, entry)))); |
68 else Branch (Leaf (key, vala), it, Leaf (it, entry)))); |
69 |
69 |
70 val example : (Nat.nat, (Nat.nat list)) searchtree = |
70 val example : (Nat.nat, (Nat.nat list)) searchtree = |