# HG changeset patch
# User wenzelm
# Date 1182287738 -7200
# Node ID 8c30dd4b3b220ac76fba80baf83b27054a2ade96
# Parent  c195f6f1376993f2d7a97672f6c91ecb709d9255
BalancedTree;

diff -r c195f6f13769 -r 8c30dd4b3b22 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -77,7 +77,7 @@
     val leafTs' = get_nonrec_types descr' sorts;
     val branchTs = get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
-      else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = get_arities descr' \ 0;
     val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
@@ -85,7 +85,7 @@
     val newTs = Library.take (length (hd descr), recTs);
     val oldTs = Library.drop (length (hd descr), recTs);
     val sumT = if null leafTs then HOLogic.unitT
-      else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
+      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
     val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
     val UnivT = HOLogic.mk_setT Univ_elT;
     val UnivT' = Univ_elT --> HOLogic.boolT;
@@ -115,10 +115,12 @@
 
     (* make injections for constructors *)
 
-    fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then
-        Const ("arbitrary", Univ_elT)
-      else
-        foldr1 (HOLogic.mk_binop Scons_name) ts);
+    fun mk_univ_inj ts = BalancedTree.access
+      {left = fn t => In0 $ t,
+        right = fn t => In1 $ t,
+        init =
+          if ts = [] then Const ("arbitrary", Univ_elT)
+          else foldr1 (HOLogic.mk_binop Scons_name) ts};
 
     (* function spaces *)
 
diff -r c195f6f13769 -r 8c30dd4b3b22 src/HOL/Tools/old_inductive_package.ML
--- a/src/HOL/Tools/old_inductive_package.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/HOL/Tools/old_inductive_package.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -680,7 +680,7 @@
 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
       params paramTs cTs cnames =
   let
-    val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
+    val sumT = BalancedTree.make (fn (T, U) => Type ("+", [T, U])) cTs;
     val setT = HOLogic.mk_setT sumT;
 
     val fp_name = if coind then gfp_name else lfp_name;
diff -r c195f6f13769 -r 8c30dd4b3b22 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/ZF/Datatype.thy	Tue Jun 19 23:15:38 2007 +0200
@@ -65,7 +65,7 @@
 
   fun mk_new ([],[]) = Const("True",FOLogic.oT)
     | mk_new (largs,rargs) =
-        fold_bal FOLogic.mk_conj
+        BalancedTree.make FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
  val datatype_ss = @{simpset};
diff -r c195f6f13769 -r 8c30dd4b3b22 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -78,7 +78,8 @@
   fun mk_tuple [] = Const("0",iT)
     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
 
-  fun mk_inject n k u = access_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, u) n k;
+  fun mk_inject n k u = BalancedTree.access
+    {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
 
   val npart = length rec_names;  (*number of mutually recursive parts*)
 
@@ -106,7 +107,7 @@
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
                             Ind_Syntax.iT
                             free
-    in  fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
+    in  BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
 
   (** Generating function variables for the case definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
@@ -141,7 +142,7 @@
   val case_tm = list_comb (case_const, case_args);
 
   val case_def = Logic.mk_defpair
-           (case_tm, fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
+    (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
   (** Generating function variables for the recursor definition
diff -r c195f6f13769 -r 8c30dd4b3b22 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -114,7 +114,7 @@
         val exfrees = term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     in foldr FOLogic.mk_exists
-             (fold_bal FOLogic.mk_conj (zeq::prems)) exfrees
+             (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
@@ -122,16 +122,16 @@
     | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
 
   (*Access to balanced disjoint sums via injections*)
-  val parts =
-      map mk_Part (accesses_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, Bound 0)
-                                (length rec_tms));
+  val parts = map mk_Part
+    (BalancedTree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
+      (length rec_tms));
 
   (*replace each set by the corresponding Part(A,h)*)
   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
 
   val fp_abs = absfree(X', iT,
                    mk_Collect(z', dom_sum,
-                              fold_bal FOLogic.mk_disj part_intrs));
+                              BalancedTree.make FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
 
@@ -237,10 +237,8 @@
      DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
 
   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
-  val mk_disj_rls =
-      let fun f rl = rl RS disjI1
-          and g rl = rl RS disjI2
-      in  accesses_bal(f, g, asm_rl)  end;
+  val mk_disj_rls = BalancedTree.accesses
+    {left = fn rl => rl RS disjI1, right = fn rl => rl RS disjI2, init = asm_rl};
 
   val intrs =
     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
@@ -398,10 +396,10 @@
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
              Abs("z", Ind_Syntax.iT,
-                 fold_bal FOLogic.mk_conj
+                 BalancedTree.make FOLogic.mk_conj
                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
      and mutual_induct_concl =
-      FOLogic.mk_Trueprop(fold_bal FOLogic.mk_conj qconcls);
+      FOLogic.mk_Trueprop(BalancedTree.make FOLogic.mk_conj qconcls);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln ("induct_concl = " ^
diff -r c195f6f13769 -r 8c30dd4b3b22 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -114,7 +114,7 @@
       fun is_ind arg = (type_of arg = iT)
   in  case List.filter is_ind (args @ cs) of
          []     => empty
-       | u_args => fold_bal mk_Un u_args
+       | u_args => BalancedTree.make mk_Un u_args
   end;
 
 (*univ or quniv constitutes the sum domain for mutual recursion;