src/HOL/Tools/record.ML

 (* theory data *)
 
 type record_data =
  {records: record_info Symtab.table,
   sel_upd:
-   {selectors: unit Symtab.table,
+   {selectors: (int * bool) Symtab.table,
     updates: string Symtab.table,
-    simpset: Simplifier.simpset},
+    simpset: Simplifier.simpset,
+    defset: Simplifier.simpset,
+    foldcong: Simplifier.simpset,
+    unfoldcong: Simplifier.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,    (* !!,!,EX - split-equalities,induct rule *)
   extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)

     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 simps = RecordsData.map (fn {records,
-  sel_upd = {selectors, updates, simpset},
-    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
-  make_record_data records
-    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
-      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
-      simpset = Simplifier.addsimps (simpset, simps)}
-      equalities extinjects extsplit splits extfields fieldext);
-
+fun put_sel_upd names more depth simps defs (folds, unfolds) 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, foldcong, unfoldcong},
+      equalities, extinjects, extsplit, splits, extfields,
+      fieldext} = RecordsData.get thy;
+    val data = make_record_data records
+      {selectors = fold Symtab.update_new sels selectors,
+        updates = fold Symtab.update_new upds updates,
+        simpset = Simplifier.addsimps (simpset, simps),
+        defset = Simplifier.addsimps (defset, defs),
+        foldcong = foldcong addcongs folds,
+        unfoldcong = unfoldcong addcongs unfolds}
+       equalities extinjects extsplit splits extfields fieldext;
+  in RecordsData.put data thy end;
 
 (* access 'equalities' *)
 
 fun add_record_equalities name thm thy =
   let

   | get_updfuns _             = [];
 
 fun get_accupd_simps thy term defset intros_tac = let
     val (acc, [body]) = strip_comb term;
     val recT          = domain_type (fastype_of acc);
-    val updfuns       = sort_distinct Term.fast_term_ord
+    val updfuns       = sort_distinct TermOrd.fast_term_ord
                            (get_updfuns body);
     fun get_simp upd  = let
         val T    = domain_type (fastype_of upd);
         val lhs  = mk_comp acc (upd $ Free ("f", T));
         val rhs  = if is_sel_upd_pair thy acc upd

         val dest = if is_sel_upd_pair thy acc upd
                    then o_eq_dest else o_eq_id_dest;
       in standard (othm RS dest) end;
   in map get_simp updfuns end;
 
-structure SymSymTab = TableFun(type key = string * string
-                                val ord = prod_ord fast_string_ord fast_string_ord);
+structure SymSymTab = Table(type key = string * string
+                            val ord = prod_ord fast_string_ord fast_string_ord);
 
 fun get_updupd_simp thy defset intros_tac u u' comp = let
     val f    = Free ("f", domain_type (fastype_of u));
     val f'   = Free ("f'", domain_type (fastype_of u'));
     val lhs  = mk_comp (u $ f) (u' $ f');

   in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
 
 fun named_cterm_instantiate values thm = let
     fun match name (Var ((name', _), _)) = name = name'
       | match name _ = false;
-    fun getvar name = case (find_first (match name) (term_vars (prop_of thm)))
+    fun getvar name = case (find_first (match name)
+                                    (OldTerm.term_vars (prop_of thm)))
       of SOME var => cterm_of (theory_of_thm thm) var
        | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
   in
     cterm_instantiate (map (apfst getvar) values) thm
   end;

                 | mk_eq_terms r = NONE
             in
               (case mk_eq_terms (upd$k$r) of
                  SOME (trm,trm',vars)
                  => SOME (prove_unfold_defs thy ss domS [] []
-                             (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
+                             (list_all(vars,(Logic.mk_equals (sel$trm, trm')))))
                | NONE => NONE)
             end
           | NONE => NONE)
         else NONE
       | _ => NONE));

          *  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 (Sign.base_name s) (domain_type T)
+            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 ("Fun.comp", funT --> funT --> funT) $ f $ f';

                   = mk_updterm upds Symtab.empty base;
         val noops' = flat (map snd (Symtab.dest noops));
       in
         if simp then
            SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
-                             (list_all(vars,(equals baseT$lhs$rhs))))
+                             (list_all(vars,(Logic.mk_equals (lhs, rhs)))))
         else NONE
       end)
 
 end
 

     end;
 
     fun mk_istuple ((thy, i), (left, rght)) =
     let
       val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
-      val nm   = suffix suff (Sign.base_name name);
+      val nm   = suffix suff (Long_Name.base_name name);
       val (cons, thy') = IsTupleSupport.add_istuple_type
                (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
     in
       ((thy', i + 1), cons $ left $ rght)
     end;

           fun group16 [] = []
             | group16 xs = Library.take (16, xs)
                              :: group16 (Library.drop (16, xs));
           val vars' = group16 vars;
           val ((thy', i'), composites) =
-                   foldl_map mk_even_istuple ((thy, i), vars');
+                   Library.foldl_map mk_even_istuple ((thy, i), vars');
         in
           build_meta_tree_type i' thy' composites more
         end
       else let
           val ((thy', i'), term)

            EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1,
                   resolve_tac prems 2,
                   asm_simp_tac HOL_ss 1]) end;
     val induct = timeit_msg "record extension induct proof:" induct_prf;
 
-    val (([inject',induct',surjective',split_meta',ext_def'],
-          [dest_convs',upd_convs']),
+    val ([inject',induct',surjective',split_meta',ext_def'],
       thm_thy) =
       defs_thy
       |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
            [("ext_inject", inject),
             ("ext_induct", induct),
-            ("ext_surjective", surjective),
+            ("ext_surjective", surject),
             ("ext_split", split_meta),
             ("ext_def", ext_def)]
 
   in (thm_thy,extT,induct',inject',split_meta',ext_def')
   end;

           timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
 
     fun get_upd_acc_congs () = let
         val symdefs  = map symmetric (sel_defs @ upd_defs);
         val fold_ss  = HOL_basic_ss addsimps symdefs;
-        val ua_congs = map (simplify fold_ss) upd_acc_cong_assists;
+        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
     val (fold_congs, unfold_congs) =
           timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
 
     val parent_induct = if null parents then [] else [#induct (hd (rev parents))];

           try_param_tac rN induct_scheme 1
           THEN try_param_tac "more" @{thm unit.induct} 1
           THEN resolve_tac prems 1)
       end;
     val induct = timeit_msg "record induct proof:" induct_prf;
-
-    fun surjective_prf () =
-      prove_standard [] surjective_prop (fn prems =>
-          (EVERY [try_param_tac rN induct_scheme 1,
-                  simp_tac (ss addsimps sel_convs_standard) 1]))
-    val surjective = timeit_msg "record surjective proof:" surjective_prf;
 
     fun cases_scheme_prf_opt () =
       let
         val (_$(Pvar$_)) = concl_of induct_scheme;
         val ind = cterm_instantiate

         try_param_tac rN cases_scheme 1
         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
     val cases = timeit_msg "record cases proof:" cases_prf;
 
     fun surjective_prf () = let
-        val o_ass_thm = symmetric (mk_meta_eq o_assoc);
-        val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]);
-        val sel_defs' = map o_reassoc sel_defs;
-        val ss        = HOL_basic_ss addsimps (ext_defs @ sel_defs');
+        val leaf_ss   = get_sel_upd_defs defs_thy
+                                addsimps (sel_defs @ (o_assoc :: id_o_apps));
+        val init_ss   = HOL_basic_ss addsimps ext_defs;
       in
         prove_standard [] surjective_prop (fn prems =>
             (EVERY [rtac surject_assist_idE 1,
-                    simp_tac ss 1,
+                    simp_tac init_ss 1,
                     REPEAT (intros_tac 1 ORELSE
                             (rtac surject_assistI 1 THEN
-                             simp_tac (HOL_basic_ss addsimps id_o_apps) 1))]))
+                             simp_tac leaf_ss 1))]))
       end;
     val surjective = timeit_msg "record surjective proof:" surjective_prf;
 
     fun split_meta_prf () =
         prove false [] split_meta_prop (fn prems =>

 
 
     fun split_ex_prf () =
       let
         val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
-        val [Pv] = term_vars (prop_of split_object);
+        val [Pv] = OldTerm.term_vars (prop_of split_object);
         val cPv  = cterm_of defs_thy Pv;
         val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
         val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
         val so4  = simplify ss so3;
       in

              (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
       end);
      val equality = timeit_msg "record equality proof:" equality_prf;
 
     val ((([sel_convs', upd_convs', sel_defs', upd_defs',
-            fold_congs', unfold_congs', surjective',
+            fold_congs', unfold_congs',
           [split_meta', split_object', split_ex'], derived_defs'],
           [surjective', equality']),
           [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
       defs_thy
       |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
          [("select_convs", sel_convs_standard),
-          ("update_convs", upd_convs),
+          ("update_convs", upd_convs_standard),
           ("select_defs", sel_defs),
           ("update_defs", upd_defs),
+          ("fold_congs", fold_congs),
+          ("unfold_congs", unfold_congs),
           ("splits", [split_meta_standard,split_object,split_ex]),
           ("defs", derived_defs)]
       ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
           [("surjective", surjective),
            ("equality", equality)]

       |> (snd oo PureThy.add_thmss)
           [((Binding.name "simps", sel_upd_simps),
             [Simplifier.simp_add, Nitpick_Const_Simps.add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
-      |> put_sel_upd_names full_moreN depth sel_upd_simps
+      |> put_sel_upd names full_moreN depth sel_upd_simps
                            sel_upd_defs (fold_congs', unfold_congs')
       |> add_record_equalities extension_id equality'
       |> add_extinjects ext_inject
       |> add_extsplit extension_name ext_split
       |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')