tuning
authorblanchet
Thu Feb 06 00:03:12 2014 +0100 (2014-02-06)
changeset 553421bd9e637ac9f
parent 55341 3d2c97392e25
child 55343 5ebf832b58a1
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 05 23:30:02 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
     1.3 @@ -186,15 +186,16 @@
     1.4      ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
     1.5    (0, lthy)
     1.6    |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     1.7 -    register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
     1.8 -        nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
     1.9 -        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss,
    1.10 -        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
    1.11 +    register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    1.12 +        nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    1.13 +        ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
    1.14 +        co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
    1.15          sel_co_iterssss = sel_co_iterssss}
    1.16        lthy)) Ts
    1.17    |> snd;
    1.18  
    1.19 -(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.20 +(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
    1.21 +   "x.x_A", "y.A"). *)
    1.22  fun quasi_unambiguous_case_names names =
    1.23    let
    1.24      val ps = map (`Long_Name.base_name) names;
    1.25 @@ -501,7 +502,7 @@
    1.26        if fp = Least_FP then
    1.27          mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
    1.28        else
    1.29 -        mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
    1.30 +        mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME);
    1.31    in
    1.32      ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
    1.33    end;
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Feb 05 23:30:02 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
     2.3 @@ -165,7 +165,7 @@
     2.4            else
     2.5              f conds t
     2.6          end
     2.7 -      | _ => f conds t)
     2.8 +      | _ => f conds t);
     2.9    in
    2.10      fld []
    2.11    end;
    2.12 @@ -224,7 +224,7 @@
    2.13              end
    2.14            | NONE => massage_leaf bound_Ts t)
    2.15          | _ => massage_leaf bound_Ts t)
    2.16 -      end
    2.17 +      end;
    2.18    in
    2.19      massage_rec
    2.20    end;
    2.21 @@ -490,11 +490,14 @@
    2.22  val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
    2.23  
    2.24  fun abstract vs =
    2.25 -  let fun a n (t $ u) = a n t $ a n u
    2.26 -        | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
    2.27 -        | a n t = let val idx = find_index (curry (op =) t) vs in
    2.28 -            if idx < 0 then t else Bound (n + idx) end
    2.29 -  in a 0 end;
    2.30 +  let
    2.31 +    fun abs n (t $ u) = abs n t $ abs n u
    2.32 +      | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b)
    2.33 +      | abs n t =
    2.34 +        let val j = find_index (curry (op =) t) vs in
    2.35 +          if j < 0 then t else Bound (n + j)
    2.36 +        end;
    2.37 +  in abs 0 end;
    2.38  
    2.39  fun mk_prod1 bound_Ts (t, u) =
    2.40    HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
    2.41 @@ -849,7 +852,7 @@
    2.42                ((c, c', a orelse a'), (x, s_not (s_conjs y)))
    2.43              ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
    2.44              ||> Logic.list_implies
    2.45 -            ||> curry Logic.list_all (map dest_Free fun_args))))
    2.46 +            ||> curry Logic.list_all (map dest_Free fun_args))));
    2.47    in
    2.48      map (list_comb o rpair corec_args) corecs
    2.49      |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
    2.50 @@ -868,7 +871,7 @@
    2.51      else
    2.52        let
    2.53          val n = 0 upto length ctr_specs
    2.54 -          |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns));
    2.55 +          |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns));
    2.56          val {ctr, disc, ...} = nth ctr_specs n;
    2.57          val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
    2.58            |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
    2.59 @@ -985,9 +988,9 @@
    2.60   space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
    2.61  *)
    2.62  
    2.63 -    val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (idx, goal) =>
    2.64 -        (idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
    2.65 -           (exclude_tac tac_opt sequential idx), goal))))
    2.66 +    val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
    2.67 +        (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
    2.68 +           (exclude_tac tac_opt sequential j), goal))))
    2.69        tac_opts sequentials excludess';
    2.70      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
    2.71      val (goal_idxss, exclude_goalss) = excludess''
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Feb 05 23:30:02 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Feb 06 00:03:12 2014 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4  fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
     3.5    let
     3.6      val splits' =
     3.7 -      map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
     3.8 +      map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits);
     3.9    in
    3.10      HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
    3.11      prelude_tac ctxt [] (fun_ctr RS trans) THEN
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 05 23:30:02 2014 +0100
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
     4.3 @@ -205,12 +205,9 @@
     4.4  fun mk_half_pairss p = mk_half_pairss' [[]] p;
     4.5  
     4.6  fun join_halves n half_xss other_half_xss =
     4.7 -  let
     4.8 -    val xsss =
     4.9 -      map2 (map2 append) (Library.chop_groups n half_xss)
    4.10 -        (transpose (Library.chop_groups n other_half_xss))
    4.11 -    val xs = splice (flat half_xss) (flat other_half_xss);
    4.12 -  in (xs, xsss) end;
    4.13 +  (splice (flat half_xss) (flat other_half_xss),
    4.14 +   map2 (map2 append) (Library.chop_groups n half_xss)
    4.15 +     (transpose (Library.chop_groups n other_half_xss)));
    4.16  
    4.17  fun mk_undefined T = Const (@{const_name undefined}, T);
    4.18  
    4.19 @@ -252,9 +249,7 @@
    4.20  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
    4.21  
    4.22  fun dest_ctr ctxt s t =
    4.23 -  let
    4.24 -    val (f, args) = Term.strip_comb t;
    4.25 -  in
    4.26 +  let val (f, args) = Term.strip_comb t in
    4.27      (case ctr_sugar_of ctxt s of
    4.28        SOME {ctrs, ...} =>
    4.29        (case find_first (can (fo_match ctxt f)) ctrs of