src/HOL/Tools/record.ML

tuned;

(*  Title:      HOL/Tools/record.ML
    Author:     Wolfgang Naraschewski, TU Muenchen
    Author:     Markus Wenzel, TU Muenchen
    Author:     Norbert Schirmer, TU Muenchen
    Author:     Thomas Sewell, NICTA

Extensible records with structural subtyping.
*)

signature RECORD =
sig
  val type_abbr: bool Config.T
  val type_as_fields: bool Config.T
  val timing: bool Config.T

  type info =
   {args: (string * sort) list,
    parent: (typ list * string) option,
    fields: (string * typ) list,
    extension: (string * typ list),
    ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    cases: thm, simps: thm list, iffs: thm list}
  val get_info: theory -> string -> info option
  val the_info: theory -> string -> info
  val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
  val add_record: (string * sort) list * binding -> (typ list * string) option ->
    (binding * typ * mixfix) list -> theory -> theory

  val last_extT: typ -> (string * typ list) option
  val dest_recTs: typ -> (string * typ list) list
  val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_parent: theory -> string -> (typ list * string) option
  val get_extension: theory -> string -> (string * typ list) option
  val get_extinjects: theory -> thm list
  val get_simpset: theory -> simpset
  val simproc: simproc
  val eq_simproc: simproc
  val upd_simproc: simproc
  val split_simproc: (term -> int) -> simproc
  val ex_sel_eq_simproc: simproc
  val split_tac: int -> tactic
  val split_simp_tac: thm list -> (term -> int) -> int -> tactic
  val split_wrapper: string * (Proof.context -> wrapper)

  val updateN: string
  val ext_typeN: string
  val extN: string
  val setup: theory -> theory
end;


signature ISO_TUPLE_SUPPORT =
sig
  val add_iso_tuple_type: binding * (string * sort) list ->
    typ * typ -> theory -> (term * term) * theory
  val mk_cons_tuple: term * term -> term
  val dest_cons_tuple: term -> term * term
  val iso_tuple_intros_tac: int -> tactic
  val named_cterm_instantiate: (string * cterm) list -> thm -> thm
end;

structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
struct

val isoN = "_Tuple_Iso";

val iso_tuple_intro = @{thm isomorphic_tuple_intro};
val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};

val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});

fun named_cterm_instantiate values thm =  (* FIXME eliminate *)
  let
    fun match name ((name', _), _) = name = name';
    fun getvar name =
      (case find_first (match name) (Term.add_vars (prop_of thm) []) of
        SOME var => cterm_of (theory_of_thm thm) (Var var)
      | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
  in
    cterm_instantiate (map (apfst getvar) values) thm
  end;

structure Iso_Tuple_Thms = Theory_Data
(
  type T = thm Symtab.table;
  val empty = Symtab.make [tuple_iso_tuple];
  val extend = I;
  fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
);

fun get_typedef_info tyco vs
    (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
  let
    val exists_thm =
      UNIV_I
      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
    val proj_constr = Abs_inverse OF [exists_thm];
    val absT = Type (tyco, map TFree vs);
  in
    thy
    |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
  end

fun do_typedef raw_tyco repT raw_vs thy =
  let
    val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
    val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
  in
    thy
    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
        (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
    |-> (fn (tyco, info) => get_typedef_info tyco vs info)
  end;

fun mk_cons_tuple (left, right) =
  let
    val (leftT, rightT) = (fastype_of left, fastype_of right);
    val prodT = HOLogic.mk_prodT (leftT, rightT);
    val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
  in
    Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
      Const (fst tuple_iso_tuple, isomT) $ left $ right
  end;

fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
  | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);

fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
  let
    val repT = HOLogic.mk_prodT (leftT, rightT);

    val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
      thy
      |> do_typedef b repT alphas
      ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)

    (*construct a type and body for the isomorphism constant by
      instantiating the theorem to which the definition will be applied*)
    val intro_inst =
      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    val isomT = fastype_of body;
    val isom_binding = Binding.suffix_name isoN b;
    val isom_name = Sign.full_name typ_thy isom_binding;
    val isom = Const (isom_name, isomT);

    val ([isom_def], cdef_thy) =
      typ_thy
      |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
      |> Global_Theory.add_defs false
        [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];

    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);

    val thm_thy =
      cdef_thy
      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
      |> Sign.restore_naming thy
  in
    ((isom, cons $ isom), thm_thy)
  end;

val iso_tuple_intros_tac =
  resolve_from_net_tac iso_tuple_intros THEN'
  CSUBGOAL (fn (cgoal, i) =>
    let
      val thy = Thm.theory_of_cterm cgoal;
      val goal = Thm.term_of cgoal;

      val isthms = Iso_Tuple_Thms.get thy;
      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);

      val goal' = Envir.beta_eta_contract goal;
      val is =
        (case goal' of
          Const (@{const_name Trueprop}, _) $
            (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
        | _ => err "unexpected goal format" goal');
      val isthm =
        (case Symtab.lookup isthms (#1 is) of
          SOME isthm => isthm
        | NONE => err "no thm found for constant" (Const is));
    in rtac isthm i end);

end;


structure Record: RECORD =
struct

val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};

val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};

val updacc_foldE = @{thm update_accessor_congruence_foldE};
val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
val updacc_noopE = @{thm update_accessor_noopE};
val updacc_noop_compE = @{thm update_accessor_noop_compE};
val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};



(** name components **)

val rN = "r";
val wN = "w";
val moreN = "more";
val schemeN = "_scheme";
val ext_typeN = "_ext";
val inner_typeN = "_inner";
val extN ="_ext";
val updateN = "_update";
val makeN = "make";
val fields_selN = "fields";
val extendN = "extend";
val truncateN = "truncate";



(*** utilities ***)

fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));


(* timing *)

val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();


(* syntax *)

val Trueprop = HOLogic.mk_Trueprop;

infix 0 :== ===;
infixr 0 ==>;

val op :== = Misc_Legacy.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;


(* constructor *)

fun mk_ext (name, T) ts =
  let val Ts = map fastype_of ts
  in list_comb (Const (suffix extN name, Ts ---> T), ts) end;


(* selector *)

fun mk_selC sT (c, T) = (c, sT --> T);

fun mk_sel s (c, T) =
  let val sT = fastype_of s
  in Const (mk_selC sT (c, T)) $ s end;


(* updates *)

fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);

fun mk_upd' sfx c v sT =
  let val vT = domain_type (fastype_of v);
  in Const (mk_updC sfx sT (c, vT)) $ v end;

fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;


(* types *)

fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
      (case try (unsuffix ext_typeN) c_ext_type of
        NONE => raise TYPE ("Record.dest_recT", [typ], [])
      | SOME c => ((c, Ts), List.last Ts))
  | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);

val is_recT = can dest_recT;

fun dest_recTs T =
  let val ((c, Ts), U) = dest_recT T
  in (c, Ts) :: dest_recTs U
  end handle TYPE _ => [];

fun last_extT T =
  let val ((c, Ts), U) = dest_recT T in
    (case last_extT U of
      NONE => SOME (c, Ts)
    | SOME l => SOME l)
  end handle TYPE _ => NONE;

fun rec_id i T =
  let
    val rTs = dest_recTs T;
    val rTs' = if i < 0 then rTs else take i rTs;
  in implode (map #1 rTs') end;



(*** extend theory by record definition ***)

(** record info **)

(* type info and parent_info *)

type info =
 {args: (string * sort) list,
  parent: (typ list * string) option,
  fields: (string * typ) list,
  extension: (string * typ list),

  ext_induct: thm,
  ext_inject: thm,
  ext_surjective: thm,
  ext_split: thm,
  ext_def: thm,

  select_convs: thm list,
  update_convs: thm list,
  select_defs: thm list,
  update_defs: thm list,
  fold_congs: thm list,  (* FIXME unused!? *)
  unfold_congs: thm list,  (* FIXME unused!? *)
  splits: thm list,
  defs: thm list,

  surjective: thm,
  equality: thm,
  induct_scheme: thm,
  induct: thm,
  cases_scheme: thm,
  cases: thm,

  simps: thm list,
  iffs: thm list};

fun make_info args parent fields extension
    ext_induct ext_inject ext_surjective ext_split ext_def
    select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
    surjective equality induct_scheme induct cases_scheme cases
    simps iffs : info =
 {args = args, parent = parent, fields = fields, extension = extension,
  ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
  ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
  update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
  fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
  surjective = surjective, equality = equality, induct_scheme = induct_scheme,
  induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};

type parent_info =
 {name: string,
  fields: (string * typ) list,
  extension: (string * typ list),
  induct_scheme: thm,
  ext_def: thm};

fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
 {name = name, fields = fields, extension = extension,
  ext_def = ext_def, induct_scheme = induct_scheme};


(* theory data *)

type data =
 {records: info Symtab.table,
  sel_upd:
   {selectors: (int * bool) Symtab.table,
    updates: string Symtab.table,
    simpset: simpset,
    defset: simpset},
  equalities: thm Symtab.table,
  extinjects: thm list,
  extsplit: thm Symtab.table,  (*maps extension name to split rule*)
  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
  extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
  fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)

fun make_data
    records sel_upd equalities extinjects extsplit splits extfields fieldext =
 {records = records, sel_upd = sel_upd,
  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
  extfields = extfields, fieldext = fieldext }: data;

structure Data = Theory_Data
(
  type T = data;
  val empty =
    make_data Symtab.empty
      {selectors = Symtab.empty, updates = Symtab.empty,
        simpset = HOL_basic_ss, defset = HOL_basic_ss}
       Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
  val extend = I;
  fun merge
   ({records = recs1,
     sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
     equalities = equalities1,
     extinjects = extinjects1,
     extsplit = extsplit1,
     splits = splits1,
     extfields = extfields1,
     fieldext = fieldext1},
    {records = recs2,
     sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
     equalities = equalities2,
     extinjects = extinjects2,
     extsplit = extsplit2,
     splits = splits2,
     extfields = extfields2,
     fieldext = fieldext2}) =
    make_data
      (Symtab.merge (K true) (recs1, recs2))
      {selectors = Symtab.merge (K true) (sels1, sels2),
        updates = Symtab.merge (K true) (upds1, upds2),
        simpset = Simplifier.merge_ss (ss1, ss2),
        defset = Simplifier.merge_ss (ds1, ds2)}
      (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
      (Thm.merge_thms (extinjects1, extinjects2))
      (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
      (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
          Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
          Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
      (Symtab.merge (K true) (extfields1, extfields2))
      (Symtab.merge (K true) (fieldext1, fieldext2));
);


(* access 'records' *)

val get_info = Symtab.lookup o #records o Data.get;

fun the_info thy name =
  (case get_info thy name of
    SOME info => info
  | NONE => error ("Unknown record type " ^ quote name));

fun put_record name info =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data (Symtab.update (name, info) records)
      sel_upd equalities extinjects extsplit splits extfields fieldext);


(* access 'sel_upd' *)

val get_sel_upd = #sel_upd o Data.get;

val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));

val get_simpset = get_ss_with_context #simpset;
val get_sel_upd_defs = get_ss_with_context #defset;

fun get_update_details u thy =
  let val sel_upd = get_sel_upd thy in
    (case Symtab.lookup (#updates sel_upd) u of
      SOME s =>
        let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
        in SOME (s, dep, ismore) end
    | NONE => NONE)
  end;

fun put_sel_upd names more depth simps defs thy =
  let
    val all = names @ [more];
    val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    val upds = map (suffix updateN) all ~~ all;

    val {records, sel_upd = {selectors, updates, simpset, defset},
      equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
    val data =
      make_data records
        {selectors = fold Symtab.update_new sels selectors,
          updates = fold Symtab.update_new upds updates,
          simpset = simpset addsimps simps,
          defset = defset addsimps defs}
         equalities extinjects extsplit splits extfields fieldext;
  in Data.put data thy end;


(* access 'equalities' *)

fun add_equalities name thm =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data records sel_upd
      (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);

val get_equalities = Symtab.lookup o #equalities o Data.get;


(* access 'extinjects' *)

fun add_extinjects thm =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
      extsplit splits extfields fieldext);

val get_extinjects = rev o #extinjects o Data.get;


(* access 'extsplit' *)

fun add_extsplit name thm =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data records sel_upd equalities extinjects
      (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);


(* access 'splits' *)

fun add_splits name thmP =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data records sel_upd equalities extinjects extsplit
      (Symtab.update_new (name, thmP) splits) extfields fieldext);

val get_splits = Symtab.lookup o #splits o Data.get;


(* parent/extension of named record *)

val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);


(* access 'extfields' *)

fun add_extfields name fields =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    make_data records sel_upd equalities extinjects extsplit splits
      (Symtab.update_new (name, fields) extfields) fieldext);

val get_extfields = Symtab.lookup o #extfields o Data.get;

fun get_extT_fields thy T =
  let
    val ((name, Ts), moreT) = dest_recT T;
    val recname =
      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
      in Long_Name.implode (rev (nm :: rst)) end;
    val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
    val {records, extfields, ...} = Data.get thy;
    val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
    val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));

    val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
    val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
  in (fields', (more, moreT)) end;

fun get_recT_fields thy T =
  let
    val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
    val (rest_fields, rest_more) =
      if is_recT root_moreT then get_recT_fields thy root_moreT
      else ([], (root_more, root_moreT));
  in (root_fields @ rest_fields, rest_more) end;


(* access 'fieldext' *)

fun add_fieldext extname_types fields =
  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    let
      val fieldext' =
        fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
    in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);

val get_fieldext = Symtab.lookup o #fieldext o Data.get;


(* parent records *)

local

fun add_parents _ NONE = I
  | add_parents thy (SOME (types, name)) =
      let
        fun err msg = error (msg ^ " parent record " ^ quote name);

        val {args, parent, ...} =
          (case get_info thy name of SOME info => info | NONE => err "Unknown");
        val _ = if length types <> length args then err "Bad number of arguments for" else ();

        fun bad_inst ((x, S), T) =
          if Sign.of_sort thy (T, S) then NONE else SOME x
        val bads = map_filter bad_inst (args ~~ types);
        val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");

        val inst = args ~~ types;
        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
        val parent' = Option.map (apfst (map subst)) parent;
      in cons (name, inst) #> add_parents thy parent' end;

in

fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];

fun get_parent_info thy parent =
  add_parents thy parent [] |> map (fn (name, inst) =>
    let
      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
      val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
      val fields' = map (apsnd subst) fields;
      val extension' = apsnd (map subst) extension;
    in make_parent_info name fields' extension' ext_def induct_scheme end);

end;



(** concrete syntax for records **)

(* parse translations *)

local

fun split_args (field :: fields) ((name, arg) :: fargs) =
      if can (unsuffix name) field then
        let val (args, rest) = split_args fields fargs
        in (arg :: args, rest) end
      else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
  | split_args [] (fargs as (_ :: _)) = ([], fargs)
  | split_args (_ :: _) [] = raise Fail "expecting more fields"
  | split_args _ _ = ([], []);

fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
      (name, arg)
  | field_type_tr t = raise TERM ("field_type_tr", [t]);

fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
      field_type_tr t :: field_types_tr u
  | field_types_tr t = [field_type_tr t];

fun record_field_types_tr more ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt;
    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
            SOME (ext, alphas) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val (fields', _) = split_last fields;
                    val types = map snd fields';
                    val (args, rest) = split_args (map fst fields') fargs
                      handle Fail msg => err msg;
                    val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
                    val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
                    val vartypes = map varifyT types;

                    val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                      handle Type.TYPE_MATCH => err "type is no proper record (extension)";
                    val alphas' =
                      map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
                        (#1 (split_last alphas));

                    val more' = mk_ext rest;
                  in
                    list_comb
                      (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                  end
              | NONE => err ("no fields defined for " ^ quote ext))
          | NONE => err (quote name ^ " is no proper field"))
      | mk_ext [] = more;
  in
    mk_ext (field_types_tr t)
  end;

fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
  | record_type_tr _ ts = raise TERM ("record_type_tr", ts);

fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
  | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);


fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
  | field_tr t = raise TERM ("field_tr", [t]);

fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
  | fields_tr t = [field_tr t];

fun record_fields_tr more ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt;
    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
            SOME (ext, _) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
                      handle Fail msg => err msg;
                    val more' = mk_ext rest;
                  in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
              | NONE => err ("no fields defined for " ^ quote ext))
          | NONE => err (quote name ^ " is no proper field"))
      | mk_ext [] = more;
  in mk_ext (fields_tr t) end;

fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
  | record_tr _ ts = raise TERM ("record_tr", ts);

fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
  | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);


fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
      Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
  | field_update_tr t = raise TERM ("field_update_tr", [t]);

fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
      field_update_tr t :: field_updates_tr u
  | field_updates_tr t = [field_update_tr t];

fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
  | record_update_tr ts = raise TERM ("record_update_tr", ts);

in

val parse_translation =
 [(@{syntax_const "_record_update"}, record_update_tr)];

val advanced_parse_translation =
 [(@{syntax_const "_record"}, record_tr),
  (@{syntax_const "_record_scheme"}, record_scheme_tr),
  (@{syntax_const "_record_type"}, record_type_tr),
  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];

end;


(* print translations *)

val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);


local

(* FIXME early extern (!??) *)
(* FIXME Syntax.free (??) *)
fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;

fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;

fun record_type_tr' ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt;

    val T = Syntax_Phases.decode_typ t;
    val varifyT = varifyT (Term.maxidx_of_typ T + 1);

    fun strip_fields T =
      (case T of
        Type (ext, args as _ :: _) =>
          (case try (unsuffix ext_typeN) ext of
            SOME ext' =>
              (case get_extfields thy ext' of
                SOME (fields as (x, _) :: _) =>
                  (case get_fieldext thy x of
                    SOME (_, alphas) =>
                     (let
                        val (f :: fs, _) = split_last fields;
                        val fields' =
                          apfst (Proof_Context.extern_const ctxt) f ::
                            map (apfst Long_Name.base_name) fs;
                        val (args', more) = split_last args;
                        val alphavars = map varifyT (#1 (split_last alphas));
                        val subst = Type.raw_matches (alphavars, args') Vartab.empty;
                        val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
                      in fields'' @ strip_fields more end
                      handle Type.TYPE_MATCH => [("", T)])
                  | _ => [("", T)])
              | _ => [("", T)])
          | _ => [("", T)])
      | _ => [("", T)]);

    val (fields, (_, moreT)) = split_last (strip_fields T);
    val _ = null fields andalso raise Match;
    val u =
      foldr1 field_types_tr'
        (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
  in
    if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
    else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
    else
      Syntax.const @{syntax_const "_record_type_scheme"} $ u $
        Syntax_Phases.term_of_typ ctxt moreT
  end;

(*try to reconstruct the record name type abbreviation from
  the (nested) extension types*)
fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
  let
    val T = Syntax_Phases.decode_typ tm;
    val varifyT = varifyT (maxidx_of_typ T + 1);

    fun mk_type_abbr subst name args =
      let val abbrT = Type (name, map (varifyT o TFree) args)
      in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;

    fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
  in
    if Config.get ctxt type_abbr then
      (case last_extT T of
        SOME (name, _) =>
          if name = last_ext then
            let val subst = match schemeT T in
              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
              then mk_type_abbr subst abbr alphas
              else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
            end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
          else raise Match (*give print translation of specialised record a chance*)
      | _ => raise Match)
    else record_type_tr' ctxt tm
  end;

in

fun record_ext_type_tr' name =
  let
    val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
    fun tr' ctxt ts =
      record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
  in (ext_type_name, tr') end;

fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
  let
    val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
    fun tr' ctxt ts =
      record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
        (list_comb (Syntax.const ext_type_name, ts));
  in (ext_type_name, tr') end;

end;


local

(* FIXME Syntax.free (??) *)
fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;

fun record_tr' ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt;

    fun strip_fields t =
      (case strip_comb t of
        (Const (ext, _), args as (_ :: _)) =>
          (case try (Lexicon.unmark_const o unsuffix extN) ext of
            SOME ext' =>
              (case get_extfields thy ext' of
                SOME fields =>
                 (let
                    val (f :: fs, _) = split_last (map fst fields);
                    val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
                    val (args', more) = split_last args;
                  in (fields' ~~ args') @ strip_fields more end
                  handle ListPair.UnequalLengths => [("", t)])
              | NONE => [("", t)])
          | NONE => [("", t)])
       | _ => [("", t)]);

    val (fields, (_, more)) = split_last (strip_fields t);
    val _ = null fields andalso raise Match;
    val u = foldr1 fields_tr' (map field_tr' fields);
  in
    (case more of
      Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
    | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more)
  end;

in

fun record_ext_tr' name =
  let
    val ext_name = Lexicon.mark_const (name ^ extN);
    fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
  in (ext_name, tr') end;

end;


local

fun dest_update ctxt c =
  (case try Lexicon.unmark_const c of
    SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
  | NONE => NONE);

fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
      (case dest_update ctxt c of
        SOME name =>
          (case try Syntax_Trans.const_abs_tr' k of
            SOME t =>
              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
                (field_updates_tr' ctxt u)
          | NONE => ([], tm))
      | NONE => ([], tm))
  | field_updates_tr' _ tm = ([], tm);

fun record_update_tr' ctxt tm =
  (case field_updates_tr' ctxt tm of
    ([], _) => raise Match
  | (ts, u) =>
      Syntax.const @{syntax_const "_record_update"} $ u $
        foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));

in

fun field_update_tr' name =
  let
    val update_name = Lexicon.mark_const (name ^ updateN);
    fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
      | tr' _ _ = raise Match;
  in (update_name, tr') end;

end;



(** record simprocs **)

fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
  (case get_updates thy u of
    SOME u_name => u_name = s
  | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));

fun mk_comp_id f =
  let val T = range_type (fastype_of f)
  in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;

fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
  | get_upd_funs _ = [];

fun get_accupd_simps thy term defset =
  let
    val (acc, [body]) = strip_comb term;
    val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
    fun get_simp upd =
      let
        (* FIXME fresh "f" (!?) *)
        val T = domain_type (fastype_of upd);
        val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
        val rhs =
          if is_sel_upd_pair thy acc upd
          then HOLogic.mk_comp (Free ("f", T), acc)
          else mk_comp_id acc;
        val prop = lhs === rhs;
        val othm =
          Goal.prove (Proof_Context.init_global thy) [] [] prop
            (fn _ =>
              simp_tac defset 1 THEN
              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
              TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1));
        val dest =
          if is_sel_upd_pair thy acc upd
          then @{thm o_eq_dest}
          else @{thm o_eq_id_dest};
      in Drule.export_without_context (othm RS dest) end;
  in map get_simp upd_funs end;

fun get_updupd_simp thy defset u u' comp =
  let
    (* FIXME fresh "f" (!?) *)
    val f = Free ("f", domain_type (fastype_of u));
    val f' = Free ("f'", domain_type (fastype_of u'));
    val lhs = HOLogic.mk_comp (u $ f, u' $ f');
    val rhs =
      if comp
      then u $ HOLogic.mk_comp (f, f')
      else HOLogic.mk_comp (u' $ f', u $ f);
    val prop = lhs === rhs;
    val othm =
      Goal.prove (Proof_Context.init_global thy) [] [] prop
        (fn _ =>
          simp_tac defset 1 THEN
          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
          TRY (simp_tac (HOL_ss addsimps @{thms id_apply}) 1));
    val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
  in Drule.export_without_context (othm RS dest) end;

fun get_updupd_simps thy term defset =
  let
    val upd_funs = get_upd_funs term;
    val cname = fst o dest_Const;
    fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
    fun build_swaps_to_eq _ [] swaps = swaps
      | build_swaps_to_eq upd (u :: us) swaps =
          let
            val key = (cname u, cname upd);
            val newswaps =
              if Symreltab.defined swaps key then swaps
              else Symreltab.insert (K true) (key, getswap u upd) swaps;
          in
            if cname u = cname upd then newswaps
            else build_swaps_to_eq upd us newswaps
          end;
    fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
      | swaps_needed (u :: us) prev seen swaps =
          if Symtab.defined seen (cname u)
          then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
          else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
  in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;

val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;

fun prove_unfold_defs thy ex_simps ex_simprs prop =
  let
    val defset = get_sel_upd_defs thy;
    val prop' = Envir.beta_eta_contract prop;
    val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
    val (_, args) = strip_comb lhs;
    val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
  in
    Goal.prove (Proof_Context.init_global thy) [] [] prop'
      (fn _ =>
        simp_tac (HOL_basic_ss addsimps (simps @ @{thms K_record_comp})) 1 THEN
        TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
  end;


local

fun eq (s1: string) (s2: string) = (s1 = s2);

fun has_field extfields f T =
  exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);

fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
      if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  | K_skeleton n T b _ = ((n, T), b);

in

(* simproc *)

(*
  Simplify selections of an record update:
    (1)  S (S_update k r) = k (S r)
    (2)  S (X_update k r) = S r

  The simproc skips multiple updates at once, eg:
   S (X_update x (Y_update y (S_update k r))) = k (S r)

  But be careful in (2) because of the extensibility of records.
  - If S is a more-selector we have to make sure that the update on component
    X does not affect the selected subrecord.
  - If X is a more-selector we have to make sure that S is not in the updated
    subrecord.
*)
val simproc =
  Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
    (fn thy => fn _ => fn t =>
      (case t of
        (sel as Const (s, Type (_, [_, rangeS]))) $
            ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
          if is_selector thy s andalso is_some (get_updates thy u) then
            let
              val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;

              fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
                    (case Symtab.lookup updates u of
                      NONE => NONE
                    | SOME u_name =>
                        if u_name = s then
                          (case mk_eq_terms r of
                            NONE =>
                              let
                                val rv = ("r", rT);
                                val rb = Bound 0;
                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
                              in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
                          | SOME (trm, trm', vars) =>
                              let
                                val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
                              in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
                        else if has_field extfields u_name rangeS orelse
                          has_field extfields s (domain_type kT) then NONE
                        else
                          (case mk_eq_terms r of
                            SOME (trm, trm', vars) =>
                              let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
                              in SOME (upd $ kb $ trm, trm', kv :: vars) end
                          | NONE =>
                              let
                                val rv = ("r", rT);
                                val rb = Bound 0;
                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
                              in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
                | mk_eq_terms _ = NONE;
            in
              (case mk_eq_terms (upd $ k $ r) of
                SOME (trm, trm', vars) =>
                  SOME
                    (prove_unfold_defs thy [] []
                      (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
              | NONE => NONE)
            end
          else NONE
      | _ => NONE));

fun get_upd_acc_cong_thm upd acc thy simpset =
  let
    val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
    val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
  in
    Goal.prove (Proof_Context.init_global thy) [] [] prop
      (fn _ =>
        simp_tac simpset 1 THEN
        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
        TRY (resolve_tac [updacc_cong_idI] 1))
  end;


(* upd_simproc *)

(*Simplify multiple updates:
    (1) "N_update y (M_update g (N_update x (M_update f r))) =
          (N_update (y o x) (M_update (g o f) r))"
    (2)  "r(|M:= M r|) = r"

  In both cases "more" updates complicate matters: for this reason
  we omit considering further updates if doing so would introduce
  both a more update and an update to a field within it.*)
val upd_simproc =
  Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
    (fn thy => fn _ => fn t =>
      let
        (*We can use more-updators with other updators as long
          as none of the other updators go deeper than any more
          updator. min here is the depth of the deepest other
          updator, max the depth of the shallowest more updator.*)
        fun include_depth (dep, true) (min, max) =
              if min <= dep
              then SOME (min, if dep <= max orelse max = ~1 then dep else max)
              else NONE
          | include_depth (dep, false) (min, max) =
              if dep <= max orelse max = ~1
              then SOME (if min <= dep then dep else min, max)
              else NONE;

        fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
              (case get_update_details u thy of
                SOME (s, dep, ismore) =>
                  (case include_depth (dep, ismore) (min, max) of
                    SOME (min', max') =>
                      let val (us, bs, _) = getupdseq tm min' max'
                      in ((upd, s, f) :: us, bs, fastype_of term) end
                  | NONE => ([], term, HOLogic.unitT))
              | NONE => ([], term, HOLogic.unitT))
          | getupdseq term _ _ = ([], term, HOLogic.unitT);

        val (upds, base, baseT) = getupdseq t 0 ~1;

        fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
              if s = s' andalso null (loose_bnos tm')
                andalso subst_bound (HOLogic.unit, tm') = tm
              then (true, Abs (n, T, Const (s', T') $ Bound 1))
              else (false, HOLogic.unit)
          | is_upd_noop _ _ _ = (false, HOLogic.unit);

        fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
          let
            val ss = get_sel_upd_defs thy;
            val uathm = get_upd_acc_cong_thm upd acc thy ss;
          in
           [Drule.export_without_context (uathm RS updacc_noopE),
            Drule.export_without_context (uathm RS updacc_noop_compE)]
          end;

        (*If f is constant then (f o g) = f.  We know that K_skeleton
          only returns constant abstractions thus when we see an
          abstraction we can discard inner updates.*)
        fun add_upd (f as Abs _) fs = [f]
          | add_upd f fs = (f :: fs);

        (*mk_updterm returns
          (orig-term-skeleton, simplified-skeleton,
            variables, duplicate-updates, simp-flag, noop-simps)

          where duplicate-updates is a table used to pass upward
          the list of update functions which can be composed
          into an update above them, simp-flag indicates whether
          any simplification was achieved, and noop-simps are
          used for eliminating case (2) defined above*)
        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
              let
                val (lhs, rhs, vars, dups, simp, noops) =
                  mk_updterm upds (Symtab.update (u, ()) above) term;
                val (fvar, skelf) =
                  K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
                val (isnoop, skelf') = is_upd_noop s f term;
                val funT = domain_type T;
                fun mk_comp_local (f, f') =
                  Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
              in
                if isnoop then
                  (upd $ skelf' $ lhs, rhs, vars,
                    Symtab.update (u, []) dups, true,
                    if Symtab.defined noops u then noops
                    else Symtab.update (u, get_noop_simps upd skelf') noops)
                else if Symtab.defined above u then
                  (upd $ skelf $ lhs, rhs, fvar :: vars,
                    Symtab.map_default (u, []) (add_upd skelf) dups,
                    true, noops)
                else
                  (case Symtab.lookup dups u of
                    SOME fs =>
                     (upd $ skelf $ lhs,
                      upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
                      fvar :: vars, dups, true, noops)
                  | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
              end
          | mk_updterm [] _ _ =
              (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);

        val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
        val noops' = maps snd (Symtab.dest noops);
      in
        if simp then
          SOME
            (prove_unfold_defs thy noops' [simproc]
              (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
        else NONE
      end);

end;