# HG changeset patch # User wenzelm # Date 1267397491 -3600 # Node ID 1ea89d2a1bd4cceb71406a4ae1d61cb51a34a6ea # Parent 5c5bb83f2bae8b5ca34b61820f3566aa5283be6e more antiquotations; diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Groebner_Basis.thy Sun Feb 28 23:51:31 2010 +0100 @@ -510,7 +510,7 @@ let val z = instantiate_cterm ([(zT,T)],[]) zr val eq = instantiate_cterm ([(eqT,T)],[]) geq - val th = Simplifier.rewrite (ss addsimps simp_thms) + val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply eq t) z))) in equal_elim (symmetric th) TrueI @@ -640,7 +640,7 @@ val comp_conv = (Simplifier.rewrite (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} - addsimps ths addsimps simp_thms + addsimps ths addsimps @{thms simp_thms} addsimprocs Numeral_Simprocs.field_cancel_numeral_factors addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Statespace/state_fun.ML Sun Feb 28 23:51:31 2010 +0100 @@ -76,7 +76,7 @@ val string_eq_simp_tac = simp_tac (HOL_basic_ss addsimps (@{thms list.inject} @ @{thms char.inject} - @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms) + @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}) addsimprocs [lazy_conj_simproc] addcongs [@{thm block_conj_cong}]) @@ -84,7 +84,7 @@ val lookup_ss = (HOL_basic_ss addsimps (@{thms list.inject} @ @{thms char.inject} - @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms + @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms} @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel}, @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}]) addsimprocs [lazy_conj_simproc] diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Sun Feb 28 23:51:31 2010 +0100 @@ -481,7 +481,7 @@ (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, REPEAT (rtac TrueI 1), - rewrite_goals_tac (mk_meta_eq choice_eq :: + rewrite_goals_tac (mk_meta_eq @{thm choice_eq} :: symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), rewrite_goals_tac (map symmetric range_eqs), REPEAT (EVERY diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Feb 28 23:51:31 2010 +0100 @@ -210,13 +210,13 @@ (map cert insts)) induct; val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts) (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1 - THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs)); + THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs)); in split_conj_thm (Skip_Proof.prove_global thy1 [] [] (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac)) end; - val rec_total_thms = map (fn r => r RS theI') rec_unique_thms; + val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms; (* define primrec combinators *) @@ -250,7 +250,7 @@ val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t (fn _ => EVERY [rewrite_goals_tac reccomb_defs, - rtac the1_equality 1, + rtac @{thm the1_equality} 1, resolve_tac rec_unique_thms 1, resolve_tac rec_intrs 1, REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])) diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Function/function.ML Sun Feb 28 23:51:31 2010 +0100 @@ -146,7 +146,7 @@ let val totality = Thm.close_derivation totality val remove_domain_condition = - full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) + full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Feb 28 23:51:31 2010 +0100 @@ -447,7 +447,8 @@ val initial_conv = Simplifier.rewrite (HOL_basic_ss addsimps nnf_simps - addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (ex_simps @ all_simps)); + addsimps [not_all, not_ex] + addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps})); val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); @@ -820,7 +821,7 @@ in make_simproc {lhss = [Thm.lhs_of idl_sub], name = "poly_eq_simproc", proc = proc, identifier = []} end; - val poly_eq_ss = HOL_basic_ss addsimps simp_thms + val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [poly_eq_simproc] local diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sun Feb 28 23:51:31 2010 +0100 @@ -60,7 +60,7 @@ (Simplifier.rewrite (HOL_basic_ss addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} - @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}, + @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}, @{thm add_number_of_left}, @{thm Suc_eq_plus1}] @ map (fn th => th RS sym) @{thms numerals})); @@ -632,9 +632,9 @@ end end; -val nat_arith = @{thms "nat_arith"}; -val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps}) - addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}]; +val nat_exp_ss = + HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) + addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]; fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Sun Feb 28 23:51:31 2010 +0100 @@ -16,7 +16,7 @@ exception COOPER of string * exn; fun simp_thms_conv ctxt = - Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms); + Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); val FWD = Drule.implies_elim_list; val true_tm = @{cterm "True"}; @@ -514,8 +514,8 @@ local val pcv = Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) - @ [not_all,all_not_ex, ex_disj_distrib])) + (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4) + @ [not_all, all_not_ex, @{thm ex_disj_distrib}])) val postcv = Simplifier.rewrite presburger_ss fun conv ctxt p = let val _ = () diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Sun Feb 28 23:51:31 2010 +0100 @@ -109,7 +109,7 @@ local val ss1 = comp_ss - addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] + addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, @{thm "zmult_int"}] @@ -120,7 +120,7 @@ @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}] addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] -val div_mod_ss = HOL_basic_ss addsimps simp_thms +val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms} @ map (symmetric o mk_meta_eq) [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/Qelim/qelim.ML Sun Feb 28 23:51:31 2010 +0100 @@ -55,9 +55,10 @@ (* Instantiation of some parameter for most common cases *) local -val pcv = Simplifier.rewrite - (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) - @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]); +val pcv = + Simplifier.rewrite + (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @ + [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}])); in fun standard_qelim_conv atcv ncv qcv p = gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/arith_data.ML Sun Feb 28 23:51:31 2010 +0100 @@ -120,7 +120,7 @@ in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; fun simplify_meta_eq rules = - let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules + let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end fun trans_tac NONE = all_tac diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Sun Feb 28 23:51:31 2010 +0100 @@ -42,7 +42,7 @@ val not_lessD = @{thm linorder_not_less} RS iffD1; val not_leD = @{thm linorder_not_le} RS iffD1; -fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI; +fun mk_Eq thm = thm RS @{thm Eq_FalseI} handle THM _ => thm RS @{thm Eq_TrueI}; val mk_Trueprop = HOLogic.mk_Trueprop; @@ -703,8 +703,8 @@ val nnf_simpset = empty_ss setmkeqTrue mk_eq_True setmksimps (mksimps mksimps_pairs) - addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, - not_all, not_ex, not_not] + addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, + @{thm de_Morgan_conj}, not_all, not_ex, not_not] fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset) in @@ -823,7 +823,7 @@ addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] (*abel_cancel helps it work in abstract algebraic domains*) addsimprocs Nat_Arith.nat_cancel_sums_add - addcongs [if_weak_cong], + addcongs [@{thm if_weak_cong}], number_of = number_of}) #> add_discrete_type @{type_name nat}; diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/meson.ML Sun Feb 28 23:51:31 2010 +0100 @@ -517,10 +517,10 @@ nnf_ss also includes the one-point simprocs, which are needed to avoid the various one-point theorems from generating junk clauses.*) val nnf_simps = - [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, - if_False, if_cancel, if_eq_cancel, cases_simp]; + [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True}, + @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}]; val nnf_extra_simps = - thms"split_ifs" @ ex_simps @ all_simps @ simp_thms; + @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms}; val nnf_ss = HOL_basic_ss addsimps nnf_extra_simps @@ -685,7 +685,7 @@ (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing double-negations.*) -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection]; +val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]; (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*) fun select_literal i cl = negate_head (make_last i cl); diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sun Feb 28 22:30:51 2010 +0100 +++ b/src/HOL/Tools/record.ML Sun Feb 28 23:51:31 2010 +0100 @@ -1416,7 +1416,7 @@ | name => (case get_equalities thy name of NONE => NONE - | SOME thm => SOME (thm RS Eq_TrueI))) + | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) | _ => NONE)); @@ -1462,7 +1462,7 @@ fun prove prop = prove_global true thy [] prop (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) - addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); + addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1); fun mkeq (lr, Teq, (sel, Tsel), x) i = if is_selector thy sel then