29 structure Nat = |
29 structure Nat = |
30 struct |
30 struct |
31 |
31 |
32 datatype nat = Suc of nat | Zero_nat; |
32 datatype nat = Suc of nat | Zero_nat; |
33 |
33 |
34 fun eq_nat Zero_nat Zero_nat = true |
34 fun eq_nat (Suc a) Zero_nat = false |
|
35 | eq_nat Zero_nat (Suc a) = false |
35 | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat' |
36 | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat' |
36 | eq_nat Zero_nat (Suc a) = false |
37 | eq_nat Zero_nat Zero_nat = true; |
37 | eq_nat (Suc a) Zero_nat = false; |
|
38 |
38 |
39 val eq_nata = {eq = eq_nat} : nat HOL.eq; |
39 val eq_nata = {eq = eq_nat} : nat HOL.eq; |
40 |
40 |
41 fun less_nat m (Suc n) = less_eq_nat m n |
41 fun less_nat m (Suc n) = less_eq_nat m n |
42 | less_nat n Zero_nat = false |
42 | less_nat n Zero_nat = false |
61 |
61 |
62 datatype ('a, 'b) searchtree = |
62 datatype ('a, 'b) searchtree = |
63 Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | |
63 Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | |
64 Leaf of 'a * 'b; |
64 Leaf of 'a * 'b; |
65 |
65 |
66 fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = |
66 fun update (A1_, A2_) (it, entry) (Leaf (key, vala)) = |
67 (if HOL.less_eq |
67 (if HOL.eqop A1_ it key then Leaf (key, entry) |
68 ((Orderings.ord_preorder o Orderings.preorder_order o |
68 else (if HOL.less_eq |
69 Orderings.order_linorder) |
69 ((Orderings.ord_preorder o Orderings.preorder_order o |
70 A2_) |
70 Orderings.order_linorder) |
71 it key |
71 A2_) |
72 then Branch (update (A1_, A2_) (it, entry) t1, key, t2) |
72 it key |
73 else Branch (t1, key, update (A1_, A2_) (it, entry) t2)) |
73 then Branch (Leaf (it, entry), it, Leaf (key, vala)) |
74 | update (A1_, A2_) (it, entry) (Leaf (key, vala)) = |
74 else Branch (Leaf (key, vala), it, Leaf (it, entry)))) |
75 (if HOL.eqop A1_ it key then Leaf (key, entry) |
75 | update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = |
76 else (if HOL.less_eq |
76 (if HOL.less_eq |
77 ((Orderings.ord_preorder o Orderings.preorder_order o |
77 ((Orderings.ord_preorder o Orderings.preorder_order o |
78 Orderings.order_linorder) |
78 Orderings.order_linorder) |
79 A2_) |
79 A2_) |
80 it key |
80 it key |
81 then Branch (Leaf (it, entry), it, Leaf (key, vala)) |
81 then Branch (update (A1_, A2_) (it, entry) t1, key, t2) |
82 else Branch (Leaf (key, vala), it, Leaf (it, entry)))); |
82 else Branch (t1, key, update (A1_, A2_) (it, entry) t2)); |
83 |
83 |
84 val example : (Nat.nat, (Nat.nat list)) searchtree = |
84 val example : (Nat.nat, (Nat.nat list)) searchtree = |
85 update (Nat.eq_nata, Nat.linorder_nat) |
85 update (Nat.eq_nata, Nat.linorder_nat) |
86 (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))), |
86 (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))), |
87 [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)]) |
87 [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)]) |