# HG changeset patch # User wenzelm # Date 924098281 -7200 # Node ID fd36b2e7d80ea0c12511e1ae9e462587991b1f14 # Parent 9a2ace82b68eb7cd6c09e97b963b6539f7c8ab5b tuned messages; diff -r 9a2ace82b68e -r fd36b2e7d80e src/HOL/Tools/datatype_abs_proofs.ML --- 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 diff -r 9a2ace82b68e -r fd36b2e7d80e src/HOL/Tools/datatype_package.ML --- 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; diff -r 9a2ace82b68e -r fd36b2e7d80e src/HOL/Tools/datatype_rep_proofs.ML --- 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))); diff -r 9a2ace82b68e -r fd36b2e7d80e src/HOL/Tools/inductive_package.ML --- 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; diff -r 9a2ace82b68e -r fd36b2e7d80e src/HOL/Tools/primrec_package.ML --- 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;