src/HOL/Tools/record.ML
changeset 32975 84d105ad5adb
parent 32974 2a1aaa2d9e64
child 32976 38364667c773
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 19:04:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 20:15:59 2009 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
     1.5    val mk_cons_tuple: term * term -> term
     1.6    val dest_cons_tuple: term -> term * term
     1.7 -  val istuple_intros_tac: theory -> int -> tactic
     1.8 +  val istuple_intros_tac: int -> tactic
     1.9    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    1.10  end;
    1.11  
    1.12 @@ -157,26 +157,26 @@
    1.13      ((isom, cons $ isom), thm_thy)
    1.14    end;
    1.15  
    1.16 -fun istuple_intros_tac thy =
    1.17 -  let
    1.18 -    val isthms = IsTupleThms.get thy;
    1.19 -    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
    1.20 -    val use_istuple_thm_tac = SUBGOAL (fn (goal, i) =>
    1.21 -      let
    1.22 -        val goal' = Envir.beta_eta_contract goal;
    1.23 -        val is =
    1.24 -          (case goal' of
    1.25 -            Const (@{const_name Trueprop}, _) $
    1.26 -              (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
    1.27 -          | _ => err "unexpected goal format" goal');
    1.28 -        val isthm =
    1.29 -          (case Symtab.lookup isthms (#1 is) of
    1.30 -            SOME isthm => isthm
    1.31 -          | NONE => err "no thm found for constant" (Const is));
    1.32 -      in rtac isthm i end);
    1.33 -  in
    1.34 -    resolve_from_net_tac istuple_intros THEN' use_istuple_thm_tac
    1.35 -  end;
    1.36 +val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
    1.37 +  CSUBGOAL (fn (cgoal, i) =>
    1.38 +    let
    1.39 +      val thy = Thm.theory_of_cterm cgoal;
    1.40 +      val goal = Thm.term_of cgoal;
    1.41 +
    1.42 +      val isthms = IsTupleThms.get thy;
    1.43 +      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
    1.44 +
    1.45 +      val goal' = Envir.beta_eta_contract goal;
    1.46 +      val is =
    1.47 +        (case goal' of
    1.48 +          Const (@{const_name Trueprop}, _) $
    1.49 +            (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
    1.50 +        | _ => err "unexpected goal format" goal');
    1.51 +      val isthm =
    1.52 +        (case Symtab.lookup isthms (#1 is) of
    1.53 +          SOME isthm => isthm
    1.54 +        | NONE => err "no thm found for constant" (Const is));
    1.55 +    in rtac isthm i end);
    1.56  
    1.57  end;
    1.58  
    1.59 @@ -305,8 +305,7 @@
    1.60        | SOME c => ((c, Ts), List.last Ts))
    1.61    | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
    1.62  
    1.63 -fun is_recT T =
    1.64 -  (case try dest_recT T of NONE => false | SOME _ => true);
    1.65 +val is_recT = can dest_recT;
    1.66  
    1.67  fun dest_recTs T =
    1.68    let val ((c, Ts), U) = dest_recT T
    1.69 @@ -1052,7 +1051,7 @@
    1.70  fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
    1.71    | get_upd_funs _ = [];
    1.72  
    1.73 -fun get_accupd_simps thy term defset intros_tac =
    1.74 +fun get_accupd_simps thy term defset =
    1.75    let
    1.76      val (acc, [body]) = strip_comb term;
    1.77      val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
    1.78 @@ -1068,10 +1067,9 @@
    1.79          val othm =
    1.80            Goal.prove (ProofContext.init thy) [] [] prop
    1.81              (fn _ =>
    1.82 -              EVERY
    1.83 -               [simp_tac defset 1,
    1.84 -                REPEAT_DETERM (intros_tac 1),
    1.85 -                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
    1.86 +              simp_tac defset 1 THEN
    1.87 +              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
    1.88 +              TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
    1.89          val dest =
    1.90            if is_sel_upd_pair thy acc upd
    1.91            then o_eq_dest
    1.92 @@ -1079,7 +1077,7 @@
    1.93        in Drule.standard (othm RS dest) end;
    1.94    in map get_simp upd_funs end;
    1.95  
    1.96 -fun get_updupd_simp thy defset intros_tac u u' comp =
    1.97 +fun get_updupd_simp thy defset u u' comp =
    1.98    let
    1.99      val f = Free ("f", domain_type (fastype_of u));
   1.100      val f' = Free ("f'", domain_type (fastype_of u'));
   1.101 @@ -1092,18 +1090,17 @@
   1.102      val othm =
   1.103        Goal.prove (ProofContext.init thy) [] [] prop
   1.104          (fn _ =>
   1.105 -          EVERY
   1.106 -           [simp_tac defset 1,
   1.107 -            REPEAT_DETERM (intros_tac 1),
   1.108 -            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
   1.109 +          simp_tac defset 1 THEN
   1.110 +          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.111 +          TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   1.112      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   1.113    in Drule.standard (othm RS dest) end;
   1.114  
   1.115 -fun get_updupd_simps thy term defset intros_tac =
   1.116 +fun get_updupd_simps thy term defset =
   1.117    let
   1.118      val upd_funs = get_upd_funs term;
   1.119      val cname = fst o dest_Const;
   1.120 -    fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
   1.121 +    fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
   1.122      fun build_swaps_to_eq _ [] swaps = swaps
   1.123        | build_swaps_to_eq upd (u :: us) swaps =
   1.124            let
   1.125 @@ -1127,14 +1124,10 @@
   1.126  fun prove_unfold_defs thy ex_simps ex_simprs prop =
   1.127    let
   1.128      val defset = get_sel_upd_defs thy;
   1.129 -    val in_tac = IsTupleSupport.istuple_intros_tac thy;
   1.130      val prop' = Envir.beta_eta_contract prop;
   1.131      val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
   1.132      val (_, args) = strip_comb lhs;
   1.133 -    val simps =
   1.134 -      if length args = 1
   1.135 -      then get_accupd_simps thy lhs defset in_tac
   1.136 -      else get_updupd_simps thy lhs defset in_tac;
   1.137 +    val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
   1.138    in
   1.139      Goal.prove (ProofContext.init thy) [] [] prop'
   1.140        (fn _ =>
   1.141 @@ -1225,17 +1218,14 @@
   1.142  
   1.143  fun get_upd_acc_cong_thm upd acc thy simpset =
   1.144    let
   1.145 -    val in_tac = IsTupleSupport.istuple_intros_tac thy;
   1.146 -
   1.147 -    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
   1.148 -    val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.149 +    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
   1.150 +    val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.151    in
   1.152      Goal.prove (ProofContext.init thy) [] [] prop
   1.153        (fn _ =>
   1.154 -        EVERY
   1.155 -         [simp_tac simpset 1,
   1.156 -          REPEAT_DETERM (in_tac 1),
   1.157 -          TRY (resolve_tac [updacc_cong_idI] 1)])
   1.158 +        simp_tac simpset 1 THEN
   1.159 +        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.160 +        TRY (resolve_tac [updacc_cong_idI] 1))
   1.161    end;
   1.162  
   1.163  
   1.164 @@ -1462,18 +1452,18 @@
   1.165    P t = 0: do not split
   1.166    P t = ~1: completely split
   1.167    P t > 0: split up to given bound of record extensions.*)
   1.168 -fun record_split_simp_tac thms P i st =
   1.169 +fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
   1.170    let
   1.171 -    val thy = Thm.theory_of_thm st;
   1.172 +    val thy = Thm.theory_of_cterm cgoal;
   1.173 +
   1.174 +    val goal = term_of cgoal;
   1.175 +    val frees = filter (is_recT o #2) (Term.add_frees goal []);
   1.176  
   1.177      val has_rec = exists_Const
   1.178        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.179            (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
   1.180          | _ => false);
   1.181  
   1.182 -    val goal = nth (Thm.prems_of st) (i - 1);    (* FIXME SUBGOAL *)
   1.183 -    val frees = filter (is_recT o type_of) (OldTerm.term_frees goal);
   1.184 -
   1.185      fun mk_split_free_tac free induct_thm i =
   1.186        let
   1.187          val cfree = cterm_of thy free;
   1.188 @@ -1481,61 +1471,58 @@
   1.189          val crec = cterm_of thy r;
   1.190          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   1.191        in
   1.192 -        EVERY
   1.193 -         [simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i,
   1.194 -          rtac thm i,
   1.195 -          simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   1.196 +        simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
   1.197 +        rtac thm i THEN
   1.198 +        simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
   1.199        end;
   1.200  
   1.201 -    fun split_free_tac P i (free as Free (_, T)) =
   1.202 -          (case rec_id ~1 T of
   1.203 -            "" => NONE
   1.204 -          | _ =>
   1.205 -              let val split = P free in
   1.206 -                if split <> 0 then
   1.207 -                  (case get_splits thy (rec_id split T) of
   1.208 -                    NONE => NONE
   1.209 -                  | SOME (_, _, _, induct_thm) =>
   1.210 -                      SOME (mk_split_free_tac free induct_thm i))
   1.211 -                else NONE
   1.212 -              end)
   1.213 -      | split_free_tac _ _ _ = NONE;
   1.214 -
   1.215 -    val split_frees_tacs = map_filter (split_free_tac P i) frees;
   1.216 +    val split_frees_tacs =
   1.217 +      frees |> map_filter (fn (x, T) =>
   1.218 +        (case rec_id ~1 T of
   1.219 +          "" => NONE
   1.220 +        | _ =>
   1.221 +            let
   1.222 +              val free = Free (x, T);
   1.223 +              val split = P free;
   1.224 +            in
   1.225 +              if split <> 0 then
   1.226 +                (case get_splits thy (rec_id split T) of
   1.227 +                  NONE => NONE
   1.228 +                | SOME (_, _, _, induct_thm) =>
   1.229 +                    SOME (mk_split_free_tac free induct_thm i))
   1.230 +              else NONE
   1.231 +            end));
   1.232  
   1.233      val simprocs = if has_rec goal then [record_split_simproc P] else [];
   1.234      val thms' = K_comp_convs @ thms;
   1.235    in
   1.236 -    st |>
   1.237 -      (EVERY split_frees_tacs THEN
   1.238 -        Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
   1.239 -  end handle Empty => Seq.empty;
   1.240 +    EVERY split_frees_tacs THEN
   1.241 +    Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
   1.242 +  end);
   1.243  
   1.244  
   1.245  (* record_split_tac *)
   1.246  
   1.247  (*Split all records in the goal, which are quantified by ! or !!.*)
   1.248 -fun record_split_tac i st =
   1.249 +val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   1.250    let
   1.251 +    val goal = term_of cgoal;
   1.252 +
   1.253      val has_rec = exists_Const
   1.254        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.255            (s = "all" orelse s = "All") andalso is_recT T
   1.256          | _ => false);
   1.257  
   1.258 -    val goal = nth (Thm.prems_of st) (i - 1);  (* FIXME SUBGOAL *)
   1.259 -
   1.260      fun is_all t =
   1.261        (case t of
   1.262          Const (quantifier, _) $ _ =>
   1.263            if quantifier = "All" orelse quantifier = "all" then ~1 else 0
   1.264        | _ => 0);
   1.265 -
   1.266    in
   1.267      if has_rec goal then
   1.268 -      Simplifier.full_simp_tac
   1.269 -        (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
   1.270 -    else Seq.empty
   1.271 -  end handle Subscript => Seq.empty;     (* FIXME SUBGOAL *)
   1.272 +      Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
   1.273 +    else no_tac
   1.274 +  end);
   1.275  
   1.276  
   1.277  (* wrapper *)
   1.278 @@ -1585,13 +1572,14 @@
   1.279    (or on s if there are no parameters).
   1.280    Instatiation of record variable (and predicate) in rule is calculated to
   1.281    avoid problems with higher order unification.*)
   1.282 -fun try_param_tac s rule i st =
   1.283 +fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
   1.284    let
   1.285 -    val cert = cterm_of (Thm.theory_of_thm st);
   1.286 -    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
   1.287 +    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
   1.288 +
   1.289 +    val g = Thm.term_of cgoal;
   1.290      val params = Logic.strip_params g;
   1.291      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
   1.292 -    val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
   1.293 +    val rule' = Thm.lift_rule cgoal rule;
   1.294      val (P, ys) = strip_comb (HOLogic.dest_Trueprop
   1.295        (Logic.strip_assums_concl (prop_of rule')));
   1.296      (*ca indicates if rule is a case analysis or induction rule*)
   1.297 @@ -1601,15 +1589,15 @@
   1.298            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   1.299        | [x] => (head_of x, false));
   1.300      val rule'' = cterm_instantiate (map (pairself cert)
   1.301 -      (case (rev params) of
   1.302 +      (case rev params of
   1.303          [] =>
   1.304 -          (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
   1.305 +          (case AList.lookup (op =) (Term.add_frees g []) s of
   1.306              NONE => sys_error "try_param_tac: no such variable"
   1.307            | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
   1.308        | (_, T) :: _ =>
   1.309            [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
   1.310              (x, list_abs (params, Bound 0))])) rule';
   1.311 -  in compose_tac (false, rule'', nprems_of rule) i st end;
   1.312 +  in compose_tac (false, rule'', nprems_of rule) i end);
   1.313  
   1.314  
   1.315  fun extension_definition name fields alphas zeta moreT more vars thy =
   1.316 @@ -1697,7 +1685,6 @@
   1.317      val ext = mk_ext vars_more;
   1.318      val s = Free (rN, extT);
   1.319      val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   1.320 -    val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   1.321  
   1.322      val inject_prop =
   1.323        let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
   1.324 @@ -1723,11 +1710,11 @@
   1.325        simplify HOL_ss
   1.326          (prove_standard [] inject_prop
   1.327            (fn _ =>
   1.328 -            EVERY
   1.329 -             [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   1.330 -              REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
   1.331 -                intros_tac 1 ORELSE
   1.332 -                resolve_tac [refl] 1)]));
   1.333 +            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.334 +            REPEAT_DETERM
   1.335 +              (rtac refl_conj_eq 1 ORELSE
   1.336 +                IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.337 +                rtac refl 1)));
   1.338  
   1.339      val inject = timeit_msg "record extension inject proof:" inject_prf;
   1.340  
   1.341 @@ -1744,7 +1731,7 @@
   1.342          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   1.343          val tactic1 =
   1.344            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.345 -          REPEAT_ALL_NEW intros_tac 1;
   1.346 +          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
   1.347          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   1.348          val [halfway] = Seq.list_of (tactic1 start);
   1.349          val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   1.350 @@ -1756,21 +1743,20 @@
   1.351      fun split_meta_prf () =
   1.352        prove_standard [] split_meta_prop
   1.353          (fn _ =>
   1.354 -          EVERY
   1.355 -           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.356 -            etac meta_allE 1, atac 1,
   1.357 -            rtac (prop_subst OF [surject]) 1,
   1.358 -            REPEAT (etac meta_allE 1), atac 1]);
   1.359 +          EVERY1
   1.360 +           [rtac equal_intr_rule, Goal.norm_hhf_tac,
   1.361 +            etac meta_allE, atac,
   1.362 +            rtac (prop_subst OF [surject]),
   1.363 +            REPEAT o etac meta_allE, atac]);
   1.364      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   1.365  
   1.366      fun induct_prf () =
   1.367        let val (assm, concl) = induct_prop in
   1.368          prove_standard [assm] concl
   1.369            (fn {prems, ...} =>
   1.370 -            EVERY
   1.371 -             [cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1,
   1.372 -              resolve_tac prems 2,
   1.373 -              asm_simp_tac HOL_ss 1])
   1.374 +            cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
   1.375 +            resolve_tac prems 2 THEN
   1.376 +            asm_simp_tac HOL_ss 1)
   1.377        end;
   1.378      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.379  
   1.380 @@ -1967,7 +1953,6 @@
   1.381          (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
   1.382  
   1.383      val ext_defs = ext_def :: map #extdef parents;
   1.384 -    val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
   1.385  
   1.386      (*Theorems from the istuple intros.
   1.387        This is complex enough to deserve a full comment.
   1.388 @@ -1994,7 +1979,7 @@
   1.389          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   1.390          val tactic =
   1.391            simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
   1.392 -          REPEAT (intros_tac 1 ORELSE terminal);
   1.393 +          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
   1.394          val updaccs = Seq.list_of (tactic init_thm);
   1.395        in
   1.396          (updaccs RL [updacc_accessor_eqE],
   1.397 @@ -2175,8 +2160,7 @@
   1.398        prove_standard [] induct_scheme_prop
   1.399          (fn _ =>
   1.400            EVERY
   1.401 -           [if null parent_induct
   1.402 -            then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.403 +           [if null parent_induct then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.404              try_param_tac rN ext_induct 1,
   1.405              asm_simp_tac HOL_basic_ss 1]);
   1.406      val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
   1.407 @@ -2203,13 +2187,13 @@
   1.408      fun cases_scheme_prf_noopt () =
   1.409        prove_standard [] cases_scheme_prop
   1.410          (fn _ =>
   1.411 -          EVERY
   1.412 -           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   1.413 -            try_param_tac rN induct_scheme 1,
   1.414 -            rtac impI 1,
   1.415 -            REPEAT (etac allE 1),
   1.416 -            etac mp 1,
   1.417 -            rtac refl 1]);
   1.418 +          EVERY1
   1.419 +           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]),
   1.420 +            try_param_tac rN induct_scheme,
   1.421 +            rtac impI,
   1.422 +            REPEAT o etac allE,
   1.423 +            etac mp,
   1.424 +            rtac refl]);
   1.425      val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
   1.426      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
   1.427  
   1.428 @@ -2230,18 +2214,20 @@
   1.429              EVERY
   1.430               [rtac surject_assist_idE 1,
   1.431                simp_tac init_ss 1,
   1.432 -              REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   1.433 +              REPEAT
   1.434 +                (IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.435 +                  (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   1.436        end;
   1.437      val surjective = timeit_msg "record surjective proof:" surjective_prf;
   1.438  
   1.439      fun split_meta_prf () =
   1.440        prove false [] split_meta_prop
   1.441          (fn _ =>
   1.442 -          EVERY
   1.443 -           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.444 -            etac meta_allE 1, atac 1,
   1.445 -            rtac (prop_subst OF [surjective]) 1,
   1.446 -            REPEAT (etac meta_allE 1), atac 1]);
   1.447 +          EVERY1
   1.448 +           [rtac equal_intr_rule, Goal.norm_hhf_tac,
   1.449 +            etac meta_allE, atac,
   1.450 +            rtac (prop_subst OF [surjective]),
   1.451 +            REPEAT o etac meta_allE, atac]);
   1.452      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
   1.453      fun split_meta_standardise () = Drule.standard split_meta;
   1.454      val split_meta_standard =
   1.455 @@ -2273,10 +2259,10 @@
   1.456      fun split_object_prf_noopt () =
   1.457        prove_standard [] split_object_prop
   1.458          (fn _ =>
   1.459 -          EVERY
   1.460 -           [rtac iffI 1,
   1.461 -            REPEAT (rtac allI 1), etac allE 1, atac 1,
   1.462 -            rtac allI 1, rtac induct_scheme 1, REPEAT (etac allE 1), atac 1]);
   1.463 +          EVERY1
   1.464 +           [rtac iffI,
   1.465 +            REPEAT o rtac allI, etac allE, atac,
   1.466 +            rtac allI, rtac induct_scheme, REPEAT o etac allE, atac]);
   1.467  
   1.468      val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
   1.469      val split_object = timeit_msg "record split_object proof:" split_object_prf;