src/HOL/Tools/record_package.ML

 
 signature BASIC_RECORD_PACKAGE =
 sig
   val record_split_tac: int -> tactic
   val record_split_wrapper: string * wrapper
+  val record_split_name: string
 end;
 
 signature RECORD_PACKAGE =
 sig
   include BASIC_RECORD_PACKAGE

 
 val quiet_mode = ref false;
 fun message s = if ! quiet_mode then () else writeln s;
 
 
+(* attributes etc. *)        (* FIXME move to Provers *)
+
+fun add_iffs_global (thy, th) =
+  let
+    val ss = Simplifier.simpset_ref_of thy;
+    val cs = Classical.claset_ref_of thy;
+    val (cs', ss') = (! cs, ! ss) addIffs [Attribute.thm_of th];
+  in ss := ss'; cs := cs'; (thy, th) end;
+
+fun add_wrapper wrapper thy =
+  let val r = claset_ref_of thy
+  in r := ! r addSWrapper wrapper; thy end;
+
+
 (* definitions and equations *)
 
 infix 0 :== ===;
 
 val (op :==) = Logic.mk_defpair;

         (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
           (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
         handle ERROR => error ("The error(s) above occurred while trying to prove "
           ^ quote (Sign.string_of_term sign goal)));
   in prove end;
+
+fun simp simps =
+  let val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps)
+  in apfst (Simplifier.full_simplify ss) end;
 
 
 
 (*** syntax operations ***)
 

 
 structure RecordsArgs =
 struct
   val name = "HOL/records";
   type T =
-    record_info Symtab.table *				(*records*)
-      (thm Symtab.table * Simplifier.simpset);		(*field split rules*)
+    record_info Symtab.table *                          (*records*)
+      (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
 
   val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
   val prep_ext = I;
   fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
     (Symtab.merge (K true) (recs1, recs2),

   in
     if exists is_fieldT params then Simplifier.full_simp_tac ss i st
     else Seq.empty
   end handle Library.LIST _ => Seq.empty;
 
-val record_split_wrapper = ("record_split_tac", fn tac => record_split_tac ORELSE' tac);
+val record_split_name = "record_split_tac";
+val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
 
 
 
 (** internal theory extenders **)
 
 (* field_type_defs *)
 
-fun field_type_def ((thy, simps), (name, tname, vs, T, U)) =
+fun field_type_def ((thy, simps, injects), (name, tname, vs, T, U)) =
   let
     val full = Sign.full_name (sign_of thy);
-    val (thy', {simps = simps', ...}) =
+    val (thy', {simps = simps', inject, ...}) =
       thy
       |> setmp DatatypePackage.quiet_mode true
         (DatatypePackage.add_datatype_i true [tname]
           [(vs, tname, Syntax.NoSyn, [(name, [T, U], Syntax.NoSyn)])]);
     val thy'' =
       thy'
       |> setmp AxClass.quiet_mode true
         (AxClass.add_inst_arity_i (full tname, [HOLogic.termS, moreS], moreS) [] [] None);
-  in (thy'', simps' @ simps) end;
-
-fun field_type_defs args thy = foldl field_type_def ((thy, []), args);
+  in (thy'', simps' @ simps, flat inject @ injects) end;
+
+fun field_type_defs args thy = foldl field_type_def ((thy, [], []), args);
 
 
 (* field_definitions *)
 
 fun field_definitions fields names zeta moreT more vars named_vars thy =

     val surj_props = map mk_surj_prop fields;
 
 
     (* 1st stage: types_thy *)
 
-    val (types_thy, simps) =
+    val (types_thy, simps, raw_injects) =
       thy
       |> field_type_defs fieldT_specs;
 
     val datatype_simps = map Attribute.tthm_of simps;
 

          (field_specs @ dest_specs);
 
     val field_defs = get_defs defs_thy field_specs;
     val dest_defs = get_defs defs_thy dest_specs;
 
+    val injects = map (simp (map (apfst Thm.symmetric) field_defs))
+      (map Attribute.tthm_of raw_injects);
+
 
     (* 3rd stage: thms_thy *)
 
     val prove = prove_simp defs_thy;
 
     val dest_convs = map (prove [] (field_defs @ dest_defs @ datatype_simps)) dest_props;
     val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
       (map (apfst Thm.symmetric) field_defs @ dest_convs)) surj_props;
 
-    fun mk_split th = SplitPairedAll.rule (standard (th RS eq_reflection));
+    fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
     val splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
 
     val thms_thy =
       defs_thy
       |> (PureThy.add_tthmss o map Attribute.none)

           ("dest_defs", dest_defs),
           ("dest_convs", dest_convs),
           ("surj_pairs", surj_pairs),
           ("splits", splits)];
 
-  in (thms_thy, dest_convs, splits) end;
+  in (thms_thy, dest_convs, injects, splits) end;
 
 
 (* record_definition *)
 
 fun record_definition (args, bname) parent (parents: parent_info list) bfields thy =

         in [more_part_update rec_scheme more' === mk_record (all_named_vars, more')] end;
 
 
     (* 1st stage: fields_thy *)
 
-    val (fields_thy, field_simps, splits) =
+    val (fields_thy, field_simps, field_injects, splits) =
       thy
       |> Theory.add_path bname
       |> field_definitions fields names zeta moreT more vars named_vars;
 
     val field_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, splits);

         [("select_defs", sel_defs),
           ("update_defs", update_defs),
           ("make_defs", make_defs),
           ("select_convs", sel_convs),
           ("update_convs", update_convs)]
-      |> PureThy.add_tthmss [(("simps", simps), [Simplifier.simp_add_global])];
+      |> PureThy.add_tthmss
+        [(("simps", simps), [Simplifier.simp_add_global]),
+         (("injects", field_injects), [add_iffs_global])];
 
 
     (* 4th stage: final_thy *)
 
     val final_thy =

 
 
 
 (** setup theory **)
 
-fun add_wrapper wrapper thy =
-  let val r = claset_ref_of thy
-  in r := ! r addSWrapper wrapper; thy end;
-
 val setup =
  [RecordsData.init,
   Theory.add_trfuns ([], parse_translation, [], []),
   add_wrapper record_split_wrapper];