src/HOL/Tools/record.ML
changeset 32743 c4e9a48bc50e
parent 32335 41fe1c93f218
child 32744 50406c4951d9
     1.1 --- a/src/HOL/Tools/record.ML	Sat Aug 15 15:29:54 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Aug 27 00:40:53 2009 +1000
     1.3 @@ -55,8 +55,6 @@
     1.4  struct
     1.5  
     1.6  val eq_reflection = thm "eq_reflection";
     1.7 -val rec_UNIV_I = thm "rec_UNIV_I";
     1.8 -val rec_True_simp = thm "rec_True_simp";
     1.9  val Pair_eq = thm "Product_Type.prod.inject";
    1.10  val atomize_all = thm "HOL.atomize_all";
    1.11  val atomize_imp = thm "HOL.atomize_imp";
    1.12 @@ -65,6 +63,34 @@
    1.13  val Pair_sel_convs = [fst_conv,snd_conv];
    1.14  val K_record_comp = @{thm "K_record_comp"};
    1.15  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    1.16 +val transitive_thm = thm "transitive";
    1.17 +val o_assoc = @{thm "o_assoc"};
    1.18 +val id_apply = @{thm id_apply};
    1.19 +val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    1.20 +
    1.21 +val refl_conj_eq = thm "refl_conj_eq";
    1.22 +val meta_all_sameI = thm "meta_all_sameI";
    1.23 +val meta_iffD2 = thm "meta_iffD2";
    1.24 +
    1.25 +val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    1.26 +val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    1.27 +
    1.28 +val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
    1.29 +val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
    1.30 +val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
    1.31 +val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
    1.32 +
    1.33 +val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
    1.34 +val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
    1.35 +val updacc_noopE = @{thm "update_accessor_noopE"};
    1.36 +val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
    1.37 +val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
    1.38 +val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
    1.39 +val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
    1.40 +
    1.41 +val o_eq_dest = thm "o_eq_dest";
    1.42 +val o_eq_id_dest = thm "o_eq_id_dest";
    1.43 +val o_eq_dest_lhs = thm "o_eq_dest_lhs";
    1.44  
    1.45  (** name components **)
    1.46  
    1.47 @@ -73,6 +99,7 @@
    1.48  val moreN = "more";
    1.49  val schemeN = "_scheme";
    1.50  val ext_typeN = "_ext_type";
    1.51 +val inner_typeN = "_inner_type";
    1.52  val extN ="_ext";
    1.53  val casesN = "_cases";
    1.54  val ext_dest = "_sel";
    1.55 @@ -232,23 +259,26 @@
    1.56    parent: (typ list * string) option,
    1.57    fields: (string * typ) list,
    1.58    extension: (string * typ list),
    1.59 -  induct: thm
    1.60 +  induct: thm,
    1.61 +  extdef: thm
    1.62   };
    1.63  
    1.64 -fun make_record_info args parent fields extension induct =
    1.65 +fun make_record_info args parent fields extension induct extdef =
    1.66   {args = args, parent = parent, fields = fields, extension = extension,
    1.67 -  induct = induct}: record_info;
    1.68 +  induct = induct, extdef = extdef}: record_info;
    1.69  
    1.70  
    1.71  type parent_info =
    1.72   {name: string,
    1.73    fields: (string * typ) list,
    1.74    extension: (string * typ list),
    1.75 -  induct: thm
    1.76 +  induct: thm,
    1.77 +  extdef: thm
    1.78  };
    1.79  
    1.80 -fun make_parent_info name fields extension induct =
    1.81 - {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
    1.82 +fun make_parent_info name fields extension induct extdef =
    1.83 + {name = name, fields = fields, extension = extension,
    1.84 +  induct = induct, extdef = extdef}: parent_info;
    1.85  
    1.86  
    1.87  (* theory data *)
    1.88 @@ -278,14 +308,18 @@
    1.89    type T = record_data;
    1.90    val empty =
    1.91      make_record_data Symtab.empty
    1.92 -      {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
    1.93 +      {selectors = Symtab.empty, updates = Symtab.empty,
    1.94 +          simpset = HOL_basic_ss, defset = HOL_basic_ss,
    1.95 +          foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
    1.96         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    1.97  
    1.98    val copy = I;
    1.99    val extend = I;
   1.100    fun merge _
   1.101     ({records = recs1,
   1.102 -     sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   1.103 +     sel_upd = {selectors = sels1, updates = upds1,
   1.104 +                simpset = ss1, defset = ds1,
   1.105 +                foldcong = fc1, unfoldcong = uc1},
   1.106       equalities = equalities1,
   1.107       extinjects = extinjects1,
   1.108       extsplit = extsplit1,
   1.109 @@ -293,7 +327,9 @@
   1.110       extfields = extfields1,
   1.111       fieldext = fieldext1},
   1.112      {records = recs2,
   1.113 -     sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   1.114 +     sel_upd = {selectors = sels2, updates = upds2,
   1.115 +                simpset = ss2, defset = ds2,
   1.116 +                foldcong = fc2, unfoldcong = uc2},
   1.117       equalities = equalities2,
   1.118       extinjects = extinjects2,
   1.119       extsplit = extsplit2,
   1.120 @@ -304,7 +340,10 @@
   1.121        (Symtab.merge (K true) (recs1, recs2))
   1.122        {selectors = Symtab.merge (K true) (sels1, sels2),
   1.123          updates = Symtab.merge (K true) (upds1, upds2),
   1.124 -        simpset = Simplifier.merge_ss (ss1, ss2)}
   1.125 +        simpset = Simplifier.merge_ss (ss1, ss2),
   1.126 +        defset = Simplifier.merge_ss (ds1, ds2),
   1.127 +        foldcong = Simplifier.merge_ss (fc1, fc2),
   1.128 +        unfoldcong = Simplifier.merge_ss (uc1, uc2)}
   1.129        (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   1.130        (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
   1.131        (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2))
   1.132 @@ -355,7 +394,21 @@
   1.133  
   1.134  val is_selector = Symtab.defined o #selectors o get_sel_upd;
   1.135  val get_updates = Symtab.lookup o #updates o get_sel_upd;
   1.136 -fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
   1.137 +fun get_ss_with_context getss thy =
   1.138 +    Simplifier.theory_context thy (getss (get_sel_upd thy));
   1.139 +
   1.140 +val get_simpset = get_ss_with_context (#simpset);
   1.141 +val get_sel_upd_defs = get_ss_with_context (#defset);
   1.142 +val get_foldcong_ss = get_ss_with_context (#foldcong);
   1.143 +val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
   1.144 +
   1.145 +fun get_update_details u thy = let
   1.146 +    val sel_upd = get_sel_upd thy;
   1.147 +  in case (Symtab.lookup (#updates sel_upd) u) of
   1.148 +    SOME s => let
   1.149 +        val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s;
   1.150 +      in SOME (s, dep, ismore) end
   1.151 +  | NONE => NONE end;
   1.152  
   1.153  fun put_sel_upd names simps = RecordsData.map (fn {records,
   1.154    sel_upd = {selectors, updates, simpset},
   1.155 @@ -489,7 +542,7 @@
   1.156        let
   1.157          fun err msg = error (msg ^ " parent record " ^ quote name);
   1.158  
   1.159 -        val {args, parent, fields, extension, induct} =
   1.160 +        val {args, parent, fields, extension, induct, extdef} =
   1.161            (case get_record thy name of SOME info => info | NONE => err "Unknown");
   1.162          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   1.163  
   1.164 @@ -505,7 +558,7 @@
   1.165          val extension' = apsnd (map subst) extension;
   1.166        in
   1.167          add_parents thy parent'
   1.168 -          (make_parent_info name fields' extension' induct :: parents)
   1.169 +          (make_parent_info name fields' extension' induct extdef :: parents)
   1.170        end;
   1.171  
   1.172  
   1.173 @@ -882,95 +935,113 @@
   1.174        then noopt ()
   1.175        else opt ();
   1.176  
   1.177 -local
   1.178 -fun abstract_over_fun_app (Abs (f,fT,t)) =
   1.179 -  let
   1.180 -     val (f',t') = Term.dest_abs (f,fT,t);
   1.181 -     val T = domain_type fT;
   1.182 -     val (x,T') = hd (Term.variant_frees t' [("x",T)]);
   1.183 -     val f_x = Free (f',fT)$(Free (x,T'));
   1.184 -     fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
   1.185 -       | is_constr _ = false;
   1.186 -     fun subst (t as u$w) = if Free (f',fT)=u
   1.187 -                            then if is_constr w then f_x
   1.188 -                                 else raise TERM ("abstract_over_fun_app",[t])
   1.189 -                            else subst u$subst w
   1.190 -       | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
   1.191 -       | subst t = t
   1.192 -     val t'' = abstract_over (f_x,subst t');
   1.193 -     val vars = strip_qnt_vars "all" t'';
   1.194 -     val bdy = strip_qnt_body "all" t'';
   1.195 -
   1.196 -  in list_abs ((x,T')::vars,bdy) end
   1.197 -  | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
   1.198 -(* Generates a theorem of the kind:
   1.199 - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
   1.200 - *)
   1.201 -fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
   1.202 +fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t'))
   1.203 +  = case (get_updates thy u)
   1.204 +    of SOME u_name => u_name = s
   1.205 +     | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]);
   1.206 +
   1.207 +fun mk_comp f g = let
   1.208 +    val x = fastype_of g;
   1.209 +    val a = domain_type x;
   1.210 +    val b = range_type x;
   1.211 +    val c = range_type (fastype_of f);
   1.212 +    val T = (b --> c) --> ((a --> b) --> (a --> c))
   1.213 +  in Const ("Fun.comp", T) $ f $ g end;
   1.214 +
   1.215 +fun mk_comp_id f = let
   1.216 +    val T = range_type (fastype_of f);
   1.217 +  in mk_comp (Const ("Fun.id", T --> T)) f end;
   1.218 +
   1.219 +fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t
   1.220 +  | get_updfuns _             = [];
   1.221 +
   1.222 +fun get_accupd_simps thy term defset intros_tac = let
   1.223 +    val (acc, [body]) = strip_comb term;
   1.224 +    val recT          = domain_type (fastype_of acc);
   1.225 +    val updfuns       = sort_distinct Term.fast_term_ord
   1.226 +                           (get_updfuns body);
   1.227 +    fun get_simp upd  = let
   1.228 +        val T    = domain_type (fastype_of upd);
   1.229 +        val lhs  = mk_comp acc (upd $ Free ("f", T));
   1.230 +        val rhs  = if is_sel_upd_pair thy acc upd
   1.231 +                   then mk_comp (Free ("f", T)) acc else mk_comp_id acc;
   1.232 +        val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   1.233 +        val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   1.234 +            EVERY [simp_tac defset 1,
   1.235 +                   REPEAT_DETERM (intros_tac 1),
   1.236 +                   TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
   1.237 +        val dest = if is_sel_upd_pair thy acc upd
   1.238 +                   then o_eq_dest else o_eq_id_dest;
   1.239 +      in standard (othm RS dest) end;
   1.240 +  in map get_simp updfuns end;
   1.241 +
   1.242 +structure SymSymTab = TableFun(type key = string * string
   1.243 +                                val ord = prod_ord fast_string_ord fast_string_ord);
   1.244 +
   1.245 +fun get_updupd_simp thy defset intros_tac u u' comp = let
   1.246 +    val f    = Free ("f", domain_type (fastype_of u));
   1.247 +    val f'   = Free ("f'", domain_type (fastype_of u'));
   1.248 +    val lhs  = mk_comp (u $ f) (u' $ f');
   1.249 +    val rhs  = if comp
   1.250 +               then u $ mk_comp f f'
   1.251 +               else mk_comp (u' $ f') (u $ f);
   1.252 +    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   1.253 +    val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   1.254 +        EVERY [simp_tac defset 1,
   1.255 +               REPEAT_DETERM (intros_tac 1),
   1.256 +               TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
   1.257 +    val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   1.258 +  in standard (othm RS dest) end;
   1.259 +
   1.260 +fun get_updupd_simps thy term defset intros_tac = let
   1.261 +    val recT          = fastype_of term;
   1.262 +    val updfuns       = get_updfuns term;
   1.263 +    val cname         = fst o dest_Const;
   1.264 +    fun getswap u u'  = get_updupd_simp thy defset intros_tac u u'
   1.265 +                              (cname u = cname u');
   1.266 +    fun buildswapstoeq upd [] swaps = swaps
   1.267 +      | buildswapstoeq upd (u::us) swaps = let
   1.268 +             val key      = (cname u, cname upd);
   1.269 +             val newswaps = if SymSymTab.defined swaps key then swaps
   1.270 +                            else SymSymTab.insert (K true)
   1.271 +                                     (key, getswap u upd) swaps;
   1.272 +          in if cname u = cname upd then newswaps
   1.273 +             else buildswapstoeq upd us newswaps end;
   1.274 +    fun swapsneeded []      prev seen swaps = map snd (SymSymTab.dest swaps)
   1.275 +      | swapsneeded (u::us) prev seen swaps =
   1.276 +           if Symtab.defined seen (cname u)
   1.277 +           then swapsneeded us prev seen
   1.278 +                   (buildswapstoeq u prev swaps)
   1.279 +           else swapsneeded us (u::prev)
   1.280 +                   (Symtab.insert (K true) (cname u, ()) seen) swaps;
   1.281 +  in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
   1.282 +
   1.283 +fun named_cterm_instantiate values thm = let
   1.284 +    fun match name (Var ((name', _), _)) = name = name'
   1.285 +      | match name _ = false;
   1.286 +    fun getvar name = case (find_first (match name) (term_vars (prop_of thm)))
   1.287 +      of SOME var => cterm_of (theory_of_thm thm) var
   1.288 +       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
   1.289 +  in
   1.290 +    cterm_instantiate (map (apfst getvar) values) thm
   1.291 +  end;
   1.292 +
   1.293 +fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
   1.294    let
   1.295 -    val rT = domain_type fT;
   1.296 -    val vars = Term.strip_qnt_vars "all" t;
   1.297 -    val Ts = map snd vars;
   1.298 -    val n = length vars;
   1.299 -    fun app_bounds 0 t = t$Bound 0
   1.300 -      | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
   1.301 -
   1.302 -
   1.303 -    val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
   1.304 -    val prop = Logic.mk_equals
   1.305 -                (list_all ((f,fT)::vars,
   1.306 -                           app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
   1.307 -                 list_all ((fst r,rT)::vars,
   1.308 -                           app_bounds (n - 1) ((Free P)$Bound n)));
   1.309 -    val prove_standard = quick_and_dirty_prove true thy;
   1.310 -    val thm = prove_standard [] prop (fn _ =>
   1.311 -	 EVERY [rtac equal_intr_rule 1,
   1.312 -                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
   1.313 -                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   1.314 -  in thm end
   1.315 -  | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
   1.316 -
   1.317 -in
   1.318 -(* During proof of theorems produced by record_simproc you can end up in
   1.319 - * situations like "!!f ... . ... f r ..." where f is an extension update function.
   1.320 - * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the
   1.321 - * usual split rules for extensions can apply.
   1.322 - *)
   1.323 -val record_split_f_more_simproc =
   1.324 -  Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"]
   1.325 -    (fn thy => fn _ => fn t =>
   1.326 -      (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
   1.327 -                  (trm as Abs _) =>
   1.328 -         (case rec_id (~1) T of
   1.329 -            "" => NONE
   1.330 -          | n => if T=T'
   1.331 -                 then (let
   1.332 -                        val P=cterm_of thy (abstract_over_fun_app trm);
   1.333 -                        val thm = mk_fun_apply_eq trm thy;
   1.334 -                        val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm)));
   1.335 -                        val thm' = cterm_instantiate [(PV,P)] thm;
   1.336 -                       in SOME  thm' end handle TERM _ => NONE)
   1.337 -                else NONE)
   1.338 -       | _ => NONE))
   1.339 -end
   1.340 -
   1.341 -fun prove_split_simp thy ss T prop =
   1.342 -  let
   1.343 -    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get thy;
   1.344 -    val extsplits =
   1.345 -            Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms)
   1.346 -                    ([],dest_recTs T);
   1.347 -    val thms = (case get_splits thy (rec_id (~1) T) of
   1.348 -                   SOME (all_thm,_,_,_) =>
   1.349 -                     all_thm::(case extsplits of [thm] => [] | _ => extsplits)
   1.350 -                              (* [thm] is the same as all_thm *)
   1.351 -                 | NONE => extsplits)
   1.352 -    val thms'=K_comp_convs@thms;
   1.353 -    val ss' = (Simplifier.inherit_context ss simpset
   1.354 -                addsimps thms'
   1.355 -                addsimprocs [record_split_f_more_simproc]);
   1.356 +    val defset = get_sel_upd_defs thy;
   1.357 +    val intros = IsTupleSupport.get_istuple_intros thy;
   1.358 +    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
   1.359 +    val prop'  = Envir.beta_eta_contract prop;
   1.360 +    val (lhs, rhs)   = Logic.dest_equals (Logic.strip_assums_concl prop');
   1.361 +    val (head, args) = strip_comb lhs;
   1.362 +    val simps        = if length args = 1
   1.363 +                       then get_accupd_simps thy lhs defset in_tac
   1.364 +                       else get_updupd_simps thy lhs defset in_tac;
   1.365    in
   1.366 -    quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1)
   1.367 +    Goal.prove (ProofContext.init thy) [] [] prop' (fn prems =>
   1.368 +              simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1
   1.369 +         THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps
   1.370 +                                          addsimprocs ex_simprs) 1))
   1.371    end;
   1.372  
   1.373  
   1.374 @@ -984,21 +1055,6 @@
   1.375       if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b)
   1.376    | K_skeleton n T b _ = ((n,T),b);
   1.377  
   1.378 -(*
   1.379 -fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = 
   1.380 -      ((n,kT),K_rec$b)
   1.381 -  | K_skeleton n _ (Bound i) 
   1.382 -      (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) =
   1.383 -        ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0)))
   1.384 -  | K_skeleton n T b  _ = ((n,T),b);
   1.385 - *)
   1.386 -
   1.387 -fun normalize_rhs thm =
   1.388 -  let
   1.389 -     val ss = HOL_basic_ss addsimps K_comp_convs; 
   1.390 -     val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd;
   1.391 -     val rhs' = (Simplifier.rewrite ss rhs);
   1.392 -  in Thm.transitive thm rhs' end;
   1.393  in
   1.394  (* record_simproc *)
   1.395  (* Simplifies selections of an record update:
   1.396 @@ -1044,7 +1100,7 @@
   1.397                               else (case mk_eq_terms r of
   1.398                                       SOME (trm,trm',vars)
   1.399                                       => let
   1.400 -                                          val (kv,kb) = 
   1.401 +                                          val (kv,kb) =
   1.402                                                   K_skeleton "k" kT (Bound (length vars)) k;
   1.403                                          in SOME (upd$kb$trm,trm',kv::vars) end
   1.404                                     | NONE
   1.405 @@ -1057,150 +1113,140 @@
   1.406              in
   1.407                (case mk_eq_terms (upd$k$r) of
   1.408                   SOME (trm,trm',vars)
   1.409 -                 => SOME (prove_split_simp thy ss domS
   1.410 -                                 (list_all(vars, Logic.mk_equals (sel $ trm, trm'))))
   1.411 +                 => SOME (prove_unfold_defs thy ss domS [] []
   1.412 +                             (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
   1.413                 | NONE => NONE)
   1.414              end
   1.415            | NONE => NONE)
   1.416          else NONE
   1.417        | _ => NONE));
   1.418  
   1.419 +fun get_upd_acc_cong_thm upd acc thy simpset = let
   1.420 +    val intros = IsTupleSupport.get_istuple_intros thy;
   1.421 +    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
   1.422 +
   1.423 +    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
   1.424 +    val prop  = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   1.425 +  in Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   1.426 +        EVERY [simp_tac simpset 1,
   1.427 +               REPEAT_DETERM (in_tac 1),
   1.428 +               TRY (resolve_tac [updacc_cong_idI] 1)])
   1.429 +  end;
   1.430 +
   1.431  (* record_upd_simproc *)
   1.432  (* simplify multiple updates:
   1.433   *  (1)  "N_update y (M_update g (N_update x (M_update f r))) =
   1.434            (N_update (y o x) (M_update (g o f) r))"
   1.435   *  (2)  "r(|M:= M r|) = r"
   1.436 - * For (2) special care of "more" updates has to be taken:
   1.437 - *    r(|more := m; A := A r|)
   1.438 - * If A is contained in the fields of m we cannot remove the update A := A r!
   1.439 - * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
   1.440 + * In both cases "more" updates complicate matters: for this reason
   1.441 + * we omit considering further updates if doing so would introduce
   1.442 + * both a more update and an update to a field within it.
   1.443  *)
   1.444  val record_upd_simproc =
   1.445    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   1.446      (fn thy => fn ss => fn t =>
   1.447 -      (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
   1.448 -         let datatype ('a,'b) calc = Init of 'b | Inter of 'a
   1.449 -             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
   1.450 -
   1.451 -             (*fun mk_abs_var x t = (x, fastype_of t);*)
   1.452 -             fun sel_name u = Long_Name.base_name (unsuffix updateN u);
   1.453 -
   1.454 -             fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   1.455 -                  if has_field extfields s (domain_type' mT) then upd else seed s r
   1.456 -               | seed _ r = r;
   1.457 -
   1.458 -             fun grow u uT k kT vars (sprout,skeleton) =
   1.459 -                   if sel_name u = moreN
   1.460 -                   then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k;
   1.461 -                        in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
   1.462 -                   else ((sprout,skeleton),vars);
   1.463 -
   1.464 -
   1.465 -             fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) =
   1.466 -                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   1.467 -               | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) =
   1.468 -                  (* eta expanded variant *)
   1.469 -                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   1.470 -               | dest_k _ = NONE;
   1.471 -
   1.472 -             fun is_upd_same (sprout,skeleton) u k =
   1.473 -               (case dest_k k of SOME (x,T,sel,s,r) =>
   1.474 -                   if (unsuffix updateN u) = s andalso (seed s sprout) = r
   1.475 -                   then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton)
   1.476 -                   else NONE
   1.477 -                | NONE => NONE);
   1.478 -
   1.479 -             fun init_seed r = ((r,Bound 0), [("r", rT)]);
   1.480 -
   1.481 -             fun add (n:string) f fmaps =
   1.482 -               (case AList.lookup (op =) fmaps n of
   1.483 -                  NONE => AList.update (op =) (n,[f]) fmaps
   1.484 -                | SOME fs => AList.update (op =) (n,f::fs) fmaps)
   1.485 -
   1.486 -             fun comps (n:string) T fmaps =
   1.487 -               (case AList.lookup (op =) fmaps n of
   1.488 -                 SOME fs =>
   1.489 -                   foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
   1.490 -                | NONE => error ("record_upd_simproc.comps"))
   1.491 -
   1.492 -             (* mk_updterm returns either
   1.493 -              *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
   1.494 -              *     where vars are the bound variables in the skeleton
   1.495 -              *  - Inter (orig-term-skeleton,simplified-term-skeleton,
   1.496 -              *           vars, (term-sprout, skeleton-sprout))
   1.497 -              *     where "All vars. orig-term-skeleton = simplified-term-skeleton" is
   1.498 -              *     the desired simplification rule,
   1.499 -              *     the sprouts accumulate the "more-updates" on the way from the seed
   1.500 -              *     to the outermost update. It is only relevant to calculate the
   1.501 -              *     possible simplification for (2)
   1.502 -              * The algorithm first walks down the updates to the seed-record while
   1.503 -              * memorising the updates in the already-table. While walking up the
   1.504 -              * updates again, the optimised term is constructed.
   1.505 -              *)
   1.506 -             fun mk_updterm upds already
   1.507 -                 (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) =
   1.508 -                 if Symtab.defined upds u
   1.509 -                 then let
   1.510 -                         fun rest already = mk_updterm upds already
   1.511 -                      in if u mem_string already
   1.512 -                         then (case (rest already r) of
   1.513 -                                 Init ((sprout,skel),vars) =>
   1.514 -                                 let
   1.515 -                                   val n = sel_name u;
   1.516 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.517 -                                   val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel);
   1.518 -                                 in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end
   1.519 -                               | Inter (trm,trm',vars,fmaps,sprout) =>
   1.520 -                                 let
   1.521 -                                   val n = sel_name u;
   1.522 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.523 -                                   val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
   1.524 -                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
   1.525 -                                 end)
   1.526 -                         else
   1.527 -                          (case rest (u::already) r of
   1.528 -                             Init ((sprout,skel),vars) =>
   1.529 -                              (case is_upd_same (sprout,skel) u k of
   1.530 -                                 SOME (K_rec,sel,skel') =>
   1.531 -                                 let
   1.532 -                                   val (sprout',vars') = grow u uT k kT vars (sprout,skel);
   1.533 -                                  in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout')
   1.534 -                                  end
   1.535 -                               | NONE =>
   1.536 -                                 let
   1.537 -                                   val n = sel_name u;
   1.538 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.539 -                                 in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
   1.540 -                           | Inter (trm,trm',vars,fmaps,sprout) =>
   1.541 -                               (case is_upd_same sprout u k of
   1.542 -                                  SOME (K_rec,sel,skel) =>
   1.543 -                                  let
   1.544 -                                    val (sprout',vars') = grow u uT k kT vars sprout
   1.545 -                                  in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout')
   1.546 -                                  end
   1.547 -                                | NONE =>
   1.548 -                                  let
   1.549 -                                    val n = sel_name u
   1.550 -                                    val T = domain_type kT
   1.551 -                                    val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.552 -                                    val (sprout',vars') = grow u uT k kT (kv::vars) sprout
   1.553 -                                    val fmaps' = add n kb fmaps
   1.554 -                                  in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
   1.555 -                                           ,vars',fmaps',sprout') end))
   1.556 -                     end
   1.557 -                 else Init (init_seed t)
   1.558 -               | mk_updterm _ _ t = Init (init_seed t);
   1.559 -
   1.560 -         in (case mk_updterm updates [] t of
   1.561 -               Inter (trm,trm',vars,_,_)
   1.562 -                => SOME (normalize_rhs 
   1.563 -                          (prove_split_simp thy ss rT
   1.564 -                            (list_all(vars, Logic.mk_equals (trm, trm')))))
   1.565 -             | _ => NONE)
   1.566 -         end
   1.567 -       | _ => NONE))
   1.568 +      let
   1.569 +        (* we can use more-updators with other updators as long
   1.570 +           as none of the other updators go deeper than any more
   1.571 +           updator. min here is the depth of the deepest other
   1.572 +           updator, max the depth of the shallowest more updator *)
   1.573 +        fun include_depth (dep, true) (min, max) =
   1.574 +          if (min <= dep)
   1.575 +          then SOME (min, if dep <= max orelse max = ~1 then dep else max)
   1.576 +          else NONE
   1.577 +          | include_depth (dep, false) (min, max) =
   1.578 +          if (dep <= max orelse max = ~1)
   1.579 +          then SOME (if min <= dep then dep else min, max)
   1.580 +          else NONE;
   1.581 +
   1.582 +        fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
   1.583 +            (case get_update_details u thy of
   1.584 +              SOME (s, dep, ismore) =>
   1.585 +                (case include_depth (dep, ismore) (min, max) of
   1.586 +                  SOME (min', max') => let
   1.587 +                        val (us, bs, _) = getupdseq tm min' max';
   1.588 +                      in ((upd, s, f) :: us, bs, fastype_of term) end
   1.589 +                | NONE => ([], term, HOLogic.unitT))
   1.590 +            | NONE => ([], term, HOLogic.unitT))
   1.591 +          | getupdseq term _ _ = ([], term, HOLogic.unitT);
   1.592 +
   1.593 +        val (upds, base, baseT) = getupdseq t 0 ~1;
   1.594 +
   1.595 +        fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
   1.596 +            if s = s' andalso null (loose_bnos tm')
   1.597 +              andalso subst_bound (HOLogic.unit, tm') = tm
   1.598 +            then (true, Abs (n, T, Const (s', T') $ Bound 1))
   1.599 +            else (false, HOLogic.unit)
   1.600 +          | is_upd_noop s f tm = (false, HOLogic.unit);
   1.601 +
   1.602 +        fun get_noop_simps (upd as Const (u, T))
   1.603 +                      (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = let
   1.604 +
   1.605 +            val ss    = get_sel_upd_defs thy;
   1.606 +            val uathm = get_upd_acc_cong_thm upd acc thy ss;
   1.607 +          in [standard (uathm RS updacc_noopE),
   1.608 +              standard (uathm RS updacc_noop_compE)] end;
   1.609 +
   1.610 +        (* if f is constant then (f o g) = f. we know that K_skeleton
   1.611 +           only returns constant abstractions thus when we see an
   1.612 +           abstraction we can discard inner updates. *)
   1.613 +        fun add_upd (f as Abs _) fs = [f]
   1.614 +          | add_upd f fs = (f :: fs);
   1.615 +
   1.616 +        (* mk_updterm returns
   1.617 +         * (orig-term-skeleton, simplified-skeleton,
   1.618 +         *  variables, duplicate-updates, simp-flag, noop-simps)
   1.619 +         *
   1.620 +         *  where duplicate-updates is a table used to pass upward
   1.621 +         *  the list of update functions which can be composed
   1.622 +         *  into an update above them, simp-flag indicates whether
   1.623 +         *  any simplification was achieved, and noop-simps are
   1.624 +         *  used for eliminating case (2) defined above
   1.625 +         *)
   1.626 +        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let
   1.627 +            val (lhs, rhs, vars, dups, simp, noops) =
   1.628 +                  mk_updterm upds (Symtab.update (u, ()) above) term;
   1.629 +            val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T)
   1.630 +                                      (Bound (length vars)) f;
   1.631 +            val (isnoop, skelf') = is_upd_noop s f term;
   1.632 +            val funT  = domain_type T;
   1.633 +            fun mk_comp_local (f, f') =
   1.634 +              Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
   1.635 +          in if isnoop
   1.636 +              then (upd $ skelf' $ lhs, rhs, vars,
   1.637 +                    Symtab.update (u, []) dups, true,
   1.638 +                    if Symtab.defined noops u then noops
   1.639 +                    else Symtab.update (u, get_noop_simps upd skelf') noops)
   1.640 +            else if Symtab.defined above u
   1.641 +              then (upd $ skelf $ lhs, rhs, fvar :: vars,
   1.642 +                    Symtab.map_default (u, []) (add_upd skelf) dups,
   1.643 +                    true, noops)
   1.644 +            else case Symtab.lookup dups u of
   1.645 +              SOME fs =>
   1.646 +                   (upd $ skelf $ lhs,
   1.647 +                    upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
   1.648 +                    fvar :: vars, dups, true, noops)
   1.649 +            | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs,
   1.650 +                       fvar :: vars, dups, simp, noops)
   1.651 +          end
   1.652 +          | mk_updterm [] above term = (Bound 0, Bound 0, [("r", baseT)],
   1.653 +                                          Symtab.empty, false, Symtab.empty)
   1.654 +          | mk_updterm us above term = raise TERM ("mk_updterm match",
   1.655 +                                              map (fn (x, y, z) => x) us);
   1.656 +
   1.657 +        val (lhs, rhs, vars, dups, simp, noops)
   1.658 +                  = mk_updterm upds Symtab.empty base;
   1.659 +        val noops' = flat (map snd (Symtab.dest noops));
   1.660 +      in
   1.661 +        if simp then
   1.662 +           SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
   1.663 +                             (list_all(vars,(equals baseT$lhs$rhs))))
   1.664 +        else NONE
   1.665 +      end)
   1.666 +
   1.667  end
   1.668  
   1.669 +
   1.670  (* record_eq_simproc *)
   1.671  (* looks up the most specific record-equality.
   1.672   * Note on efficiency:
   1.673 @@ -1467,28 +1513,6 @@
   1.674                  i st)) (st,((length params) - 1) downto 0))
   1.675    end;
   1.676  
   1.677 -fun extension_typedef name repT alphas thy =
   1.678 -  let
   1.679 -    fun get_thms thy name =
   1.680 -      let
   1.681 -        val SOME { Abs_induct = abs_induct,
   1.682 -          Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
   1.683 -        val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
   1.684 -      in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
   1.685 -    val tname = Binding.name (Long_Name.base_name name);
   1.686 -  in
   1.687 -    thy
   1.688 -    |> Typecopy.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
   1.689 -    |-> (fn (name, _) => `(fn thy => get_thms thy name))
   1.690 -  end;
   1.691 -
   1.692 -fun mixit convs refls =
   1.693 -  let
   1.694 -    fun f ((res,lhs,rhs),refl) =
   1.695 -      ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
   1.696 -  in #1 (Library.foldl f (([],[],convs),refls)) end;
   1.697 -
   1.698 -
   1.699  fun extension_definition full name fields names alphas zeta moreT more vars thy =
   1.700    let
   1.701      val base = Long_Name.base_name;
   1.702 @@ -1498,7 +1522,6 @@
   1.703      val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
   1.704      val extT_name = suffix ext_typeN name
   1.705      val extT = Type (extT_name, alphas_zetaTs);
   1.706 -    val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
   1.707      val fields_more = fields@[(full moreN,moreT)];
   1.708      val fields_moreTs = fieldTs@[moreT];
   1.709      val bfields_more = map (apfst base) fields_more;
   1.710 @@ -1506,61 +1529,97 @@
   1.711      val len = length fields;
   1.712      val idxms = 0 upto len;
   1.713  
   1.714 +    (* before doing anything else, create the tree of new types
   1.715 +       that will back the record extension *)
   1.716 +    
   1.717 +    fun mktreeT [] = raise (TYPE ("mktreeT: empty list", [], []))
   1.718 +      | mktreeT [T] = T
   1.719 +      | mktreeT xs =
   1.720 +    let
   1.721 +      val len   = length xs;
   1.722 +      val half  = len div 2;
   1.723 +      val left  = List.take (xs, half);
   1.724 +      val right = List.drop (xs, half);
   1.725 +    in
   1.726 +      HOLogic.mk_prodT (mktreeT left, mktreeT right)
   1.727 +    end;
   1.728 +
   1.729 +    fun mktreeV [] = raise (TYPE ("mktreeV: empty list", [], []))
   1.730 +      | mktreeV [T] = T
   1.731 +      | mktreeV xs =
   1.732 +    let
   1.733 +      val len   = length xs;
   1.734 +      val half  = len div 2;
   1.735 +      val left  = List.take (xs, half);
   1.736 +      val right = List.drop (xs, half);
   1.737 +    in
   1.738 +      HOLogic.mk_prod (mktreeV left, mktreeV right)
   1.739 +    end;
   1.740 +
   1.741 +    fun mk_istuple ((thy, i), (left, rght)) =
   1.742 +    let
   1.743 +      val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
   1.744 +      val nm   = suffix suff (Sign.base_name name);
   1.745 +      val (cons, thy') = IsTupleSupport.add_istuple_type
   1.746 +               (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   1.747 +    in
   1.748 +      ((thy', i + 1), cons $ left $ rght)
   1.749 +    end;
   1.750 +
   1.751 +    (* trying to create a 1-element istuple will fail, and
   1.752 +       is pointless anyway *)
   1.753 +    fun mk_even_istuple ((thy, i), [arg]) =
   1.754 +        ((thy, i), arg)
   1.755 +      | mk_even_istuple ((thy, i), args) =
   1.756 +        mk_istuple ((thy, i), HOLogic.dest_prod (mktreeV args));
   1.757 +
   1.758 +    fun build_meta_tree_type i thy vars more =
   1.759 +    let
   1.760 +      val len   = length vars;
   1.761 +    in
   1.762 +      if len < 1
   1.763 +      then raise (TYPE ("meta_tree_type args too short", [], vars))
   1.764 +      else if len > 16
   1.765 +      then let
   1.766 +          fun group16 [] = []
   1.767 +            | group16 xs = Library.take (16, xs)
   1.768 +                             :: group16 (Library.drop (16, xs));
   1.769 +          val vars' = group16 vars;
   1.770 +          val ((thy', i'), composites) =
   1.771 +                   foldl_map mk_even_istuple ((thy, i), vars');
   1.772 +        in
   1.773 +          build_meta_tree_type i' thy' composites more
   1.774 +        end
   1.775 +      else let
   1.776 +          val ((thy', i'), term)
   1.777 +             = mk_istuple ((thy, 0), (mktreeV vars, more));
   1.778 +        in
   1.779 +          (term, thy')
   1.780 +        end
   1.781 +    end;
   1.782 +
   1.783 +    val _ = timing_msg "record extension preparing definitions";
   1.784 +
   1.785 +    (* 1st stage part 1: introduce the tree of new types *)
   1.786 +    fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
   1.787 +    val (ext_body, typ_thy) =
   1.788 +      timeit_msg "record extension nested type def:" get_meta_tree;
   1.789 +
   1.790      (* prepare declarations and definitions *)
   1.791  
   1.792      (*fields constructor*)
   1.793      val ext_decl = (mk_extC (name,extT) fields_moreTs);
   1.794 -    (*
   1.795 -    val ext_spec = Const ext_decl :==
   1.796 -         (foldr (uncurry lambda)
   1.797 -            (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more]))
   1.798 -    *)
   1.799 -    val ext_spec = list_comb (Const ext_decl,vars@[more]) :==
   1.800 -         (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])));
   1.801 +    val ext_spec = list_comb (Const ext_decl,vars@[more]) :== ext_body;
   1.802  
   1.803      fun mk_ext args = list_comb (Const ext_decl, args);
   1.804  
   1.805 -    (*destructors*)
   1.806 -    val _ = timing_msg "record extension preparing definitions";
   1.807 -    val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
   1.808 -
   1.809 -    fun mk_dest_spec (i, (c,T)) =
   1.810 -      let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r))
   1.811 -      in Const (mk_selC extT (suffix ext_dest c,T))
   1.812 -         :== (lambda r (if i=len then snds else HOLogic.mk_fst snds))
   1.813 -      end;
   1.814 -    val dest_specs =
   1.815 -      ListPair.map mk_dest_spec (idxms, fields_more);
   1.816 -
   1.817 -    (*updates*)
   1.818 -    val upd_decls = map (mk_updC updN extT) bfields_more;
   1.819 -    fun mk_upd_spec (c,T) =
   1.820 -      let
   1.821 -        val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$
   1.822 -                                                  (mk_sel r (suffix ext_dest n,nT))
   1.823 -                                     else (mk_sel r (suffix ext_dest n,nT)))
   1.824 -                       fields_more;
   1.825 -      in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r
   1.826 -          :== mk_ext args
   1.827 -      end;
   1.828 -    val upd_specs = map mk_upd_spec fields_more;
   1.829 -
   1.830 -    (* 1st stage: defs_thy *)
   1.831 +    (* 1st stage part 2: define the ext constant *)
   1.832      fun mk_defs () =
   1.833 -      thy
   1.834 -      |> extension_typedef name repT (alphas @ [zeta])
   1.835 -      ||> Sign.add_consts_i
   1.836 -            (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
   1.837 -      ||>> PureThy.add_defs false
   1.838 -            (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
   1.839 -      ||>> PureThy.add_defs false
   1.840 -            (map (Thm.no_attributes o apfst Binding.name) upd_specs)
   1.841 -      |-> (fn args as ((_, dest_defs), upd_defs) =>
   1.842 -          fold Code.add_default_eqn dest_defs
   1.843 -          #> fold Code.add_default_eqn upd_defs
   1.844 -          #> pair args);
   1.845 -    val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) =
   1.846 -      timeit_msg "record extension type/selector/update defs:" mk_defs;
   1.847 +      typ_thy
   1.848 +      |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
   1.849 +      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
   1.850 +    val ([ext_def], defs_thy) =
   1.851 +      timeit_msg "record extension constructor def:" mk_defs;
   1.852  
   1.853      (* prepare propositions *)
   1.854      val _ = timing_msg "record extension preparing propositions";
   1.855 @@ -1572,14 +1631,17 @@
   1.856      val w     = Free (wN, extT);
   1.857      val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
   1.858      val C = Free (Name.variant variants "C", HOLogic.boolT);
   1.859 +    val intros = IsTupleSupport.get_istuple_intros defs_thy;
   1.860 +    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
   1.861  
   1.862      val inject_prop =
   1.863        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
   1.864 -      in All (map dest_Free (vars_more@vars_more'))
   1.865 -          ((HOLogic.eq_const extT $
   1.866 -            mk_ext vars_more$mk_ext vars_more')
   1.867 -           ===
   1.868 -           foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
   1.869 +      in
   1.870 +        ((HOLogic.mk_conj (HOLogic.eq_const extT $
   1.871 +          mk_ext vars_more$mk_ext vars_more', HOLogic.true_const))
   1.872 +         ===
   1.873 +         foldr1 HOLogic.mk_conj
   1.874 +           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const]))
   1.875        end;
   1.876  
   1.877      val induct_prop =
   1.878 @@ -1590,22 +1652,6 @@
   1.879          (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C))
   1.880        ==> Trueprop C;
   1.881  
   1.882 -    (*destructors*)
   1.883 -    val dest_conv_props =
   1.884 -       map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
   1.885 -
   1.886 -    (*updates*)
   1.887 -    fun mk_upd_prop (i,(c,T)) =
   1.888 -      let val x' = Free (Name.variant variants (base c ^ "'"),T --> T)
   1.889 -          val args' = nth_map i  (K (x'$nth vars_more i)) vars_more
   1.890 -      in mk_upd updN c x' ext === mk_ext args'  end;
   1.891 -    val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   1.892 -
   1.893 -    val surjective_prop =
   1.894 -      let val args =
   1.895 -           map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more;
   1.896 -      in s === mk_ext args end;
   1.897 -
   1.898      val split_meta_prop =
   1.899        let val P = Free (Name.variant variants "P", extT-->Term.propT) in
   1.900          Logic.mk_equals
   1.901 @@ -1618,110 +1664,65 @@
   1.902        let val tac = simp_all_tac HOL_ss simps
   1.903        in fn prop => prove stndrd [] prop (K tac) end;
   1.904  
   1.905 -    fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop);
   1.906 +    fun inject_prf () =
   1.907 +      simplify HOL_ss (
   1.908 +        prove_standard [] inject_prop (fn prems =>
   1.909 +           EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   1.910 +                  REPEAT_DETERM (resolve_tac [refl_conj_eq] 1
   1.911 +                                  ORELSE intros_tac 1
   1.912 +                                  ORELSE resolve_tac [refl] 1)]));
   1.913 +
   1.914      val inject = timeit_msg "record extension inject proof:" inject_prf;
   1.915  
   1.916 +    (* We need a surjection property r = (| f = f r, g = g r ... |)
   1.917 +       to prove other theorems. We haven't given names to the accessors
   1.918 +       f, g etc yet however, so we generate an ext structure with
   1.919 +       free variables as all arguments and allow the introduction tactic to
   1.920 +       operate on it as far as it can. We then use standard to convert
   1.921 +       the free variables into unifiable variables and unify them with
   1.922 +       (roughly) the definition of the accessor. *)
   1.923 +    fun surject_prf () = let
   1.924 +        val cterm_ext = cterm_of defs_thy ext;
   1.925 +        val start     = named_cterm_instantiate [("y", cterm_ext)]
   1.926 +                              surject_assist_idE;
   1.927 +        val tactic1   = simp_tac (HOL_basic_ss addsimps [ext_def]) 1
   1.928 +                        THEN REPEAT_ALL_NEW intros_tac 1
   1.929 +        val tactic2   = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   1.930 +        val [halfway] = Seq.list_of (tactic1 start);
   1.931 +        val [surject] = Seq.list_of (tactic2 (standard halfway));
   1.932 +      in
   1.933 +        surject
   1.934 +      end;
   1.935 +    val surject = timeit_msg "record extension surjective proof:" surject_prf;
   1.936 +
   1.937 +    fun split_meta_prf () =
   1.938 +        prove_standard [] split_meta_prop (fn prems =>
   1.939 +         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   1.940 +                etac meta_allE 1, atac 1,
   1.941 +                rtac (prop_subst OF [surject]) 1,
   1.942 +                REPEAT (etac meta_allE 1), atac 1]);
   1.943 +    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   1.944 +
   1.945      fun induct_prf () =
   1.946        let val (assm, concl) = induct_prop
   1.947        in prove_standard [assm] concl (fn {prems, ...} =>
   1.948 -           EVERY [try_param_tac rN abs_induct 1,
   1.949 -                  simp_tac (HOL_ss addsimps [split_paired_all]) 1,
   1.950 -                  resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
   1.951 -      end;
   1.952 +           EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1,
   1.953 +                  resolve_tac prems 2,
   1.954 +                  asm_simp_tac HOL_ss 1]) end;
   1.955      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.956  
   1.957 -    fun cases_prf_opt () =
   1.958 -      let
   1.959 -        val (_$(Pvar$_)) = concl_of induct;
   1.960 -        val ind = cterm_instantiate
   1.961 -                    [(cterm_of defs_thy Pvar, cterm_of defs_thy
   1.962 -                            (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))]
   1.963 -                    induct;
   1.964 -        in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   1.965 -
   1.966 -    fun cases_prf_noopt () =
   1.967 -        prove_standard [] cases_prop (fn _ =>
   1.968 -         EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   1.969 -                try_param_tac rN induct 1,
   1.970 -                rtac impI 1,
   1.971 -                REPEAT (etac allE 1),
   1.972 -                etac mp 1,
   1.973 -                rtac refl 1])
   1.974 -
   1.975 -    val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt;
   1.976 -    val cases = timeit_msg "record extension cases proof:" cases_prf;
   1.977 -
   1.978 -    fun dest_convs_prf () = map (prove_simp false
   1.979 -                      ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
   1.980 -    val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
   1.981 -    fun dest_convs_standard_prf () = map standard dest_convs;
   1.982 -
   1.983 -    val dest_convs_standard =
   1.984 -        timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf;
   1.985 -
   1.986 -    fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs))
   1.987 -                                       upd_conv_props;
   1.988 -    fun upd_convs_prf_opt () =
   1.989 -      let
   1.990 -
   1.991 -        fun mkrefl (c,T) = Thm.reflexive
   1.992 -                    (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T)));
   1.993 -        val refls = map mkrefl fields_more;
   1.994 -        val dest_convs' = map mk_meta_eq dest_convs;
   1.995 -        val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
   1.996 -
   1.997 -        val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
   1.998 -
   1.999 -        fun mkthm (udef,(fld_refl,thms)) =
  1.1000 -          let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
  1.1001 -               (* (|N=N (|N=N,M=M,K=K,more=more|)
  1.1002 -                    M=M (|N=N,M=M,K=K,more=more|)
  1.1003 -                    K=K'
  1.1004 -                    more = more (|N=N,M=M,K=K,more=more|) =
  1.1005 -                  (|N=N,M=M,K=K',more=more|)
  1.1006 -                *)
  1.1007 -              val (_$(_$v$r)$_) = prop_of udef;
  1.1008 -              val (_$(v'$_)$_) = prop_of fld_refl;
  1.1009 -              val udef' = cterm_instantiate
  1.1010 -                            [(cterm_of defs_thy v,cterm_of defs_thy v'),
  1.1011 -                             (cterm_of defs_thy r,cterm_of defs_thy ext)] udef;
  1.1012 -          in  standard (Thm.transitive udef' bdyeq) end;
  1.1013 -      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' map_eqs)) end;
  1.1014 -
  1.1015 -    val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt;
  1.1016 -
  1.1017 -    val upd_convs =
  1.1018 -         timeit_msg "record extension upd_convs proof:" upd_convs_prf;
  1.1019 -
  1.1020 -    fun surjective_prf () =
  1.1021 -      prove_standard [] surjective_prop (fn _ =>
  1.1022 -          (EVERY [try_param_tac rN induct 1,
  1.1023 -                  simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1]));
  1.1024 -    val surjective = timeit_msg "record extension surjective proof:" surjective_prf;
  1.1025 -
  1.1026 -    fun split_meta_prf () =
  1.1027 -        prove_standard [] split_meta_prop (fn _ =>
  1.1028 -         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.1029 -                etac meta_allE 1, atac 1,
  1.1030 -                rtac (prop_subst OF [surjective]) 1,
  1.1031 -                REPEAT (etac meta_allE 1), atac 1]);
  1.1032 -    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
  1.1033 -
  1.1034 -
  1.1035 -    val (([inject',induct',cases',surjective',split_meta'],
  1.1036 +    val (([inject',induct',surjective',split_meta',ext_def'],
  1.1037            [dest_convs',upd_convs']),
  1.1038        thm_thy) =
  1.1039        defs_thy
  1.1040        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  1.1041             [("ext_inject", inject),
  1.1042              ("ext_induct", induct),
  1.1043 -            ("ext_cases", cases),
  1.1044              ("ext_surjective", surjective),
  1.1045 -            ("ext_split", split_meta)]
  1.1046 -      ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
  1.1047 -            [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
  1.1048 -
  1.1049 -  in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
  1.1050 +            ("ext_split", split_meta),
  1.1051 +            ("ext_def", ext_def)]
  1.1052 +
  1.1053 +  in (thm_thy,extT,induct',inject',split_meta',ext_def')
  1.1054    end;
  1.1055  
  1.1056  fun chunks []      []   = []
  1.1057 @@ -1826,7 +1827,7 @@
  1.1058      val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  1.1059  
  1.1060      (* 1st stage: extension_thy *)
  1.1061 -    val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) =
  1.1062 +    val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) =
  1.1063        thy
  1.1064        |> Sign.add_path bname
  1.1065        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  1.1066 @@ -1862,6 +1863,9 @@
  1.1067  
  1.1068      val r_rec0 = mk_rec all_vars_more 0;
  1.1069      val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  1.1070 +    val r_rec0_Vars = let
  1.1071 +        fun to_Var (Free (c, T)) = Var ((c, 0), T);
  1.1072 +      in mk_rec (map to_Var all_vars_more) 0 end;
  1.1073  
  1.1074      fun r n = Free (rN, rec_schemeT n)
  1.1075      val r0 = r 0;
  1.1076 @@ -1916,21 +1920,63 @@
  1.1077        [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  1.1078          (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
  1.1079  
  1.1080 +    val ext_defs = ext_def :: map #extdef parents;
  1.1081 +    val intros = IsTupleSupport.get_istuple_intros extension_thy;
  1.1082 +    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
  1.1083 +
  1.1084 +    (* Theorems from the istuple intros.
  1.1085 +       This is complex enough to deserve a full comment.
  1.1086 +       By unfolding ext_defs from r_rec0 we create a tree of constructor
  1.1087 +       calls (many of them Pair, but others as well). The introduction
  1.1088 +       rules for update_accessor_eq_assist can unify two different ways
  1.1089 +       on these constructors. If we take the complete result sequence of
  1.1090 +       running a the introduction tactic, we get one theorem for each upd/acc
  1.1091 +       pair, from which we can derive the bodies of our selector and
  1.1092 +       updator and their convs. *)
  1.1093 +    fun get_access_update_thms () = let
  1.1094 +        val cterm_rec = cterm_of extension_thy r_rec0;
  1.1095 +        val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
  1.1096 +        val insts     = [("v", cterm_rec), ("v'", cterm_vrs)];
  1.1097 +        val init_thm  = named_cterm_instantiate insts updacc_eq_triv;
  1.1098 +        val terminal  = rtac updacc_eq_idI 1 THEN rtac refl 1;
  1.1099 +        val tactic    = simp_tac (HOL_basic_ss addsimps ext_defs) 1
  1.1100 +                        THEN REPEAT (intros_tac 1 ORELSE terminal);
  1.1101 +        val updaccs   = Seq.list_of (tactic init_thm);
  1.1102 +      in
  1.1103 +        (updaccs RL [updacc_accessor_eqE],
  1.1104 +         updaccs RL [updacc_updator_eqE],
  1.1105 +         updaccs RL [updacc_cong_from_eq])
  1.1106 +      end;
  1.1107 +    val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  1.1108 +       timeit_msg "record getting tree access/updates:" get_access_update_thms;
  1.1109 +
  1.1110 +    fun lastN xs = List.drop (xs, parent_fields_len);
  1.1111 +
  1.1112      (*selectors*)
  1.1113 -    fun mk_sel_spec (c,T) =
  1.1114 -         Const (mk_selC rec_schemeT0 (c,T))
  1.1115 -          :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
  1.1116 -    val sel_specs = map mk_sel_spec fields_more;
  1.1117 +    fun mk_sel_spec ((c,T), thm) =
  1.1118 +      let
  1.1119 +        val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1.1120 +                               o Envir.beta_eta_contract o concl_of) thm;
  1.1121 +        val _ = if (arg aconv r_rec0) then ()
  1.1122 +                else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.1123 +      in
  1.1124 +        Const (mk_selC rec_schemeT0 (c,T))
  1.1125 +          :== acc
  1.1126 +      end;
  1.1127 +    val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  1.1128  
  1.1129      (*updates*)
  1.1130  
  1.1131 -    fun mk_upd_spec (c,T) =
  1.1132 +    fun mk_upd_spec ((c,T), thm) =
  1.1133        let
  1.1134 -        val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*);
  1.1135 -      in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0
  1.1136 -          :== (parent_more_upd new r0)
  1.1137 +        val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1.1138 +                                   o Envir.beta_eta_contract o concl_of) thm;
  1.1139 +        val _ = if (arg aconv r_rec0) then ()
  1.1140 +                else raise TERM ("mk_sel_spec: different arg", [arg]);
  1.1141 +      in Const (mk_updC updateN rec_schemeT0 (c,T))
  1.1142 +          :== upd
  1.1143        end;
  1.1144 -    val upd_specs = map mk_upd_spec fields_more;
  1.1145 +    val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  1.1146  
  1.1147      (*derived operations*)
  1.1148      val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  1.1149 @@ -2052,16 +2098,26 @@
  1.1150      val ss = get_simpset defs_thy;
  1.1151  
  1.1152      fun sel_convs_prf () = map (prove_simp false ss
  1.1153 -                           (sel_defs@ext_dest_convs)) sel_conv_props;
  1.1154 +                           (sel_defs@accessor_thms)) sel_conv_props;
  1.1155      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  1.1156      fun sel_convs_standard_prf () = map standard sel_convs
  1.1157      val sel_convs_standard =
  1.1158            timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  1.1159  
  1.1160 -    fun upd_convs_prf () =
  1.1161 -          map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props;
  1.1162 -
  1.1163 +    fun upd_convs_prf () = map (prove_simp false ss
  1.1164 +                           (upd_defs@updator_thms)) upd_conv_props;
  1.1165      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  1.1166 +    fun upd_convs_standard_prf () = map standard upd_convs
  1.1167 +    val upd_convs_standard =
  1.1168 +          timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  1.1169 +
  1.1170 +    fun get_upd_acc_congs () = let
  1.1171 +        val symdefs  = map symmetric (sel_defs @ upd_defs);
  1.1172 +        val fold_ss  = HOL_basic_ss addsimps symdefs;
  1.1173 +        val ua_congs = map (simplify fold_ss) upd_acc_cong_assists;
  1.1174 +      in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
  1.1175 +    val (fold_congs, unfold_congs) =
  1.1176 +          timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  1.1177  
  1.1178      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  1.1179  
  1.1180 @@ -2114,14 +2170,31 @@
  1.1181          THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  1.1182      val cases = timeit_msg "record cases proof:" cases_prf;
  1.1183  
  1.1184 +    fun surjective_prf () = let
  1.1185 +        val o_ass_thm = symmetric (mk_meta_eq o_assoc);
  1.1186 +        val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]);
  1.1187 +        val sel_defs' = map o_reassoc sel_defs;
  1.1188 +        val ss        = HOL_basic_ss addsimps (ext_defs @ sel_defs');
  1.1189 +      in
  1.1190 +        prove_standard [] surjective_prop (fn prems =>
  1.1191 +            (EVERY [rtac surject_assist_idE 1,
  1.1192 +                    simp_tac ss 1,
  1.1193 +                    REPEAT (intros_tac 1 ORELSE
  1.1194 +                            (rtac surject_assistI 1 THEN
  1.1195 +                             simp_tac (HOL_basic_ss addsimps id_o_apps) 1))]))
  1.1196 +      end;
  1.1197 +    val surjective = timeit_msg "record surjective proof:" surjective_prf;
  1.1198 +
  1.1199      fun split_meta_prf () =
  1.1200 -        prove false [] split_meta_prop (fn _ =>
  1.1201 +        prove false [] split_meta_prop (fn prems =>
  1.1202           EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1.1203                  etac meta_allE 1, atac 1,
  1.1204                  rtac (prop_subst OF [surjective]) 1,
  1.1205                  REPEAT (etac meta_allE 1), atac 1]);
  1.1206      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  1.1207 -    val split_meta_standard = standard split_meta;
  1.1208 +    fun split_meta_standardise () = standard split_meta;
  1.1209 +    val split_meta_standard = timeit_msg "record split_meta standard:"
  1.1210 +        split_meta_standardise;
  1.1211  
  1.1212      fun split_object_prf_opt () =
  1.1213        let
  1.1214 @@ -2155,16 +2228,16 @@
  1.1215  
  1.1216  
  1.1217      fun split_ex_prf () =
  1.1218 -        prove_standard [] split_ex_prop (fn _ =>
  1.1219 -          EVERY [rtac iffI 1,
  1.1220 -                   etac exE 1,
  1.1221 -                   simp_tac (HOL_basic_ss addsimps [split_meta_standard]) 1,
  1.1222 -                   ex_inst_tac 1,
  1.1223 -                   (*REPEAT (rtac exI 1),*)
  1.1224 -                   atac 1,
  1.1225 -                 REPEAT (etac exE 1),
  1.1226 -                 rtac exI 1,
  1.1227 -                 atac 1]);
  1.1228 +      let
  1.1229 +        val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
  1.1230 +        val [Pv] = term_vars (prop_of split_object);
  1.1231 +        val cPv  = cterm_of defs_thy Pv;
  1.1232 +        val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
  1.1233 +        val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
  1.1234 +        val so4  = simplify ss so3;
  1.1235 +      in
  1.1236 +        prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
  1.1237 +      end;
  1.1238      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  1.1239  
  1.1240      fun equality_tac thms =
  1.1241 @@ -2183,6 +2256,7 @@
  1.1242       val equality = timeit_msg "record equality proof:" equality_prf;
  1.1243  
  1.1244      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
  1.1245 +            fold_congs', unfold_congs', surjective',
  1.1246            [split_meta', split_object', split_ex'], derived_defs'],
  1.1247            [surjective', equality']),
  1.1248            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
  1.1249 @@ -2205,15 +2279,18 @@
  1.1250  
  1.1251  
  1.1252      val sel_upd_simps = sel_convs' @ upd_convs';
  1.1253 +    val sel_upd_defs = sel_defs' @ upd_defs';
  1.1254      val iffs = [ext_inject]
  1.1255 +    val depth = parent_len + 1;
  1.1256      val final_thy =
  1.1257        thms_thy
  1.1258        |> (snd oo PureThy.add_thmss)
  1.1259            [((Binding.name "simps", sel_upd_simps),
  1.1260              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
  1.1261             ((Binding.name "iffs", iffs), [iff_add])]
  1.1262 -      |> put_record name (make_record_info args parent fields extension induct_scheme')
  1.1263 -      |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
  1.1264 +      |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
  1.1265 +      |> put_sel_upd_names full_moreN depth sel_upd_simps
  1.1266 +                           sel_upd_defs (fold_congs', unfold_congs')
  1.1267        |> add_record_equalities extension_id equality'
  1.1268        |> add_extinjects ext_inject
  1.1269        |> add_extsplit extension_name ext_split