--- a/src/HOL/Tools/function_package/sum_tools.ML Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/Tools/function_package/sum_tools.ML Wed Sep 13 12:05:50 2006 +0200
@@ -17,6 +17,7 @@
val projr_inr: thm
val mk_tree : typ list -> typ * sum_tree * sum_path list
+ val mk_tree_distinct : typ list -> typ * sum_tree * sum_path list
val mk_proj: sum_tree -> sum_path -> term -> term
val mk_inj: sum_tree -> sum_path -> term -> term
@@ -37,12 +38,9 @@
val projl_inl = thm "FunDef.lproj_inl"
val projr_inr = thm "FunDef.rproj_inr"
-
-
fun mk_sumT LT RT = Type ("+", [LT, RT])
fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
-
datatype sum_tree
= Leaf of typ
| Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
@@ -72,6 +70,23 @@
end
+fun mk_tree_distinct Ts =
+ let
+ fun insert_once T Ts =
+ let
+ val i = find_index_eq T Ts
+ in
+ if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
+ end
+
+ val (idxs, dist_Ts) = fold_map insert_once Ts []
+
+ val (ST, tree, pths) = mk_tree dist_Ts
+ in
+ (ST, tree, map (nth pths) idxs)
+ end
+
+
fun mk_inj (Leaf _) [] t = t
| mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t =
Const (inlN, LT --> ST) $ mk_inj tr pth t