# HG changeset patch
# User blanchet
# Date 1394198475 -3600
# Node ID 94242fa87638c2afc8e29d466d98e302fa256264
# Parent  5dadc93ff3df973a6b0d4ce3e2d8cd29be01bd61
tuning

diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Fun_Def.thy	Fri Mar 07 14:21:15 2014 +0100
@@ -83,7 +83,6 @@
   by (simp add: wfP_def)
 
 ML_file "Tools/Function/function_core.ML"
-ML_file "Tools/Function/sum_tree.ML"
 ML_file "Tools/Function/mutual.ML"
 ML_file "Tools/Function/pattern_split.ML"
 ML_file "Tools/Function/relation.ML"
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Fun_Def_Base.thy
--- a/src/HOL/Fun_Def_Base.thy	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Fun_Def_Base.thy	Fri Mar 07 14:21:15 2014 +0100
@@ -12,5 +12,6 @@
 ML_file "Tools/Function/function_common.ML"
 ML_file "Tools/Function/context_tree.ML"
 setup Function_Ctx_Tree.setup
+ML_file "Tools/Function/sum_tree.ML"
 
 end
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -478,8 +478,8 @@
       define_co_rec Least_FP fpT Cs (mk_binding recN)
         (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
            map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
-               mk_case_absumprod ctor_rec_absT rep fs
-                 (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
+               mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
+                 (map flat_rec_arg_args xsss))
              ctor_rec_absTs reps fss xssss)))
     end;
 
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -139,11 +139,10 @@
 
   val mk_case_sum: term * term -> term
   val mk_case_sumN: term list -> term
-  val mk_case_absumprod: typ -> term -> term list -> term list -> term list list -> term
+  val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term
 
   val mk_Inl: typ -> term -> term
   val mk_Inr: typ -> term -> term
-  val mk_tuple_balanced: term list -> term
   val mk_absumprod: typ -> term -> int -> int -> term list -> term
 
   val dest_sumT: typ -> typ * typ
@@ -374,35 +373,19 @@
 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
 
-(* FIXME: reuse "mk_inj" in function package *)
-fun mk_InN_balanced sum_T n t k =
-  let
-    fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
-      | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
-      | repair_types _ t = t
-    and repair_inj_types T s get t =
-      let val T' = get (dest_sumT T) in
-        Const (s, T' --> T) $ repair_types T' t
-      end;
-  in
-    Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
-    |> repair_types sum_T
-  end;
-
 fun mk_tuple_balanced [] = HOLogic.unit
   | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
 
 fun mk_absumprod absT abs0 n k ts =
   let val abs = mk_abs absT abs0;
-  in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end;
+  in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
 
 fun mk_case_sum (f, g) =
   let
-    val fT = fastype_of f;
-    val gT = fastype_of g;
+    val (fT, T') = dest_funT (fastype_of f);
+    val (gT, _) = dest_funT (fastype_of g);
   in
-    Const (@{const_name case_sum},
-      fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
+    Sum_Tree.mk_sumcase fT gT T' f g
   end;
 
 val mk_case_sumN = Library.foldr1 mk_case_sum;
@@ -411,8 +394,9 @@
 fun mk_tupled_fun f x xs =
   if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
 
-fun mk_case_absumprod absT rep fs xs xss =
-  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs xs xss), mk_rep absT rep);
+fun mk_case_absumprod absT rep fs xss xss' =
+  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
+    mk_rep absT rep);
 
 fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
 fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -114,7 +114,7 @@
         val args = HOLogic.mk_tuple arg_vars;
         val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-        val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
 
         val cprop = cert prop;
 
@@ -155,4 +155,3 @@
 end;
 
 end;
-
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -11,7 +11,6 @@
   val induction_schema_tac : Proof.context -> thm list -> tactic
 end
 
-
 structure Induction_Schema : INDUCTION_SCHEMA =
 struct
 
@@ -111,7 +110,7 @@
     fun PT_of (SchemeBranch { xs, ...}) =
       foldr1 HOLogic.mk_prodT (map snd xs)
 
-    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) (map PT_of branches)
   in
     IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   end
@@ -146,7 +145,7 @@
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
   let
     fun inject i ts =
-       SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+       Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
 
     val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
 
@@ -199,7 +198,7 @@
       |> Object_Logic.drop_judgment thy
       |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
-    SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+    Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
   end
 
 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
@@ -212,7 +211,7 @@
     val scases_idx = map_index I scases
 
     fun inject i ts =
-      SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+      Sum_Tree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
     val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
 
     val P_comp = mk_ind_goal ctxt branches
@@ -372,12 +371,12 @@
     fun project (i, SchemeBranch {xs, ...}) =
       let
         val inst = (foldr1 HOLogic.mk_prod (map Free xs))
-          |> SumTree.mk_inj ST (length branches) (i + 1)
+          |> Sum_Tree.mk_inj ST (length branches) (i + 1)
           |> cert
       in
         indthm
         |> Drule.instantiate' [] [SOME inst]
-        |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
+        |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
         |> Conv.fconv_rule (ind_rulify ctxt'')
       end
 
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -6,10 +6,8 @@
 
 signature MEASURE_FUNCTIONS =
 sig
-
   val get_measure_functions : Proof.context -> typ -> term list
   val setup : theory -> theory
-
 end
 
 structure MeasureFunctions : MEASURE_FUNCTIONS =
@@ -40,12 +38,12 @@
 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
 
 fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
-  map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
-  @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
+  map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
+  @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   | mk_funorder_funs T = [ constant_1 T ]
 
 fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
-    map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
+    map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
       (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   | mk_ext_base_funs ctxt T = find_measures ctxt T
 
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -6,7 +6,6 @@
 
 signature FUNCTION_MUTUAL =
 sig
-
   val prepare_function_mutual : Function_Common.function_config
     -> string (* defname *)
     -> ((string * typ) * mixfix) list
@@ -15,10 +14,8 @@
     -> ((thm (* goalstate *)
         * (thm -> Function_Common.function_result) (* proof continuation *)
        ) * local_theory)
-
 end
 
-
 structure Function_Mutual: FUNCTION_MUTUAL =
 struct
 
@@ -88,8 +85,8 @@
     val dresultTs = distinct (op =) resultTs
     val n' = length dresultTs
 
-    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
-    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
+    val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
+    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
 
     val fsum_type = ST --> RST
 
@@ -101,7 +98,7 @@
         val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
         val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
 
-        val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
+        val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
         val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
 
         val rew = (n, fold_rev lambda vars f_exp)
@@ -117,8 +114,8 @@
         val rhs' = rhs
           |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
       in
-        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
+        (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
+         Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs'))
       end
 
     val qglrs = map convert_eqs fqgars
@@ -227,21 +224,21 @@
       end
 
     val Ps = map2 mk_P parts newPs
-    val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
+    val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
 
     val induct_inst =
       Thm.forall_elim (cert case_exp) induct
-      |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+      |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
       |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
 
     fun project rule (MutualPart {cargTs, i, ...}) k =
       let
         val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
-        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
+        val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
       in
         (rule
          |> Thm.forall_elim (cert inj)
-         |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+         |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
          |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
          k + length cargTs)
       end
@@ -260,7 +257,7 @@
 
     val cert = cterm_of (Proof_Context.theory_of ctxt)
 
-    val sumtree_inj = SumTree.mk_inj ST n i args
+    val sumtree_inj = Sum_Tree.mk_inj ST n i args
 
     val sum_elims =
       @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]}
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/sum_tree.ML
--- a/src/HOL/Tools/Function/sum_tree.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -16,7 +16,7 @@
   val mk_sumcases: typ -> term list -> term
 end
 
-structure SumTree: SUM_TREE =
+structure Sum_Tree: SUM_TREE =
 struct
 
 (* Theory dependencies *)
diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -6,7 +6,6 @@
 
 signature TERMINATION =
 sig
-
   type data
   datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
 
@@ -122,7 +121,7 @@
 (* Build case expression *)
 fun mk_sumcases (sk, _, _, _, _) T fs =
   mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
-          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+          (fn ((f, fT), (g, gT)) => (Sum_Tree.mk_sumcase fT gT T f g, Sum_Tree.mk_sumT fT gT))
           sk
   |> fst