--- a/src/HOL/Tools/record_package.ML Wed Oct 21 16:34:18 1998 +0200
+++ b/src/HOL/Tools/record_package.ML Wed Oct 21 16:38:46 1998 +0200
@@ -8,8 +8,8 @@
signature BASIC_RECORD_PACKAGE =
sig
val record_split_tac: int -> tactic
+ val record_split_name: string
val record_split_wrapper: string * wrapper
- val record_split_name: string
end;
signature RECORD_PACKAGE =
@@ -57,7 +57,7 @@
in ss := ss'; cs := cs'; (thy, th) end;
fun add_wrapper wrapper thy =
- let val r = claset_ref_of thy
+ let val r = Classical.claset_ref_of thy
in r := ! r addSWrapper wrapper; thy end;
@@ -86,10 +86,6 @@
^ 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 ***)
@@ -114,6 +110,14 @@
(** generic operations **)
+(* adhoc priming of vars *)
+
+fun prime (Free (x, T)) = Free (x ^ "'", T)
+ | prime t = raise TERM ("prime: no free variable", [t]);
+
+
+(* product case *)
+
fun fst_fn T U = Abs ("x", T, Abs ("y", U, Bound 1));
fun snd_fn T U = Abs ("x", T, Abs ("y", U, Bound 0));
@@ -439,10 +443,10 @@
(* field_type_defs *)
-fun field_type_def ((thy, simps, injects), (name, tname, vs, T, U)) =
+fun field_type_def ((thy, simps), (name, tname, vs, T, U)) =
let
val full = Sign.full_name (sign_of thy);
- val (thy', {simps = simps', inject, ...}) =
+ val (thy', {simps = simps', ...}) =
thy
|> setmp DatatypePackage.quiet_mode true
(DatatypePackage.add_datatype_i true [tname]
@@ -451,9 +455,9 @@
thy'
|> setmp AxClass.quiet_mode true
(AxClass.add_inst_arity_i (full tname, [HOLogic.termS, moreS], moreS) [] [] None);
- in (thy'', simps' @ simps, flat inject @ injects) end;
+ in (thy'', simps' @ simps) end;
-fun field_type_defs args thy = foldl field_type_def ((thy, [], []), args);
+fun field_type_defs args thy = foldl field_type_def ((thy, []), args);
(* field_definitions *)
@@ -493,6 +497,12 @@
(* prepare theorems *)
+ (*constructor injects*)
+ fun mk_inject_prop (c, v) =
+ HOLogic.mk_eq (mk_field ((c, v), more), mk_field ((c, prime v), prime more)) ===
+ (HOLogic.conj $ HOLogic.mk_eq (v, prime v) $ HOLogic.mk_eq (more, prime more));
+ val inject_props = map mk_inject_prop named_vars;
+
(*destructor conversions*)
fun mk_dest_prop dest dest' (c, v) =
dest (mk_field ((c, v), more)) === dest' (v, more);
@@ -509,7 +519,7 @@
(* 1st stage: types_thy *)
- val (types_thy, simps, raw_injects) =
+ val (types_thy, simps) =
thy
|> field_type_defs fieldT_specs;
@@ -528,20 +538,19 @@
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 prove_std = prove [] (field_defs @ dest_defs @ datatype_simps);
- val dest_convs = map (prove [] (field_defs @ dest_defs @ datatype_simps)) dest_props;
+ val field_injects = map prove_std inject_props;
+ val dest_convs = map prove_std 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 (th RS eq_reflection);
- val splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
+ val field_splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
val thms_thy =
defs_thy
@@ -550,9 +559,9 @@
("dest_defs", dest_defs),
("dest_convs", dest_convs),
("surj_pairs", surj_pairs),
- ("splits", splits)];
+ ("field_splits", field_splits)];
- in (thms_thy, dest_convs, injects, splits) end;
+ in (thms_thy, dest_convs, field_injects, field_splits) end;
(* record_definition *)
@@ -678,12 +687,12 @@
(* 1st stage: fields_thy *)
- val (fields_thy, field_simps, field_injects, splits) =
+ val (fields_thy, field_simps, field_injects, field_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);
+ val named_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, field_splits);
(* 2nd stage: defs_thy *)
@@ -725,7 +734,7 @@
("update_convs", update_convs)]
|> PureThy.add_tthmss
[(("simps", simps), [Simplifier.simp_add_global]),
- (("injects", field_injects), [add_iffs_global])];
+ (("iffs", field_injects), [add_iffs_global])];
(* 4th stage: final_thy *)
@@ -733,7 +742,7 @@
val final_thy =
thms_thy
|> put_record name {args = args, parent = parent, fields = fields, simps = simps}
- |> add_record_splits field_splits
+ |> add_record_splits named_splits
|> Theory.parent_path;
in final_thy end;