src/HOL/Tools/record.ML
changeset 32799 7478ea535416
parent 32770 c6e6a4665ff5
child 32808 0059238fe4bc
     1.1 --- a/src/HOL/Tools/record.ML	Thu Oct 01 00:32:00 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 01 01:03:36 2009 +0200
     1.3 @@ -202,22 +202,18 @@
     1.4  struct
     1.5  
     1.6  val eq_reflection = @{thm eq_reflection};
     1.7 -val Pair_eq = @{thm Product_Type.prod.inject};
     1.8  val atomize_all = @{thm HOL.atomize_all};
     1.9  val atomize_imp = @{thm HOL.atomize_imp};
    1.10  val meta_allE = @{thm Pure.meta_allE};
    1.11  val prop_subst = @{thm prop_subst};
    1.12 -val Pair_sel_convs = [fst_conv, snd_conv];
    1.13  val K_record_comp = @{thm K_record_comp};
    1.14  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    1.15 -val transitive_thm = @{thm transitive};
    1.16  val o_assoc = @{thm o_assoc};
    1.17  val id_apply = @{thm id_apply};
    1.18  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    1.19  val Not_eq_iff = @{thm Not_eq_iff};
    1.20  
    1.21  val refl_conj_eq = @{thm refl_conj_eq};
    1.22 -val meta_all_sameI = @{thm meta_all_sameI};
    1.23  
    1.24  val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    1.25  val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    1.26 @@ -250,7 +246,6 @@
    1.27  val ext_typeN = "_ext_type";
    1.28  val inner_typeN = "_inner_type";
    1.29  val extN ="_ext";
    1.30 -val casesN = "_cases";
    1.31  val ext_dest = "_sel";
    1.32  val updateN = "_update";
    1.33  val updN = "_upd";
    1.34 @@ -259,10 +254,6 @@
    1.35  val extendN = "extend";
    1.36  val truncateN = "truncate";
    1.37  
    1.38 -(*see typedef.ML*)
    1.39 -val RepN = "Rep_";
    1.40 -val AbsN = "Abs_";
    1.41 -
    1.42  
    1.43  
    1.44  (*** utilities ***)
    1.45 @@ -273,24 +264,6 @@
    1.46    let fun varify (a, S) = TVar ((a, midx + 1), S);
    1.47    in map_type_tfree varify end;
    1.48  
    1.49 -fun domain_type' T =
    1.50 -  domain_type T handle Match => T;
    1.51 -
    1.52 -fun range_type' T =
    1.53 -  range_type T handle Match => T;
    1.54 -
    1.55 -
    1.56 -(* messages *)  (* FIXME proper context *)
    1.57 -
    1.58 -fun trace_thm str thm =
    1.59 -  tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm));
    1.60 -
    1.61 -fun trace_thms str thms =
    1.62 -  (tracing str; map (trace_thm "") thms);
    1.63 -
    1.64 -fun trace_term str t =
    1.65 -  tracing (str ^ Syntax.string_of_term_global Pure.thy t);
    1.66 -
    1.67  
    1.68  (* timing *)
    1.69  
    1.70 @@ -302,7 +275,6 @@
    1.71  (* syntax *)
    1.72  
    1.73  fun prune n xs = Library.drop (n, xs);
    1.74 -fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
    1.75  
    1.76  val Trueprop = HOLogic.mk_Trueprop;
    1.77  fun All xs t = Term.list_all_free (xs, t);
    1.78 @@ -311,22 +283,10 @@
    1.79  infix 0 :== ===;
    1.80  infixr 0 ==>;
    1.81  
    1.82 -val (op $$) = Term.list_comb;
    1.83 -val (op :==) = PrimitiveDefs.mk_defpair;
    1.84 -val (op ===) = Trueprop o HOLogic.mk_eq;
    1.85 -val (op ==>) = Logic.mk_implies;
    1.86 -
    1.87 -
    1.88 -(* morphisms *)
    1.89 -
    1.90 -fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
    1.91 -fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
    1.92 -
    1.93 -fun mk_Rep name repT absT =
    1.94 -  Const (suffix ext_typeN (prefix_base RepN name), absT --> repT);
    1.95 -
    1.96 -fun mk_Abs name repT absT =
    1.97 -  Const (mk_AbsN name, repT --> absT);
    1.98 +val op $$ = Term.list_comb;
    1.99 +val op :== = PrimitiveDefs.mk_defpair;
   1.100 +val op === = Trueprop o HOLogic.mk_eq;
   1.101 +val op ==> = Logic.mk_implies;
   1.102  
   1.103  
   1.104  (* constructor *)
   1.105 @@ -338,15 +298,6 @@
   1.106    in list_comb (Const (mk_extC (name, T) Ts), ts) end;
   1.107  
   1.108  
   1.109 -(* cases *)
   1.110 -
   1.111 -fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT);
   1.112 -
   1.113 -fun mk_cases (name, T, vT) f =
   1.114 -  let val Ts = binder_types (fastype_of f)
   1.115 -  in Const (mk_casesC (name, T, vT) Ts) $ f end;
   1.116 -
   1.117 -
   1.118  (* selector *)
   1.119  
   1.120  fun mk_selC sT (c, T) = (c, sT --> T);
   1.121 @@ -369,7 +320,7 @@
   1.122  
   1.123  (* types *)
   1.124  
   1.125 -fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) =
   1.126 +fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
   1.127        (case try (unsuffix ext_typeN) c_ext_type of
   1.128          NONE => raise TYPE ("Record.dest_recT", [typ], [])
   1.129        | SOME c => ((c, Ts), List.last Ts))
   1.130 @@ -549,8 +500,6 @@
   1.131  
   1.132  val get_simpset = get_ss_with_context #simpset;
   1.133  val get_sel_upd_defs = get_ss_with_context #defset;
   1.134 -val get_foldcong_ss = get_ss_with_context #foldcong;
   1.135 -val get_unfoldcong_ss = get_ss_with_context #unfoldcong;
   1.136  
   1.137  fun get_update_details u thy =
   1.138    let val sel_upd = get_sel_upd thy in
   1.139 @@ -618,8 +567,6 @@
   1.140        extfields fieldext;
   1.141    in RecordsData.put data thy end;
   1.142  
   1.143 -val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
   1.144 -
   1.145  
   1.146  (* access 'splits' *)
   1.147  
   1.148 @@ -659,7 +606,7 @@
   1.149    let
   1.150      val ((name, Ts), moreT) = dest_recT T;
   1.151      val recname =
   1.152 -      let val (nm :: recn :: rst) = rev (Long_Name.explode name)
   1.153 +      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
   1.154        in Long_Name.implode (rev (nm :: rst)) end;
   1.155      val midx = maxidx_of_typs (moreT :: Ts);
   1.156      val varifyT = varifyT midx;
   1.157 @@ -698,7 +645,7 @@
   1.158  
   1.159  (* parent records *)
   1.160  
   1.161 -fun add_parents thy NONE parents = parents
   1.162 +fun add_parents _ NONE parents = parents
   1.163    | add_parents thy (SOME (types, name)) parents =
   1.164        let
   1.165          fun err msg = error (msg ^ " parent record " ^ quote name);
   1.166 @@ -787,7 +734,7 @@
   1.167        | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.168        | splitargs _ _ = ([], []);
   1.169  
   1.170 -    fun mk_ext (fargs as (name, arg) :: _) =
   1.171 +    fun mk_ext (fargs as (name, _) :: _) =
   1.172            (case get_fieldext thy (Sign.intern_const thy name) of
   1.173              SOME (ext, _) =>
   1.174                (case get_extfields thy ext of
   1.175 @@ -816,7 +763,7 @@
   1.176        | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.177        | splitargs _ _ = ([], []);
   1.178  
   1.179 -    fun mk_ext (fargs as (name, arg) :: _) =
   1.180 +    fun mk_ext (fargs as (name, _) :: _) =
   1.181            (case get_fieldext thy (Sign.intern_const thy name) of
   1.182              SOME (ext, alphas) =>
   1.183                (case get_extfields thy ext of
   1.184 @@ -838,7 +785,7 @@
   1.185                      val more' = mk_ext rest;
   1.186                    in
   1.187                      list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
   1.188 -                  end handle TYPE_MATCH =>
   1.189 +                  end handle Type.TYPE_MATCH =>
   1.190                      raise TERM (msg ^ "type is no proper record (extension)", [t]))
   1.191                | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   1.192            | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   1.193 @@ -896,7 +843,7 @@
   1.194            (case k of
   1.195              Abs (_, _, Abs (_, _, t) $ Bound 0) =>
   1.196                if null (loose_bnos t) then t else raise Match
   1.197 -          | Abs (x, _, t) =>
   1.198 +          | Abs (_, _, t) =>
   1.199                if null (loose_bnos t) then t else raise Match
   1.200            | _ => raise Match);
   1.201  
   1.202 @@ -1012,7 +959,7 @@
   1.203                if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
   1.204                then mk_type_abbr subst abbr alphas
   1.205                else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
   1.206 -            end handle TYPE_MATCH => default_tr' ctxt tm)
   1.207 +            end handle Type.TYPE_MATCH => default_tr' ctxt tm)
   1.208            else raise Match (*give print translation of specialised record a chance*)
   1.209        | _ => raise Match)
   1.210      else default_tr' ctxt tm
   1.211 @@ -1045,8 +992,7 @@
   1.212                          val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
   1.213                          val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
   1.214                        in flds'' @ field_lst more end
   1.215 -                      handle TYPE_MATCH => [("", T)]
   1.216 -                        | Library.UnequalLengths => [("", T)])
   1.217 +                      handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)])
   1.218                    | NONE => [("", T)])
   1.219                | NONE => [("", T)])
   1.220            | NONE => [("", T)])
   1.221 @@ -1106,7 +1052,8 @@
   1.222    then noopt ()
   1.223    else opt ();
   1.224  
   1.225 -fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) =
   1.226 +(* FIXME non-standard name for partial identity; rename to check_... (??) *)
   1.227 +fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   1.228    (case get_updates thy u of
   1.229      SOME u_name => u_name = s
   1.230    | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
   1.231 @@ -1130,7 +1077,6 @@
   1.232  fun get_accupd_simps thy term defset intros_tac =
   1.233    let
   1.234      val (acc, [body]) = strip_comb term;
   1.235 -    val recT = domain_type (fastype_of acc);
   1.236      val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
   1.237      fun get_simp upd =
   1.238        let
   1.239 @@ -1140,10 +1086,10 @@
   1.240            if is_sel_upd_pair thy acc upd
   1.241            then mk_comp (Free ("f", T)) acc
   1.242            else mk_comp_id acc;
   1.243 -        val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   1.244 +        val prop = lhs === rhs;
   1.245          val othm =
   1.246            Goal.prove (ProofContext.init thy) [] [] prop
   1.247 -            (fn prems =>
   1.248 +            (fn _ =>
   1.249                EVERY
   1.250                 [simp_tac defset 1,
   1.251                  REPEAT_DETERM (intros_tac 1),
   1.252 @@ -1164,10 +1110,10 @@
   1.253        if comp
   1.254        then u $ mk_comp f f'
   1.255        else mk_comp (u' $ f') (u $ f);
   1.256 -    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   1.257 +    val prop = lhs === rhs;
   1.258      val othm =
   1.259        Goal.prove (ProofContext.init thy) [] [] prop
   1.260 -        (fn prems =>
   1.261 +        (fn _ =>
   1.262            EVERY
   1.263             [simp_tac defset 1,
   1.264              REPEAT_DETERM (intros_tac 1),
   1.265 @@ -1177,11 +1123,10 @@
   1.266  
   1.267  fun get_updupd_simps thy term defset intros_tac =
   1.268    let
   1.269 -    val recT = fastype_of term;
   1.270      val upd_funs = get_upd_funs term;
   1.271      val cname = fst o dest_Const;
   1.272      fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
   1.273 -    fun build_swaps_to_eq upd [] swaps = swaps
   1.274 +    fun build_swaps_to_eq _ [] swaps = swaps
   1.275        | build_swaps_to_eq upd (u :: us) swaps =
   1.276            let
   1.277              val key = (cname u, cname upd);
   1.278 @@ -1192,7 +1137,7 @@
   1.279              if cname u = cname upd then newswaps
   1.280              else build_swaps_to_eq upd us newswaps
   1.281            end;
   1.282 -    fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps)
   1.283 +    fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
   1.284        | swaps_needed (u :: us) prev seen swaps =
   1.285            if Symtab.defined seen (cname u)
   1.286            then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
   1.287 @@ -1201,20 +1146,20 @@
   1.288  
   1.289  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   1.290  
   1.291 -fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
   1.292 +fun prove_unfold_defs thy ex_simps ex_simprs prop =
   1.293    let
   1.294      val defset = get_sel_upd_defs thy;
   1.295      val in_tac = IsTupleSupport.istuple_intros_tac thy;
   1.296      val prop' = Envir.beta_eta_contract prop;
   1.297 -    val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
   1.298 -    val (head, args) = strip_comb lhs;
   1.299 +    val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
   1.300 +    val (_, args) = strip_comb lhs;
   1.301      val simps =
   1.302        if length args = 1
   1.303        then get_accupd_simps thy lhs defset in_tac
   1.304        else get_updupd_simps thy lhs defset in_tac;
   1.305    in
   1.306      Goal.prove (ProofContext.init thy) [] [] prop'
   1.307 -      (fn prems =>
   1.308 +      (fn _ =>
   1.309          simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
   1.310          TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
   1.311    end;
   1.312 @@ -1251,55 +1196,52 @@
   1.313  *)
   1.314  val record_simproc =
   1.315    Simplifier.simproc @{theory HOL} "record_simp" ["x"]
   1.316 -    (fn thy => fn ss => fn t =>
   1.317 +    (fn thy => fn _ => fn t =>
   1.318        (case t of
   1.319 -        (sel as Const (s, Type (_, [domS, rangeS]))) $
   1.320 +        (sel as Const (s, Type (_, [_, rangeS]))) $
   1.321              ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
   1.322 -          if is_selector thy s then
   1.323 -            (case get_updates thy u of
   1.324 -              SOME u_name =>
   1.325 -                let
   1.326 -                  val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
   1.327 -
   1.328 -                  fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
   1.329 -                        (case Symtab.lookup updates u of
   1.330 -                          NONE => NONE
   1.331 -                        | SOME u_name =>
   1.332 -                            if u_name = s then
   1.333 -                              (case mk_eq_terms r of
   1.334 -                                NONE =>
   1.335 -                                  let
   1.336 -                                    val rv = ("r", rT);
   1.337 -                                    val rb = Bound 0;
   1.338 -                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   1.339 -                                  in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
   1.340 -                              | SOME (trm, trm', vars) =>
   1.341 -                                  let
   1.342 -                                    val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
   1.343 -                                  in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
   1.344 -                            else if has_field extfields u_name rangeS orelse
   1.345 -                              has_field extfields s (domain_type kT) then NONE
   1.346 -                            else
   1.347 -                              (case mk_eq_terms r of
   1.348 -                                SOME (trm, trm', vars) =>
   1.349 -                                  let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
   1.350 -                                  in SOME (upd $ kb $ trm, trm', kv :: vars) end
   1.351 -                              | NONE =>
   1.352 -                                  let
   1.353 -                                    val rv = ("r", rT);
   1.354 -                                    val rb = Bound 0;
   1.355 -                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   1.356 -                                  in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
   1.357 -                    | mk_eq_terms r = NONE;
   1.358 -                in
   1.359 -                  (case mk_eq_terms (upd $ k $ r) of
   1.360 -                    SOME (trm, trm', vars) =>
   1.361 -                      SOME
   1.362 -                        (prove_unfold_defs thy ss domS [] []
   1.363 -                          (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
   1.364 -                  | NONE => NONE)
   1.365 -                end
   1.366 -            | NONE => NONE)
   1.367 +          if is_selector thy s andalso is_some (get_updates thy u) then
   1.368 +            let
   1.369 +              val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
   1.370 +
   1.371 +              fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
   1.372 +                    (case Symtab.lookup updates u of
   1.373 +                      NONE => NONE
   1.374 +                    | SOME u_name =>
   1.375 +                        if u_name = s then
   1.376 +                          (case mk_eq_terms r of
   1.377 +                            NONE =>
   1.378 +                              let
   1.379 +                                val rv = ("r", rT);
   1.380 +                                val rb = Bound 0;
   1.381 +                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   1.382 +                              in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
   1.383 +                          | SOME (trm, trm', vars) =>
   1.384 +                              let
   1.385 +                                val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
   1.386 +                              in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
   1.387 +                        else if has_field extfields u_name rangeS orelse
   1.388 +                          has_field extfields s (domain_type kT) then NONE
   1.389 +                        else
   1.390 +                          (case mk_eq_terms r of
   1.391 +                            SOME (trm, trm', vars) =>
   1.392 +                              let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
   1.393 +                              in SOME (upd $ kb $ trm, trm', kv :: vars) end
   1.394 +                          | NONE =>
   1.395 +                              let
   1.396 +                                val rv = ("r", rT);
   1.397 +                                val rb = Bound 0;
   1.398 +                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   1.399 +                              in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
   1.400 +                | mk_eq_terms _ = NONE;
   1.401 +            in
   1.402 +              (case mk_eq_terms (upd $ k $ r) of
   1.403 +                SOME (trm, trm', vars) =>
   1.404 +                  SOME
   1.405 +                    (prove_unfold_defs thy [] []
   1.406 +                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
   1.407 +              | NONE => NONE)
   1.408 +            end
   1.409            else NONE
   1.410        | _ => NONE));
   1.411  
   1.412 @@ -1311,7 +1253,7 @@
   1.413      val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.414    in
   1.415      Goal.prove (ProofContext.init thy) [] [] prop
   1.416 -      (fn prems =>
   1.417 +      (fn _ =>
   1.418          EVERY
   1.419           [simp_tac simpset 1,
   1.420            REPEAT_DETERM (in_tac 1),
   1.421 @@ -1331,7 +1273,7 @@
   1.422    both a more update and an update to a field within it.*)
   1.423  val record_upd_simproc =
   1.424    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   1.425 -    (fn thy => fn ss => fn t =>
   1.426 +    (fn thy => fn _ => fn t =>
   1.427        let
   1.428          (*We can use more-updators with other updators as long
   1.429            as none of the other updators go deeper than any more
   1.430 @@ -1346,7 +1288,7 @@
   1.431                then SOME (if min <= dep then dep else min, max)
   1.432                else NONE;
   1.433  
   1.434 -        fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
   1.435 +        fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
   1.436                (case get_update_details u thy of
   1.437                  SOME (s, dep, ismore) =>
   1.438                    (case include_depth (dep, ismore) (min, max) of
   1.439 @@ -1359,15 +1301,14 @@
   1.440  
   1.441          val (upds, base, baseT) = getupdseq t 0 ~1;
   1.442  
   1.443 -        fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
   1.444 +        fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
   1.445                if s = s' andalso null (loose_bnos tm')
   1.446                  andalso subst_bound (HOLogic.unit, tm') = tm
   1.447                then (true, Abs (n, T, Const (s', T') $ Bound 1))
   1.448                else (false, HOLogic.unit)
   1.449 -          | is_upd_noop s f tm = (false, HOLogic.unit);
   1.450 -
   1.451 -        fun get_noop_simps (upd as Const (u, T))
   1.452 -            (f as Abs (n, T', (acc as Const (s, T'')) $ _)) =
   1.453 +          | is_upd_noop _ _ _ = (false, HOLogic.unit);
   1.454 +
   1.455 +        fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
   1.456            let
   1.457              val ss = get_sel_upd_defs thy;
   1.458              val uathm = get_upd_acc_cong_thm upd acc thy ss;
   1.459 @@ -1417,17 +1358,16 @@
   1.460                        fvar :: vars, dups, true, noops)
   1.461                    | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
   1.462                end
   1.463 -          | mk_updterm [] above term =
   1.464 +          | mk_updterm [] _ _ =
   1.465                (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
   1.466 -          | mk_updterm us above term =
   1.467 -              raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us);
   1.468 -
   1.469 -        val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base;
   1.470 +          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
   1.471 +
   1.472 +        val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
   1.473          val noops' = flat (map snd (Symtab.dest noops));
   1.474        in
   1.475          if simp then
   1.476            SOME
   1.477 -            (prove_unfold_defs thy ss baseT noops' [record_simproc]
   1.478 +            (prove_unfold_defs thy noops' [record_simproc]
   1.479                (list_all (vars, Logic.mk_equals (lhs, rhs))))
   1.480          else NONE
   1.481        end);
   1.482 @@ -1473,11 +1413,11 @@
   1.483    Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
   1.484      (fn thy => fn _ => fn t =>
   1.485        (case t of
   1.486 -        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm =>
   1.487 +        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   1.488            if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
   1.489              (case rec_id ~1 T of
   1.490                "" => NONE
   1.491 -            | name =>
   1.492 +            | _ =>
   1.493                  let val split = P t in
   1.494                    if split <> 0 then
   1.495                      (case get_splits thy (rec_id split T) of
   1.496 @@ -1568,10 +1508,10 @@
   1.497            simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   1.498        end;
   1.499  
   1.500 -    fun split_free_tac P i (free as Free (n, T)) =
   1.501 +    fun split_free_tac P i (free as Free (_, T)) =
   1.502            (case rec_id ~1 T of
   1.503              "" => NONE
   1.504 -          | name =>
   1.505 +          | _ =>
   1.506                let val split = P free in
   1.507                  if split <> 0 then
   1.508                    (case get_splits thy (rec_id split T) of
   1.509 @@ -1598,8 +1538,6 @@
   1.510  (*Split all records in the goal, which are quantified by ! or !!.*)
   1.511  fun record_split_tac i st =
   1.512    let
   1.513 -    val thy = Thm.theory_of_thm st;
   1.514 -
   1.515      val has_rec = exists_Const
   1.516        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.517            (s = "all" orelse s = "All") andalso is_recT T
   1.518 @@ -1695,40 +1633,16 @@
   1.519    in compose_tac (false, rule'', nprems_of rule) i st end;
   1.520  
   1.521  
   1.522 -(*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
   1.523 -  instantiates x1 ... xn with parameters x1 ... xn*)
   1.524 -fun ex_inst_tac i st =
   1.525 -  let
   1.526 -    val thy = Thm.theory_of_thm st;
   1.527 -    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
   1.528 -    val params = Logic.strip_params g;
   1.529 -    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
   1.530 -    val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI'));
   1.531 -    val cx = cterm_of thy (fst (strip_comb x));
   1.532 -  in
   1.533 -    Seq.single (Library.foldl (fn (st, v) =>
   1.534 -      Seq.hd
   1.535 -        (compose_tac
   1.536 -          (false,
   1.537 -            cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st))
   1.538 -        (st, (length params - 1) downto 0))
   1.539 -  end;
   1.540 -
   1.541 -fun extension_definition full name fields names alphas zeta moreT more vars thy =
   1.542 +fun extension_definition name fields alphas zeta moreT more vars thy =
   1.543    let
   1.544      val base = Long_Name.base_name;
   1.545      val fieldTs = (map snd fields);
   1.546      val alphas_zeta = alphas @ [zeta];
   1.547      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
   1.548 -    val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
   1.549      val extT_name = suffix ext_typeN name
   1.550      val extT = Type (extT_name, alphas_zetaTs);
   1.551 -    val fields_more = fields @ [(full moreN, moreT)];
   1.552      val fields_moreTs = fieldTs @ [moreT];
   1.553 -    val bfields_more = map (apfst base) fields_more;
   1.554 -    val r = Free (rN, extT);
   1.555 -    val len = length fields;
   1.556 -    val idxms = 0 upto len;
   1.557 +
   1.558  
   1.559      (*before doing anything else, create the tree of new types
   1.560        that will back the record extension*)
   1.561 @@ -1739,7 +1653,7 @@
   1.562        let
   1.563          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   1.564          val nm = suffix suff (Long_Name.base_name name);
   1.565 -        val (isom, cons, thy') =
   1.566 +        val (_, cons, thy') =
   1.567            IsTupleSupport.add_istuple_type
   1.568              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   1.569        in
   1.570 @@ -1763,7 +1677,7 @@
   1.571              build_meta_tree_type i' thy' composites more
   1.572            end
   1.573          else
   1.574 -          let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0)
   1.575 +          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
   1.576            in (term, thy') end
   1.577        end;
   1.578  
   1.579 @@ -1795,16 +1709,15 @@
   1.580      val ([ext_def], defs_thy) =
   1.581        timeit_msg "record extension constructor def:" mk_defs;
   1.582  
   1.583 +
   1.584      (* prepare propositions *)
   1.585 +
   1.586      val _ = timing_msg "record extension preparing propositions";
   1.587      val vars_more = vars @ [more];
   1.588 -    val named_vars_more = (names @ [full moreN]) ~~ vars_more;
   1.589      val variants = map (fn Free (x, _) => x) vars_more;
   1.590      val ext = mk_ext vars_more;
   1.591      val s = Free (rN, extT);
   1.592 -    val w = Free (wN, extT);
   1.593      val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   1.594 -    val C = Free (Name.variant variants "C", HOLogic.boolT);
   1.595      val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   1.596  
   1.597      val inject_prop =
   1.598 @@ -1819,27 +1732,18 @@
   1.599      val induct_prop =
   1.600        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
   1.601  
   1.602 -    val cases_prop =
   1.603 -      All (map dest_Free vars_more)
   1.604 -        (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C)
   1.605 -      ==> Trueprop C;
   1.606 -
   1.607      val split_meta_prop =
   1.608 -      let val P = Free (Name.variant variants "P", extT-->Term.propT) in
   1.609 +      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
   1.610          Logic.mk_equals
   1.611           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   1.612        end;
   1.613  
   1.614 -    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
   1.615      val prove_standard = quick_and_dirty_prove true defs_thy;
   1.616 -    fun prove_simp stndrd simps =
   1.617 -      let val tac = simp_all_tac HOL_ss simps
   1.618 -      in fn prop => prove stndrd [] prop (K tac) end;
   1.619  
   1.620      fun inject_prf () =
   1.621        simplify HOL_ss
   1.622          (prove_standard [] inject_prop
   1.623 -          (fn prems =>
   1.624 +          (fn _ =>
   1.625              EVERY
   1.626               [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   1.627                REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
   1.628 @@ -1872,7 +1776,7 @@
   1.629  
   1.630      fun split_meta_prf () =
   1.631        prove_standard [] split_meta_prop
   1.632 -        (fn prems =>
   1.633 +        (fn _ =>
   1.634            EVERY
   1.635             [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.636              etac meta_allE 1, atac 1,
   1.637 @@ -1909,8 +1813,8 @@
   1.638    | chop_last [x] = ([], x)
   1.639    | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
   1.640  
   1.641 -fun subst_last s [] = error "subst_last: list should not be empty"
   1.642 -  | subst_last s [x] = [s]
   1.643 +fun subst_last _ [] = error "subst_last: list should not be empty"
   1.644 +  | subst_last s [_] = [s]
   1.645    | subst_last s (x :: xs) = x :: subst_last s xs;
   1.646  
   1.647  
   1.648 @@ -1965,7 +1869,6 @@
   1.649      val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
   1.650      val parent_vars = ListPair.map Free (parent_variants, parent_types);
   1.651      val parent_len = length parents;
   1.652 -    val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
   1.653  
   1.654      val fields = map (apfst full) bfields;
   1.655      val names = map fst fields;
   1.656 @@ -1979,13 +1882,10 @@
   1.657          (map fst bfields);
   1.658      val vars = ListPair.map Free (variants, types);
   1.659      val named_vars = names ~~ vars;
   1.660 -    val idxs = 0 upto (len - 1);
   1.661      val idxms = 0 upto len;
   1.662  
   1.663      val all_fields = parent_fields @ fields;
   1.664 -    val all_names = parent_names @ names;
   1.665      val all_types = parent_types @ types;
   1.666 -    val all_len = parent_fields_len + len;
   1.667      val all_variants = parent_variants @ variants;
   1.668      val all_vars = parent_vars @ vars;
   1.669      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
   1.670 @@ -1997,7 +1897,6 @@
   1.671      val full_moreN = full moreN;
   1.672      val bfields_more = bfields @ [(moreN, moreT)];
   1.673      val fields_more = fields @ [(full_moreN, moreT)];
   1.674 -    val vars_more = vars @ [more];
   1.675      val named_vars_more = named_vars @ [(full_moreN, more)];
   1.676      val all_vars_more = all_vars @ [more];
   1.677      val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
   1.678 @@ -2008,7 +1907,7 @@
   1.679      val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
   1.680        thy
   1.681        |> Sign.add_path bname
   1.682 -      |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
   1.683 +      |> extension_definition extN fields alphas_ext zeta moreT more vars;
   1.684  
   1.685      val _ = timing_msg "record preparing definitions";
   1.686      val Type extension_scheme = extT;
   1.687 @@ -2080,16 +1979,6 @@
   1.688  
   1.689      (* prepare definitions *)
   1.690  
   1.691 -    fun parent_more s =
   1.692 -      if null parents then s
   1.693 -      else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
   1.694 -
   1.695 -    fun parent_more_upd v s =
   1.696 -      if null parents then v $ s
   1.697 -      else
   1.698 -        let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
   1.699 -        in mk_upd updateN mp v s end;
   1.700 -
   1.701      (*record (scheme) type abbreviation*)
   1.702      val recordT_specs =
   1.703        [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
   1.704 @@ -2233,14 +2122,12 @@
   1.705  
   1.706      (*cases*)
   1.707      val cases_scheme_prop =
   1.708 -      (All (map dest_Free all_vars_more)
   1.709 -        (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C))
   1.710 -      ==> Trueprop C;
   1.711 +      (All (map dest_Free all_vars_more) (r0 === r_rec0 ==> Trueprop C))
   1.712 +        ==> Trueprop C;
   1.713  
   1.714      val cases_prop =
   1.715 -      (All (map dest_Free all_vars)
   1.716 -        (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C))
   1.717 -       ==> Trueprop C;
   1.718 +      (All (map dest_Free all_vars) (r_unit0 === r_rec_unit0 ==> Trueprop C))
   1.719 +         ==> Trueprop C;
   1.720  
   1.721      (*split*)
   1.722      val split_meta_prop =
   1.723 @@ -2359,7 +2246,7 @@
   1.724          val init_ss = HOL_basic_ss addsimps ext_defs;
   1.725        in
   1.726          prove_standard [] surjective_prop
   1.727 -          (fn prems =>
   1.728 +          (fn _ =>
   1.729              EVERY
   1.730               [rtac surject_assist_idE 1,
   1.731                simp_tac init_ss 1,
   1.732 @@ -2369,7 +2256,7 @@
   1.733  
   1.734      fun split_meta_prf () =
   1.735        prove false [] split_meta_prop
   1.736 -        (fn prems =>
   1.737 +        (fn _ =>
   1.738            EVERY
   1.739             [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.740              etac meta_allE 1, atac 1,
   1.741 @@ -2423,7 +2310,7 @@
   1.742          val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
   1.743          val so'' = simplify ss so';
   1.744        in
   1.745 -        prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
   1.746 +        prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
   1.747        end;
   1.748      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
   1.749