src/HOL/Tools/record.ML
changeset 32761 54fee94b2b29
parent 32760 ea6672bff5dd
child 32763 ebfaf9e3c03a
     1.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 18:14:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 21:34:59 2009 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4  
     1.5    val last_extT: typ -> (string * typ list) option
     1.6    val dest_recTs : typ -> (string * typ list) list
     1.7 -  val get_extT_fields:  theory -> typ -> (string * typ) list * (string * typ)
     1.8 -  val get_recT_fields:  theory -> typ -> (string * typ) list * (string * typ)
     1.9 +  val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    1.10 +  val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    1.11    val get_parent: theory -> string -> (typ list * string) option
    1.12    val get_extension: theory -> string -> (string * typ list) option
    1.13    val get_extinjects: theory -> thm list
    1.14 @@ -54,18 +54,17 @@
    1.15  
    1.16  signature ISTUPLE_SUPPORT =
    1.17  sig
    1.18 -  val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    1.19 -            (term * term * theory);
    1.20 -
    1.21 -  val mk_cons_tuple: term * term -> term;
    1.22 -  val dest_cons_tuple: term -> term * term;
    1.23 -
    1.24 -  val istuple_intros_tac: theory -> int -> tactic;
    1.25 -
    1.26 -  val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
    1.27 +  val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> term * term * theory
    1.28 +
    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 named_cterm_instantiate: (string * cterm) list -> thm -> thm
    1.35  end;
    1.36  
    1.37 -structure IsTupleSupport : ISTUPLE_SUPPORT =
    1.38 +structure IsTupleSupport: ISTUPLE_SUPPORT =
    1.39  struct
    1.40  
    1.41  val isomN = "_TupleIsom";
    1.42 @@ -85,13 +84,14 @@
    1.43  
    1.44  val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    1.45  
    1.46 -fun named_cterm_instantiate values thm = let
    1.47 +fun named_cterm_instantiate values thm =
    1.48 +  let
    1.49      fun match name ((name', _), _) = name = name'
    1.50        | match name _ = false;
    1.51 -    fun getvar name = case (find_first (match name)
    1.52 -                                    (Term.add_vars (prop_of thm) []))
    1.53 -      of SOME var => cterm_of (theory_of_thm thm) (Var var)
    1.54 -       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    1.55 +    fun getvar name =
    1.56 +      (case find_first (match name) (Term.add_vars (prop_of thm) []) of
    1.57 +        SOME var => cterm_of (theory_of_thm thm) (Var var)
    1.58 +      | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
    1.59    in
    1.60      cterm_instantiate (map (apfst getvar) values) thm
    1.61    end;
    1.62 @@ -120,78 +120,82 @@
    1.63      |-> (fn (name, _) => `(fn thy => get_thms thy name))
    1.64    end;
    1.65  
    1.66 -fun mk_cons_tuple (left, right) = let
    1.67 +fun mk_cons_tuple (left, right) =
    1.68 +  let
    1.69      val (leftT, rightT) = (fastype_of left, fastype_of right);
    1.70 -    val prodT           = HOLogic.mk_prodT (leftT, rightT);
    1.71 -    val isomT           = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    1.72 +    val prodT = HOLogic.mk_prodT (leftT, rightT);
    1.73 +    val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    1.74    in
    1.75 -    Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
    1.76 -      $ Const (fst tuple_istuple, isomT) $ left $ right
    1.77 +    Const (istuple_consN, isomT --> leftT --> rightT --> prodT) $
    1.78 +      Const (fst tuple_istuple, isomT) $ left $ right
    1.79    end;
    1.80  
    1.81 -fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
    1.82 -  = if ic = istuple_consN then (left, right)
    1.83 -    else raise TERM ("dest_cons_tuple", [v])
    1.84 +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) =
    1.85 +      if ic = istuple_consN then (left, right)
    1.86 +      else raise TERM ("dest_cons_tuple", [v])
    1.87    | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
    1.88  
    1.89  fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    1.90 -let
    1.91 -  val repT = HOLogic.mk_prodT (leftT, rightT);
    1.92 -
    1.93 -  val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
    1.94 -    thy
    1.95 -    |> do_typedef name repT alphas
    1.96 -    ||> Sign.add_path name;
    1.97 -
    1.98 -  (* construct a type and body for the isomorphism constant by
    1.99 -     instantiating the theorem to which the definition will be applied *)
   1.100 -  val intro_inst = rep_inject RS
   1.101 -                   (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
   1.102 -                        istuple_intro);
   1.103 -  val (_, body)  = Logic.dest_equals (List.last (prems_of intro_inst));
   1.104 -  val isomT      = fastype_of body;
   1.105 -  val isom_bind  = Binding.name (name ^ isomN);
   1.106 -  val isom       = Const (Sign.full_name typ_thy isom_bind, isomT);
   1.107 -  val isom_spec  = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   1.108 -
   1.109 -  val ([isom_def], cdef_thy) =
   1.110 -    typ_thy
   1.111 -    |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
   1.112 -    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   1.113 -
   1.114 -  val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   1.115 -  val cons    = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
   1.116 -
   1.117 -  val thm_thy =
   1.118 -    cdef_thy
   1.119 -    |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
   1.120 -                           (constname isom, istuple))
   1.121 -    |> Sign.parent_path;
   1.122 -in
   1.123 -  (isom, cons $ isom, thm_thy)
   1.124 -end;
   1.125 -
   1.126 -fun istuple_intros_tac thy = let
   1.127 -    val isthms  = IsTupleThms.get thy;
   1.128 +  let
   1.129 +    val repT = HOLogic.mk_prodT (leftT, rightT);
   1.130 +
   1.131 +    val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
   1.132 +      thy
   1.133 +      |> do_typedef name repT alphas
   1.134 +      ||> Sign.add_path name;
   1.135 +
   1.136 +    (*construct a type and body for the isomorphism constant by
   1.137 +      instantiating the theorem to which the definition will be applied*)
   1.138 +    val intro_inst =
   1.139 +      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
   1.140 +    val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
   1.141 +    val isomT = fastype_of body;
   1.142 +    val isom_bind = Binding.name (name ^ isomN);
   1.143 +    val isom = Const (Sign.full_name typ_thy isom_bind, isomT);
   1.144 +    val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   1.145 +
   1.146 +    val ([isom_def], cdef_thy) =
   1.147 +      typ_thy
   1.148 +      |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
   1.149 +      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   1.150 +
   1.151 +    val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   1.152 +    val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT);
   1.153 +
   1.154 +    val thm_thy =
   1.155 +      cdef_thy
   1.156 +      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (constname isom, istuple))
   1.157 +      |> Sign.parent_path;
   1.158 +  in
   1.159 +    (isom, cons $ isom, thm_thy)
   1.160 +  end;
   1.161 +
   1.162 +fun istuple_intros_tac thy =
   1.163 +  let
   1.164 +    val isthms = IsTupleThms.get thy;
   1.165      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   1.166 -    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
   1.167 +    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) =>
   1.168 +      let
   1.169          val goal' = Envir.beta_eta_contract goal;
   1.170 -        val isom  = case goal' of (Const tp $ (Const pr $ Const is))
   1.171 -                    => if fst tp = "Trueprop" andalso fst pr = istuple_constN
   1.172 -                       then Const is
   1.173 -                       else err "unexpected goal predicate" goal'
   1.174 -            | _ => err "unexpected goal format" goal';
   1.175 -        val isthm = case Symtab.lookup isthms (constname isom) of
   1.176 -                    SOME isthm => isthm
   1.177 -                  | NONE => err "no thm found for constant" isom;
   1.178 +        val isom =
   1.179 +          (case goal' of
   1.180 +            Const tp $ (Const pr $ Const is) =>
   1.181 +              if fst tp = "Trueprop" andalso fst pr = istuple_constN
   1.182 +              then Const is
   1.183 +              else err "unexpected goal predicate" goal'
   1.184 +          | _ => err "unexpected goal format" goal');
   1.185 +        val isthm =
   1.186 +          (case Symtab.lookup isthms (constname isom) of
   1.187 +            SOME isthm => isthm
   1.188 +          | NONE => err "no thm found for constant" isom);
   1.189        in rtac isthm n end);
   1.190    in
   1.191 -    fn n => resolve_from_net_tac istuple_intros n
   1.192 -            THEN use_istuple_thm_tac n
   1.193 +    fn n => resolve_from_net_tac istuple_intros n THEN use_istuple_thm_tac n
   1.194    end;
   1.195  
   1.196  end;
   1.197  
   1.198 +
   1.199  structure Record: RECORD =
   1.200  struct
   1.201  
   1.202 @@ -201,7 +205,7 @@
   1.203  val atomize_imp = thm "HOL.atomize_imp";
   1.204  val meta_allE = thm "Pure.meta_allE";
   1.205  val prop_subst = thm "prop_subst";
   1.206 -val Pair_sel_convs = [fst_conv,snd_conv];
   1.207 +val Pair_sel_convs = [fst_conv, snd_conv];
   1.208  val K_record_comp = @{thm "K_record_comp"};
   1.209  val K_comp_convs = [@{thm o_apply}, K_record_comp]
   1.210  val transitive_thm = thm "transitive";
   1.211 @@ -234,6 +238,8 @@
   1.212  val o_eq_id_dest = thm "o_eq_id_dest";
   1.213  val o_eq_dest_lhs = thm "o_eq_dest_lhs";
   1.214  
   1.215 +
   1.216 +
   1.217  (** name components **)
   1.218  
   1.219  val rN = "r";
   1.220 @@ -267,29 +273,29 @@
   1.221    in map_type_tfree varify end;
   1.222  
   1.223  fun domain_type' T =
   1.224 -    domain_type T handle Match => T;
   1.225 +  domain_type T handle Match => T;
   1.226  
   1.227  fun range_type' T =
   1.228 -    range_type T handle Match => T;
   1.229 -
   1.230 -
   1.231 -(* messages *)
   1.232 +  range_type T handle Match => T;
   1.233 +
   1.234 +
   1.235 +(* messages *)  (* FIXME proper context *)
   1.236  
   1.237  fun trace_thm str thm =
   1.238 -    tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
   1.239 +  tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm));
   1.240  
   1.241  fun trace_thms str thms =
   1.242 -    (tracing str; map (trace_thm "") thms);
   1.243 +  (tracing str; map (trace_thm "") thms);
   1.244  
   1.245  fun trace_term str t =
   1.246 -    tracing (str ^ Syntax.string_of_term_global Pure.thy t);
   1.247 +  tracing (str ^ Syntax.string_of_term_global Pure.thy t);
   1.248  
   1.249  
   1.250  (* timing *)
   1.251  
   1.252  val timing = Unsynchronized.ref false;
   1.253 -fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
   1.254 -fun timing_msg s = if !timing then warning s else ();
   1.255 +fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
   1.256 +fun timing_msg s = if ! timing then warning s else ();
   1.257  
   1.258  
   1.259  (* syntax *)
   1.260 @@ -315,54 +321,54 @@
   1.261  fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
   1.262  fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
   1.263  
   1.264 -fun mk_Rep name repT absT  =
   1.265 -  Const (suffix ext_typeN (prefix_base RepN name),absT --> repT);
   1.266 +fun mk_Rep name repT absT =
   1.267 +  Const (suffix ext_typeN (prefix_base RepN name), absT --> repT);
   1.268  
   1.269  fun mk_Abs name repT absT =
   1.270 -  Const (mk_AbsN name,repT --> absT);
   1.271 +  Const (mk_AbsN name, repT --> absT);
   1.272  
   1.273  
   1.274  (* constructor *)
   1.275  
   1.276 -fun mk_extC (name,T) Ts  = (suffix extN name, Ts ---> T);
   1.277 -
   1.278 -fun mk_ext (name,T) ts =
   1.279 +fun mk_extC (name, T) Ts = (suffix extN name, Ts ---> T);
   1.280 +
   1.281 +fun mk_ext (name, T) ts =
   1.282    let val Ts = map fastype_of ts
   1.283 -  in list_comb (Const (mk_extC (name,T) Ts),ts) end;
   1.284 +  in list_comb (Const (mk_extC (name, T) Ts), ts) end;
   1.285  
   1.286  
   1.287  (* cases *)
   1.288  
   1.289 -fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT)
   1.290 -
   1.291 -fun mk_cases (name,T,vT) f =
   1.292 +fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT);
   1.293 +
   1.294 +fun mk_cases (name, T, vT) f =
   1.295    let val Ts = binder_types (fastype_of f)
   1.296 -  in Const (mk_casesC (name,T,vT) Ts) $ f end;
   1.297 +  in Const (mk_casesC (name, T, vT) Ts) $ f end;
   1.298  
   1.299  
   1.300  (* selector *)
   1.301  
   1.302 -fun mk_selC sT (c,T) = (c,sT --> T);
   1.303 -
   1.304 -fun mk_sel s (c,T) =
   1.305 +fun mk_selC sT (c, T) = (c, sT --> T);
   1.306 +
   1.307 +fun mk_sel s (c, T) =
   1.308    let val sT = fastype_of s
   1.309 -  in Const (mk_selC sT (c,T)) $ s end;
   1.310 +  in Const (mk_selC sT (c, T)) $ s end;
   1.311  
   1.312  
   1.313  (* updates *)
   1.314  
   1.315 -fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT);
   1.316 +fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
   1.317  
   1.318  fun mk_upd' sfx c v sT =
   1.319    let val vT = domain_type (fastype_of v);
   1.320 -  in Const (mk_updC sfx sT (c, vT)) $ v  end;
   1.321 -
   1.322 -fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s
   1.323 +  in Const (mk_updC sfx sT (c, vT)) $ v end;
   1.324 +
   1.325 +fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
   1.326  
   1.327  
   1.328  (* types *)
   1.329  
   1.330 -fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
   1.331 +fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) =
   1.332        (case try (unsuffix ext_typeN) c_ext_type of
   1.333          NONE => raise TYPE ("Record.dest_recT", [typ], [])
   1.334        | SOME c => ((c, Ts), List.last Ts))
   1.335 @@ -377,16 +383,17 @@
   1.336    end handle TYPE _ => [];
   1.337  
   1.338  fun last_extT T =
   1.339 -  let val ((c, Ts), U) = dest_recT T
   1.340 -  in (case last_extT U of
   1.341 -        NONE => SOME (c,Ts)
   1.342 -      | SOME l => SOME l)
   1.343 -  end handle TYPE _ => NONE
   1.344 +  let val ((c, Ts), U) = dest_recT T in
   1.345 +    (case last_extT U of
   1.346 +      NONE => SOME (c, Ts)
   1.347 +    | SOME l => SOME l)
   1.348 +  end handle TYPE _ => NONE;
   1.349  
   1.350  fun rec_id i T =
   1.351 -  let val rTs = dest_recTs T
   1.352 -      val rTs' = if i < 0 then rTs else Library.take (i,rTs)
   1.353 -  in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end;
   1.354 +  let
   1.355 +    val rTs = dest_recTs T;
   1.356 +    val rTs' = if i < 0 then rTs else Library.take (i, rTs);
   1.357 +  in Library.foldl (fn (s, (c, T)) => s ^ c) ("", rTs') end;   (* FIXME ? *)
   1.358  
   1.359  
   1.360  
   1.361 @@ -394,7 +401,7 @@
   1.362  
   1.363  (** record info **)
   1.364  
   1.365 -(* type record_info and parent_info  *)
   1.366 +(* type record_info and parent_info *)
   1.367  
   1.368  type record_info =
   1.369   {args: (string * sort) list,
   1.370 @@ -402,8 +409,7 @@
   1.371    fields: (string * typ) list,
   1.372    extension: (string * typ list),
   1.373    induct: thm,
   1.374 -  extdef: thm
   1.375 - };
   1.376 +  extdef: thm};
   1.377  
   1.378  fun make_record_info args parent fields extension induct extdef =
   1.379   {args = args, parent = parent, fields = fields, extension = extension,
   1.380 @@ -415,8 +421,7 @@
   1.381    fields: (string * typ) list,
   1.382    extension: (string * typ list),
   1.383    induct: thm,
   1.384 -  extdef: thm
   1.385 -};
   1.386 +  extdef: thm};
   1.387  
   1.388  fun make_parent_info name fields extension induct extdef =
   1.389   {name = name, fields = fields, extension = extension,
   1.390 @@ -436,14 +441,13 @@
   1.391      unfoldcong: Simplifier.simpset},
   1.392    equalities: thm Symtab.table,
   1.393    extinjects: thm list,
   1.394 -  extsplit: thm Symtab.table, (* maps extension name to split rule *)
   1.395 -  splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *)
   1.396 -  extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
   1.397 -  fieldext: (string*typ list) Symtab.table   (* maps field to its extension *)
   1.398 -};
   1.399 +  extsplit: thm Symtab.table,  (* maps extension name to split rule *)
   1.400 +  splits: (thm*thm*thm*thm) Symtab.table,  (* !!, !, EX - split-equalities, induct rule *)
   1.401 +  extfields: (string*typ) list Symtab.table,  (* maps extension to its fields *)
   1.402 +  fieldext: (string*typ list) Symtab.table};  (* maps field to its extension *)
   1.403  
   1.404  fun make_record_data
   1.405 -      records sel_upd equalities extinjects extsplit splits extfields fieldext =
   1.406 +    records sel_upd equalities extinjects extsplit splits extfields fieldext =
   1.407   {records = records, sel_upd = sel_upd,
   1.408    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   1.409    extfields = extfields, fieldext = fieldext }: record_data;
   1.410 @@ -462,9 +466,10 @@
   1.411    val extend = I;
   1.412    fun merge _
   1.413     ({records = recs1,
   1.414 -     sel_upd = {selectors = sels1, updates = upds1,
   1.415 -                simpset = ss1, defset = ds1,
   1.416 -                foldcong = fc1, unfoldcong = uc1},
   1.417 +     sel_upd =
   1.418 +      {selectors = sels1, updates = upds1,
   1.419 +       simpset = ss1, defset = ds1,
   1.420 +       foldcong = fc1, unfoldcong = uc1},
   1.421       equalities = equalities1,
   1.422       extinjects = extinjects1,
   1.423       extsplit = extsplit1,
   1.424 @@ -472,9 +477,10 @@
   1.425       extfields = extfields1,
   1.426       fieldext = fieldext1},
   1.427      {records = recs2,
   1.428 -     sel_upd = {selectors = sels2, updates = upds2,
   1.429 -                simpset = ss2, defset = ds2,
   1.430 -                foldcong = fc2, unfoldcong = uc2},
   1.431 +     sel_upd =
   1.432 +      {selectors = sels2, updates = upds2,
   1.433 +       simpset = ss2, defset = ds2,
   1.434 +       foldcong = fc2, unfoldcong = uc2},
   1.435       equalities = equalities2,
   1.436       extinjects = extinjects2,
   1.437       extsplit = extsplit2,
   1.438 @@ -491,13 +497,12 @@
   1.439          unfoldcong = Simplifier.merge_ss (uc1, uc2)}
   1.440        (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   1.441        (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
   1.442 -      (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2))
   1.443 -      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z))
   1.444 -                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso
   1.445 -                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z))
   1.446 -                    (splits1, splits2))
   1.447 -      (Symtab.merge (K true) (extfields1,extfields2))
   1.448 -      (Symtab.merge (K true) (fieldext1,fieldext2));
   1.449 +      (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
   1.450 +      (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
   1.451 +          Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
   1.452 +          Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
   1.453 +      (Symtab.merge (K true) (extfields1, extfields2))
   1.454 +      (Symtab.merge (K true) (fieldext1, fieldext2));
   1.455  );
   1.456  
   1.457  fun print_records thy =
   1.458 @@ -526,8 +531,8 @@
   1.459  
   1.460  fun put_record name info thy =
   1.461    let
   1.462 -    val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} =
   1.463 -          RecordsData.get thy;
   1.464 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.465 +      RecordsData.get thy;
   1.466      val data = make_record_data (Symtab.update (name, info) records)
   1.467        sel_upd equalities extinjects extsplit splits extfields fieldext;
   1.468    in RecordsData.put data thy end;
   1.469 @@ -547,24 +552,23 @@
   1.470  val get_foldcong_ss = get_ss_with_context (#foldcong);
   1.471  val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
   1.472  
   1.473 -fun get_update_details u thy = let
   1.474 -    val sel_upd = get_sel_upd thy;
   1.475 -  in case (Symtab.lookup (#updates sel_upd) u) of
   1.476 -    SOME s => let
   1.477 -        val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s;
   1.478 -      in SOME (s, dep, ismore) end
   1.479 -  | NONE => NONE end;
   1.480 +fun get_update_details u thy =
   1.481 +  let val sel_upd = get_sel_upd thy in
   1.482 +    (case Symtab.lookup (#updates sel_upd) u of
   1.483 +      SOME s =>
   1.484 +        let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
   1.485 +        in SOME (s, dep, ismore) end
   1.486 +    | NONE => NONE)
   1.487 +  end;
   1.488  
   1.489  fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
   1.490    let
   1.491 -    val all  = names @ [more];
   1.492 +    val all = names @ [more];
   1.493      val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
   1.494      val upds = map (suffix updateN) all ~~ all;
   1.495  
   1.496 -    val {records, sel_upd = {selectors, updates, simpset,
   1.497 -                             defset, foldcong, unfoldcong},
   1.498 -      equalities, extinjects, extsplit, splits, extfields,
   1.499 -      fieldext} = RecordsData.get thy;
   1.500 +    val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
   1.501 +      equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy;
   1.502      val data = make_record_data records
   1.503        {selectors = fold Symtab.update_new sels selectors,
   1.504          updates = fold Symtab.update_new upds updates,
   1.505 @@ -575,29 +579,29 @@
   1.506         equalities extinjects extsplit splits extfields fieldext;
   1.507    in RecordsData.put data thy end;
   1.508  
   1.509 +
   1.510  (* access 'equalities' *)
   1.511  
   1.512  fun add_record_equalities name thm thy =
   1.513    let
   1.514 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   1.515 -          RecordsData.get thy;
   1.516 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.517 +      RecordsData.get thy;
   1.518      val data = make_record_data records sel_upd
   1.519 -           (Symtab.update_new (name, thm) equalities) extinjects extsplit
   1.520 -           splits extfields fieldext;
   1.521 +      (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
   1.522    in RecordsData.put data thy end;
   1.523  
   1.524 -val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
   1.525 +val get_equalities = Symtab.lookup o #equalities o RecordsData.get;
   1.526  
   1.527  
   1.528  (* access 'extinjects' *)
   1.529  
   1.530  fun add_extinjects thm thy =
   1.531    let
   1.532 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   1.533 -          RecordsData.get thy;
   1.534 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.535 +      RecordsData.get thy;
   1.536      val data =
   1.537 -      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
   1.538 -        splits extfields fieldext;
   1.539 +      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   1.540 +        extsplit splits extfields fieldext;
   1.541    in RecordsData.put data thy end;
   1.542  
   1.543  val get_extinjects = rev o #extinjects o RecordsData.get;
   1.544 @@ -607,8 +611,8 @@
   1.545  
   1.546  fun add_extsplit name thm thy =
   1.547    let
   1.548 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   1.549 -          RecordsData.get thy;
   1.550 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.551 +      RecordsData.get thy;
   1.552      val data = make_record_data records sel_upd
   1.553        equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
   1.554        extfields fieldext;
   1.555 @@ -621,8 +625,8 @@
   1.556  
   1.557  fun add_record_splits name thmP thy =
   1.558    let
   1.559 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   1.560 -          RecordsData.get thy;
   1.561 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.562 +      RecordsData.get thy;
   1.563      val data = make_record_data records sel_upd
   1.564        equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
   1.565        extfields fieldext;
   1.566 @@ -641,37 +645,39 @@
   1.567  
   1.568  fun add_extfields name fields thy =
   1.569    let
   1.570 -    val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} =
   1.571 -          RecordsData.get thy;
   1.572 -    val data = make_record_data records sel_upd
   1.573 -         equalities extinjects extsplit splits
   1.574 -         (Symtab.update_new (name, fields) extfields) fieldext;
   1.575 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.576 +      RecordsData.get thy;
   1.577 +    val data =
   1.578 +      make_record_data records sel_upd
   1.579 +        equalities extinjects extsplit splits
   1.580 +        (Symtab.update_new (name, fields) extfields) fieldext;
   1.581    in RecordsData.put data thy end;
   1.582  
   1.583  val get_extfields = Symtab.lookup o #extfields o RecordsData.get;
   1.584  
   1.585  fun get_extT_fields thy T =
   1.586    let
   1.587 -    val ((name,Ts),moreT) = dest_recT T;
   1.588 -    val recname = let val (nm::recn::rst) = rev (Long_Name.explode name)
   1.589 -                  in Long_Name.implode (rev (nm::rst)) end;
   1.590 -    val midx = maxidx_of_typs (moreT::Ts);
   1.591 +    val ((name, Ts), moreT) = dest_recT T;
   1.592 +    val recname =
   1.593 +      let val (nm :: recn :: rst) = rev (Long_Name.explode name)
   1.594 +      in Long_Name.implode (rev (nm :: rst)) end;
   1.595 +    val midx = maxidx_of_typs (moreT :: Ts);
   1.596      val varifyT = varifyT midx;
   1.597 -    val {records,extfields,...} = RecordsData.get thy;
   1.598 -    val (flds,(more,_)) = split_last (Symtab.lookup_list extfields name);
   1.599 +    val {records, extfields, ...} = RecordsData.get thy;
   1.600 +    val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name);
   1.601      val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
   1.602  
   1.603      val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty);
   1.604      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
   1.605 -  in (flds',(more,moreT)) end;
   1.606 +  in (flds', (more, moreT)) end;
   1.607  
   1.608  fun get_recT_fields thy T =
   1.609    let
   1.610 -    val (root_flds,(root_more,root_moreT)) = get_extT_fields thy T;
   1.611 -    val (rest_flds,rest_more) =
   1.612 -           if is_recT root_moreT then get_recT_fields thy root_moreT
   1.613 -           else ([],(root_more,root_moreT));
   1.614 -  in (root_flds@rest_flds,rest_more) end;
   1.615 +    val (root_flds, (root_more, root_moreT)) = get_extT_fields thy T;
   1.616 +    val (rest_flds, rest_more) =
   1.617 +      if is_recT root_moreT then get_recT_fields thy root_moreT
   1.618 +      else ([], (root_more, root_moreT));
   1.619 +  in (root_flds @ rest_flds, rest_more) end;
   1.620  
   1.621  
   1.622  (* access 'fieldext' *)
   1.623 @@ -679,14 +685,14 @@
   1.624  fun add_fieldext extname_types fields thy =
   1.625    let
   1.626      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.627 -           RecordsData.get thy;
   1.628 +      RecordsData.get thy;
   1.629      val fieldext' =
   1.630        fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   1.631 -    val data=make_record_data records sel_upd equalities extinjects extsplit
   1.632 -              splits extfields fieldext';
   1.633 +    val data =
   1.634 +      make_record_data records sel_upd equalities extinjects
   1.635 +        extsplit splits extfields fieldext';
   1.636    in RecordsData.put data thy end;
   1.637  
   1.638 -
   1.639  val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
   1.640  
   1.641  
   1.642 @@ -735,7 +741,7 @@
   1.643  (* parse translations *)
   1.644  
   1.645  fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   1.646 -      if c = mark then Syntax.const (suffix sfx name) $ (Abs ("_",dummyT, arg))
   1.647 +      if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg)
   1.648        else raise TERM ("gen_field_tr: " ^ mark, [t])
   1.649    | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   1.650  
   1.651 @@ -755,87 +761,88 @@
   1.652        (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   1.653    | update_name_tr ts = raise TERM ("update_name_tr", ts);
   1.654  
   1.655 -fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) =
   1.656 -     if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t])
   1.657 -  | dest_ext_field _ t = raise TERM ("dest_ext_field", [t])
   1.658 -
   1.659 -fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) =
   1.660 -     if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u
   1.661 -     else [dest_ext_field mark trm]
   1.662 -  | dest_ext_fields _ mark t = [dest_ext_field mark t]
   1.663 +fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) =
   1.664 +      if c = mark then (name, arg)
   1.665 +      else raise TERM ("dest_ext_field: " ^ mark, [t])
   1.666 +  | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]);
   1.667 +
   1.668 +fun dest_ext_fields sep mark (trm as (Const (c, _) $ t $ u)) =
   1.669 +      if c = sep then dest_ext_field mark t :: dest_ext_fields sep mark u
   1.670 +      else [dest_ext_field mark trm]
   1.671 +  | dest_ext_fields _ mark t = [dest_ext_field mark t];
   1.672  
   1.673  fun gen_ext_fields_tr sep mark sfx more ctxt t =
   1.674    let
   1.675      val thy = ProofContext.theory_of ctxt;
   1.676      val msg = "error in record input: ";
   1.677 +
   1.678      val fieldargs = dest_ext_fields sep mark t;
   1.679 -    fun splitargs (field::fields) ((name,arg)::fargs) =
   1.680 +    fun splitargs (field :: fields) ((name, arg) :: fargs) =
   1.681            if can (unsuffix name) field
   1.682 -          then let val (args,rest) = splitargs fields fargs
   1.683 -               in (arg::args,rest) end
   1.684 +          then
   1.685 +            let val (args, rest) = splitargs fields fargs
   1.686 +            in (arg :: args, rest) end
   1.687            else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   1.688 -      | splitargs [] (fargs as (_::_)) = ([],fargs)
   1.689 -      | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.690 -      | splitargs _ _ = ([],[]);
   1.691 -
   1.692 -    fun mk_ext (fargs as (name,arg)::_) =
   1.693 -         (case get_fieldext thy (Sign.intern_const thy name) of
   1.694 -            SOME (ext,_) => (case get_extfields thy ext of
   1.695 -                               SOME flds
   1.696 -                                 => let val (args,rest) =
   1.697 -                                               splitargs (map fst (but_last flds)) fargs;
   1.698 -                                        val more' = mk_ext rest;
   1.699 -                                    in list_comb (Syntax.const (suffix sfx ext),args@[more'])
   1.700 -                                    end
   1.701 -                             | NONE => raise TERM(msg ^ "no fields defined for "
   1.702 -                                                   ^ ext,[t]))
   1.703 -          | NONE => raise TERM (msg ^ name ^" is no proper field",[t]))
   1.704 -      | mk_ext [] = more
   1.705 -
   1.706 +      | splitargs [] (fargs as (_ :: _)) = ([], fargs)
   1.707 +      | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.708 +      | splitargs _ _ = ([], []);
   1.709 +
   1.710 +    fun mk_ext (fargs as (name, arg) :: _) =
   1.711 +          (case get_fieldext thy (Sign.intern_const thy name) of
   1.712 +            SOME (ext, _) =>
   1.713 +              (case get_extfields thy ext of
   1.714 +                SOME flds =>
   1.715 +                  let
   1.716 +                    val (args, rest) = splitargs (map fst (but_last flds)) fargs;
   1.717 +                    val more' = mk_ext rest;
   1.718 +                  in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end
   1.719 +              | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   1.720 +          | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   1.721 +      | mk_ext [] = more;
   1.722    in mk_ext fieldargs end;
   1.723  
   1.724  fun gen_ext_type_tr sep mark sfx more ctxt t =
   1.725    let
   1.726      val thy = ProofContext.theory_of ctxt;
   1.727      val msg = "error in record-type input: ";
   1.728 +
   1.729      val fieldargs = dest_ext_fields sep mark t;
   1.730 -    fun splitargs (field::fields) ((name,arg)::fargs) =
   1.731 -          if can (unsuffix name) field
   1.732 -          then let val (args,rest) = splitargs fields fargs
   1.733 -               in (arg::args,rest) end
   1.734 +    fun splitargs (field :: fields) ((name, arg) :: fargs) =
   1.735 +          if can (unsuffix name) field then
   1.736 +            let val (args, rest) = splitargs fields fargs
   1.737 +            in (arg :: args, rest) end
   1.738            else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   1.739 -      | splitargs [] (fargs as (_::_)) = ([],fargs)
   1.740 -      | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.741 -      | splitargs _ _ = ([],[]);
   1.742 -
   1.743 -    fun mk_ext (fargs as (name,arg)::_) =
   1.744 -         (case get_fieldext thy (Sign.intern_const thy name) of
   1.745 -            SOME (ext,alphas) =>
   1.746 +      | splitargs [] (fargs as (_ :: _)) = ([], fargs)
   1.747 +      | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   1.748 +      | splitargs _ _ = ([], []);
   1.749 +
   1.750 +    fun mk_ext (fargs as (name, arg) :: _) =
   1.751 +          (case get_fieldext thy (Sign.intern_const thy name) of
   1.752 +            SOME (ext, alphas) =>
   1.753                (case get_extfields thy ext of
   1.754 -                 SOME flds
   1.755 -                  => (let
   1.756 -                       val flds' = but_last flds;
   1.757 -                       val types = map snd flds';
   1.758 -                       val (args,rest) = splitargs (map fst flds') fargs;
   1.759 -                       val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
   1.760 -                       val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
   1.761 -                                    argtypes 0;
   1.762 -                       val varifyT = varifyT midx;
   1.763 -                       val vartypes = map varifyT types;
   1.764 -
   1.765 -                       val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes)
   1.766 -                                            Vartab.empty;
   1.767 -                       val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o
   1.768 -                                          Envir.norm_type subst o varifyT)
   1.769 -                                         (but_last alphas);
   1.770 -
   1.771 -                       val more' = mk_ext rest;
   1.772 -                     in list_comb (Syntax.const (suffix sfx ext),alphas'@[more'])
   1.773 -                     end handle TYPE_MATCH => raise
   1.774 -                           TERM (msg ^ "type is no proper record (extension)", [t]))
   1.775 -               | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t]))
   1.776 -          | NONE => raise TERM (msg ^ name ^" is no proper field",[t]))
   1.777 -      | mk_ext [] = more
   1.778 +                SOME flds =>
   1.779 +                 (let
   1.780 +                    val flds' = but_last flds;
   1.781 +                    val types = map snd flds';
   1.782 +                    val (args, rest) = splitargs (map fst flds') fargs;
   1.783 +                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
   1.784 +                    val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0;
   1.785 +                    val varifyT = varifyT midx;
   1.786 +                    val vartypes = map varifyT types;
   1.787 +
   1.788 +                    val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty;
   1.789 +                    val alphas' =
   1.790 +                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
   1.791 +                        (but_last alphas);
   1.792 +
   1.793 +                    val more' = mk_ext rest;
   1.794 +                  in
   1.795 +                    list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
   1.796 +                  end handle TYPE_MATCH =>
   1.797 +                    raise TERM (msg ^ "type is no proper record (extension)", [t]))
   1.798 +              | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   1.799 +          | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   1.800 +      | mk_ext [] = more;
   1.801  
   1.802    in mk_ext fieldargs end;
   1.803  
   1.804 @@ -856,25 +863,26 @@
   1.805    | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   1.806  
   1.807  val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
   1.808 +
   1.809  val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
   1.810  
   1.811  val adv_record_type_tr =
   1.812 -      gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
   1.813 -        (Syntax.term_of_typ false (HOLogic.unitT));
   1.814 +  gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
   1.815 +    (Syntax.term_of_typ false (HOLogic.unitT));
   1.816 +
   1.817  val adv_record_type_scheme_tr =
   1.818 -      gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   1.819 +  gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   1.820  
   1.821  
   1.822  val parse_translation =
   1.823   [("_record_update", record_update_tr),
   1.824    ("_update_name", update_name_tr)];
   1.825  
   1.826 -
   1.827  val adv_parse_translation =
   1.828 - [("_record",adv_record_tr),
   1.829 -  ("_record_scheme",adv_record_scheme_tr),
   1.830 -  ("_record_type",adv_record_type_tr),
   1.831 -  ("_record_type_scheme",adv_record_type_scheme_tr)];
   1.832 + [("_record", adv_record_tr),
   1.833 +  ("_record_scheme", adv_record_scheme_tr),
   1.834 +  ("_record_type", adv_record_type_tr),
   1.835 +  ("_record_type_scheme", adv_record_type_scheme_tr)];
   1.836  
   1.837  
   1.838  (* print translations *)
   1.839 @@ -883,27 +891,33 @@
   1.840  val print_record_type_as_fields = Unsynchronized.ref true;
   1.841  
   1.842  fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
   1.843 -  let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) 
   1.844 -                  => if null (loose_bnos t) then t else raise Match
   1.845 -               | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match
   1.846 -               | _ => raise Match)
   1.847 -
   1.848 -      (* (case k of (Const ("K_record",_)$t) => t
   1.849 -               | Abs (x,_,Const ("K_record",_)$t$Bound 0) => t
   1.850 -               | _ => raise Match)*)
   1.851 -  in
   1.852 -    (case try (unsuffix sfx) name_field of
   1.853 -      SOME name =>
   1.854 -        apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   1.855 -     | NONE => ([], tm))
   1.856 -  end
   1.857 +      let
   1.858 +        val t =
   1.859 +          (case k of
   1.860 +            Abs (_, _, Abs (_, _, t) $ Bound 0) =>
   1.861 +              if null (loose_bnos t) then t else raise Match
   1.862 +          | Abs (x, _, t) =>
   1.863 +              if null (loose_bnos t) then t else raise Match
   1.864 +          | _ => raise Match);
   1.865 +
   1.866 +          (* FIXME ? *)
   1.867 +          (* (case k of (Const ("K_record", _) $ t) => t
   1.868 +                   | Abs (x, _, Const ("K_record", _) $ t $ Bound 0) => t
   1.869 +                   | _ => raise Match)*)
   1.870 +      in
   1.871 +        (case try (unsuffix sfx) name_field of
   1.872 +          SOME name =>
   1.873 +            apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   1.874 +        | NONE => ([], tm))
   1.875 +      end
   1.876    | gen_field_upds_tr' _ _ tm = ([], tm);
   1.877  
   1.878  fun record_update_tr' tm =
   1.879    let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   1.880      if null ts then raise Match
   1.881 -    else Syntax.const "_record_update" $ u $
   1.882 -          foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   1.883 +    else
   1.884 +      Syntax.const "_record_update" $ u $
   1.885 +        foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   1.886    end;
   1.887  
   1.888  fun gen_field_tr' sfx tr' name =
   1.889 @@ -913,95 +927,96 @@
   1.890  fun record_tr' sep mark record record_scheme unit ctxt t =
   1.891    let
   1.892      val thy = ProofContext.theory_of ctxt;
   1.893 +
   1.894      fun field_lst t =
   1.895        (case strip_comb t of
   1.896 -        (Const (ext,_),args as (_::_))
   1.897 -         => (case try (unsuffix extN) (Sign.intern_const thy ext) of
   1.898 -               SOME ext'
   1.899 -               => (case get_extfields thy ext' of
   1.900 -                     SOME flds
   1.901 -                     => (let
   1.902 -                          val (f::fs) = but_last (map fst flds);
   1.903 -                          val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   1.904 -                          val (args',more) = split_last args;
   1.905 -                         in (flds'~~args')@field_lst more end
   1.906 -                         handle Library.UnequalLengths => [("",t)])
   1.907 -                   | NONE => [("",t)])
   1.908 -             | NONE => [("",t)])
   1.909 -       | _ => [("",t)])
   1.910 -
   1.911 -    val (flds,(_,more)) = split_last (field_lst t);
   1.912 +        (Const (ext, _), args as (_ :: _)) =>
   1.913 +          (case try (unsuffix extN) (Sign.intern_const thy ext) of
   1.914 +            SOME ext' =>
   1.915 +              (case get_extfields thy ext' of
   1.916 +                SOME flds =>
   1.917 +                 (let
   1.918 +                    val f :: fs = but_last (map fst flds);
   1.919 +                    val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   1.920 +                    val (args', more) = split_last args;
   1.921 +                  in (flds' ~~ args') @ field_lst more end
   1.922 +                  handle Library.UnequalLengths => [("", t)])
   1.923 +              | NONE => [("", t)])
   1.924 +          | NONE => [("", t)])
   1.925 +       | _ => [("", t)]);
   1.926 +
   1.927 +    val (flds, (_, more)) = split_last (field_lst t);
   1.928      val _ = if null flds then raise Match else ();
   1.929 -    val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds;
   1.930 -    val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
   1.931 -
   1.932 -  in if unit more
   1.933 -     then Syntax.const record$flds''
   1.934 -     else Syntax.const record_scheme$flds''$more
   1.935 -  end
   1.936 +    val flds' = map (fn (n, t) => Syntax.const mark $ Syntax.const n $ t) flds;
   1.937 +    val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds';
   1.938 +  in
   1.939 +    if unit more
   1.940 +    then Syntax.const record $ flds''
   1.941 +    else Syntax.const record_scheme $ flds'' $ more
   1.942 +  end;
   1.943  
   1.944  fun gen_record_tr' name =
   1.945 -  let val name_sfx = suffix extN name;
   1.946 -      val unit = (fn Const (@{const_syntax "Product_Type.Unity"},_) => true | _ => false);
   1.947 -      fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
   1.948 -                       (list_comb (Syntax.const name_sfx,ts))
   1.949 -  in (name_sfx,tr')
   1.950 -  end
   1.951 +  let
   1.952 +    val name_sfx = suffix extN name;
   1.953 +    val unit = (fn Const (@{const_syntax "Product_Type.Unity"}, _) => true | _ => false);
   1.954 +    fun tr' ctxt ts =
   1.955 +      record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
   1.956 +        (list_comb (Syntax.const name_sfx, ts));
   1.957 +  in (name_sfx, tr') end;
   1.958  
   1.959  fun print_translation names =
   1.960    map (gen_field_tr' updateN record_update_tr') names;
   1.961  
   1.962  
   1.963 -(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
   1.964 -(* the (nested) extension types.                                                    *)
   1.965 +(* record_type_abbr_tr' *)
   1.966 +
   1.967 +(*try to reconstruct the record name type abbreviation from
   1.968 +  the (nested) extension types*)
   1.969  fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
   1.970    let
   1.971 -      val thy = ProofContext.theory_of ctxt;
   1.972 -      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
   1.973 -      (* type from tm so that we can continue on the type level rather then the term level.*)
   1.974 -
   1.975 -      (* WORKAROUND:
   1.976 -       * If a record type occurs in an error message of type inference there
   1.977 -       * may be some internal frees donoted by ??:
   1.978 -       * (Const "_tfree",_)$Free ("??'a",_).
   1.979 -
   1.980 -       * This will unfortunately be translated to Type ("??'a",[]) instead of
   1.981 -       * TFree ("??'a",_) by typ_of_term, which will confuse unify below.
   1.982 -       * fixT works around.
   1.983 -       *)
   1.984 -      fun fixT (T as Type (x,[])) =
   1.985 -            if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T
   1.986 -        | fixT (Type (x,xs)) = Type (x,map fixT xs)
   1.987 -        | fixT T = T;
   1.988 -
   1.989 -      val T = fixT (decode_type thy tm);
   1.990 -      val midx = maxidx_of_typ T;
   1.991 -      val varifyT = varifyT midx;
   1.992 -
   1.993 -      fun mk_type_abbr subst name alphas =
   1.994 -          let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas);
   1.995 -          in Syntax.term_of_typ (! Syntax.show_sorts)
   1.996 -               (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
   1.997 -
   1.998 -      fun match rT T = (Sign.typ_match thy (varifyT rT,T)
   1.999 -                                                Vartab.empty);
  1.1000 -
  1.1001 -   in
  1.1002 -     if !print_record_type_abbr then
  1.1003 -       (case last_extT T of
  1.1004 -         SOME (name, _) =>
  1.1005 +    val thy = ProofContext.theory_of ctxt;
  1.1006 +
  1.1007 +    (*tm is term representation of a (nested) field type. We first reconstruct the
  1.1008 +      type from tm so that we can continue on the type level rather then the term level*)
  1.1009 +
  1.1010 +    (*WORKAROUND:
  1.1011 +      If a record type occurs in an error message of type inference there
  1.1012 +      may be some internal frees donoted by ??:
  1.1013 +      (Const "_tfree",_) $ Free ("??'a", _).
  1.1014 +
  1.1015 +      This will unfortunately be translated to Type ("??'a", []) instead of
  1.1016 +      TFree ("??'a", _) by typ_of_term, which will confuse unify below.
  1.1017 +      fixT works around.*)
  1.1018 +    fun fixT (T as Type (x, [])) =
  1.1019 +          if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T
  1.1020 +      | fixT (Type (x, xs)) = Type (x, map fixT xs)
  1.1021 +      | fixT T = T;
  1.1022 +
  1.1023 +    val T = fixT (decode_type thy tm);
  1.1024 +    val midx = maxidx_of_typ T;
  1.1025 +    val varifyT = varifyT midx;
  1.1026 +
  1.1027 +    fun mk_type_abbr subst name alphas =
  1.1028 +      let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
  1.1029 +        Syntax.term_of_typ (! Syntax.show_sorts)
  1.1030 +          (Sign.extern_typ thy (Envir.norm_type subst abbrT))
  1.1031 +      end;
  1.1032 +
  1.1033 +    fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
  1.1034 +  in
  1.1035 +    if ! print_record_type_abbr then
  1.1036 +      (case last_extT T of
  1.1037 +        SOME (name, _) =>
  1.1038            if name = lastExt then
  1.1039 -            (let
  1.1040 -               val subst = match schemeT T
  1.1041 -             in
  1.1042 +           (let val subst = match schemeT T in
  1.1043                if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
  1.1044                then mk_type_abbr subst abbr alphas
  1.1045                else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
  1.1046 -             end handle TYPE_MATCH => default_tr' ctxt tm)
  1.1047 -           else raise Match (* give print translation of specialised record a chance *)
  1.1048 -        | _ => raise Match)
  1.1049 -       else default_tr' ctxt tm
  1.1050 -  end
  1.1051 +            end handle TYPE_MATCH => default_tr' ctxt tm)
  1.1052 +          else raise Match (*give print translation of specialised record a chance*)
  1.1053 +      | _ => raise Match)
  1.1054 +    else default_tr' ctxt tm
  1.1055 +  end;
  1.1056  
  1.1057  fun record_type_tr' sep mark record record_scheme ctxt t =
  1.1058    let
  1.1059 @@ -1010,62 +1025,62 @@
  1.1060      val T = decode_type thy t;
  1.1061      val varifyT = varifyT (Term.maxidx_of_typ T);
  1.1062  
  1.1063 -    fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T);
  1.1064 +    fun term_of_type T = Syntax.term_of_typ (! Syntax.show_sorts) (Sign.extern_typ thy T);
  1.1065  
  1.1066      fun field_lst T =
  1.1067        (case T of
  1.1068 -        Type (ext, args)
  1.1069 -         => (case try (unsuffix ext_typeN) ext of
  1.1070 -               SOME ext'
  1.1071 -               => (case get_extfields thy ext' of
  1.1072 -                     SOME flds
  1.1073 -                     => (case get_fieldext thy (fst (hd flds)) of
  1.1074 -                           SOME (_, alphas)
  1.1075 -                           => (let
  1.1076 -                                val (f :: fs) = but_last flds;
  1.1077 -                                val flds' = apfst (Sign.extern_const thy) f
  1.1078 -                                  :: map (apfst Long_Name.base_name) fs;
  1.1079 -                                val (args', more) = split_last args;
  1.1080 -                                val alphavars = map varifyT (but_last alphas);
  1.1081 -                                val subst = fold2 (curry (Sign.typ_match thy))
  1.1082 -                                  alphavars args' Vartab.empty;
  1.1083 -                                val flds'' = (map o apsnd)
  1.1084 -                                  (Envir.norm_type subst o varifyT) flds';
  1.1085 -                              in flds'' @ field_lst more end
  1.1086 -                              handle TYPE_MATCH => [("", T)]
  1.1087 -                                  | Library.UnequalLengths => [("", T)])
  1.1088 -                         | NONE => [("", T)])
  1.1089 -                   | NONE => [("", T)])
  1.1090 -             | NONE => [("", T)])
  1.1091 -        | _ => [("", T)])
  1.1092 +        Type (ext, args) =>
  1.1093 +          (case try (unsuffix ext_typeN) ext of
  1.1094 +            SOME ext' =>
  1.1095 +              (case get_extfields thy ext' of
  1.1096 +                SOME flds =>
  1.1097 +                  (case get_fieldext thy (fst (hd flds)) of
  1.1098 +                    SOME (_, alphas) =>
  1.1099 +                     (let
  1.1100 +                        val f :: fs = but_last flds;
  1.1101 +                        val flds' = apfst (Sign.extern_const thy) f ::
  1.1102 +                          map (apfst Long_Name.base_name) fs;
  1.1103 +                        val (args', more) = split_last args;
  1.1104 +                        val alphavars = map varifyT (but_last alphas);
  1.1105 +                        val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
  1.1106 +                        val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
  1.1107 +                      in flds'' @ field_lst more end
  1.1108 +                      handle TYPE_MATCH => [("", T)]
  1.1109 +                        | Library.UnequalLengths => [("", T)])
  1.1110 +                  | NONE => [("", T)])
  1.1111 +              | NONE => [("", T)])
  1.1112 +          | NONE => [("", T)])
  1.1113 +      | _ => [("", T)]);
  1.1114  
  1.1115      val (flds, (_, moreT)) = split_last (field_lst T);
  1.1116      val flds' = map (fn (n, T) => Syntax.const mark $ Syntax.const n $ term_of_type T) flds;
  1.1117 -    val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds' handle Empty => raise Match;
  1.1118 -
  1.1119 -  in if not (!print_record_type_as_fields) orelse null flds then raise Match
  1.1120 -     else if moreT = HOLogic.unitT
  1.1121 -          then Syntax.const record$flds''
  1.1122 -          else Syntax.const record_scheme$flds''$term_of_type moreT
  1.1123 -  end
  1.1124 +    val flds'' =
  1.1125 +      foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds'
  1.1126 +        handle Empty => raise Match;
  1.1127 +  in
  1.1128 +    if not (! print_record_type_as_fields) orelse null flds then raise Match
  1.1129 +    else if moreT = HOLogic.unitT then Syntax.const record $ flds''
  1.1130 +    else Syntax.const record_scheme $ flds'' $ term_of_type moreT
  1.1131 +  end;
  1.1132  
  1.1133  
  1.1134  fun gen_record_type_tr' name =
  1.1135 -  let val name_sfx = suffix ext_typeN name;
  1.1136 -      fun tr' ctxt ts = record_type_tr' "_field_types" "_field_type"
  1.1137 -                       "_record_type" "_record_type_scheme" ctxt
  1.1138 -                       (list_comb (Syntax.const name_sfx,ts))
  1.1139 -  in (name_sfx,tr')
  1.1140 -  end
  1.1141 +  let
  1.1142 +    val name_sfx = suffix ext_typeN name;
  1.1143 +    fun tr' ctxt ts =
  1.1144 +      record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme"
  1.1145 +        ctxt (list_comb (Syntax.const name_sfx, ts))
  1.1146 +  in (name_sfx, tr') end;
  1.1147  
  1.1148  
  1.1149  fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
  1.1150 -  let val name_sfx = suffix ext_typeN name;
  1.1151 -      val default_tr' = record_type_tr' "_field_types" "_field_type"
  1.1152 -                               "_record_type" "_record_type_scheme"
  1.1153 -      fun tr' ctxt ts =
  1.1154 -          record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
  1.1155 -                               (list_comb (Syntax.const name_sfx,ts))
  1.1156 +  let
  1.1157 +    val name_sfx = suffix ext_typeN name;
  1.1158 +    val default_tr' =
  1.1159 +      record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme";
  1.1160 +    fun tr' ctxt ts =
  1.1161 +      record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
  1.1162 +        (list_comb (Syntax.const name_sfx, ts));
  1.1163    in (name_sfx, tr') end;
  1.1164  
  1.1165  
  1.1166 @@ -1076,26 +1091,28 @@
  1.1167  
  1.1168  
  1.1169  fun quick_and_dirty_prove stndrd thy asms prop tac =
  1.1170 -  if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
  1.1171 -  then Goal.prove (ProofContext.init thy) [] []
  1.1172 -        (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
  1.1173 -        (K (SkipProof.cheat_tac @{theory HOL}))
  1.1174 -        (* standard can take quite a while for large records, thats why
  1.1175 -         * we varify the proposition manually here.*)
  1.1176 -  else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
  1.1177 -       in if stndrd then standard prf else prf end;
  1.1178 +  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
  1.1179 +    Goal.prove (ProofContext.init thy) [] []
  1.1180 +      (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
  1.1181 +      (K (SkipProof.cheat_tac @{theory HOL}))
  1.1182 +      (*Drule.standard can take quite a while for large records, thats why
  1.1183 +        we varify the proposition manually here.*)
  1.1184 +  else
  1.1185 +    let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
  1.1186 +    in if stndrd then standard prf else prf end;
  1.1187  
  1.1188  fun quick_and_dirty_prf noopt opt () =
  1.1189 -      if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
  1.1190 -      then noopt ()
  1.1191 -      else opt ();
  1.1192 -
  1.1193 -fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t'))
  1.1194 -  = case (get_updates thy u)
  1.1195 -    of SOME u_name => u_name = s
  1.1196 -     | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]);
  1.1197 -
  1.1198 -fun mk_comp f g = let
  1.1199 +  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
  1.1200 +  then noopt ()
  1.1201 +  else opt ();
  1.1202 +
  1.1203 +fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) =
  1.1204 +  (case get_updates thy u of
  1.1205 +    SOME u_name => u_name = s
  1.1206 +  | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
  1.1207 +
  1.1208 +fun mk_comp f g =
  1.1209 +  let
  1.1210      val x = fastype_of g;
  1.1211      val a = domain_type x;
  1.1212      val b = range_type x;
  1.1213 @@ -1103,72 +1120,87 @@
  1.1214      val T = (b --> c) --> ((a --> b) --> (a --> c))
  1.1215    in Const ("Fun.comp", T) $ f $ g end;
  1.1216  
  1.1217 -fun mk_comp_id f = let
  1.1218 -    val T = range_type (fastype_of f);
  1.1219 +fun mk_comp_id f =
  1.1220 +  let val T = range_type (fastype_of f)
  1.1221    in mk_comp (Const ("Fun.id", T --> T)) f end;
  1.1222  
  1.1223  fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
  1.1224 -  | get_upd_funs _             = [];
  1.1225 -
  1.1226 -fun get_accupd_simps thy term defset intros_tac = let
  1.1227 +  | get_upd_funs _ = [];
  1.1228 +
  1.1229 +fun get_accupd_simps thy term defset intros_tac =
  1.1230 +  let
  1.1231      val (acc, [body]) = strip_comb term;
  1.1232 -    val recT          = domain_type (fastype_of acc);
  1.1233 -    val upd_funs      = sort_distinct TermOrd.fast_term_ord
  1.1234 -                           (get_upd_funs body);
  1.1235 -    fun get_simp upd  = let
  1.1236 -        val T    = domain_type (fastype_of upd);
  1.1237 -        val lhs  = mk_comp acc (upd $ Free ("f", T));
  1.1238 -        val rhs  = if is_sel_upd_pair thy acc upd
  1.1239 -                   then mk_comp (Free ("f", T)) acc else mk_comp_id acc;
  1.1240 +    val recT = domain_type (fastype_of acc);
  1.1241 +    val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
  1.1242 +    fun get_simp upd =
  1.1243 +      let
  1.1244 +        val T = domain_type (fastype_of upd);
  1.1245 +        val lhs = mk_comp acc (upd $ Free ("f", T));
  1.1246 +        val rhs =
  1.1247 +          if is_sel_upd_pair thy acc upd
  1.1248 +          then mk_comp (Free ("f", T)) acc
  1.1249 +          else mk_comp_id acc;
  1.1250          val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
  1.1251 -        val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
  1.1252 -            EVERY [simp_tac defset 1,
  1.1253 -                   REPEAT_DETERM (intros_tac 1),
  1.1254 -                   TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
  1.1255 -        val dest = if is_sel_upd_pair thy acc upd
  1.1256 -                   then o_eq_dest else o_eq_id_dest;
  1.1257 +        val othm =
  1.1258 +          Goal.prove (ProofContext.init thy) [] [] prop
  1.1259 +            (fn prems =>
  1.1260 +              EVERY
  1.1261 +               [simp_tac defset 1,
  1.1262 +                REPEAT_DETERM (intros_tac 1),
  1.1263 +                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
  1.1264 +        val dest =
  1.1265 +          if is_sel_upd_pair thy acc upd
  1.1266 +          then o_eq_dest
  1.1267 +          else o_eq_id_dest;
  1.1268        in standard (othm RS dest) end;
  1.1269    in map get_simp upd_funs end;
  1.1270  
  1.1271 -structure SymSymTab = Table(type key = string * string
  1.1272 -                            val ord = prod_ord fast_string_ord fast_string_ord);
  1.1273 -
  1.1274 -fun get_updupd_simp thy defset intros_tac u u' comp = let
  1.1275 -    val f    = Free ("f", domain_type (fastype_of u));
  1.1276 -    val f'   = Free ("f'", domain_type (fastype_of u'));
  1.1277 -    val lhs  = mk_comp (u $ f) (u' $ f');
  1.1278 -    val rhs  = if comp
  1.1279 -               then u $ mk_comp f f'
  1.1280 -               else mk_comp (u' $ f') (u $ f);
  1.1281 +(* FIXME dup? *)
  1.1282 +structure SymSymTab =
  1.1283 +  Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
  1.1284 +
  1.1285 +fun get_updupd_simp thy defset intros_tac u u' comp =
  1.1286 +  let
  1.1287 +    val f = Free ("f", domain_type (fastype_of u));
  1.1288 +    val f' = Free ("f'", domain_type (fastype_of u'));
  1.1289 +    val lhs = mk_comp (u $ f) (u' $ f');
  1.1290 +    val rhs =
  1.1291 +      if comp
  1.1292 +      then u $ mk_comp f f'
  1.1293 +      else mk_comp (u' $ f') (u $ f);
  1.1294      val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
  1.1295 -    val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
  1.1296 -        EVERY [simp_tac defset 1,
  1.1297 -               REPEAT_DETERM (intros_tac 1),
  1.1298 -               TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
  1.1299 +    val othm =
  1.1300 +      Goal.prove (ProofContext.init thy) [] [] prop
  1.1301 +        (fn prems =>
  1.1302 +          EVERY
  1.1303 +           [simp_tac defset 1,
  1.1304 +            REPEAT_DETERM (intros_tac 1),
  1.1305 +            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
  1.1306      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
  1.1307    in standard (othm RS dest) end;
  1.1308  
  1.1309 -fun get_updupd_simps thy term defset intros_tac = let
  1.1310 -    val recT          = fastype_of term;
  1.1311 -    val upd_funs      = get_upd_funs term;
  1.1312 -    val cname         = fst o dest_Const;
  1.1313 -    fun getswap u u'  = get_updupd_simp thy defset intros_tac u u'
  1.1314 -                              (cname u = cname u');
  1.1315 +fun get_updupd_simps thy term defset intros_tac =
  1.1316 +  let
  1.1317 +    val recT = fastype_of term;
  1.1318 +    val upd_funs = get_upd_funs term;
  1.1319 +    val cname = fst o dest_Const;
  1.1320 +    fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
  1.1321      fun build_swaps_to_eq upd [] swaps = swaps
  1.1322 -      | build_swaps_to_eq upd (u::us) swaps = let
  1.1323 -             val key      = (cname u, cname upd);
  1.1324 -             val newswaps = if SymSymTab.defined swaps key then swaps
  1.1325 -                            else SymSymTab.insert (K true)
  1.1326 -                                     (key, getswap u upd) swaps;
  1.1327 -          in if cname u = cname upd then newswaps
  1.1328 -             else build_swaps_to_eq upd us newswaps end;
  1.1329 -    fun swaps_needed []      prev seen swaps = map snd (SymSymTab.dest swaps)
  1.1330 -      | swaps_needed (u::us) prev seen swaps =
  1.1331 -           if Symtab.defined seen (cname u)
  1.1332 -           then swaps_needed us prev seen
  1.1333 -                   (build_swaps_to_eq u prev swaps)
  1.1334 -           else swaps_needed us (u::prev)
  1.1335 -                   (Symtab.insert (K true) (cname u, ()) seen) swaps;
  1.1336 +      | build_swaps_to_eq upd (u :: us) swaps =
  1.1337 +          let
  1.1338 +            val key = (cname u, cname upd);
  1.1339 +            val newswaps =
  1.1340 +              if SymSymTab.defined swaps key then swaps
  1.1341 +              else SymSymTab.insert (K true) (key, getswap u upd) swaps;
  1.1342 +          in
  1.1343 +            if cname u = cname upd then newswaps
  1.1344 +            else build_swaps_to_eq upd us newswaps
  1.1345 +          end;
  1.1346 +    fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps)
  1.1347 +      | swaps_needed (u :: us) prev seen swaps =
  1.1348 +          if Symtab.defined seen (cname u)
  1.1349 +          then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
  1.1350 +          else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
  1.1351    in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
  1.1352  
  1.1353  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
  1.1354 @@ -1177,326 +1209,351 @@
  1.1355    let
  1.1356      val defset = get_sel_upd_defs thy;
  1.1357      val in_tac = IsTupleSupport.istuple_intros_tac thy;
  1.1358 -    val prop'  = Envir.beta_eta_contract prop;
  1.1359 -    val (lhs, rhs)   = Logic.dest_equals (Logic.strip_assums_concl prop');
  1.1360 +    val prop' = Envir.beta_eta_contract prop;
  1.1361 +    val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
  1.1362      val (head, args) = strip_comb lhs;
  1.1363 -    val simps        = if length args = 1
  1.1364 -                       then get_accupd_simps thy lhs defset in_tac
  1.1365 -                       else get_updupd_simps thy lhs defset in_tac;
  1.1366 +    val simps =
  1.1367 +      if length args = 1
  1.1368 +      then get_accupd_simps thy lhs defset in_tac
  1.1369 +      else get_updupd_simps thy lhs defset in_tac;
  1.1370    in
  1.1371 -    Goal.prove (ProofContext.init thy) [] [] prop' (fn prems =>
  1.1372 -              simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1
  1.1373 -         THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps
  1.1374 -                                          addsimprocs ex_simprs) 1))
  1.1375 +    Goal.prove (ProofContext.init thy) [] [] prop'
  1.1376 +      (fn prems =>
  1.1377 +        simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
  1.1378 +        TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
  1.1379    end;
  1.1380  
  1.1381  
  1.1382  local
  1.1383 -fun eq (s1:string) (s2:string) = (s1 = s2);
  1.1384 +
  1.1385 +fun eq (s1: string) (s2: string) = (s1 = s2);
  1.1386 +
  1.1387  fun has_field extfields f T =
  1.1388 -     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN))
  1.1389 -       (dest_recTs T);
  1.1390 -
  1.1391 -fun K_skeleton n (T as Type (_,[_,kT])) (b as Bound i) (Abs (x,xT,t)) =
  1.1392 -     if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b)
  1.1393 -  | K_skeleton n T b _ = ((n,T),b);
  1.1394 +  exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
  1.1395 +
  1.1396 +fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
  1.1397 +      if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  1.1398 +  | K_skeleton n T b _ = ((n, T), b);
  1.1399  
  1.1400  in
  1.1401 +
  1.1402  (* record_simproc *)
  1.1403 -(* Simplifies selections of an record update:
  1.1404 - *  (1)  S (S_update k r) = k (S r)
  1.1405 - *  (2)  S (X_update k r) = S r
  1.1406 - * The simproc skips multiple updates at once, eg:
  1.1407 - *  S (X_update x (Y_update y (S_update k r))) = k (S r)
  1.1408 - * But be careful in (2) because of the extendibility of records.
  1.1409 - * - If S is a more-selector we have to make sure that the update on component
  1.1410 - *   X does not affect the selected subrecord.
  1.1411 - * - If X is a more-selector we have to make sure that S is not in the updated
  1.1412 - *   subrecord.
  1.1413 - *)
  1.1414 +
  1.1415 +(*
  1.1416 +  Simplify selections of an record update:
  1.1417 +    (1)  S (S_update k r) = k (S r)
  1.1418 +    (2)  S (X_update k r) = S r
  1.1419 +
  1.1420 +  The simproc skips multiple updates at once, eg:
  1.1421 +   S (X_update x (Y_update y (S_update k r))) = k (S r)
  1.1422 +
  1.1423 +  But be careful in (2) because of the extensibility of records.
  1.1424 +  - If S is a more-selector we have to make sure that the update on component
  1.1425 +    X does not affect the selected subrecord.
  1.1426 +  - If X is a more-selector we have to make sure that S is not in the updated
  1.1427 +    subrecord.
  1.1428 +*)
  1.1429  val record_simproc =
  1.1430    Simplifier.simproc @{theory HOL} "record_simp" ["x"]
  1.1431      (fn thy => fn ss => fn t =>
  1.1432 -      (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
  1.1433 -                   ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
  1.1434 -        if is_selector thy s then
  1.1435 -          (case get_updates thy u of SOME u_name =>
  1.1436 -            let
  1.1437 -              val {sel_upd={updates,...},extfields,...} = RecordsData.get thy;
  1.1438 -
  1.1439 -              fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) =
  1.1440 -                  (case Symtab.lookup updates u of
  1.1441 -                     NONE => NONE
  1.1442 -                   | SOME u_name
  1.1443 -                     => if u_name = s
  1.1444 -                        then (case mk_eq_terms r of
  1.1445 -                               NONE =>
  1.1446 -                                 let
  1.1447 -                                   val rv = ("r",rT)
  1.1448 -                                   val rb = Bound 0
  1.1449 -                                   val (kv,kb) = K_skeleton "k" kT (Bound 1) k;
  1.1450 -                                  in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end
  1.1451 -                              | SOME (trm,trm',vars) =>
  1.1452 -                                 let
  1.1453 -                                   val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k;
  1.1454 -                                 in SOME (upd$kb$trm,kb$trm',kv::vars) end)
  1.1455 -                        else if has_field extfields u_name rangeS
  1.1456 -                             orelse has_field extfields s (domain_type kT)
  1.1457 -                             then NONE
  1.1458 -                             else (case mk_eq_terms r of
  1.1459 -                                     SOME (trm,trm',vars)
  1.1460 -                                     => let
  1.1461 -                                          val (kv,kb) =
  1.1462 -                                                 K_skeleton "k" kT (Bound (length vars)) k;
  1.1463 -                                        in SOME (upd$kb$trm,trm',kv::vars) end
  1.1464 -                                   | NONE
  1.1465 -                                     => let
  1.1466 -                                          val rv = ("r",rT)
  1.1467 -                                          val rb = Bound 0
  1.1468 -                                          val (kv,kb) = K_skeleton "k" kT (Bound 1) k;
  1.1469 -                                        in SOME (upd$kb$rb,sel$rb,[kv,rv]) end))
  1.1470 -                | mk_eq_terms r = NONE
  1.1471 -            in
  1.1472 -              (case mk_eq_terms (upd$k$r) of
  1.1473 -                 SOME (trm,trm',vars)
  1.1474 -                 => SOME (prove_unfold_defs thy ss domS [] []
  1.1475 -                             (list_all(vars,(Logic.mk_equals (sel$trm, trm')))))
  1.1476 -               | NONE => NONE)
  1.1477 -            end
  1.1478 -          | NONE => NONE)
  1.1479 -        else NONE
  1.1480 +      (case t of
  1.1481 +        (sel as Const (s, Type (_, [domS, rangeS]))) $
  1.1482 +            ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
  1.1483 +          if is_selector thy s then
  1.1484 +            (case get_updates thy u of
  1.1485 +              SOME u_name =>
  1.1486 +                let
  1.1487 +                  val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
  1.1488 +
  1.1489 +                  fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
  1.1490 +                        (case Symtab.lookup updates u of
  1.1491 +                          NONE => NONE
  1.1492 +                        | SOME u_name =>
  1.1493 +                            if u_name = s then
  1.1494 +                              (case mk_eq_terms r of
  1.1495 +                                NONE =>
  1.1496 +                                  let
  1.1497 +                                    val rv = ("r", rT);
  1.1498 +                                    val rb = Bound 0;
  1.1499 +                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1.1500 +                                  in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
  1.1501 +                              | SOME (trm, trm', vars) =>
  1.1502 +                                  let
  1.1503 +                                    val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
  1.1504 +                                  in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
  1.1505 +                            else if has_field extfields u_name rangeS orelse
  1.1506 +                              has_field extfields s (domain_type kT) then NONE
  1.1507 +                            else
  1.1508 +                              (case mk_eq_terms r of
  1.1509 +                                SOME (trm, trm', vars) =>
  1.1510 +                                  let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
  1.1511 +                                  in SOME (upd $ kb $ trm, trm', kv :: vars) end
  1.1512 +                              | NONE =>
  1.1513 +                                  let
  1.1514 +                                    val rv = ("r", rT);
  1.1515 +                                    val rb = Bound 0;
  1.1516 +                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1.1517 +                                  in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
  1.1518 +                    | mk_eq_terms r = NONE;
  1.1519 +                in
  1.1520 +                  (case mk_eq_terms (upd $ k $ r) of
  1.1521 +                    SOME (trm, trm', vars) =>
  1.1522 +                      SOME
  1.1523 +                        (prove_unfold_defs thy ss domS [] []
  1.1524 +                          (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
  1.1525 +                  | NONE => NONE)
  1.1526 +                end
  1.1527 +            | NONE => NONE)
  1.1528 +          else NONE
  1.1529        | _ => NONE));
  1.1530  
  1.1531 -fun get_upd_acc_cong_thm upd acc thy simpset = let
  1.1532 +fun get_upd_acc_cong_thm upd acc thy simpset =
  1.1533 +  let
  1.1534      val in_tac = IsTupleSupport.istuple_intros_tac thy;
  1.1535  
  1.1536      val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
  1.1537 -    val prop  = concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1.1538 -  in Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
  1.1539 -        EVERY [simp_tac simpset 1,
  1.1540 -               REPEAT_DETERM (in_tac 1),
  1.1541 -               TRY (resolve_tac [updacc_cong_idI] 1)])
  1.1542 +    val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1.1543 +  in
  1.1544 +    Goal.prove (ProofContext.init thy) [] [] prop
  1.1545 +      (fn prems =>
  1.1546 +        EVERY
  1.1547 +         [simp_tac simpset 1,
  1.1548 +          REPEAT_DETERM (in_tac 1),
  1.1549 +          TRY (resolve_tac [updacc_cong_idI] 1)])
  1.1550    end;
  1.1551  
  1.1552 +
  1.1553  (* record_upd_simproc *)
  1.1554 -(* simplify multiple updates:
  1.1555 - *  (1)  "N_update y (M_update g (N_update x (M_update f r))) =
  1.1556 +
  1.1557 +(*Simplify multiple updates:
  1.1558 +    (1) "N_update y (M_update g (N_update x (M_update f r))) =
  1.1559            (N_update (y o x) (M_update (g o f) r))"
  1.1560 - *  (2)  "r(|M:= M r|) = r"
  1.1561 - * In both cases "more" updates complicate matters: for this reason
  1.1562 - * we omit considering further updates if doing so would introduce
  1.1563 - * both a more update and an update to a field within it.
  1.1564 -*)
  1.1565 +    (2)  "r(|M:= M r|) = r"
  1.1566 +
  1.1567 +  In both cases "more" updates complicate matters: for this reason
  1.1568 +  we omit considering further updates if doing so would introduce
  1.1569 +  both a more update and an update to a field within it.*)
  1.1570  val record_upd_simproc =
  1.1571    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
  1.1572      (fn thy => fn ss => fn t =>
  1.1573        let
  1.1574 -        (* we can use more-updators with other updators as long
  1.1575 -           as none of the other updators go deeper than any more
  1.1576 -           updator. min here is the depth of the deepest other
  1.1577 -           updator, max the depth of the shallowest more updator *)
  1.1578 +        (*We can use more-updators with other updators as long
  1.1579 +          as none of the other updators go deeper than any more
  1.1580 +          updator. min here is the depth of the deepest other
  1.1581 +          updator, max the depth of the shallowest more updator.*)
  1.1582          fun include_depth (dep, true) (min, max) =
  1.1583 -          if (min <= dep)
  1.1584 -          then SOME (min, if dep <= max orelse max = ~1 then dep else max)
  1.1585 -          else NONE
  1.1586 +              if min <= dep
  1.1587 +              then SOME (min, if dep <= max orelse max = ~1 then dep else max)
  1.1588 +              else NONE
  1.1589            | include_depth (dep, false) (min, max) =
  1.1590 -          if (dep <= max orelse max = ~1)
  1.1591 -          then SOME (if min <= dep then dep else min, max)
  1.1592 -          else NONE;
  1.1593 +              if dep <= max orelse max = ~1
  1.1594 +              then SOME (if min <= dep then dep else min, max)
  1.1595 +              else NONE;
  1.1596  
  1.1597          fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
  1.1598 -            (case get_update_details u thy of
  1.1599 -              SOME (s, dep, ismore) =>
  1.1600 -                (case include_depth (dep, ismore) (min, max) of
  1.1601 -                  SOME (min', max') => let
  1.1602 -                        val (us, bs, _) = getupdseq tm min' max';
  1.1603 +              (case get_update_details u thy of
  1.1604 +                SOME (s, dep, ismore) =>
  1.1605 +                  (case include_depth (dep, ismore) (min, max) of
  1.1606 +                    SOME (min', max') =>
  1.1607 +                      let val (us, bs, _) = getupdseq tm min' max'
  1.1608                        in ((upd, s, f) :: us, bs, fastype_of term) end
  1.1609 -                | NONE => ([], term, HOLogic.unitT))
  1.1610 -            | NONE => ([], term, HOLogic.unitT))
  1.1611 +                  | NONE => ([], term, HOLogic.unitT))
  1.1612 +              | NONE => ([], term, HOLogic.unitT))
  1.1613            | getupdseq term _ _ = ([], term, HOLogic.unitT);
  1.1614  
  1.1615          val (upds, base, baseT) = getupdseq t 0 ~1;
  1.1616  
  1.1617          fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
  1.1618 -            if s = s' andalso null (loose_bnos tm')
  1.1619 -              andalso subst_bound (HOLogic.unit, tm') = tm
  1.1620 -            then (true, Abs (n, T, Const (s', T') $ Bound 1))
  1.1621 -            else (false, HOLogic.unit)
  1.1622 +              if s = s' andalso null (loose_bnos tm')
  1.1623 +                andalso subst_bound (HOLogic.unit, tm') = tm
  1.1624 +              then (true, Abs (n, T, Const (s', T') $ Bound 1))
  1.1625 +              else (false, HOLogic.unit)
  1.1626            | is_upd_noop s f tm = (false, HOLogic.unit);
  1.1627  
  1.1628          fun get_noop_simps (upd as Const (u, T))
  1.1629 -                      (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = let
  1.1630 -
  1.1631 -            val ss    = get_sel_upd_defs thy;
  1.1632 +            (f as Abs (n, T', (acc as Const (s, T'')) $ _)) =
  1.1633 +          let
  1.1634 +            val ss = get_sel_upd_defs thy;
  1.1635              val uathm = get_upd_acc_cong_thm upd acc thy ss;
  1.1636 -          in [standard (uathm RS updacc_noopE),
  1.1637 -              standard (uathm RS updacc_noop_compE)] end;
  1.1638 -
  1.1639 -        (* if f is constant then (f o g) = f. we know that K_skeleton
  1.1640 -           only returns constant abstractions thus when we see an
  1.1641 -           abstraction we can discard inner updates. *)
  1.1642 +          in
  1.1643 +            [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
  1.1644 +          end;
  1.1645 +
  1.1646 +        (*If f is constant then (f o g) = f. we know that K_skeleton
  1.1647 +          only returns constant abstractions thus when we see an
  1.1648 +          abstraction we can discard inner updates.*)
  1.1649          fun add_upd (f as Abs _) fs = [f]
  1.1650            | add_upd f fs = (f :: fs);
  1.1651  
  1.1652 -        (* mk_updterm returns
  1.1653 -         * (orig-term-skeleton, simplified-skeleton,
  1.1654 -         *  variables, duplicate-updates, simp-flag, noop-simps)
  1.1655 -         *
  1.1656 -         *  where duplicate-updates is a table used to pass upward
  1.1657 -         *  the list of update functions which can be composed
  1.1658 -         *  into an update above them, simp-flag indicates whether
  1.1659 -         *  any simplification was achieved, and noop-simps are
  1.1660 -         *  used for eliminating case (2) defined above
  1.1661 -         *)
  1.1662 -        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let
  1.1663 -            val (lhs, rhs, vars, dups, simp, noops) =
  1.1664 +        (*mk_updterm returns
  1.1665 +          (orig-term-skeleton, simplified-skeleton,
  1.1666 +            variables, duplicate-updates, simp-flag, noop-simps)
  1.1667 +
  1.1668 +          where duplicate-updates is a table used to pass upward
  1.1669 +          the list of update functions which can be composed
  1.1670 +          into an update above them, simp-flag indicates whether
  1.1671 +          any simplification was achieved, and noop-simps are
  1.1672 +          used for eliminating case (2) defined above*)
  1.1673 +        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
  1.1674 +              let
  1.1675 +                val (lhs, rhs, vars, dups, simp, noops) =
  1.1676                    mk_updterm upds (Symtab.update (u, ()) above) term;
  1.1677 -            val (fvar, skelf) = K_skeleton (Long_Name.base_name s) (domain_type T)
  1.1678 -                                      (Bound (length vars)) f;
  1.1679 -            val (isnoop, skelf') = is_upd_noop s f term;
  1.1680 -            val funT  = domain_type T;
  1.1681 -            fun mk_comp_local (f, f') =
  1.1682 -              Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
  1.1683 -          in if isnoop
  1.1684 -              then (upd $ skelf' $ lhs, rhs, vars,
  1.1685 +                val (fvar, skelf) =
  1.1686 +                  K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
  1.1687 +                val (isnoop, skelf') = is_upd_noop s f term;
  1.1688 +                val funT = domain_type T;
  1.1689 +                fun mk_comp_local (f, f') = Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
  1.1690 +              in
  1.1691 +                if isnoop then
  1.1692 +                  (upd $ skelf' $ lhs, rhs, vars,
  1.1693                      Symtab.update (u, []) dups, true,
  1.1694                      if Symtab.defined noops u then noops
  1.1695                      else Symtab.update (u, get_noop_simps upd skelf') noops)
  1.1696 -            else if Symtab.defined above u
  1.1697 -              then (upd $ skelf $ lhs, rhs, fvar :: vars,
  1.1698 +                else if Symtab.defined above u then
  1.1699 +                  (upd $ skelf $ lhs, rhs, fvar :: vars,
  1.1700                      Symtab.map_default (u, []) (add_upd skelf) dups,
  1.1701                      true, noops)
  1.1702 -            else case Symtab.lookup dups u of
  1.1703 -              SOME fs =>
  1.1704 -                   (upd $ skelf $ lhs,
  1.1705 -                    upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
  1.1706 -                    fvar :: vars, dups, true, noops)
  1.1707 -            | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs,
  1.1708 -                       fvar :: vars, dups, simp, noops)
  1.1709 -          end
  1.1710 -          | mk_updterm [] above term = (Bound 0, Bound 0, [("r", baseT)],
  1.1711 -                                          Symtab.empty, false, Symtab.empty)
  1.1712 -          | mk_updterm us above term = raise TERM ("mk_updterm match",
  1.1713 -                                              map (fn (x, y, z) => x) us);
  1.1714 -
  1.1715 -        val (lhs, rhs, vars, dups, simp, noops)
  1.1716 -                  = mk_updterm upds Symtab.empty base;
  1.1717 +                else
  1.1718 +                  (case Symtab.lookup dups u of
  1.1719 +                    SOME fs =>
  1.1720 +                     (upd $ skelf $ lhs,
  1.1721 +                      upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
  1.1722 +                      fvar :: vars, dups, true, noops)
  1.1723 +                  | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
  1.1724 +              end
  1.1725 +          | mk_updterm [] above term =
  1.1726 +              (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
  1.1727 +          | mk_updterm us above term =
  1.1728 +              raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us);
  1.1729 +
  1.1730 +        val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base;
  1.1731          val noops' = flat (map snd (Symtab.dest noops));
  1.1732        in
  1.1733          if simp then
  1.1734 -           SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
  1.1735 -                             (list_all(vars,(Logic.mk_equals (lhs, rhs)))))
  1.1736 +          SOME
  1.1737 +            (prove_unfold_defs thy ss baseT noops' [record_simproc]
  1.1738 +              (list_all (vars, Logic.mk_equals (lhs, rhs))))
  1.1739          else NONE
  1.1740 -      end)
  1.1741 -
  1.1742 -end
  1.1743 +      end);
  1.1744 +
  1.1745 +end;
  1.1746  
  1.1747  
  1.1748  (* record_eq_simproc *)
  1.1749 -(* looks up the most specific record-equality.
  1.1750 - * Note on efficiency:
  1.1751 - * Testing equality of records boils down to the test of equality of all components.
  1.1752 - * Therefore the complexity is: #components * complexity for single component.
  1.1753 - * Especially if a record has a lot of components it may be better to split up
  1.1754 - * the record first and do simplification on that (record_split_simp_tac).
  1.1755 - * e.g. r(|lots of updates|) = x
  1.1756 - *
  1.1757 - *               record_eq_simproc       record_split_simp_tac
  1.1758 - * Complexity: #components * #updates     #updates
  1.1759 - *
  1.1760 - *)
  1.1761 +
  1.1762 +(*Looks up the most specific record-equality.
  1.1763 +
  1.1764 + Note on efficiency:
  1.1765 + Testing equality of records boils down to the test of equality of all components.
  1.1766 + Therefore the complexity is: #components * complexity for single component.
  1.1767 + Especially if a record has a lot of components it may be better to split up
  1.1768 + the record first and do simplification on that (record_split_simp_tac).
  1.1769 + e.g. r(|lots of updates|) = x
  1.1770 +
  1.1771 +             record_eq_simproc          record_split_simp_tac
  1.1772 + Complexity: #components * #updates     #updates
  1.1773 +*)
  1.1774  val record_eq_simproc =
  1.1775    Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
  1.1776      (fn thy => fn _ => fn t =>
  1.1777        (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
  1.1778 -        (case rec_id (~1) T of
  1.1779 -           "" => NONE
  1.1780 -         | name => (case get_equalities thy name of
  1.1781 -                                NONE => NONE
  1.1782 -                              | SOME thm => SOME (thm RS Eq_TrueI)))
  1.1783 -       | _ => NONE));
  1.1784 +        (case rec_id ~1 T of
  1.1785 +          "" => NONE
  1.1786 +        | name =>
  1.1787 +            (case get_equalities thy name of
  1.1788 +              NONE => NONE
  1.1789 +            | SOME thm => SOME (thm RS Eq_TrueI)))
  1.1790 +      | _ => NONE));
  1.1791 +
  1.1792  
  1.1793  (* record_split_simproc *)
  1.1794 -(* splits quantified occurrences of records, for which P holds. P can peek on the
  1.1795 - * subterm starting at the quantified occurrence of the record (including the quantifier)
  1.1796 - * P t = 0: do not split
  1.1797 - * P t = ~1: completely split
  1.1798 - * P t > 0: split up to given bound of record extensions
  1.1799 - *)
  1.1800 +
  1.1801 +(*Split quantified occurrences of records, for which P holds.  P can peek on the
  1.1802 +  subterm starting at the quantified occurrence of the record (including the quantifier):
  1.1803 +    P t = 0: do not split
  1.1804 +    P t = ~1: completely split
  1.1805 +    P t > 0: split up to given bound of record extensions.*)
  1.1806  fun record_split_simproc P =
  1.1807    Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
  1.1808      (fn thy => fn _ => fn t =>
  1.1809 -      (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
  1.1810 -         if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
  1.1811 -         then (case rec_id (~1) T of
  1.1812 -                 "" => NONE
  1.1813 -               | name
  1.1814 -                  => let val split = P t
  1.1815 -                     in if split <> 0 then
  1.1816 -                        (case get_splits thy (rec_id split T) of
  1.1817 -                              NONE => NONE
  1.1818 -                            | SOME (all_thm, All_thm, Ex_thm,_)
  1.1819 -                               => SOME (case quantifier of
  1.1820 -                                          "all" => all_thm
  1.1821 -                                        | "All" => All_thm RS eq_reflection
  1.1822 -                                        | "Ex"  => Ex_thm RS eq_reflection
  1.1823 -                                        | _     => error "record_split_simproc"))
  1.1824 -                        else NONE
  1.1825 -                      end)
  1.1826 -         else NONE
  1.1827 -       | _ => NONE))
  1.1828 +      (case t of
  1.1829 +        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm =>
  1.1830 +          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
  1.1831 +            (case rec_id ~1 T of
  1.1832 +              "" => NONE
  1.1833 +            | name =>
  1.1834 +                let val split = P t in
  1.1835 +                  if split <> 0 then
  1.1836 +                    (case get_splits thy (rec_id split T) of
  1.1837 +                      NONE => NONE
  1.1838 +                    | SOME (all_thm, All_thm, Ex_thm, _) =>
  1.1839 +                        SOME
  1.1840 +                          (case quantifier of
  1.1841 +                            "all" => all_thm
  1.1842 +                          | "All" => All_thm RS eq_reflection
  1.1843 +                          | "Ex" => Ex_thm RS eq_reflection
  1.1844 +                          | _ => error "record_split_simproc"))
  1.1845 +                  else NONE
  1.1846 +                end)
  1.1847 +          else NONE
  1.1848 +      | _ => NONE));
  1.1849  
  1.1850  val record_ex_sel_eq_simproc =
  1.1851    Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
  1.1852      (fn thy => fn ss => fn t =>
  1.1853 -       let
  1.1854 -         fun prove prop =
  1.1855 -           quick_and_dirty_prove true thy [] prop
  1.1856 -             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1.1857 -               addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
  1.1858 -
  1.1859 -         fun mkeq (lr,Teq,(sel,Tsel),x) i =
  1.1860 -              if is_selector thy sel then
  1.1861 -                 let val x' = if not (loose_bvar1 (x,0))
  1.1862 -                              then Free ("x" ^ string_of_int i, range_type Tsel)
  1.1863 -                              else raise TERM ("",[x]);
  1.1864 -                     val sel' = Const (sel,Tsel)$Bound 0;
  1.1865 -                     val (l,r) = if lr then (sel',x') else (x',sel');
  1.1866 -                  in Const ("op =",Teq)$l$r end
  1.1867 -              else raise TERM ("",[Const (sel,Tsel)]);
  1.1868 -
  1.1869 -         fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) =
  1.1870 -                           (true,Teq,(sel,Tsel),X)
  1.1871 -           | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) =
  1.1872 -                           (false,Teq,(sel,Tsel),X)
  1.1873 -           | dest_sel_eq _ = raise TERM ("",[]);
  1.1874 -
  1.1875 -       in
  1.1876 -         (case t of
  1.1877 -           (Const ("Ex",Tex)$Abs(s,T,t)) =>
  1.1878 -             (let val eq = mkeq (dest_sel_eq t) 0;
  1.1879 -                 val prop = list_all ([("r",T)],
  1.1880 -                              Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
  1.1881 -                                               HOLogic.true_const));
  1.1882 -             in SOME (prove prop) end
  1.1883 -             handle TERM _ => NONE)
  1.1884 -          | _ => NONE)
  1.1885 -         end)
  1.1886 +      let
  1.1887 +        fun prove prop =
  1.1888 +          quick_and_dirty_prove true thy [] prop
  1.1889 +            (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1.1890 +                addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
  1.1891 +
  1.1892 +        fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1.1893 +          if is_selector thy sel then
  1.1894 +            let
  1.1895 +              val x' =
  1.1896 +                if not (loose_bvar1 (x, 0))
  1.1897 +                then Free ("x" ^ string_of_int i, range_type Tsel)
  1.1898 +                else raise TERM ("", [x]);
  1.1899 +              val sel' = Const (sel, Tsel) $ Bound 0;
  1.1900 +              val (l, r) = if lr then (sel', x') else (x', sel');
  1.1901 +            in Const ("op =", Teq) $ l $ r end
  1.1902 +          else raise TERM ("", [Const (sel, Tsel)]);
  1.1903 +
  1.1904 +        fun dest_sel_eq (Const ("op =", Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
  1.1905 +              (true, Teq, (sel, Tsel), X)
  1.1906 +          | dest_sel_eq (Const ("op =", Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
  1.1907 +              (false, Teq, (sel, Tsel), X)
  1.1908 +          | dest_sel_eq _ = raise TERM ("", []);
  1.1909 +      in
  1.1910 +        (case t of
  1.1911 +          Const ("Ex", Tex) $ Abs (s, T, t) =>
  1.1912 +           (let
  1.1913 +              val eq = mkeq (dest_sel_eq t) 0;
  1.1914 +              val prop =
  1.1915 +                list_all ([("r", T)],
  1.1916 +                  Logic.mk_equals (Const ("Ex", Tex) $ Abs (s, T, eq), HOLogic.true_const));
  1.1917 +            in SOME (prove prop) end
  1.1918 +            handle TERM _ => NONE)
  1.1919 +        | _ => NONE)
  1.1920 +      end);
  1.1921  
  1.1922  
  1.1923  local
  1.1924 +
  1.1925  val inductive_atomize = thms "induct_atomize";
  1.1926  val inductive_rulify = thms "induct_rulify";
  1.1927 +
  1.1928  in
  1.1929 +
  1.1930  (* record_split_simp_tac *)
  1.1931 -(* splits (and simplifies) all records in the goal for which P holds.
  1.1932 - * For quantified occurrences of a record
  1.1933 - * P can peek on the whole subterm (including the quantifier); for free variables P
  1.1934 - * can only peek on the variable itself.
  1.1935 - * P t = 0: do not split
  1.1936 - * P t = ~1: completely split
  1.1937 - * P t > 0: split up to given bound of record extensions
  1.1938 - *)
  1.1939 +
  1.1940 +(*Split (and simplify) all records in the goal for which P holds.
  1.1941 +  For quantified occurrences of a record
  1.1942 +  P can peek on the whole subterm (including the quantifier); for free variables P
  1.1943 +  can only peek on the variable itself.
  1.1944 +  P t = 0: do not split
  1.1945 +  P t = ~1: completely split
  1.1946 +  P t > 0: split up to given bound of record extensions.*)
  1.1947  fun record_split_simp_tac thms P i st =
  1.1948    let
  1.1949      val thy = Thm.theory_of_thm st;
  1.1950 @@ -1510,40 +1567,47 @@
  1.1951      val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
  1.1952  
  1.1953      fun mk_split_free_tac free induct_thm i =
  1.1954 -        let val cfree = cterm_of thy free;
  1.1955 -            val (_$(_$r)) = concl_of induct_thm;
  1.1956 -            val crec = cterm_of thy r;
  1.1957 -            val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
  1.1958 -        in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
  1.1959 -                  rtac thm i,
  1.1960 -                  simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
  1.1961 -        end;
  1.1962 -
  1.1963 -    fun split_free_tac P i (free as Free (n,T)) =
  1.1964 -        (case rec_id (~1) T of
  1.1965 -           "" => NONE
  1.1966 -         | name => let val split = P free
  1.1967 -                   in if split <> 0 then
  1.1968 -                      (case get_splits thy (rec_id split T) of
  1.1969 -                             NONE => NONE
  1.1970 -                           | SOME (_,_,_,induct_thm)
  1.1971 -                               => SOME (mk_split_free_tac free induct_thm i))
  1.1972 -                      else NONE
  1.1973 -                   end)
  1.1974 -     | split_free_tac _ _ _ = NONE;
  1.1975 +      let
  1.1976 +        val cfree = cterm_of thy free;
  1.1977 +        val _$ (_ $ r) = concl_of induct_thm;
  1.1978 +        val crec = cterm_of thy r;
  1.1979 +        val thm = cterm_instantiate [(crec, cfree)] induct_thm;
  1.1980 +      in
  1.1981 +        EVERY
  1.1982 +         [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
  1.1983 +          rtac thm i,
  1.1984 +          simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
  1.1985 +      end;
  1.1986 +
  1.1987 +    fun split_free_tac P i (free as Free (n, T)) =
  1.1988 +          (case rec_id ~1 T of
  1.1989 +            "" => NONE
  1.1990 +          | name =>
  1.1991 +              let val split = P free in
  1.1992 +                if split <> 0 then
  1.1993 +                  (case get_splits thy (rec_id split T) of
  1.1994 +                    NONE => NONE
  1.1995 +                  | SOME (_, _, _, induct_thm) =>
  1.1996 +                      SOME (mk_split_free_tac free induct_thm i))
  1.1997 +                else NONE
  1.1998 +              end)
  1.1999 +      | split_free_tac _ _ _ = NONE;
  1.2000  
  1.2001      val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
  1.2002  
  1.2003      val simprocs = if has_rec goal then [record_split_simproc P] else [];
  1.2004 -    val thms' = K_comp_convs@thms
  1.2005 -  in st |> ((EVERY split_frees_tacs)
  1.2006 -           THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i))
  1.2007 +    val thms' = K_comp_convs @ thms;
  1.2008 +  in
  1.2009 +    st |>
  1.2010 +      (EVERY split_frees_tacs THEN
  1.2011 +        Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
  1.2012    end handle Empty => Seq.empty;
  1.2013  end;
  1.2014  
  1.2015  
  1.2016  (* record_split_tac *)
  1.2017 -(* splits all records in the goal, which are quantified by ! or !!. *)
  1.2018 +
  1.2019 +(*Split all records in the goal, which are quantified by ! or !!.*)
  1.2020  fun record_split_tac i st =
  1.2021    let
  1.2022      val thy = Thm.theory_of_thm st;
  1.2023 @@ -1553,18 +1617,20 @@
  1.2024            (s = "all" orelse s = "All") andalso is_recT T
  1.2025          | _ => false);
  1.2026  
  1.2027 -    val goal = nth (Thm.prems_of st) (i - 1);
  1.2028 +    val goal = nth (Thm.prems_of st) (i - 1);  (* FIXME SUBGOAL *)
  1.2029  
  1.2030      fun is_all t =
  1.2031 -      (case t of (Const (quantifier, _)$_) =>
  1.2032 -         if quantifier = "All" orelse quantifier = "all" then ~1 else 0
  1.2033 -       | _ => 0);
  1.2034 -
  1.2035 -  in if has_rec goal
  1.2036 -     then Simplifier.full_simp_tac
  1.2037 -           (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
  1.2038 -     else Seq.empty
  1.2039 -  end handle Subscript => Seq.empty;
  1.2040 +      (case t of
  1.2041 +        Const (quantifier, _) $ _ =>
  1.2042 +          if quantifier = "All" orelse quantifier = "all" then ~1 else 0
  1.2043 +      | _ => 0);
  1.2044 +
  1.2045 +  in
  1.2046 +    if has_rec goal then
  1.2047 +      Simplifier.full_simp_tac
  1.2048 +        (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
  1.2049 +    else Seq.empty
  1.2050 +  end handle Subscript => Seq.empty;     (* FIXME SUBGOAL *)
  1.2051  
  1.2052  
  1.2053  (* wrapper *)
  1.2054 @@ -1593,7 +1659,8 @@
  1.2055  fun cert_typ ctxt raw_T env =
  1.2056    let
  1.2057      val thy = ProofContext.theory_of ctxt;
  1.2058 -    val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg;
  1.2059 +    val T = Type.no_tvars (Sign.certify_typ thy raw_T)
  1.2060 +      handle TYPE (msg, _, _) => error msg;
  1.2061      val env' = OldTerm.add_typ_tfrees (T, env);
  1.2062    in (T, env') end;
  1.2063  
  1.2064 @@ -1609,156 +1676,155 @@
  1.2065  
  1.2066  fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
  1.2067  
  1.2068 -(* do case analysis / induction according to rule on last parameter of ith subgoal
  1.2069 - * (or on s if there are no parameters);
  1.2070 - * Instatiation of record variable (and predicate) in rule is calculated to
  1.2071 - * avoid problems with higher order unification.
  1.2072 - *)
  1.2073 -
  1.2074 +(*Do case analysis / induction according to rule on last parameter of ith subgoal
  1.2075 +  (or on s if there are no parameters).
  1.2076 +  Instatiation of record variable (and predicate) in rule is calculated to
  1.2077 +  avoid problems with higher order unification.*)
  1.2078  fun try_param_tac s rule i st =
  1.2079    let
  1.2080      val cert = cterm_of (Thm.theory_of_thm st);
  1.2081 -    val g = nth (prems_of st) (i - 1);
  1.2082 +    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
  1.2083      val params = Logic.strip_params g;
  1.2084      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
  1.2085      val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
  1.2086      val (P, ys) = strip_comb (HOLogic.dest_Trueprop
  1.2087        (Logic.strip_assums_concl (prop_of rule')));
  1.2088 -    (* ca indicates if rule is a case analysis or induction rule *)
  1.2089 -    val (x, ca) = (case rev (Library.drop (length params, ys)) of
  1.2090 +    (*ca indicates if rule is a case analysis or induction rule*)
  1.2091 +    val (x, ca) =
  1.2092 +      (case rev (Library.drop (length params, ys)) of
  1.2093          [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  1.2094            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
  1.2095        | [x] => (head_of x, false));
  1.2096 -    val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
  1.2097 -        [] => (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
  1.2098 -          NONE => sys_error "try_param_tac: no such variable"
  1.2099 -        | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl),
  1.2100 -            (x, Free (s, T))])
  1.2101 -      | (_, T) :: _ => [(P, list_abs (params, if ca then concl
  1.2102 -          else incr_boundvars 1 (Abs (s, T, concl)))),
  1.2103 -        (x, list_abs (params, Bound 0))])) rule'
  1.2104 +    val rule'' = cterm_instantiate (map (pairself cert)
  1.2105 +      (case (rev params) of
  1.2106 +        [] =>
  1.2107 +          (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
  1.2108 +            NONE => sys_error "try_param_tac: no such variable"
  1.2109 +          | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
  1.2110 +      | (_, T) :: _ =>
  1.2111 +          [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
  1.2112 +            (x, list_abs (params, Bound 0))])) rule';
  1.2113    in compose_tac (false, rule'', nprems_of rule) i st end;
  1.2114  
  1.2115  
  1.2116 -(* !!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
  1.2117 -   instantiates x1 ... xn with parameters x1 ... xn *)
  1.2118 +(*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
  1.2119 +  instantiates x1 ... xn with parameters x1 ... xn*)
  1.2120  fun ex_inst_tac i st =
  1.2121    let
  1.2122      val thy = Thm.theory_of_thm st;
  1.2123 -    val g = nth (prems_of st) (i - 1);
  1.2124 +    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
  1.2125      val params = Logic.strip_params g;
  1.2126      val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
  1.2127 -    val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
  1.2128 +    val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI'));
  1.2129      val cx = cterm_of thy (fst (strip_comb x));
  1.2130 -
  1.2131 -  in Seq.single (Library.foldl (fn (st,v) =>
  1.2132 -        Seq.hd
  1.2133 -        (compose_tac (false, cterm_instantiate
  1.2134 -                                [(cx,cterm_of thy (list_abs (params,Bound v)))] exI',1)
  1.2135 -                i st)) (st,((length params) - 1) downto 0))
  1.2136 +  in
  1.2137 +    Seq.single (Library.foldl (fn (st, v) =>
  1.2138 +      Seq.hd
  1.2139 +        (compose_tac
  1.2140 +          (false,
  1.2141 +            cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st))
  1.2142 +        (st, (length params - 1) downto 0))
  1.2143    end;
  1.2144  
  1.2145  fun extension_definition full name fields names alphas zeta moreT more vars thy =
  1.2146    let
  1.2147      val base = Long_Name.base_name;
  1.2148      val fieldTs = (map snd fields);
  1.2149 -    val alphas_zeta = alphas@[zeta];
  1.2150 +    val alphas_zeta = alphas @ [zeta];
  1.2151      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
  1.2152      val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
  1.2153      val extT_name = suffix ext_typeN name
  1.2154      val extT = Type (extT_name, alphas_zetaTs);
  1.2155 -    val fields_more = fields@[(full moreN,moreT)];
  1.2156 -    val fields_moreTs = fieldTs@[moreT];
  1.2157 +    val fields_more = fields @ [(full moreN, moreT)];
  1.2158 +    val fields_moreTs = fieldTs @ [moreT];
  1.2159      val bfields_more = map (apfst base) fields_more;
  1.2160 -    val r = Free (rN,extT)
  1.2161 +    val r = Free (rN, extT);
  1.2162      val len = length fields;
  1.2163      val idxms = 0 upto len;
  1.2164  
  1.2165 -    (* before doing anything else, create the tree of new types
  1.2166 -       that will back the record extension *)
  1.2167 -    
  1.2168 -    fun mktreeT [] = raise (TYPE ("mktreeT: empty list", [], []))
  1.2169 +    (*before doing anything else, create the tree of new types
  1.2170 +      that will back the record extension*)
  1.2171 +
  1.2172 +    fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
  1.2173        | mktreeT [T] = T
  1.2174        | mktreeT xs =
  1.2175 -    let
  1.2176 -      val len   = length xs;
  1.2177 -      val half  = len div 2;
  1.2178 -      val left  = List.take (xs, half);
  1.2179 -      val right = List.drop (xs, half);
  1.2180 -    in
  1.2181 -      HOLogic.mk_prodT (mktreeT left, mktreeT right)
  1.2182 -    end;
  1.2183 -
  1.2184 -    fun mktreeV [] = raise (TYPE ("mktreeV: empty list", [], []))
  1.2185 +          let
  1.2186 +            val len = length xs;
  1.2187 +            val half = len div 2;
  1.2188 +            val left = List.take (xs, half);
  1.2189 +            val right = List.drop (xs, half);
  1.2190 +          in
  1.2191 +            HOLogic.mk_prodT (mktreeT left, mktreeT right)
  1.2192 +          end;
  1.2193 +
  1.2194 +    fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
  1.2195        | mktreeV [T] = T
  1.2196        | mktreeV xs =
  1.2197 -    let
  1.2198 -      val len   = length xs;
  1.2199 -      val half  = len div 2;
  1.2200 -      val left  = List.take (xs, half);
  1.2201 -      val right = List.drop (xs, half);
  1.2202 -    in
  1.2203 -      IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
  1.2204 -    end;
  1.2205 +          let
  1.2206 +            val len = length xs;
  1.2207 +            val half = len div 2;
  1.2208 +            val left = List.take (xs, half);
  1.2209 +            val right = List.drop (xs, half);
  1.2210 +          in
  1.2211 +            IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
  1.2212 +          end;
  1.2213  
  1.2214      fun mk_istuple ((thy, i), (left, rght)) =
  1.2215 -    let
  1.2216 -      val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
  1.2217 -      val nm   = suffix suff (Long_Name.base_name name);
  1.2218 -      val (isom, cons, thy') = IsTupleSupport.add_istuple_type
  1.2219 -               (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
  1.2220 -    in
  1.2221 -      ((thy', i + 1), cons $ left $ rght)
  1.2222 -    end;
  1.2223 -
  1.2224 -    (* trying to create a 1-element istuple will fail, and
  1.2225 -       is pointless anyway *)
  1.2226 -    fun mk_even_istuple ((thy, i), [arg]) =
  1.2227 -        ((thy, i), arg)
  1.2228 +      let
  1.2229 +        val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
  1.2230 +        val nm = suffix suff (Long_Name.base_name name);
  1.2231 +        val (isom, cons, thy') =
  1.2232 +          IsTupleSupport.add_istuple_type
  1.2233 +            (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
  1.2234 +      in
  1.2235 +        ((thy', i + 1), cons $ left $ rght)
  1.2236 +      end;
  1.2237 +
  1.2238 +    (*trying to create a 1-element istuple will fail, and
  1.2239 +      is pointless anyway*)
  1.2240 +    fun mk_even_istuple ((thy, i), [arg]) = ((thy, i), arg)
  1.2241        | mk_even_istuple ((thy, i), args) =
  1.2242 -        mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
  1.2243 +          mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
  1.2244  
  1.2245      fun build_meta_tree_type i thy vars more =
  1.2246 -    let
  1.2247 -      val len   = length vars;
  1.2248 -    in
  1.2249 -      if len < 1
  1.2250 -      then raise (TYPE ("meta_tree_type args too short", [], vars))
  1.2251 -      else if len > 16
  1.2252 -      then let
  1.2253 -          fun group16 [] = []
  1.2254 -            | group16 xs = Library.take (16, xs)
  1.2255 -                             :: group16 (Library.drop (16, xs));
  1.2256 -          val vars' = group16 vars;
  1.2257 -          val ((thy', i'), composites) =
  1.2258 -                   Library.foldl_map mk_even_istuple ((thy, i), vars');
  1.2259 -        in
  1.2260 -          build_meta_tree_type i' thy' composites more
  1.2261 -        end
  1.2262 -      else let
  1.2263 -          val ((thy', i'), term)
  1.2264 -             = mk_istuple ((thy, 0), (mktreeV vars, more));
  1.2265 -        in
  1.2266 -          (term, thy')
  1.2267 -        end
  1.2268 -    end;
  1.2269 +      let val len = length vars in
  1.2270 +        if len < 1 then raise (TYPE ("meta_tree_type args too short", [], vars))
  1.2271 +        else if len > 16 then
  1.2272 +          let
  1.2273 +            fun group16 [] = []
  1.2274 +              | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
  1.2275 +            val vars' = group16 vars;
  1.2276 +            val ((thy', i'), composites) =
  1.2277 +              Library.foldl_map mk_even_istuple ((thy, i), vars');   (* FIXME fold_map !? *)
  1.2278 +          in
  1.2279 +            build_meta_tree_type i' thy' composites more
  1.2280 +          end
  1.2281 +        else
  1.2282 +          let val ((thy', i'), term) = mk_istuple ((thy, 0), (mktreeV vars, more))
  1.2283 +          in (term, thy') end
  1.2284 +      end;
  1.2285  
  1.2286      val _ = timing_msg "record extension preparing definitions";
  1.2287  
  1.2288 +
  1.2289      (* 1st stage part 1: introduce the tree of new types *)
  1.2290 +
  1.2291      fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
  1.2292      val (ext_body, typ_thy) =
  1.2293        timeit_msg "record extension nested type def:" get_meta_tree;
  1.2294  
  1.2295 +
  1.2296      (* prepare declarations and definitions *)
  1.2297  
  1.2298      (*fields constructor*)
  1.2299 -    val ext_decl = (mk_extC (name,extT) fields_moreTs);
  1.2300 -    val ext_spec = list_comb (Const ext_decl,vars@[more]) :== ext_body;
  1.2301 +    val ext_decl = mk_extC (name, extT) fields_moreTs;
  1.2302 +    val ext_spec = list_comb (Const ext_decl, vars @ [more]) :== ext_body;
  1.2303  
  1.2304      fun mk_ext args = list_comb (Const ext_decl, args);
  1.2305  
  1.2306 +
  1.2307      (* 1st stage part 2: define the ext constant *)
  1.2308 +
  1.2309      fun mk_defs () =
  1.2310        typ_thy
  1.2311        |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
  1.2312 @@ -1768,32 +1834,31 @@
  1.2313  
  1.2314      (* prepare propositions *)
  1.2315      val _ = timing_msg "record extension preparing propositions";
  1.2316 -    val vars_more = vars@[more];
  1.2317 -    val named_vars_more = (names@[full moreN])~~vars_more;
  1.2318 -    val variants = map (fn (Free (x,_))=>x) vars_more;
  1.2319 +    val vars_more = vars @ [more];
  1.2320 +    val named_vars_more = (names @ [full moreN]) ~~ vars_more;
  1.2321 +    val variants = map (fn Free (x, _) => x) vars_more;
  1.2322      val ext = mk_ext vars_more;
  1.2323 -    val s     = Free (rN, extT);
  1.2324 -    val w     = Free (wN, extT);
  1.2325 +    val s = Free (rN, extT);
  1.2326 +    val w = Free (wN, extT);
  1.2327      val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
  1.2328      val C = Free (Name.variant variants "C", HOLogic.boolT);
  1.2329      val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
  1.2330  
  1.2331      val inject_prop =
  1.2332 -      let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
  1.2333 -      in
  1.2334 -        ((HOLogic.mk_conj (HOLogic.eq_const extT $
  1.2335 -          mk_ext vars_more$mk_ext vars_more', HOLogic.true_const))
  1.2336 -         ===
  1.2337 -         foldr1 HOLogic.mk_conj
  1.2338 -           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const]))
  1.2339 +      let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
  1.2340 +        HOLogic.mk_conj (HOLogic.eq_const extT $
  1.2341 +          mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
  1.2342 +        ===
  1.2343 +        foldr1 HOLogic.mk_conj
  1.2344 +          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
  1.2345        end;
  1.2346  
  1.2347      val induct_prop =
  1.2348        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
  1.2349  
  1.2350      val cases_prop =
  1.2351 -      (All (map dest_Free vars_more)
  1.2352 -        (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C))
  1.2353 +      All (map dest_Free vars_more)
  1.2354 +        (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C)
  1.2355        ==> Trueprop C;
  1.2356  
  1.2357      val split_meta_prop =
  1.2358 @@ -1809,89 +1874,97 @@
  1.2359        in fn prop => prove stndrd [] prop (K tac) end;
  1.2360  
  1.2361      fun inject_prf () =
  1.2362 -      simplify HOL_ss (
  1.2363 -        prove_standard [] inject_prop (fn prems =>
  1.2364 -           EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
  1.2365 -                  REPEAT_DETERM (resolve_tac [refl_conj_eq] 1
  1.2366 -                                  ORELSE intros_tac 1
  1.2367 -                                  ORELSE resolve_tac [refl] 1)]));
  1.2368 +      simplify HOL_ss
  1.2369 +        (prove_standard [] inject_prop
  1.2370 +          (fn prems =>
  1.2371 +            EVERY
  1.2372 +             [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
  1.2373 +              REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
  1.2374 +                intros_tac 1 ORELSE
  1.2375 +                resolve_tac [refl] 1)]));
  1.2376  
  1.2377      val inject = timeit_msg "record extension inject proof:" inject_prf;
  1.2378  
  1.2379 -    (* We need a surjection property r = (| f = f r, g = g r ... |)
  1.2380 -       to prove other theorems. We haven't given names to the accessors
  1.2381 -       f, g etc yet however, so we generate an ext structure with
  1.2382 -       free variables as all arguments and allow the introduction tactic to
  1.2383 -       operate on it as far as it can. We then use standard to convert
  1.2384 -       the free variables into unifiable variables and unify them with
  1.2385 -       (roughly) the definition of the accessor. *)
  1.2386 -    fun surject_prf () = let
  1.2387 +    (*We need a surjection property r = (| f = f r, g = g r ... |)
  1.2388 +      to prove other theorems. We haven't given names to the accessors
  1.2389 +      f, g etc yet however, so we generate an ext structure with
  1.2390 +      free variables as all arguments and allow the introduction tactic to
  1.2391 +      operate on it as far as it can. We then use standard to convert
  1.2392 +      the free variables into unifiable variables and unify them with
  1.2393 +      (roughly) the definition of the accessor.*)
  1.2394 +    fun surject_prf () =
  1.2395 +      let
  1.2396          val cterm_ext = cterm_of defs_thy ext;
  1.2397 -        val start     = named_cterm_instantiate [("y", cterm_ext)]
  1.2398 -                              surject_assist_idE;
  1.2399 -        val tactic1   = simp_tac (HOL_basic_ss addsimps [ext_def]) 1
  1.2400 -                        THEN REPEAT_ALL_NEW intros_tac 1
  1.2401 -        val tactic2   = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
  1.2402 -        val [halfway] = Seq.list_of (tactic1 start);
  1.2403 -        val [surject] = Seq.list_of (tactic2 (standard halfway));
  1.2404 +        val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
  1.2405 +        val tactic1 =
  1.2406 +          simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
  1.2407 +          REPEAT_ALL_NEW intros_tac 1;
  1.2408 +        val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
  1.2409 +        val [halfway] = Seq.list_of (tactic1 start);    (* FIXME Seq.lift_of ?? *)
  1.2410 +        val [surject] = Seq.list_of (tactic2 (standard halfway));    (* FIXME Seq.lift_of ?? *)
  1.2411        in
  1.2412          surject
  1.2413        end;
  1.2414      val surject = timeit_msg "record extension surjective proof:" surject_prf;
  1.2415  
  1.2416      fun split_meta_prf () =
  1.2417 -        prove_standard [] split_meta_prop (fn prems =>
  1.2418 -         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.2419 -                etac meta_allE 1, atac 1,
  1.2420 -                rtac (prop_subst OF [surject]) 1,
  1.2421 -                REPEAT (etac meta_allE 1), atac 1]);
  1.2422 +      prove_standard [] split_meta_prop
  1.2423 +        (fn prems =>
  1.2424 +          EVERY
  1.2425 +           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.2426 +            etac meta_allE 1, atac 1,
  1.2427 +            rtac (prop_subst OF [surject]) 1,
  1.2428 +            REPEAT (etac meta_allE 1), atac 1]);
  1.2429      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
  1.2430  
  1.2431      fun induct_prf () =
  1.2432 -      let val (assm, concl) = induct_prop
  1.2433 -      in prove_standard [assm] concl (fn {prems, ...} =>
  1.2434 -           EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1,
  1.2435 -                  resolve_tac prems 2,
  1.2436 -                  asm_simp_tac HOL_ss 1]) end;
  1.2437 +      let val (assm, concl) = induct_prop in
  1.2438 +        prove_standard [assm] concl
  1.2439 +          (fn {prems, ...} =>
  1.2440 +            EVERY
  1.2441 +             [cut_rules_tac [split_meta RS meta_iffD2] 1,
  1.2442 +              resolve_tac prems 2,
  1.2443 +              asm_simp_tac HOL_ss 1])
  1.2444 +      end;
  1.2445      val induct = timeit_msg "record extension induct proof:" induct_prf;
  1.2446  
  1.2447 -    val ([inject',induct',surjective',split_meta'],
  1.2448 -      thm_thy) =
  1.2449 +    val ([inject', induct', surjective', split_meta'], thm_thy) =
  1.2450        defs_thy
  1.2451        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  1.2452             [("ext_inject", inject),
  1.2453              ("ext_induct", induct),
  1.2454              ("ext_surjective", surject),
  1.2455 -            ("ext_split", split_meta)]
  1.2456 -
  1.2457 -  in (thm_thy,extT,induct',inject',split_meta',ext_def)
  1.2458 -  end;
  1.2459 -
  1.2460 -fun chunks []      []   = []
  1.2461 -  | chunks []      xs   = [xs]
  1.2462 -  | chunks (l::ls) xs  = Library.take (l,xs)::chunks ls (Library.drop (l,xs));
  1.2463 +            ("ext_split", split_meta)];
  1.2464 +
  1.2465 +  in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
  1.2466 +
  1.2467 +fun chunks [] [] = []
  1.2468 +  | chunks [] xs = [xs]
  1.2469 +  | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
  1.2470  
  1.2471  fun chop_last [] = error "last: list should not be empty"
  1.2472 -  | chop_last [x] = ([],x)
  1.2473 -  | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
  1.2474 -
  1.2475 -fun subst_last s []      = error "subst_last: list should not be empty"
  1.2476 -  | subst_last s ([x])   = [s]
  1.2477 -  | subst_last s (x::xs) = (x::subst_last s xs);
  1.2478 -
  1.2479 -(* mk_recordT builds up the record type from the current extension tpye extT and a list
  1.2480 - * of parent extensions, starting with the root of the record hierarchy
  1.2481 -*)
  1.2482 +  | chop_last [x] = ([], x)
  1.2483 +  | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
  1.2484 +
  1.2485 +fun subst_last s [] = error "subst_last: list should not be empty"
  1.2486 +  | subst_last s [x] = [s]
  1.2487 +  | subst_last s (x :: xs) = x :: subst_last s xs;
  1.2488 +
  1.2489 +
  1.2490 +(* mk_recordT *)
  1.2491 +
  1.2492 +(*builds up the record type from the current extension tpye extT and a list
  1.2493 +  of parent extensions, starting with the root of the record hierarchy*)
  1.2494  fun mk_recordT extT =
  1.2495 -    fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
  1.2496 -
  1.2497 +  fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
  1.2498  
  1.2499  
  1.2500  fun obj_to_meta_all thm =
  1.2501    let
  1.2502 -    fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of
  1.2503 -                  SOME thm' => E thm'
  1.2504 -                | NONE => thm;
  1.2505 +    fun E thm =  (* FIXME proper name *)
  1.2506 +      (case (SOME (spec OF [thm]) handle THM _ => NONE) of
  1.2507 +        SOME thm' => E thm'
  1.2508 +      | NONE => thm);
  1.2509      val th1 = E thm;
  1.2510      val th2 = Drule.forall_intr_vars th1;
  1.2511    in th2 end;
  1.2512 @@ -1902,13 +1975,9 @@
  1.2513      val prop = Thm.prop_of thm;
  1.2514      val params = Logic.strip_params prop;
  1.2515      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
  1.2516 -    val ct = cterm_of thy
  1.2517 -      (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1.2518 +    val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1.2519      val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
  1.2520 -  in
  1.2521 -    Thm.implies_elim thm' thm
  1.2522 -  end;
  1.2523 -
  1.2524 +  in Thm.implies_elim thm' thm end;
  1.2525  
  1.2526  
  1.2527  (* record_definition *)
  1.2528 @@ -1922,7 +1991,8 @@
  1.2529      val full = Sign.full_bname_path thy bname;
  1.2530      val base = Long_Name.base_name;
  1.2531  
  1.2532 -    val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1.2533 +    val (bfields, field_syntax) =
  1.2534 +      split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1.2535  
  1.2536      val parent_fields = List.concat (map #fields parents);
  1.2537      val parent_chunks = map (length o #fields) parents;
  1.2538 @@ -1961,15 +2031,17 @@
  1.2539      val moreT = TFree (zeta, HOLogic.typeS);
  1.2540      val more = Free (moreN, moreT);
  1.2541      val full_moreN = full moreN;
  1.2542 -    val bfields_more = bfields @ [(moreN,moreT)];
  1.2543 -    val fields_more = fields @ [(full_moreN,moreT)];
  1.2544 +    val bfields_more = bfields @ [(moreN, moreT)];
  1.2545 +    val fields_more = fields @ [(full_moreN, moreT)];
  1.2546      val vars_more = vars @ [more];
  1.2547 -    val named_vars_more = named_vars @[(full_moreN,more)];
  1.2548 +    val named_vars_more = named_vars @ [(full_moreN, more)];
  1.2549      val all_vars_more = all_vars @ [more];
  1.2550 -    val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  1.2551 +    val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
  1.2552 +
  1.2553  
  1.2554      (* 1st stage: extension_thy *)
  1.2555 -    val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) =
  1.2556 +
  1.2557 +    val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
  1.2558        thy
  1.2559        |> Sign.add_path bname
  1.2560        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  1.2561 @@ -1977,26 +2049,25 @@
  1.2562      val _ = timing_msg "record preparing definitions";
  1.2563      val Type extension_scheme = extT;
  1.2564      val extension_name = unsuffix ext_typeN (fst extension_scheme);
  1.2565 -    val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end;
  1.2566 -    val extension_names =
  1.2567 -         (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
  1.2568 -    val extension_id = Library.foldl (op ^) ("",extension_names);
  1.2569 +    val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
  1.2570 +    val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
  1.2571 +    val extension_id = Library.foldl (op ^) ("", extension_names);  (* FIXME implode!? *)
  1.2572  
  1.2573  
  1.2574      fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
  1.2575      val rec_schemeT0 = rec_schemeT 0;
  1.2576  
  1.2577      fun recT n =
  1.2578 -      let val (c,Ts) = extension
  1.2579 -      in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts))
  1.2580 -      end;
  1.2581 +      let val (c, Ts) = extension
  1.2582 +      in mk_recordT (map #extension (prune n parents)) (Type (c, subst_last HOLogic.unitT Ts)) end;
  1.2583      val recT0 = recT 0;
  1.2584  
  1.2585      fun mk_rec args n =
  1.2586 -      let val (args',more) = chop_last args;
  1.2587 -          fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
  1.2588 -          fun build Ts =
  1.2589 -           List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
  1.2590 +      let
  1.2591 +        val (args', more) = chop_last args;
  1.2592 +        fun mk_ext' (((name, T), args), more) = mk_ext (name, T) (args @ [more]);
  1.2593 +        fun build Ts =
  1.2594 +          List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')));
  1.2595        in
  1.2596          if more = HOLogic.unit
  1.2597          then build (map recT (0 upto parent_len))
  1.2598 @@ -2004,7 +2075,7 @@
  1.2599        end;
  1.2600  
  1.2601      val r_rec0 = mk_rec all_vars_more 0;
  1.2602 -    val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  1.2603 +    val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
  1.2604  
  1.2605      fun r n = Free (rN, rec_schemeT n)
  1.2606      val r0 = r 0;
  1.2607 @@ -2012,26 +2083,27 @@
  1.2608      val r_unit0 = r_unit 0;
  1.2609      val w = Free (wN, rec_schemeT 0)
  1.2610  
  1.2611 +
  1.2612      (* prepare print translation functions *)
  1.2613 +
  1.2614      val field_tr's =
  1.2615        print_translation (distinct (op =) (maps external_names (full_moreN :: names)));
  1.2616  
  1.2617      val adv_ext_tr's =
  1.2618 -    let
  1.2619 -      val trnames = external_names extN;
  1.2620 -    in map (gen_record_tr') trnames end;
  1.2621 +      let val trnames = external_names extN
  1.2622 +      in map (gen_record_tr') trnames end;
  1.2623  
  1.2624      val adv_record_type_abbr_tr's =
  1.2625 -      let val trnames = external_names (hd extension_names);
  1.2626 -          val lastExt = unsuffix ext_typeN (fst extension);
  1.2627 -      in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames
  1.2628 -      end;
  1.2629 +      let
  1.2630 +        val trnames = external_names (hd extension_names);
  1.2631 +        val lastExt = unsuffix ext_typeN (fst extension);
  1.2632 +      in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end;
  1.2633  
  1.2634      val adv_record_type_tr's =
  1.2635 -      let val trnames = if parent_len > 0 then external_names extN else [];
  1.2636 -                        (* avoid conflict with adv_record_type_abbr_tr's *)
  1.2637 -      in map (gen_record_type_tr') trnames
  1.2638 -      end;
  1.2639 +      let
  1.2640 +        val trnames = if parent_len > 0 then external_names extN else [];
  1.2641 +        (*avoid conflict with adv_record_type_abbr_tr's*)
  1.2642 +      in map (gen_record_type_tr') trnames end;
  1.2643  
  1.2644  
  1.2645      (* prepare declarations *)
  1.2646 @@ -2046,13 +2118,14 @@
  1.2647      (* prepare definitions *)
  1.2648  
  1.2649      fun parent_more s =
  1.2650 -         if null parents then s
  1.2651 -         else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
  1.2652 +      if null parents then s
  1.2653 +      else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
  1.2654  
  1.2655      fun parent_more_upd v s =
  1.2656 -      if null parents then v$s
  1.2657 -      else let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
  1.2658 -           in mk_upd updateN mp v s end;
  1.2659 +      if null parents then v $ s
  1.2660 +      else
  1.2661 +        let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
  1.2662 +        in mk_upd updateN mp v s end;
  1.2663  
  1.2664      (*record (scheme) type abbreviation*)
  1.2665      val recordT_specs =
  1.2666 @@ -2062,64 +2135,66 @@
  1.2667      val ext_defs = ext_def :: map #extdef parents;
  1.2668      val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
  1.2669  
  1.2670 -    (* Theorems from the istuple intros.
  1.2671 -       This is complex enough to deserve a full comment.
  1.2672 -       By unfolding ext_defs from r_rec0 we create a tree of constructor
  1.2673 -       calls (many of them Pair, but others as well). The introduction
  1.2674 -       rules for update_accessor_eq_assist can unify two different ways
  1.2675 -       on these constructors. If we take the complete result sequence of
  1.2676 -       running a the introduction tactic, we get one theorem for each upd/acc
  1.2677 -       pair, from which we can derive the bodies of our selector and
  1.2678 -       updator and their convs. *)
  1.2679 -    fun get_access_update_thms () = let
  1.2680 -        val r_rec0_Vars = let
  1.2681 -            (* pick variable indices of 1 to avoid possible variable
  1.2682 -               collisions with existing variables in updacc_eq_triv *)
  1.2683 +    (*Theorems from the istuple intros.
  1.2684 +      This is complex enough to deserve a full comment.
  1.2685 +      By unfolding ext_defs from r_rec0 we create a tree of constructor
  1.2686 +      calls (many of them Pair, but others as well). The introduction
  1.2687 +      rules for update_accessor_eq_assist can unify two different ways
  1.2688 +      on these constructors. If we take the complete result sequence of
  1.2689 +      running a the introduction tactic, we get one theorem for each upd/acc
  1.2690 +      pair, from which we can derive the bodies of our selector and
  1.2691 +      updator and their convs.*)
  1.2692 +    fun get_access_update_thms () =
  1.2693 +      let
  1.2694 +        val r_rec0_Vars =
  1.2695 +          let
  1.2696 +            (*pick variable indices of 1 to avoid possible variable
  1.2697 +              collisions with existing variables in updacc_eq_triv*)
  1.2698              fun to_Var (Free (c, T)) = Var ((c, 1), T);
  1.2699            in mk_rec (map to_Var all_vars_more) 0 end;
  1.2700  
  1.2701          val cterm_rec = cterm_of extension_thy r_rec0;
  1.2702          val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
  1.2703 -        val insts     = [("v", cterm_rec), ("v'", cterm_vrs)];
  1.2704 -        val init_thm  = named_cterm_instantiate insts updacc_eq_triv;
  1.2705 -        val terminal  = rtac updacc_eq_idI 1 THEN rtac refl 1;
  1.2706 -        val tactic    = simp_tac (HOL_basic_ss addsimps ext_defs) 1
  1.2707 -                        THEN REPEAT (intros_tac 1 ORELSE terminal);
  1.2708 -        val updaccs   = Seq.list_of (tactic init_thm);
  1.2709 +        val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
  1.2710 +        val init_thm = named_cterm_instantiate insts updacc_eq_triv;
  1.2711 +        val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
  1.2712 +        val tactic =
  1.2713 +          simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
  1.2714 +          REPEAT (intros_tac 1 ORELSE terminal);
  1.2715 +        val updaccs = Seq.list_of (tactic init_thm);  (* FIXME Seq.lift_of *)
  1.2716        in
  1.2717          (updaccs RL [updacc_accessor_eqE],
  1.2718           updaccs RL [updacc_updator_eqE],
  1.2719           updaccs RL [updacc_cong_from_eq])
  1.2720        end;
  1.2721      val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  1.2722 -       timeit_msg "record getting tree access/updates:" get_access_update_thms;
  1.2723 +      timeit_msg "record getting tree access/updates:" get_access_update_thms;
  1.2724  
  1.2725      fun lastN xs = List.drop (xs, parent_fields_len);
  1.2726  
  1.2727      (*selectors*)
  1.2728 -    fun mk_sel_spec ((c,T), thm) =
  1.2729 +    fun mk_sel_spec ((c, T), thm) =
  1.2730        let
  1.2731 -        val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1.2732 -                               o Envir.beta_eta_contract o concl_of) thm;
  1.2733 -        val _ = if (arg aconv r_rec0) then ()
  1.2734 -                else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.2735 +        val acc $ arg =
  1.2736 +          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
  1.2737 +        val _ =
  1.2738 +          if (arg aconv r_rec0) then ()
  1.2739 +          else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.2740        in
  1.2741 -        Const (mk_selC rec_schemeT0 (c,T))
  1.2742 -          :== acc
  1.2743 +        Const (mk_selC rec_schemeT0 (c, T)) :== acc
  1.2744        end;
  1.2745      val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  1.2746  
  1.2747 +
  1.2748      (*updates*)
  1.2749 -
  1.2750 -    fun mk_upd_spec ((c,T), thm) =
  1.2751 +    fun mk_upd_spec ((c, T), thm) =
  1.2752        let
  1.2753 -        val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1.2754 -                                   o Envir.beta_eta_contract o concl_of) thm;
  1.2755 -        val _ = if (arg aconv r_rec0) then ()
  1.2756 -                else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.2757 -      in Const (mk_updC updateN rec_schemeT0 (c,T))
  1.2758 -          :== upd
  1.2759 -      end;
  1.2760 +        val (upd $ _ $ arg) =
  1.2761 +          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
  1.2762 +        val _ =
  1.2763 +          if (arg aconv r_rec0) then ()
  1.2764 +          else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.2765 +      in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
  1.2766      val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  1.2767  
  1.2768      (*derived operations*)
  1.2769 @@ -2133,14 +2208,14 @@
  1.2770      val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
  1.2771        mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  1.2772  
  1.2773 +
  1.2774      (* 2st stage: defs_thy *)
  1.2775  
  1.2776      fun mk_defs () =
  1.2777        extension_thy
  1.2778 -      |> Sign.add_trfuns
  1.2779 -          ([],[],field_tr's, [])
  1.2780 +      |> Sign.add_trfuns ([], [], field_tr's, [])
  1.2781        |> Sign.add_advanced_trfuns
  1.2782 -          ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
  1.2783 +          ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, [])
  1.2784        |> Sign.parent_path
  1.2785        |> Sign.add_tyabbrs_i recordT_specs
  1.2786        |> Sign.add_path bname
  1.2787 @@ -2153,7 +2228,8 @@
  1.2788        ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
  1.2789        ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
  1.2790               [make_spec, fields_spec, extend_spec, truncate_spec])
  1.2791 -      |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
  1.2792 +      |->
  1.2793 +        (fn defs as ((sel_defs, upd_defs), derived_defs) =>
  1.2794            fold Code.add_default_eqn sel_defs
  1.2795            #> fold Code.add_default_eqn upd_defs
  1.2796            #> fold Code.add_default_eqn derived_defs
  1.2797 @@ -2162,23 +2238,23 @@
  1.2798        timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
  1.2799          mk_defs;
  1.2800  
  1.2801 -
  1.2802      (* prepare propositions *)
  1.2803      val _ = timing_msg "record preparing propositions";
  1.2804 -    val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
  1.2805 +    val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
  1.2806      val C = Free (Name.variant all_variants "C", HOLogic.boolT);
  1.2807 -    val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT);
  1.2808 +    val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
  1.2809  
  1.2810      (*selectors*)
  1.2811      val sel_conv_props =
  1.2812 -       map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
  1.2813 +       map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
  1.2814  
  1.2815      (*updates*)
  1.2816 -    fun mk_upd_prop (i,(c,T)) =
  1.2817 -      let val x' = Free (Name.variant all_variants (base c ^ "'"),T-->T);
  1.2818 -          val n = parent_fields_len + i;
  1.2819 -          val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more
  1.2820 -      in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
  1.2821 +    fun mk_upd_prop (i, (c, T)) =
  1.2822 +      let
  1.2823 +        val x' = Free (Name.variant all_variants (base c ^ "'"), T --> T);
  1.2824 +        val n = parent_fields_len + i;
  1.2825 +        val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more
  1.2826 +      in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
  1.2827      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
  1.2828  
  1.2829      (*induct*)
  1.2830 @@ -2186,22 +2262,22 @@
  1.2831        All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  1.2832      val induct_prop =
  1.2833        (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
  1.2834 -       Trueprop (P_unit $ r_unit0));
  1.2835 +        Trueprop (P_unit $ r_unit0));
  1.2836  
  1.2837      (*surjective*)
  1.2838      val surjective_prop =
  1.2839 -      let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
  1.2840 +      let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
  1.2841        in r0 === mk_rec args 0 end;
  1.2842  
  1.2843      (*cases*)
  1.2844      val cases_scheme_prop =
  1.2845        (All (map dest_Free all_vars_more)
  1.2846 -        (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C))
  1.2847 +        (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C))
  1.2848        ==> Trueprop C;
  1.2849  
  1.2850      val cases_prop =
  1.2851        (All (map dest_Free all_vars)
  1.2852 -        (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C))
  1.2853 +        (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C))
  1.2854         ==> Trueprop C;
  1.2855  
  1.2856      (*split*)
  1.2857 @@ -2211,24 +2287,24 @@
  1.2858           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  1.2859        end;
  1.2860  
  1.2861 +    (* FIXME eliminate old List.foldr *)
  1.2862 +
  1.2863      val split_object_prop =
  1.2864 -      let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
  1.2865 -      in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
  1.2866 -      end;
  1.2867 -
  1.2868 +      let fun ALL vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_all (v, T, t)) t vs
  1.2869 +      in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) end;
  1.2870  
  1.2871      val split_ex_prop =
  1.2872 -      let fun EX vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs
  1.2873 -      in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
  1.2874 -      end;
  1.2875 +      let fun EX vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_exists (v, T, t)) t vs
  1.2876 +      in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) end;
  1.2877  
  1.2878      (*equality*)
  1.2879      val equality_prop =
  1.2880        let
  1.2881 -        val s' = Free (rN ^ "'", rec_schemeT0)
  1.2882 -        fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T)
  1.2883 -        val seleqs = map mk_sel_eq all_named_vars_more
  1.2884 -      in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
  1.2885 +        val s' = Free (rN ^ "'", rec_schemeT0);
  1.2886 +        fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
  1.2887 +        val seleqs = map mk_sel_eq all_named_vars_more;
  1.2888 +      in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
  1.2889 +
  1.2890  
  1.2891      (* 3rd stage: thms_thy *)
  1.2892  
  1.2893 @@ -2241,40 +2317,43 @@
  1.2894  
  1.2895      val ss = get_simpset defs_thy;
  1.2896  
  1.2897 -    fun sel_convs_prf () = map (prove_simp false ss
  1.2898 -                           (sel_defs@accessor_thms)) sel_conv_props;
  1.2899 +    fun sel_convs_prf () =
  1.2900 +      map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
  1.2901      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  1.2902      fun sel_convs_standard_prf () = map standard sel_convs
  1.2903      val sel_convs_standard =
  1.2904 -          timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  1.2905 -
  1.2906 -    fun upd_convs_prf () = map (prove_simp false ss
  1.2907 -                           (upd_defs@updator_thms)) upd_conv_props;
  1.2908 +      timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  1.2909 +
  1.2910 +    fun upd_convs_prf () =
  1.2911 +      map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
  1.2912      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  1.2913      fun upd_convs_standard_prf () = map standard upd_convs
  1.2914      val upd_convs_standard =
  1.2915 -          timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  1.2916 -
  1.2917 -    fun get_upd_acc_congs () = let
  1.2918 -        val symdefs  = map symmetric (sel_defs @ upd_defs);
  1.2919 -        val fold_ss  = HOL_basic_ss addsimps symdefs;
  1.2920 +      timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  1.2921 +
  1.2922 +    fun get_upd_acc_congs () =
  1.2923 +      let
  1.2924 +        val symdefs = map symmetric (sel_defs @ upd_defs);
  1.2925 +        val fold_ss = HOL_basic_ss addsimps symdefs;
  1.2926          val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
  1.2927        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
  1.2928      val (fold_congs, unfold_congs) =
  1.2929 -          timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  1.2930 +      timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  1.2931  
  1.2932      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  1.2933  
  1.2934 -    fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn _ =>
  1.2935 -          (EVERY [if null parent_induct
  1.2936 -                  then all_tac else try_param_tac rN (hd parent_induct) 1,
  1.2937 -                  try_param_tac rN ext_induct 1,
  1.2938 -                  asm_simp_tac HOL_basic_ss 1]));
  1.2939 +    fun induct_scheme_prf () =
  1.2940 +      prove_standard [] induct_scheme_prop
  1.2941 +        (fn _ =>
  1.2942 +          EVERY
  1.2943 +           [if null parent_induct
  1.2944 +            then all_tac else try_param_tac rN (hd parent_induct) 1,
  1.2945 +            try_param_tac rN ext_induct 1,
  1.2946 +            asm_simp_tac HOL_basic_ss 1]);
  1.2947      val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
  1.2948  
  1.2949      fun induct_prf () =
  1.2950 -      let val (assm, concl) = induct_prop;
  1.2951 -      in
  1.2952 +      let val (assm, concl) = induct_prop in
  1.2953          prove_standard [assm] concl (fn {prems, ...} =>
  1.2954            try_param_tac rN induct_scheme 1
  1.2955            THEN try_param_tac "more" @{thm unit.induct} 1
  1.2956 @@ -2284,81 +2363,91 @@
  1.2957  
  1.2958      fun cases_scheme_prf_opt () =
  1.2959        let
  1.2960 -        val (_$(Pvar$_)) = concl_of induct_scheme;
  1.2961 -        val ind = cterm_instantiate
  1.2962 -                    [(cterm_of defs_thy Pvar, cterm_of defs_thy
  1.2963 -                            (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))]
  1.2964 -                    induct_scheme;
  1.2965 +        val _ $ (Pvar $ _) = concl_of induct_scheme;
  1.2966 +        val ind =
  1.2967 +          cterm_instantiate
  1.2968 +            [(cterm_of defs_thy Pvar, cterm_of defs_thy
  1.2969 +              (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
  1.2970 +            induct_scheme;
  1.2971          in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
  1.2972  
  1.2973      fun cases_scheme_prf_noopt () =
  1.2974 -        prove_standard [] cases_scheme_prop (fn _ =>
  1.2975 -         EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  1.2976 -               try_param_tac rN induct_scheme 1,
  1.2977 -               rtac impI 1,
  1.2978 -               REPEAT (etac allE 1),
  1.2979 -               etac mp 1,
  1.2980 -               rtac refl 1])
  1.2981 +      prove_standard [] cases_scheme_prop
  1.2982 +        (fn _ =>
  1.2983 +          EVERY
  1.2984 +           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  1.2985 +            try_param_tac rN induct_scheme 1,
  1.2986 +            rtac impI 1,
  1.2987 +            REPEAT (etac allE 1),
  1.2988 +            etac mp 1,
  1.2989 +            rtac refl 1]);
  1.2990      val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
  1.2991      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  1.2992  
  1.2993      fun cases_prf () =
  1.2994 -      prove_standard [] cases_prop  (fn _ =>
  1.2995 -        try_param_tac rN cases_scheme 1
  1.2996 -        THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  1.2997 +      prove_standard [] cases_prop
  1.2998 +        (fn _ =>
  1.2999 +          try_param_tac rN cases_scheme 1 THEN
  1.3000 +          simp_all_tac HOL_basic_ss [unit_all_eq1]);
  1.3001      val cases = timeit_msg "record cases proof:" cases_prf;
  1.3002  
  1.3003 -    fun surjective_prf () = let
  1.3004 -        val leaf_ss   = get_sel_upd_defs defs_thy
  1.3005 -                                addsimps (sel_defs @ (o_assoc :: id_o_apps));
  1.3006 -        val init_ss   = HOL_basic_ss addsimps ext_defs;
  1.3007 +    fun surjective_prf () =
  1.3008 +      let
  1.3009 +        val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps));
  1.3010 +        val init_ss = HOL_basic_ss addsimps ext_defs;
  1.3011        in
  1.3012 -        prove_standard [] surjective_prop (fn prems =>
  1.3013 -            (EVERY [rtac surject_assist_idE 1,
  1.3014 -                    simp_tac init_ss 1,
  1.3015 -                    REPEAT (intros_tac 1 ORELSE
  1.3016 -                            (rtac surject_assistI 1 THEN
  1.3017 -                             simp_tac leaf_ss 1))]))
  1.3018 +        prove_standard [] surjective_prop
  1.3019 +          (fn prems =>
  1.3020 +            EVERY
  1.3021 +             [rtac surject_assist_idE 1,
  1.3022 +              simp_tac init_ss 1,
  1.3023 +              REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
  1.3024        end;
  1.3025      val surjective = timeit_msg "record surjective proof:" surjective_prf;
  1.3026  
  1.3027      fun split_meta_prf () =
  1.3028 -        prove false [] split_meta_prop (fn prems =>
  1.3029 -         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.3030 -                etac meta_allE 1, atac 1,
  1.3031 -                rtac (prop_subst OF [surjective]) 1,
  1.3032 -                REPEAT (etac meta_allE 1), atac 1]);
  1.3033 +      prove false [] split_meta_prop
  1.3034 +        (fn prems =>
  1.3035 +          EVERY
  1.3036 +           [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.3037 +            etac meta_allE 1, atac 1,
  1.3038 +            rtac (prop_subst OF [surjective]) 1,
  1.3039 +            REPEAT (etac meta_allE 1), atac 1]);
  1.3040      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  1.3041      fun split_meta_standardise () = standard split_meta;
  1.3042 -    val split_meta_standard = timeit_msg "record split_meta standard:"
  1.3043 -        split_meta_standardise;
  1.3044 +    val split_meta_standard =
  1.3045 +      timeit_msg "record split_meta standard:" split_meta_standardise;
  1.3046  
  1.3047      fun split_object_prf_opt () =
  1.3048        let
  1.3049 -        val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P$r0)));
  1.3050 -        val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard));
  1.3051 +        val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
  1.3052 +        val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
  1.3053          val cP = cterm_of defs_thy P;
  1.3054 -        val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard;
  1.3055 -        val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
  1.3056 +        val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
  1.3057 +        val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
  1.3058          val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
  1.3059          val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
  1.3060 -        val thl = assume cl                 (*All r. P r*) (* 1 *)
  1.3061 -                |> obj_to_meta_all          (*!!r. P r*)
  1.3062 -                |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
  1.3063 -                |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
  1.3064 -                |> implies_intr cl          (* 1 ==> 2 *)
  1.3065 -        val thr = assume cr                           (*All n m more. P (ext n m more)*)
  1.3066 -                |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
  1.3067 -                |> equal_elim (symmetric split_meta') (*!!r. P r*)
  1.3068 -                |> meta_to_obj_all                    (*All r. P r*)
  1.3069 -                |> implies_intr cr                    (* 2 ==> 1 *)
  1.3070 +        val thl =
  1.3071 +          assume cl                   (*All r. P r*) (* 1 *)
  1.3072 +          |> obj_to_meta_all          (*!!r. P r*)
  1.3073 +          |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
  1.3074 +          |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
  1.3075 +          |> implies_intr cl          (* 1 ==> 2 *)
  1.3076 +        val thr =
  1.3077 +          assume cr                             (*All n m more. P (ext n m more)*)
  1.3078 +          |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
  1.3079 +          |> equal_elim (symmetric split_meta') (*!!r. P r*)
  1.3080 +          |> meta_to_obj_all                    (*All r. P r*)
  1.3081 +          |> implies_intr cr                    (* 2 ==> 1 *)
  1.3082       in standard (thr COMP (thl COMP iffI)) end;
  1.3083  
  1.3084      fun split_object_prf_noopt () =
  1.3085 -        prove_standard [] split_object_prop (fn _ =>
  1.3086 -         EVERY [rtac iffI 1,
  1.3087 -                REPEAT (rtac allI 1), etac allE 1, atac 1,
  1.3088 -                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  1.3089 +      prove_standard [] split_object_prop
  1.3090 +        (fn _ =>
  1.3091 +          EVERY
  1.3092 +           [rtac iffI 1,
  1.3093 +            REPEAT (rtac allI 1), etac allE 1, atac 1,
  1.3094 +            rtac allI 1, rtac induct_scheme 1, REPEAT (etac allE 1), atac 1]);
  1.3095  
  1.3096      val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
  1.3097      val split_object = timeit_msg "record split_object proof:" split_object_prf;
  1.3098 @@ -2366,30 +2455,33 @@
  1.3099  
  1.3100      fun split_ex_prf () =
  1.3101        let
  1.3102 -        val ss    = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
  1.3103 -        val P_nm  = fst (dest_Free P);
  1.3104 +        val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
  1.3105 +        val P_nm = fst (dest_Free P);
  1.3106          val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
  1.3107 -        val so'   = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
  1.3108 -        val so''  = simplify ss so';
  1.3109 +        val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
  1.3110 +        val so'' = simplify ss so';
  1.3111        in
  1.3112          prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
  1.3113        end;
  1.3114      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  1.3115  
  1.3116      fun equality_tac thms =
  1.3117 -      let val (s'::s::eqs) = rev thms;
  1.3118 -          val ss' = ss addsimps (s'::s::sel_convs_standard);
  1.3119 -          val eqs' = map (simplify ss') eqs;
  1.3120 -      in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
  1.3121 -
  1.3122 -   fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} =>
  1.3123 -      fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  1.3124 -        st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
  1.3125 -        THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
  1.3126 -        THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
  1.3127 -             (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
  1.3128 -      end);
  1.3129 -     val equality = timeit_msg "record equality proof:" equality_prf;
  1.3130 +      let
  1.3131 +        val s' :: s :: eqs = rev thms;
  1.3132 +        val ss' = ss addsimps (s' :: s :: sel_convs_standard);
  1.3133 +        val eqs' = map (simplify ss') eqs;
  1.3134 +      in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
  1.3135 +
  1.3136 +    fun equality_prf () =
  1.3137 +      prove_standard [] equality_prop (fn {context, ...} =>
  1.3138 +        fn st =>
  1.3139 +          let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  1.3140 +            st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
  1.3141 +              res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
  1.3142 +              Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
  1.3143 +             (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
  1.3144 +          end);
  1.3145 +    val equality = timeit_msg "record equality proof:" equality_prf;
  1.3146  
  1.3147      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
  1.3148              fold_congs', unfold_congs',
  1.3149 @@ -2404,7 +2496,7 @@
  1.3150            ("update_defs", upd_defs),
  1.3151            ("fold_congs", fold_congs),
  1.3152            ("unfold_congs", unfold_congs),
  1.3153 -          ("splits", [split_meta_standard,split_object,split_ex]),
  1.3154 +          ("splits", [split_meta_standard, split_object, split_ex]),
  1.3155            ("defs", derived_defs)]
  1.3156        ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  1.3157            [("surjective", surjective),
  1.3158 @@ -2415,7 +2507,6 @@
  1.3159           (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
  1.3160           (("cases", cases), cases_type_global name)];
  1.3161  
  1.3162 -
  1.3163      val sel_upd_simps = sel_convs' @ upd_convs';
  1.3164      val sel_upd_defs = sel_defs' @ upd_defs';
  1.3165      val iffs = [ext_inject]
  1.3166 @@ -2432,19 +2523,18 @@
  1.3167        |> add_record_equalities extension_id equality'
  1.3168        |> add_extinjects ext_inject
  1.3169        |> add_extsplit extension_name ext_split
  1.3170 -      |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
  1.3171 -      |> add_extfields extension_name (fields @ [(full_moreN,moreT)])
  1.3172 -      |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
  1.3173 +      |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
  1.3174 +      |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
  1.3175 +      |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
  1.3176        |> Sign.parent_path;
  1.3177  
  1.3178 -  in final_thy
  1.3179 -  end;
  1.3180 +  in final_thy end;
  1.3181  
  1.3182  
  1.3183  (* add_record *)
  1.3184  
  1.3185 -(*we do all preparations and error checks here, deferring the real
  1.3186 -  work to record_definition*)
  1.3187 +(*We do all preparations and error checks here, deferring the real
  1.3188 +  work to record_definition.*)
  1.3189  fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy =
  1.3190    let
  1.3191      val _ = Theory.requires thy "Record" "record definitions";
  1.3192 @@ -2520,8 +2610,9 @@
  1.3193      val errs =
  1.3194        err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  1.3195        err_dup_fields @ err_bad_fields @ err_dup_sorts;
  1.3196 +
  1.3197 +    val _ = if null errs then () else error (cat_lines errs);
  1.3198    in
  1.3199 -    if null errs then () else error (cat_lines errs)  ;
  1.3200      thy |> record_definition (args, bname) parent parents bfields
  1.3201    end
  1.3202    handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);