src/HOL/Tools/record.ML
changeset 33055 5a733f325939
parent 33053 dabf9d1bb552
parent 33049 c38f02fdf35d
child 33063 4d462963a7db
     1.1 --- a/src/HOL/Tools/record.ML	Wed Oct 21 16:54:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Oct 21 16:57:57 2009 +0200
     1.3 @@ -26,17 +26,13 @@
     1.4  sig
     1.5    include BASIC_RECORD
     1.6    val timing: bool Unsynchronized.ref
     1.7 -  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
     1.8    val updateN: string
     1.9 -  val updN: string
    1.10    val ext_typeN: string
    1.11    val extN: string
    1.12    val makeN: string
    1.13    val moreN: string
    1.14 -  val ext_dest: string
    1.15 -
    1.16    val last_extT: typ -> (string * typ list) option
    1.17 -  val dest_recTs : typ -> (string * typ list) list
    1.18 +  val dest_recTs: typ -> (string * typ list) list
    1.19    val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    1.20    val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    1.21    val get_parent: theory -> string -> (typ list * string) option
    1.22 @@ -56,13 +52,10 @@
    1.23  
    1.24  signature ISTUPLE_SUPPORT =
    1.25  sig
    1.26 -  val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> term * term * theory
    1.27 -
    1.28 +  val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    1.29    val mk_cons_tuple: term * term -> term
    1.30    val dest_cons_tuple: term -> term * term
    1.31 -
    1.32 -  val istuple_intros_tac: theory -> int -> tactic
    1.33 -
    1.34 +  val istuple_intros_tac: int -> tactic
    1.35    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    1.36  end;
    1.37  
    1.38 @@ -70,21 +63,11 @@
    1.39  struct
    1.40  
    1.41  val isomN = "_TupleIsom";
    1.42 -val defN = "_def";
    1.43 -
    1.44 -val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    1.45 -val istuple_True_simp = @{thm "istuple_True_simp"};
    1.46 -
    1.47 -val istuple_intro = @{thm "isomorphic_tuple_intro"};
    1.48 -val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    1.49 -
    1.50 -val constname = fst o dest_Const;
    1.51 -val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    1.52 -
    1.53 -val istuple_constN = constname @{term isomorphic_tuple};
    1.54 -val istuple_consN = constname @{term istuple_cons};
    1.55 -
    1.56 -val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    1.57 +
    1.58 +val istuple_intro = @{thm isomorphic_tuple_intro};
    1.59 +val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    1.60 +
    1.61 +val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple});
    1.62  
    1.63  fun named_cterm_instantiate values thm =
    1.64    let
    1.65 @@ -111,11 +94,13 @@
    1.66    let
    1.67      fun get_thms thy name =
    1.68        let
    1.69 -        val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
    1.70 -          Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
    1.71 -        val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    1.72 -      in (map rewrite_rule [rep_inject, abs_inverse],
    1.73 -            Const (absN, repT --> absT), absT) end;
    1.74 +        val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    1.75 +          Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
    1.76 +        val rewrite_rule =
    1.77 +          MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}];
    1.78 +      in
    1.79 +        (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
    1.80 +      end;
    1.81    in
    1.82      thy
    1.83      |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    1.84 @@ -126,16 +111,14 @@
    1.85    let
    1.86      val (leftT, rightT) = (fastype_of left, fastype_of right);
    1.87      val prodT = HOLogic.mk_prodT (leftT, rightT);
    1.88 -    val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    1.89 +    val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
    1.90    in
    1.91 -    Const (istuple_consN, isomT --> leftT --> rightT --> prodT) $
    1.92 +    Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $
    1.93        Const (fst tuple_istuple, isomT) $ left $ right
    1.94    end;
    1.95  
    1.96 -fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) =
    1.97 -      if ic = istuple_consN then (left, right)
    1.98 -      else raise TERM ("dest_cons_tuple", [v])
    1.99 -  | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
   1.100 +fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   1.101 +  | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
   1.102  
   1.103  fun add_istuple_type (name, alphas) (leftT, rightT) thy =
   1.104    let
   1.105 @@ -153,8 +136,9 @@
   1.106      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
   1.107      val isomT = fastype_of body;
   1.108      val isom_bind = Binding.name (name ^ isomN);
   1.109 -    val isom = Const (Sign.full_name typ_thy isom_bind, isomT);
   1.110 -    val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   1.111 +    val isom_name = Sign.full_name typ_thy isom_bind;
   1.112 +    val isom = Const (isom_name, isomT);
   1.113 +    val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body));
   1.114  
   1.115      val ([isom_def], cdef_thy) =
   1.116        typ_thy
   1.117 @@ -162,38 +146,36 @@
   1.118        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   1.119  
   1.120      val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   1.121 -    val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT);
   1.122 +    val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT);
   1.123  
   1.124      val thm_thy =
   1.125        cdef_thy
   1.126 -      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (constname isom, istuple))
   1.127 +      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
   1.128        |> Sign.parent_path;
   1.129    in
   1.130 -    (isom, cons $ isom, thm_thy)
   1.131 +    ((isom, cons $ isom), thm_thy)
   1.132    end;
   1.133  
   1.134 -fun istuple_intros_tac thy =
   1.135 -  let
   1.136 -    val isthms = IsTupleThms.get thy;
   1.137 -    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   1.138 -    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) =>
   1.139 -      let
   1.140 -        val goal' = Envir.beta_eta_contract goal;
   1.141 -        val isom =
   1.142 -          (case goal' of
   1.143 -            Const tp $ (Const pr $ Const is) =>
   1.144 -              if fst tp = "Trueprop" andalso fst pr = istuple_constN
   1.145 -              then Const is
   1.146 -              else err "unexpected goal predicate" goal'
   1.147 -          | _ => err "unexpected goal format" goal');
   1.148 -        val isthm =
   1.149 -          (case Symtab.lookup isthms (constname isom) of
   1.150 -            SOME isthm => isthm
   1.151 -          | NONE => err "no thm found for constant" isom);
   1.152 -      in rtac isthm n end);
   1.153 -  in
   1.154 -    fn n => resolve_from_net_tac istuple_intros n THEN use_istuple_thm_tac n
   1.155 -  end;
   1.156 +val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
   1.157 +  CSUBGOAL (fn (cgoal, i) =>
   1.158 +    let
   1.159 +      val thy = Thm.theory_of_cterm cgoal;
   1.160 +      val goal = Thm.term_of cgoal;
   1.161 +
   1.162 +      val isthms = IsTupleThms.get thy;
   1.163 +      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   1.164 +
   1.165 +      val goal' = Envir.beta_eta_contract goal;
   1.166 +      val is =
   1.167 +        (case goal' of
   1.168 +          Const (@{const_name Trueprop}, _) $
   1.169 +            (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
   1.170 +        | _ => err "unexpected goal format" goal');
   1.171 +      val isthm =
   1.172 +        (case Symtab.lookup isthms (#1 is) of
   1.173 +          SOME isthm => isthm
   1.174 +        | NONE => err "no thm found for constant" (Const is));
   1.175 +    in rtac isthm i end);
   1.176  
   1.177  end;
   1.178  
   1.179 @@ -246,9 +228,7 @@
   1.180  val ext_typeN = "_ext_type";
   1.181  val inner_typeN = "_inner_type";
   1.182  val extN ="_ext";
   1.183 -val ext_dest = "_sel";
   1.184  val updateN = "_update";
   1.185 -val updN = "_upd";
   1.186  val makeN = "make";
   1.187  val fields_selN = "fields";
   1.188  val extendN = "extend";
   1.189 @@ -274,8 +254,6 @@
   1.190  
   1.191  (* syntax *)
   1.192  
   1.193 -fun prune n xs = Library.drop (n, xs);
   1.194 -
   1.195  val Trueprop = HOLogic.mk_Trueprop;
   1.196  fun All xs t = Term.list_all_free (xs, t);
   1.197  
   1.198 @@ -326,8 +304,7 @@
   1.199        | SOME c => ((c, Ts), List.last Ts))
   1.200    | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
   1.201  
   1.202 -fun is_recT T =
   1.203 -  (case try dest_recT T of NONE => false | SOME _ => true);
   1.204 +val is_recT = can dest_recT;
   1.205  
   1.206  fun dest_recTs T =
   1.207    let val ((c, Ts), U) = dest_recT T
   1.208 @@ -773,7 +750,7 @@
   1.209                      val types = map snd flds';
   1.210                      val (args, rest) = splitargs (map fst flds') fargs;
   1.211                      val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
   1.212 -                    val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0;
   1.213 +                    val midx = fold Term.maxidx_typ argtypes 0;
   1.214                      val varifyT = varifyT midx;
   1.215                      val vartypes = map varifyT types;
   1.216  
   1.217 @@ -1033,24 +1010,19 @@
   1.218  
   1.219  (** record simprocs **)
   1.220  
   1.221 -val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
   1.222 -
   1.223 -
   1.224  fun quick_and_dirty_prove stndrd thy asms prop tac =
   1.225 -  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
   1.226 +  if ! quick_and_dirty then
   1.227      Goal.prove (ProofContext.init thy) [] []
   1.228        (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
   1.229 -      (K (SkipProof.cheat_tac @{theory HOL}))
   1.230 +      (K (Skip_Proof.cheat_tac @{theory HOL}))
   1.231        (*Drule.standard can take quite a while for large records, thats why
   1.232          we varify the proposition manually here.*)
   1.233    else
   1.234      let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
   1.235 -    in if stndrd then standard prf else prf end;
   1.236 +    in if stndrd then Drule.standard prf else prf end;
   1.237  
   1.238  fun quick_and_dirty_prf noopt opt () =
   1.239 -  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
   1.240 -  then noopt ()
   1.241 -  else opt ();
   1.242 +  if ! quick_and_dirty then noopt () else opt ();
   1.243  
   1.244  fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   1.245    (case get_updates thy u of
   1.246 @@ -1059,11 +1031,11 @@
   1.247  
   1.248  fun mk_comp f g =
   1.249    let
   1.250 -    val x = fastype_of g;
   1.251 -    val a = domain_type x;
   1.252 -    val b = range_type x;
   1.253 -    val c = range_type (fastype_of f);
   1.254 -    val T = (b --> c) --> ((a --> b) --> (a --> c))
   1.255 +    val X = fastype_of g;
   1.256 +    val A = domain_type X;
   1.257 +    val B = range_type X;
   1.258 +    val C = range_type (fastype_of f);
   1.259 +    val T = (B --> C) --> (A --> B) --> A --> C;
   1.260    in Const ("Fun.comp", T) $ f $ g end;
   1.261  
   1.262  fun mk_comp_id f =
   1.263 @@ -1073,7 +1045,7 @@
   1.264  fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   1.265    | get_upd_funs _ = [];
   1.266  
   1.267 -fun get_accupd_simps thy term defset intros_tac =
   1.268 +fun get_accupd_simps thy term defset =
   1.269    let
   1.270      val (acc, [body]) = strip_comb term;
   1.271      val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
   1.272 @@ -1089,18 +1061,17 @@
   1.273          val othm =
   1.274            Goal.prove (ProofContext.init thy) [] [] prop
   1.275              (fn _ =>
   1.276 -              EVERY
   1.277 -               [simp_tac defset 1,
   1.278 -                REPEAT_DETERM (intros_tac 1),
   1.279 -                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
   1.280 +              simp_tac defset 1 THEN
   1.281 +              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.282 +              TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
   1.283          val dest =
   1.284            if is_sel_upd_pair thy acc upd
   1.285            then o_eq_dest
   1.286            else o_eq_id_dest;
   1.287 -      in standard (othm RS dest) end;
   1.288 +      in Drule.standard (othm RS dest) end;
   1.289    in map get_simp upd_funs end;
   1.290  
   1.291 -fun get_updupd_simp thy defset intros_tac u u' comp =
   1.292 +fun get_updupd_simp thy defset u u' comp =
   1.293    let
   1.294      val f = Free ("f", domain_type (fastype_of u));
   1.295      val f' = Free ("f'", domain_type (fastype_of u'));
   1.296 @@ -1113,18 +1084,17 @@
   1.297      val othm =
   1.298        Goal.prove (ProofContext.init thy) [] [] prop
   1.299          (fn _ =>
   1.300 -          EVERY
   1.301 -           [simp_tac defset 1,
   1.302 -            REPEAT_DETERM (intros_tac 1),
   1.303 -            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
   1.304 +          simp_tac defset 1 THEN
   1.305 +          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.306 +          TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   1.307      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   1.308 -  in standard (othm RS dest) end;
   1.309 -
   1.310 -fun get_updupd_simps thy term defset intros_tac =
   1.311 +  in Drule.standard (othm RS dest) end;
   1.312 +
   1.313 +fun get_updupd_simps thy term defset =
   1.314    let
   1.315      val upd_funs = get_upd_funs term;
   1.316      val cname = fst o dest_Const;
   1.317 -    fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
   1.318 +    fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
   1.319      fun build_swaps_to_eq _ [] swaps = swaps
   1.320        | build_swaps_to_eq upd (u :: us) swaps =
   1.321            let
   1.322 @@ -1148,14 +1118,10 @@
   1.323  fun prove_unfold_defs thy ex_simps ex_simprs prop =
   1.324    let
   1.325      val defset = get_sel_upd_defs thy;
   1.326 -    val in_tac = IsTupleSupport.istuple_intros_tac thy;
   1.327      val prop' = Envir.beta_eta_contract prop;
   1.328      val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
   1.329      val (_, args) = strip_comb lhs;
   1.330 -    val simps =
   1.331 -      if length args = 1
   1.332 -      then get_accupd_simps thy lhs defset in_tac
   1.333 -      else get_updupd_simps thy lhs defset in_tac;
   1.334 +    val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
   1.335    in
   1.336      Goal.prove (ProofContext.init thy) [] [] prop'
   1.337        (fn _ =>
   1.338 @@ -1246,17 +1212,14 @@
   1.339  
   1.340  fun get_upd_acc_cong_thm upd acc thy simpset =
   1.341    let
   1.342 -    val in_tac = IsTupleSupport.istuple_intros_tac thy;
   1.343 -
   1.344 -    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
   1.345 -    val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.346 +    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
   1.347 +    val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.348    in
   1.349      Goal.prove (ProofContext.init thy) [] [] prop
   1.350        (fn _ =>
   1.351 -        EVERY
   1.352 -         [simp_tac simpset 1,
   1.353 -          REPEAT_DETERM (in_tac 1),
   1.354 -          TRY (resolve_tac [updacc_cong_idI] 1)])
   1.355 +        simp_tac simpset 1 THEN
   1.356 +        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.357 +        TRY (resolve_tac [updacc_cong_idI] 1))
   1.358    end;
   1.359  
   1.360  
   1.361 @@ -1312,10 +1275,11 @@
   1.362              val ss = get_sel_upd_defs thy;
   1.363              val uathm = get_upd_acc_cong_thm upd acc thy ss;
   1.364            in
   1.365 -            [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
   1.366 +           [Drule.standard (uathm RS updacc_noopE),
   1.367 +            Drule.standard (uathm RS updacc_noop_compE)]
   1.368            end;
   1.369  
   1.370 -        (*If f is constant then (f o g) = f. we know that K_skeleton
   1.371 +        (*If f is constant then (f o g) = f.  We know that K_skeleton
   1.372            only returns constant abstractions thus when we see an
   1.373            abstraction we can discard inner updates.*)
   1.374          fun add_upd (f as Abs _) fs = [f]
   1.375 @@ -1376,7 +1340,7 @@
   1.376  
   1.377  (* record_eq_simproc *)
   1.378  
   1.379 -(*Looks up the most specific record-equality.
   1.380 +(*Look up the most specific record-equality.
   1.381  
   1.382   Note on efficiency:
   1.383   Testing equality of records boils down to the test of equality of all components.
   1.384 @@ -1482,18 +1446,18 @@
   1.385    P t = 0: do not split
   1.386    P t = ~1: completely split
   1.387    P t > 0: split up to given bound of record extensions.*)
   1.388 -fun record_split_simp_tac thms P i st =
   1.389 +fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
   1.390    let
   1.391 -    val thy = Thm.theory_of_thm st;
   1.392 +    val thy = Thm.theory_of_cterm cgoal;
   1.393 +
   1.394 +    val goal = term_of cgoal;
   1.395 +    val frees = filter (is_recT o #2) (Term.add_frees goal []);
   1.396  
   1.397      val has_rec = exists_Const
   1.398        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.399            (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
   1.400          | _ => false);
   1.401  
   1.402 -    val goal = nth (Thm.prems_of st) (i - 1);    (* FIXME SUBGOAL *)
   1.403 -    val frees = filter (is_recT o type_of) (OldTerm.term_frees goal);
   1.404 -
   1.405      fun mk_split_free_tac free induct_thm i =
   1.406        let
   1.407          val cfree = cterm_of thy free;
   1.408 @@ -1501,61 +1465,58 @@
   1.409          val crec = cterm_of thy r;
   1.410          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   1.411        in
   1.412 -        EVERY
   1.413 -         [simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i,
   1.414 -          rtac thm i,
   1.415 -          simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   1.416 +        simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
   1.417 +        rtac thm i THEN
   1.418 +        simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
   1.419        end;
   1.420  
   1.421 -    fun split_free_tac P i (free as Free (_, T)) =
   1.422 -          (case rec_id ~1 T of
   1.423 -            "" => NONE
   1.424 -          | _ =>
   1.425 -              let val split = P free in
   1.426 -                if split <> 0 then
   1.427 -                  (case get_splits thy (rec_id split T) of
   1.428 -                    NONE => NONE
   1.429 -                  | SOME (_, _, _, induct_thm) =>
   1.430 -                      SOME (mk_split_free_tac free induct_thm i))
   1.431 -                else NONE
   1.432 -              end)
   1.433 -      | split_free_tac _ _ _ = NONE;
   1.434 -
   1.435 -    val split_frees_tacs = map_filter (split_free_tac P i) frees;
   1.436 +    val split_frees_tacs =
   1.437 +      frees |> map_filter (fn (x, T) =>
   1.438 +        (case rec_id ~1 T of
   1.439 +          "" => NONE
   1.440 +        | _ =>
   1.441 +            let
   1.442 +              val free = Free (x, T);
   1.443 +              val split = P free;
   1.444 +            in
   1.445 +              if split <> 0 then
   1.446 +                (case get_splits thy (rec_id split T) of
   1.447 +                  NONE => NONE
   1.448 +                | SOME (_, _, _, induct_thm) =>
   1.449 +                    SOME (mk_split_free_tac free induct_thm i))
   1.450 +              else NONE
   1.451 +            end));
   1.452  
   1.453      val simprocs = if has_rec goal then [record_split_simproc P] else [];
   1.454      val thms' = K_comp_convs @ thms;
   1.455    in
   1.456 -    st |>
   1.457 -      (EVERY split_frees_tacs THEN
   1.458 -        Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
   1.459 -  end handle Empty => Seq.empty;
   1.460 +    EVERY split_frees_tacs THEN
   1.461 +    Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
   1.462 +  end);
   1.463  
   1.464  
   1.465  (* record_split_tac *)
   1.466  
   1.467  (*Split all records in the goal, which are quantified by ! or !!.*)
   1.468 -fun record_split_tac i st =
   1.469 +val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   1.470    let
   1.471 +    val goal = term_of cgoal;
   1.472 +
   1.473      val has_rec = exists_Const
   1.474        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.475            (s = "all" orelse s = "All") andalso is_recT T
   1.476          | _ => false);
   1.477  
   1.478 -    val goal = nth (Thm.prems_of st) (i - 1);  (* FIXME SUBGOAL *)
   1.479 -
   1.480      fun is_all t =
   1.481        (case t of
   1.482          Const (quantifier, _) $ _ =>
   1.483            if quantifier = "All" orelse quantifier = "all" then ~1 else 0
   1.484        | _ => 0);
   1.485 -
   1.486    in
   1.487      if has_rec goal then
   1.488 -      Simplifier.full_simp_tac
   1.489 -        (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
   1.490 -    else Seq.empty
   1.491 -  end handle Subscript => Seq.empty;     (* FIXME SUBGOAL *)
   1.492 +      Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
   1.493 +    else no_tac
   1.494 +  end);
   1.495  
   1.496  
   1.497  (* wrapper *)
   1.498 @@ -1605,13 +1566,14 @@
   1.499    (or on s if there are no parameters).
   1.500    Instatiation of record variable (and predicate) in rule is calculated to
   1.501    avoid problems with higher order unification.*)
   1.502 -fun try_param_tac s rule i st =
   1.503 +fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
   1.504    let
   1.505 -    val cert = cterm_of (Thm.theory_of_thm st);
   1.506 -    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
   1.507 +    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
   1.508 +
   1.509 +    val g = Thm.term_of cgoal;
   1.510      val params = Logic.strip_params g;
   1.511      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
   1.512 -    val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
   1.513 +    val rule' = Thm.lift_rule cgoal rule;
   1.514      val (P, ys) = strip_comb (HOLogic.dest_Trueprop
   1.515        (Logic.strip_assums_concl (prop_of rule')));
   1.516      (*ca indicates if rule is a case analysis or induction rule*)
   1.517 @@ -1621,23 +1583,23 @@
   1.518            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   1.519        | [x] => (head_of x, false));
   1.520      val rule'' = cterm_instantiate (map (pairself cert)
   1.521 -      (case (rev params) of
   1.522 +      (case rev params of
   1.523          [] =>
   1.524 -          (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
   1.525 +          (case AList.lookup (op =) (Term.add_frees g []) s of
   1.526              NONE => sys_error "try_param_tac: no such variable"
   1.527            | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
   1.528        | (_, T) :: _ =>
   1.529            [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
   1.530              (x, list_abs (params, Bound 0))])) rule';
   1.531 -  in compose_tac (false, rule'', nprems_of rule) i st end;
   1.532 +  in compose_tac (false, rule'', nprems_of rule) i end);
   1.533  
   1.534  
   1.535  fun extension_definition name fields alphas zeta moreT more vars thy =
   1.536    let
   1.537      val base = Long_Name.base_name;
   1.538 -    val fieldTs = (map snd fields);
   1.539 +    val fieldTs = map snd fields;
   1.540      val alphas_zeta = alphas @ [zeta];
   1.541 -    val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
   1.542 +    val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
   1.543      val extT_name = suffix ext_typeN name
   1.544      val extT = Type (extT_name, alphas_zetaTs);
   1.545      val fields_moreTs = fieldTs @ [moreT];
   1.546 @@ -1652,7 +1614,7 @@
   1.547        let
   1.548          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   1.549          val nm = suffix suff (Long_Name.base_name name);
   1.550 -        val (_, cons, thy') =
   1.551 +        val ((_, cons), thy') =
   1.552            IsTupleSupport.add_istuple_type
   1.553              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   1.554        in
   1.555 @@ -1717,7 +1679,6 @@
   1.556      val ext = mk_ext vars_more;
   1.557      val s = Free (rN, extT);
   1.558      val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   1.559 -    val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   1.560  
   1.561      val inject_prop =
   1.562        let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
   1.563 @@ -1743,11 +1704,11 @@
   1.564        simplify HOL_ss
   1.565          (prove_standard [] inject_prop
   1.566            (fn _ =>
   1.567 -            EVERY
   1.568 -             [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   1.569 -              REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
   1.570 -                intros_tac 1 ORELSE
   1.571 -                resolve_tac [refl] 1)]));
   1.572 +            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.573 +            REPEAT_DETERM
   1.574 +              (rtac refl_conj_eq 1 ORELSE
   1.575 +                IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.576 +                rtac refl 1)));
   1.577  
   1.578      val inject = timeit_msg "record extension inject proof:" inject_prf;
   1.579  
   1.580 @@ -1755,7 +1716,7 @@
   1.581        to prove other theorems. We haven't given names to the accessors
   1.582        f, g etc yet however, so we generate an ext structure with
   1.583        free variables as all arguments and allow the introduction tactic to
   1.584 -      operate on it as far as it can. We then use standard to convert
   1.585 +      operate on it as far as it can. We then use Drule.standard to convert
   1.586        the free variables into unifiable variables and unify them with
   1.587        (roughly) the definition of the accessor.*)
   1.588      fun surject_prf () =
   1.589 @@ -1764,10 +1725,10 @@
   1.590          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   1.591          val tactic1 =
   1.592            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.593 -          REPEAT_ALL_NEW intros_tac 1;
   1.594 +          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
   1.595          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   1.596 -        val [halfway] = Seq.list_of (tactic1 start);    (* FIXME Seq.lift_of ?? *)
   1.597 -        val [surject] = Seq.list_of (tactic2 (standard halfway));    (* FIXME Seq.lift_of ?? *)
   1.598 +        val [halfway] = Seq.list_of (tactic1 start);
   1.599 +        val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   1.600        in
   1.601          surject
   1.602        end;
   1.603 @@ -1776,21 +1737,20 @@
   1.604      fun split_meta_prf () =
   1.605        prove_standard [] split_meta_prop
   1.606          (fn _ =>
   1.607 -          EVERY
   1.608 -           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.609 -            etac meta_allE 1, atac 1,
   1.610 -            rtac (prop_subst OF [surject]) 1,
   1.611 -            REPEAT (etac meta_allE 1), atac 1]);
   1.612 +          EVERY1
   1.613 +           [rtac equal_intr_rule, Goal.norm_hhf_tac,
   1.614 +            etac meta_allE, atac,
   1.615 +            rtac (prop_subst OF [surject]),
   1.616 +            REPEAT o etac meta_allE, atac]);
   1.617      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   1.618  
   1.619      fun induct_prf () =
   1.620        let val (assm, concl) = induct_prop in
   1.621          prove_standard [assm] concl
   1.622            (fn {prems, ...} =>
   1.623 -            EVERY
   1.624 -             [cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1,
   1.625 -              resolve_tac prems 2,
   1.626 -              asm_simp_tac HOL_ss 1])
   1.627 +            cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
   1.628 +            resolve_tac prems 2 THEN
   1.629 +            asm_simp_tac HOL_ss 1)
   1.630        end;
   1.631      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.632  
   1.633 @@ -1873,8 +1833,8 @@
   1.634      val names = map fst fields;
   1.635      val extN = full bname;
   1.636      val types = map snd fields;
   1.637 -    val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
   1.638 -    val alphas_ext = alphas inter alphas_fields;
   1.639 +    val alphas_fields = fold Term.add_tfree_namesT types [];
   1.640 +    val alphas_ext = inter (op =) alphas_fields alphas;
   1.641      val len = length fields;
   1.642      val variants =
   1.643        Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
   1.644 @@ -1915,20 +1875,23 @@
   1.645      val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
   1.646      val extension_id = implode extension_names;
   1.647  
   1.648 -    fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
   1.649 +    fun rec_schemeT n = mk_recordT (map #extension (Library.drop (n, parents))) extT;
   1.650      val rec_schemeT0 = rec_schemeT 0;
   1.651  
   1.652      fun recT n =
   1.653 -      let val (c, Ts) = extension
   1.654 -      in mk_recordT (map #extension (prune n parents)) (Type (c, subst_last HOLogic.unitT Ts)) end;
   1.655 +      let val (c, Ts) = extension in
   1.656 +        mk_recordT (map #extension (Library.drop (n, parents)))
   1.657 +          (Type (c, subst_last HOLogic.unitT Ts))
   1.658 +      end;
   1.659      val recT0 = recT 0;
   1.660  
   1.661      fun mk_rec args n =
   1.662        let
   1.663          val (args', more) = chop_last args;
   1.664 -        fun mk_ext' (((name, T), args), more) = mk_ext (name, T) (args @ [more]);
   1.665 +        fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
   1.666          fun build Ts =
   1.667 -          List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')));
   1.668 +          fold_rev mk_ext' (Library.drop (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
   1.669 +            more;
   1.670        in
   1.671          if more = HOLogic.unit
   1.672          then build (map recT (0 upto parent_len))
   1.673 @@ -1984,7 +1947,6 @@
   1.674          (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
   1.675  
   1.676      val ext_defs = ext_def :: map #extdef parents;
   1.677 -    val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
   1.678  
   1.679      (*Theorems from the istuple intros.
   1.680        This is complex enough to deserve a full comment.
   1.681 @@ -2011,8 +1973,8 @@
   1.682          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   1.683          val tactic =
   1.684            simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
   1.685 -          REPEAT (intros_tac 1 ORELSE terminal);
   1.686 -        val updaccs = Seq.list_of (tactic init_thm);  (* FIXME Seq.lift_of *)
   1.687 +          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
   1.688 +        val updaccs = Seq.list_of (tactic init_thm);
   1.689        in
   1.690          (updaccs RL [updacc_accessor_eqE],
   1.691           updaccs RL [updacc_updator_eqE],
   1.692 @@ -2021,7 +1983,7 @@
   1.693      val (accessor_thms, updator_thms, upd_acc_cong_assists) =
   1.694        timeit_msg "record getting tree access/updates:" get_access_update_thms;
   1.695  
   1.696 -    fun lastN xs = List.drop (xs, parent_fields_len);
   1.697 +    fun lastN xs = Library.drop (parent_fields_len, xs);
   1.698  
   1.699      (*selectors*)
   1.700      fun mk_sel_spec ((c, T), thm) =
   1.701 @@ -2135,15 +2097,13 @@
   1.702           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
   1.703        end;
   1.704  
   1.705 -    (* FIXME eliminate old List.foldr *)
   1.706 -
   1.707      val split_object_prop =
   1.708 -      let fun ALL vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_all (v, T, t)) t vs
   1.709 -      in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) end;
   1.710 +      let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
   1.711 +      in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
   1.712  
   1.713      val split_ex_prop =
   1.714 -      let fun EX vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_exists (v, T, t)) t vs
   1.715 -      in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) end;
   1.716 +      let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
   1.717 +      in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
   1.718  
   1.719      (*equality*)
   1.720      val equality_prop =
   1.721 @@ -2168,14 +2128,14 @@
   1.722      fun sel_convs_prf () =
   1.723        map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
   1.724      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
   1.725 -    fun sel_convs_standard_prf () = map standard sel_convs
   1.726 +    fun sel_convs_standard_prf () = map Drule.standard sel_convs
   1.727      val sel_convs_standard =
   1.728        timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
   1.729  
   1.730      fun upd_convs_prf () =
   1.731        map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
   1.732      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
   1.733 -    fun upd_convs_standard_prf () = map standard upd_convs
   1.734 +    fun upd_convs_standard_prf () = map Drule.standard upd_convs
   1.735      val upd_convs_standard =
   1.736        timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
   1.737  
   1.738 @@ -2183,7 +2143,7 @@
   1.739        let
   1.740          val symdefs = map symmetric (sel_defs @ upd_defs);
   1.741          val fold_ss = HOL_basic_ss addsimps symdefs;
   1.742 -        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
   1.743 +        val ua_congs = map (Drule.standard o simplify fold_ss) upd_acc_cong_assists;
   1.744        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   1.745      val (fold_congs, unfold_congs) =
   1.746        timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   1.747 @@ -2194,8 +2154,7 @@
   1.748        prove_standard [] induct_scheme_prop
   1.749          (fn _ =>
   1.750            EVERY
   1.751 -           [if null parent_induct
   1.752 -            then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.753 +           [if null parent_induct then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.754              try_param_tac rN ext_induct 1,
   1.755              asm_simp_tac HOL_basic_ss 1]);
   1.756      val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
   1.757 @@ -2217,18 +2176,18 @@
   1.758              [(cterm_of defs_thy Pvar, cterm_of defs_thy
   1.759                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
   1.760              induct_scheme;
   1.761 -        in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   1.762 +        in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   1.763  
   1.764      fun cases_scheme_prf_noopt () =
   1.765        prove_standard [] cases_scheme_prop
   1.766          (fn _ =>
   1.767 -          EVERY
   1.768 -           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   1.769 -            try_param_tac rN induct_scheme 1,
   1.770 -            rtac impI 1,
   1.771 -            REPEAT (etac allE 1),
   1.772 -            etac mp 1,
   1.773 -            rtac refl 1]);
   1.774 +          EVERY1
   1.775 +           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]),
   1.776 +            try_param_tac rN induct_scheme,
   1.777 +            rtac impI,
   1.778 +            REPEAT o etac allE,
   1.779 +            etac mp,
   1.780 +            rtac refl]);
   1.781      val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
   1.782      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
   1.783  
   1.784 @@ -2249,20 +2208,22 @@
   1.785              EVERY
   1.786               [rtac surject_assist_idE 1,
   1.787                simp_tac init_ss 1,
   1.788 -              REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   1.789 +              REPEAT
   1.790 +                (IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.791 +                  (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   1.792        end;
   1.793      val surjective = timeit_msg "record surjective proof:" surjective_prf;
   1.794  
   1.795      fun split_meta_prf () =
   1.796        prove false [] split_meta_prop
   1.797          (fn _ =>
   1.798 -          EVERY
   1.799 -           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.800 -            etac meta_allE 1, atac 1,
   1.801 -            rtac (prop_subst OF [surjective]) 1,
   1.802 -            REPEAT (etac meta_allE 1), atac 1]);
   1.803 +          EVERY1
   1.804 +           [rtac equal_intr_rule, Goal.norm_hhf_tac,
   1.805 +            etac meta_allE, atac,
   1.806 +            rtac (prop_subst OF [surjective]),
   1.807 +            REPEAT o etac meta_allE, atac]);
   1.808      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
   1.809 -    fun split_meta_standardise () = standard split_meta;
   1.810 +    fun split_meta_standardise () = Drule.standard split_meta;
   1.811      val split_meta_standard =
   1.812        timeit_msg "record split_meta standard:" split_meta_standardise;
   1.813  
   1.814 @@ -2287,15 +2248,15 @@
   1.815            |> equal_elim (symmetric split_meta') (*!!r. P r*)
   1.816            |> meta_to_obj_all                    (*All r. P r*)
   1.817            |> implies_intr cr                    (* 2 ==> 1 *)
   1.818 -     in standard (thr COMP (thl COMP iffI)) end;
   1.819 +     in Drule.standard (thr COMP (thl COMP iffI)) end;
   1.820  
   1.821      fun split_object_prf_noopt () =
   1.822        prove_standard [] split_object_prop
   1.823          (fn _ =>
   1.824 -          EVERY
   1.825 -           [rtac iffI 1,
   1.826 -            REPEAT (rtac allI 1), etac allE 1, atac 1,
   1.827 -            rtac allI 1, rtac induct_scheme 1, REPEAT (etac allE 1), atac 1]);
   1.828 +          EVERY1
   1.829 +           [rtac iffI,
   1.830 +            REPEAT o rtac allI, etac allE, atac,
   1.831 +            rtac allI, rtac induct_scheme, REPEAT o etac allE, atac]);
   1.832  
   1.833      val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
   1.834      val split_object = timeit_msg "record split_object proof:" split_object_prf;
   1.835 @@ -2400,7 +2361,7 @@
   1.836      val init_env =
   1.837        (case parent of
   1.838          NONE => []
   1.839 -      | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types);
   1.840 +      | SOME (types, _) => fold Term.add_tfreesT types []);
   1.841  
   1.842  
   1.843      (* fields *)