tuning
authorblanchet
Fri Mar 07 14:21:15 2014 +0100 (2014-03-07)
changeset 5596894242fa87638
parent 55967 5dadc93ff3df
child 55969 8820ddb8f9f4
tuning
src/HOL/Fun_Def.thy
src/HOL/Fun_Def_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/Function/function_elims.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/Fun_Def.thy	Fri Mar 07 12:35:06 2014 +0000
     1.2 +++ b/src/HOL/Fun_Def.thy	Fri Mar 07 14:21:15 2014 +0100
     1.3 @@ -83,7 +83,6 @@
     1.4    by (simp add: wfP_def)
     1.5  
     1.6  ML_file "Tools/Function/function_core.ML"
     1.7 -ML_file "Tools/Function/sum_tree.ML"
     1.8  ML_file "Tools/Function/mutual.ML"
     1.9  ML_file "Tools/Function/pattern_split.ML"
    1.10  ML_file "Tools/Function/relation.ML"
     2.1 --- a/src/HOL/Fun_Def_Base.thy	Fri Mar 07 12:35:06 2014 +0000
     2.2 +++ b/src/HOL/Fun_Def_Base.thy	Fri Mar 07 14:21:15 2014 +0100
     2.3 @@ -12,5 +12,6 @@
     2.4  ML_file "Tools/Function/function_common.ML"
     2.5  ML_file "Tools/Function/context_tree.ML"
     2.6  setup Function_Ctx_Tree.setup
     2.7 +ML_file "Tools/Function/sum_tree.ML"
     2.8  
     2.9  end
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 12:35:06 2014 +0000
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
     3.3 @@ -478,8 +478,8 @@
     3.4        define_co_rec Least_FP fpT Cs (mk_binding recN)
     3.5          (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
     3.6             map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
     3.7 -               mk_case_absumprod ctor_rec_absT rep fs
     3.8 -                 (map (mk_tuple_balanced o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
     3.9 +               mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
    3.10 +                 (map flat_rec_arg_args xsss))
    3.11               ctor_rec_absTs reps fss xssss)))
    3.12      end;
    3.13  
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 12:35:06 2014 +0000
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
     4.3 @@ -139,11 +139,10 @@
     4.4  
     4.5    val mk_case_sum: term * term -> term
     4.6    val mk_case_sumN: term list -> term
     4.7 -  val mk_case_absumprod: typ -> term -> term list -> term list -> term list list -> term
     4.8 +  val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term
     4.9  
    4.10    val mk_Inl: typ -> term -> term
    4.11    val mk_Inr: typ -> term -> term
    4.12 -  val mk_tuple_balanced: term list -> term
    4.13    val mk_absumprod: typ -> term -> int -> int -> term list -> term
    4.14  
    4.15    val dest_sumT: typ -> typ * typ
    4.16 @@ -374,35 +373,19 @@
    4.17  fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
    4.18  fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
    4.19  
    4.20 -(* FIXME: reuse "mk_inj" in function package *)
    4.21 -fun mk_InN_balanced sum_T n t k =
    4.22 -  let
    4.23 -    fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t
    4.24 -      | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t
    4.25 -      | repair_types _ t = t
    4.26 -    and repair_inj_types T s get t =
    4.27 -      let val T' = get (dest_sumT T) in
    4.28 -        Const (s, T' --> T) $ repair_types T' t
    4.29 -      end;
    4.30 -  in
    4.31 -    Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k
    4.32 -    |> repair_types sum_T
    4.33 -  end;
    4.34 -
    4.35  fun mk_tuple_balanced [] = HOLogic.unit
    4.36    | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
    4.37  
    4.38  fun mk_absumprod absT abs0 n k ts =
    4.39    let val abs = mk_abs absT abs0;
    4.40 -  in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end;
    4.41 +  in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
    4.42  
    4.43  fun mk_case_sum (f, g) =
    4.44    let
    4.45 -    val fT = fastype_of f;
    4.46 -    val gT = fastype_of g;
    4.47 +    val (fT, T') = dest_funT (fastype_of f);
    4.48 +    val (gT, _) = dest_funT (fastype_of g);
    4.49    in
    4.50 -    Const (@{const_name case_sum},
    4.51 -      fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
    4.52 +    Sum_Tree.mk_sumcase fT gT T' f g
    4.53    end;
    4.54  
    4.55  val mk_case_sumN = Library.foldr1 mk_case_sum;
    4.56 @@ -411,8 +394,9 @@
    4.57  fun mk_tupled_fun f x xs =
    4.58    if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    4.59  
    4.60 -fun mk_case_absumprod absT rep fs xs xss =
    4.61 -  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs xs xss), mk_rep absT rep);
    4.62 +fun mk_case_absumprod absT rep fs xss xss' =
    4.63 +  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
    4.64 +    mk_rep absT rep);
    4.65  
    4.66  fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
    4.67  fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
     5.1 --- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 12:35:06 2014 +0000
     5.2 +++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 14:21:15 2014 +0100
     5.3 @@ -114,7 +114,7 @@
     5.4          val args = HOLogic.mk_tuple arg_vars;
     5.5          val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
     5.6  
     5.7 -        val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
     5.8 +        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
     5.9  
    5.10          val cprop = cert prop;
    5.11  
    5.12 @@ -155,4 +155,3 @@
    5.13  end;
    5.14  
    5.15  end;
    5.16 -
     6.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 12:35:06 2014 +0000
     6.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 14:21:15 2014 +0100
     6.3 @@ -11,7 +11,6 @@
     6.4    val induction_schema_tac : Proof.context -> thm list -> tactic
     6.5  end
     6.6  
     6.7 -
     6.8  structure Induction_Schema : INDUCTION_SCHEMA =
     6.9  struct
    6.10  
    6.11 @@ -111,7 +110,7 @@
    6.12      fun PT_of (SchemeBranch { xs, ...}) =
    6.13        foldr1 HOLogic.mk_prodT (map snd xs)
    6.14  
    6.15 -    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
    6.16 +    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) (map PT_of branches)
    6.17    in
    6.18      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
    6.19    end
    6.20 @@ -146,7 +145,7 @@
    6.21  fun mk_ineqs R (IndScheme {T, cases, branches}) =
    6.22    let
    6.23      fun inject i ts =
    6.24 -       SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
    6.25 +       Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
    6.26  
    6.27      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
    6.28  
    6.29 @@ -199,7 +198,7 @@
    6.30        |> Object_Logic.drop_judgment thy
    6.31        |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
    6.32    in
    6.33 -    SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
    6.34 +    Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
    6.35    end
    6.36  
    6.37  fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
    6.38 @@ -212,7 +211,7 @@
    6.39      val scases_idx = map_index I scases
    6.40  
    6.41      fun inject i ts =
    6.42 -      SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
    6.43 +      Sum_Tree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
    6.44      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
    6.45  
    6.46      val P_comp = mk_ind_goal ctxt branches
    6.47 @@ -372,12 +371,12 @@
    6.48      fun project (i, SchemeBranch {xs, ...}) =
    6.49        let
    6.50          val inst = (foldr1 HOLogic.mk_prod (map Free xs))
    6.51 -          |> SumTree.mk_inj ST (length branches) (i + 1)
    6.52 +          |> Sum_Tree.mk_inj ST (length branches) (i + 1)
    6.53            |> cert
    6.54        in
    6.55          indthm
    6.56          |> Drule.instantiate' [] [SOME inst]
    6.57 -        |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
    6.58 +        |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
    6.59          |> Conv.fconv_rule (ind_rulify ctxt'')
    6.60        end
    6.61  
     7.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 07 12:35:06 2014 +0000
     7.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Mar 07 14:21:15 2014 +0100
     7.3 @@ -6,10 +6,8 @@
     7.4  
     7.5  signature MEASURE_FUNCTIONS =
     7.6  sig
     7.7 -
     7.8    val get_measure_functions : Proof.context -> typ -> term list
     7.9    val setup : theory -> theory
    7.10 -
    7.11  end
    7.12  
    7.13  structure MeasureFunctions : MEASURE_FUNCTIONS =
    7.14 @@ -40,12 +38,12 @@
    7.15  fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    7.16  
    7.17  fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    7.18 -  map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    7.19 -  @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    7.20 +  map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    7.21 +  @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    7.22    | mk_funorder_funs T = [ constant_1 T ]
    7.23  
    7.24  fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    7.25 -    map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    7.26 +    map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
    7.27        (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    7.28    | mk_ext_base_funs ctxt T = find_measures ctxt T
    7.29  
     8.1 --- a/src/HOL/Tools/Function/mutual.ML	Fri Mar 07 12:35:06 2014 +0000
     8.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Mar 07 14:21:15 2014 +0100
     8.3 @@ -6,7 +6,6 @@
     8.4  
     8.5  signature FUNCTION_MUTUAL =
     8.6  sig
     8.7 -
     8.8    val prepare_function_mutual : Function_Common.function_config
     8.9      -> string (* defname *)
    8.10      -> ((string * typ) * mixfix) list
    8.11 @@ -15,10 +14,8 @@
    8.12      -> ((thm (* goalstate *)
    8.13          * (thm -> Function_Common.function_result) (* proof continuation *)
    8.14         ) * local_theory)
    8.15 -
    8.16  end
    8.17  
    8.18 -
    8.19  structure Function_Mutual: FUNCTION_MUTUAL =
    8.20  struct
    8.21  
    8.22 @@ -88,8 +85,8 @@
    8.23      val dresultTs = distinct (op =) resultTs
    8.24      val n' = length dresultTs
    8.25  
    8.26 -    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
    8.27 -    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
    8.28 +    val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
    8.29 +    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
    8.30  
    8.31      val fsum_type = ST --> RST
    8.32  
    8.33 @@ -101,7 +98,7 @@
    8.34          val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
    8.35          val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
    8.36  
    8.37 -        val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
    8.38 +        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))
    8.39          val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
    8.40  
    8.41          val rew = (n, fold_rev lambda vars f_exp)
    8.42 @@ -117,8 +114,8 @@
    8.43          val rhs' = rhs
    8.44            |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
    8.45        in
    8.46 -        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
    8.47 -         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
    8.48 +        (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
    8.49 +         Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs'))
    8.50        end
    8.51  
    8.52      val qglrs = map convert_eqs fqgars
    8.53 @@ -227,21 +224,21 @@
    8.54        end
    8.55  
    8.56      val Ps = map2 mk_P parts newPs
    8.57 -    val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
    8.58 +    val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
    8.59  
    8.60      val induct_inst =
    8.61        Thm.forall_elim (cert case_exp) induct
    8.62 -      |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
    8.63 +      |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
    8.64        |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
    8.65  
    8.66      fun project rule (MutualPart {cargTs, i, ...}) k =
    8.67        let
    8.68          val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
    8.69 -        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
    8.70 +        val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
    8.71        in
    8.72          (rule
    8.73           |> Thm.forall_elim (cert inj)
    8.74 -         |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
    8.75 +         |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
    8.76           |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
    8.77           k + length cargTs)
    8.78        end
    8.79 @@ -260,7 +257,7 @@
    8.80  
    8.81      val cert = cterm_of (Proof_Context.theory_of ctxt)
    8.82  
    8.83 -    val sumtree_inj = SumTree.mk_inj ST n i args
    8.84 +    val sumtree_inj = Sum_Tree.mk_inj ST n i args
    8.85  
    8.86      val sum_elims =
    8.87        @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]}
     9.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Fri Mar 07 12:35:06 2014 +0000
     9.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Mar 07 14:21:15 2014 +0100
     9.3 @@ -16,7 +16,7 @@
     9.4    val mk_sumcases: typ -> term list -> term
     9.5  end
     9.6  
     9.7 -structure SumTree: SUM_TREE =
     9.8 +structure Sum_Tree: SUM_TREE =
     9.9  struct
    9.10  
    9.11  (* Theory dependencies *)
    10.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Mar 07 12:35:06 2014 +0000
    10.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 07 14:21:15 2014 +0100
    10.3 @@ -6,7 +6,6 @@
    10.4  
    10.5  signature TERMINATION =
    10.6  sig
    10.7 -
    10.8    type data
    10.9    datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
   10.10  
   10.11 @@ -122,7 +121,7 @@
   10.12  (* Build case expression *)
   10.13  fun mk_sumcases (sk, _, _, _, _) T fs =
   10.14    mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
   10.15 -          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
   10.16 +          (fn ((f, fT), (g, gT)) => (Sum_Tree.mk_sumcase fT gT T f g, Sum_Tree.mk_sumT fT gT))
   10.17            sk
   10.18    |> fst
   10.19