modernized Balanced_Tree;
authorwenzelm
Tue Sep 29 22:48:24 2009 +0200 (2009-09-29)
changeset 327653032c0308019
parent 32764 690f9cccf232
child 32766 87491cac8b83
modernized Balanced_Tree;
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/record.ML
src/Pure/General/balanced_tree.ML
src/Pure/axclass.ML
src/Pure/conjunction.ML
src/Pure/logic.ML
src/ZF/Datatype_ZF.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4      val leafTs' = get_nonrec_types descr' sorts;
     1.5      val branchTs = get_branching_types descr' sorts;
     1.6      val branchT = if null branchTs then HOLogic.unitT
     1.7 -      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     1.8 +      else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     1.9      val arities = get_arities descr' \ 0;
    1.10      val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    1.11      val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    1.12 @@ -86,7 +86,7 @@
    1.13      val newTs = Library.take (length (hd descr), recTs);
    1.14      val oldTs = Library.drop (length (hd descr), recTs);
    1.15      val sumT = if null leafTs then HOLogic.unitT
    1.16 -      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    1.17 +      else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    1.18      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    1.19      val UnivT = HOLogic.mk_setT Univ_elT;
    1.20      val UnivT' = Univ_elT --> HOLogic.boolT;
    1.21 @@ -116,7 +116,7 @@
    1.22  
    1.23      (* make injections for constructors *)
    1.24  
    1.25 -    fun mk_univ_inj ts = BalancedTree.access
    1.26 +    fun mk_univ_inj ts = Balanced_Tree.access
    1.27        {left = fn t => In0 $ t,
    1.28          right = fn t => In1 $ t,
    1.29          init =
     2.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:33:27 2009 +0200
     2.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:48:24 2009 +0200
     2.3 @@ -120,7 +120,7 @@
     2.4        fun PT_of (SchemeBranch { xs, ...}) =
     2.5              foldr1 HOLogic.mk_prodT (map snd xs)
     2.6  
     2.7 -      val ST = BalancedTree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
     2.8 +      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
     2.9      in
    2.10        IndScheme {T=ST, cases=map mk_case cases', branches=branches }
    2.11      end
     3.1 --- a/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:33:27 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Sep 29 22:48:24 2009 +0200
     3.3 @@ -103,8 +103,8 @@
     3.4          val dresultTs = distinct (op =) resultTs
     3.5          val n' = length dresultTs
     3.6  
     3.7 -        val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
     3.8 -        val ST = BalancedTree.make (uncurry SumTree.mk_sumT) argTs
     3.9 +        val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
    3.10 +        val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
    3.11  
    3.12          val fsum_type = ST --> RST
    3.13  
     4.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Tue Sep 29 22:33:27 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Tue Sep 29 22:48:24 2009 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  
     4.5  (* top-down access in balanced tree *)
     4.6  fun access_top_down {left, right, init} len i =
     4.7 -    BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
     4.8 +    Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
     4.9  
    4.10  (* Sum types *)
    4.11  fun mk_sumT LT RT = Type ("+", [LT, RT])
    4.12 @@ -36,7 +36,7 @@
    4.13      |> snd
    4.14  
    4.15  fun mk_sumcases T fs =
    4.16 -      BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
    4.17 +      Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
    4.18                          (map (fn f => (f, domain_type (fastype_of f))) fs)
    4.19        |> fst
    4.20  
     5.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 22:33:27 2009 +0200
     5.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 22:48:24 2009 +0200
     5.3 @@ -1732,7 +1732,7 @@
     5.4  
     5.5      (*before doing anything else, create the tree of new types
     5.6        that will back the record extension*)
     5.7 -    (* FIXME cf. BalancedTree.make *)
     5.8 +    (* FIXME cf. Balanced_Tree.make *)
     5.9      fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
    5.10        | mktreeT [T] = T
    5.11        | mktreeT xs =
    5.12 @@ -1745,7 +1745,7 @@
    5.13              HOLogic.mk_prodT (mktreeT left, mktreeT right)
    5.14            end;
    5.15  
    5.16 -    (* FIXME cf. BalancedTree.make *)
    5.17 +    (* FIXME cf. Balanced_Tree.make *)
    5.18      fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
    5.19        | mktreeV [T] = T
    5.20        | mktreeV xs =
     6.1 --- a/src/Pure/General/balanced_tree.ML	Tue Sep 29 22:33:27 2009 +0200
     6.2 +++ b/src/Pure/General/balanced_tree.ML	Tue Sep 29 22:48:24 2009 +0200
     6.3 @@ -12,7 +12,7 @@
     6.4    val accesses: {left: 'a -> 'a, right: 'a -> 'a, init: 'a} -> int -> 'a list
     6.5  end;
     6.6  
     6.7 -structure BalancedTree: BALANCED_TREE =
     6.8 +structure Balanced_Tree: BALANCED_TREE =
     6.9  struct
    6.10  
    6.11  fun make _ [] = raise Empty
     7.1 --- a/src/Pure/axclass.ML	Tue Sep 29 22:33:27 2009 +0200
     7.2 +++ b/src/Pure/axclass.ML	Tue Sep 29 22:48:24 2009 +0200
     7.3 @@ -419,7 +419,7 @@
     7.4        if n = 0 then []
     7.5        else
     7.6          (eq RS Drule.equal_elim_rule1)
     7.7 -        |> BalancedTree.dest (fn th =>
     7.8 +        |> Balanced_Tree.dest (fn th =>
     7.9            (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
    7.10    in (intro, dests) end;
    7.11  
     8.1 --- a/src/Pure/conjunction.ML	Tue Sep 29 22:33:27 2009 +0200
     8.2 +++ b/src/Pure/conjunction.ML	Tue Sep 29 22:48:24 2009 +0200
     8.3 @@ -38,7 +38,7 @@
     8.4  fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
     8.5  
     8.6  fun mk_conjunction_balanced [] = true_prop
     8.7 -  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
     8.8 +  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
     8.9  
    8.10  fun dest_conjunction ct =
    8.11    (case Thm.term_of ct of
    8.12 @@ -117,10 +117,10 @@
    8.13  (* balanced conjuncts *)
    8.14  
    8.15  fun intr_balanced [] = asm_rl
    8.16 -  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
    8.17 +  | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
    8.18  
    8.19  fun elim_balanced 0 _ = []
    8.20 -  | elim_balanced n th = BalancedTree.dest elim n th;
    8.21 +  | elim_balanced n th = Balanced_Tree.dest elim n th;
    8.22  
    8.23  
    8.24  (* currying *)
     9.1 --- a/src/Pure/logic.ML	Tue Sep 29 22:33:27 2009 +0200
     9.2 +++ b/src/Pure/logic.ML	Tue Sep 29 22:48:24 2009 +0200
     9.3 @@ -169,7 +169,7 @@
     9.4  
     9.5  (*(A &&& B) &&& (C &&& D) -- balanced*)
     9.6  fun mk_conjunction_balanced [] = true_prop
     9.7 -  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
     9.8 +  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
     9.9  
    9.10  
    9.11  (*A &&& B*)
    9.12 @@ -184,7 +184,7 @@
    9.13  
    9.14  (*(A &&& B) &&& (C &&& D) -- balanced*)
    9.15  fun dest_conjunction_balanced 0 _ = []
    9.16 -  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
    9.17 +  | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
    9.18  
    9.19  (*((A &&& B) &&& C) &&& D &&& E -- flat*)
    9.20  fun dest_conjunctions t =
    10.1 --- a/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:33:27 2009 +0200
    10.2 +++ b/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:48:24 2009 +0200
    10.3 @@ -63,7 +63,7 @@
    10.4  
    10.5    fun mk_new ([],[]) = Const("True",FOLogic.oT)
    10.6      | mk_new (largs,rargs) =
    10.7 -        BalancedTree.make FOLogic.mk_conj
    10.8 +        Balanced_Tree.make FOLogic.mk_conj
    10.9                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
   10.10  
   10.11   val datatype_ss = @{simpset};
    11.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:33:27 2009 +0200
    11.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 29 22:48:24 2009 +0200
    11.3 @@ -94,7 +94,7 @@
    11.4    fun mk_tuple [] = @{const "0"}
    11.5      | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
    11.6  
    11.7 -  fun mk_inject n k u = BalancedTree.access
    11.8 +  fun mk_inject n k u = Balanced_Tree.access
    11.9      {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
   11.10  
   11.11    val npart = length rec_names;  (*number of mutually recursive parts*)
   11.12 @@ -123,7 +123,7 @@
   11.13                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
   11.14                              @{typ i}
   11.15                              free
   11.16 -    in  BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
   11.17 +    in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
   11.18  
   11.19    (** Generating function variables for the case definition
   11.20        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   11.21 @@ -158,7 +158,7 @@
   11.22    val case_tm = list_comb (case_const, case_args);
   11.23  
   11.24    val case_def = PrimitiveDefs.mk_defpair
   11.25 -    (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
   11.26 +    (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
   11.27  
   11.28  
   11.29    (** Generating function variables for the recursor definition
    12.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:33:27 2009 +0200
    12.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 29 22:48:24 2009 +0200
    12.3 @@ -113,7 +113,7 @@
    12.4          val exfrees = OldTerm.term_frees intr \\ rec_params
    12.5          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
    12.6      in List.foldr FOLogic.mk_exists
    12.7 -             (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
    12.8 +             (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
    12.9      end;
   12.10  
   12.11    (*The Part(A,h) terms -- compose injections to make h*)
   12.12 @@ -122,7 +122,7 @@
   12.13  
   12.14    (*Access to balanced disjoint sums via injections*)
   12.15    val parts = map mk_Part
   12.16 -    (BalancedTree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
   12.17 +    (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
   12.18        (length rec_tms));
   12.19  
   12.20    (*replace each set by the corresponding Part(A,h)*)
   12.21 @@ -130,7 +130,7 @@
   12.22  
   12.23    val fp_abs = absfree(X', iT,
   12.24                     mk_Collect(z', dom_sum,
   12.25 -                              BalancedTree.make FOLogic.mk_disj part_intrs));
   12.26 +                              Balanced_Tree.make FOLogic.mk_disj part_intrs));
   12.27  
   12.28    val fp_rhs = Fp.oper $ dom_sum $ fp_abs
   12.29  
   12.30 @@ -238,7 +238,7 @@
   12.31       DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   12.32  
   12.33    (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   12.34 -  val mk_disj_rls = BalancedTree.accesses
   12.35 +  val mk_disj_rls = Balanced_Tree.accesses
   12.36      {left = fn rl => rl RS @{thm disjI1},
   12.37       right = fn rl => rl RS @{thm disjI2},
   12.38       init = @{thm asm_rl}};
   12.39 @@ -398,10 +398,10 @@
   12.40             (Ind_Syntax.mk_all_imp
   12.41              (big_rec_tm,
   12.42               Abs("z", Ind_Syntax.iT,
   12.43 -                 BalancedTree.make FOLogic.mk_conj
   12.44 +                 Balanced_Tree.make FOLogic.mk_conj
   12.45                   (ListPair.map mk_rec_imp (rec_tms, preds)))))
   12.46       and mutual_induct_concl =
   12.47 -      FOLogic.mk_Trueprop(BalancedTree.make FOLogic.mk_conj qconcls);
   12.48 +      FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
   12.49  
   12.50       val dummy = if !Ind_Syntax.trace then
   12.51                   (writeln ("induct_concl = " ^
    13.1 --- a/src/ZF/ind_syntax.ML	Tue Sep 29 22:33:27 2009 +0200
    13.2 +++ b/src/ZF/ind_syntax.ML	Tue Sep 29 22:48:24 2009 +0200
    13.3 @@ -99,7 +99,7 @@
    13.4        fun is_ind arg = (type_of arg = iT)
    13.5    in  case List.filter is_ind (args @ cs) of
    13.6           []     => @{const 0}
    13.7 -       | u_args => BalancedTree.make mk_Un u_args
    13.8 +       | u_args => Balanced_Tree.make mk_Un u_args
    13.9    end;
   13.10  
   13.11