--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 15:58:01 1999 +0200
@@ -60,7 +60,7 @@
fun prove_casedist_thms new_type_names descr sorts induct thy =
let
- val _ = message "Proving case distinction theorems...";
+ val _ = message "Proving case distinction theorems ...";
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -99,7 +99,7 @@
fun prove_primrec_thms flat_names new_type_names descr sorts
(dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
let
- val _ = message "Constructing primrec combinators...";
+ val _ = message "Constructing primrec combinators ...";
val big_name = space_implode "_" new_type_names;
val thy0 = add_path flat_names big_name thy;
@@ -174,7 +174,7 @@
(* prove uniqueness and termination of primrec combinators *)
- val _ = message "Proving termination and uniqueness of primrec functions...";
+ val _ = message "Proving termination and uniqueness of primrec functions ...";
fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
let
@@ -263,7 +263,7 @@
(* prove characteristic equations for primrec combinators *)
- val _ = message "Proving characteristic theorems for primrec combinators..."
+ val _ = message "Proving characteristic theorems for primrec combinators ..."
val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
(cterm_of (Theory.sign_of thy2) t) (fn _ =>
@@ -284,7 +284,7 @@
fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = message "Proving characteristic theorems for case combinators...";
+ val _ = message "Proving characteristic theorems for case combinators ...";
val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
@@ -430,7 +430,7 @@
fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
casedist_thms case_thms thy =
let
- val _ = message "Proving equations for case splitting...";
+ val _ = message "Proving equations for case splitting ...";
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -466,7 +466,7 @@
fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = message "Proving equations for size function...";
+ val _ = message "Proving equations for size function ...";
val big_name = space_implode "_" new_type_names;
val thy1 = add_path flat_names big_name thy;
@@ -527,7 +527,7 @@
fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
let
- val _ = message "Proving additional theorems for TFL...";
+ val _ = message "Proving additional theorems for TFL ...";
fun prove_nchotomy (t, exhaustion) =
let
--- a/src/HOL/Tools/datatype_package.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Apr 14 15:58:01 1999 +0200
@@ -529,7 +529,7 @@
val sorts = add_term_tfrees (concl_of induction', []);
val dt_info = get_datatypes thy1;
- val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
+ val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val (thy2, casedist_thms) = thy1 |>
DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 15:58:01 1999 +0200
@@ -105,7 +105,7 @@
(************** generate introduction rules for representing set **********)
- val _ = message "Constructing representing sets...";
+ val _ = message "Constructing representing sets ...";
(* make introduction rule for a single constructor *)
@@ -215,7 +215,7 @@
(*********** isomorphisms for new types (introduced by typedef) ***********)
- val _ = message "Proving isomorphism properties...";
+ val _ = message "Proving isomorphism properties ...";
(* get axioms from theory *)
@@ -439,7 +439,7 @@
(******************* freeness theorems for constructors *******************)
- val _ = message "Proving freeness of constructors...";
+ val _ = message "Proving freeness of constructors ...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
@@ -491,7 +491,7 @@
(*************************** induction theorem ****************************)
- val _ = message "Proving induction rule for datatypes...";
+ val _ = message "Proving induction rule for datatypes ...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
(map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
--- a/src/HOL/Tools/inductive_package.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML Wed Apr 14 15:58:01 1999 +0200
@@ -238,7 +238,7 @@
fun prove_mono setT fp_fun monos thy =
let
- val _ = message " Proving monotonicity...";
+ val _ = message " Proving monotonicity ...";
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
@@ -252,7 +252,7 @@
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
let
- val _ = message " Proving the introduction rules...";
+ val _ = message " Proving the introduction rules ...";
val unfold = standard (mono RS (fp_def RS
(if coind then def_gfp_Tarski else def_lfp_Tarski)));
@@ -284,7 +284,7 @@
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
let
- val _ = message " Proving the elimination rules...";
+ val _ = message " Proving the elimination rules ...";
val rules1 = [CollectE, disjE, make_elim vimageD];
val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
@@ -335,7 +335,7 @@
fun prove_indrule cs cTs sumT rec_const params intr_ts mono
fp_def rec_sets_defs thy =
let
- val _ = message " Proving the induction rule...";
+ val _ = message " Proving the induction rule ...";
val sign = Theory.sign_of thy;
--- a/src/HOL/Tools/primrec_package.ML Wed Apr 14 14:44:04 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML Wed Apr 14 15:58:01 1999 +0200
@@ -8,6 +8,7 @@
signature PRIMREC_PACKAGE =
sig
+ val quiet_mode: bool ref
val add_primrec: string -> ((bstring * string) * Args.src list) list
-> theory -> theory * thm list
val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
@@ -23,7 +24,13 @@
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
fun primrec_eq_err sign s eq =
- primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
+ primrec_err (s ^ "\nin equation\n" ^ quote (Sign.string_of_term sign eq));
+
+
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
(* preprocessing of equations *)
@@ -101,7 +108,7 @@
val rest = drop (rpos, ts);
val (x, rs) = (hd rest, tl rest)
handle _ => raise RecError ("not enough arguments\
- \ in recursive application\nof function " ^ fname' ^ " on rhs")
+ \ in recursive application\nof function " ^ quote fname' ^ " on rhs")
in
(case assoc (subs, x) of
None =>
@@ -126,8 +133,8 @@
fun trans eqns ((cname, cargs), (fnames', fnss', fns)) =
(case assoc (eqns, cname) of
- None => (warning ("no equation for constructor " ^ cname ^
- "\nin definition of function " ^ fname);
+ None => (warning ("no equation for constructor " ^ quote cname ^
+ "\nin definition of function " ^ quote fname);
(fnames', fnss', (Const ("arbitrary", dummyT))::fns))
| Some (ls, cargs', rs, rhs, eq) =>
let
@@ -148,7 +155,7 @@
in (case assoc (fnames, i) of
None =>
if exists (equal fname o snd) fnames then
- raise RecError ("inconsistent functions for datatype " ^ tname)
+ raise RecError ("inconsistent functions for datatype " ^ quote tname)
else
let
val (_, _, eqns) = the (assoc (rec_eqns, fname));
@@ -159,7 +166,7 @@
end
| Some fname' =>
if fname = fname' then (fnames, fnss)
- else raise RecError ("inconsistent functions for datatype " ^ tname))
+ else raise RecError ("inconsistent functions for datatype " ^ quote tname))
end;
@@ -172,7 +179,7 @@
val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
replicate ((length cargs) + (length (filter is_rec_type cargs)))
dummyT ---> HOLogic.unitT)) constrs;
- val _ = warning ("no function definition for datatype " ^ tname)
+ val _ = warning ("No function definition for datatype " ^ quote tname)
in
(dummy_fns @ fs, defs)
end
@@ -197,7 +204,7 @@
fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname::tnames) =
(case Symtab.lookup (dt_info, tname) of
- None => primrec_err (tname ^ " is not a datatype")
+ None => primrec_err (quote tname ^ " is not a datatype")
| Some dt =>
if tnames' subset (map (#1 o snd) (#descr dt)) then
(tname, dt)::(find_dts dt_info tnames' tnames)
@@ -234,8 +241,7 @@
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive"));
val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
- val _ = writeln ("Proving equations for primrec function(s)\n" ^
- commas_quote names1 ^ " ...");
+ val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;
val simps = char_thms;