more antiquotations;
authorwenzelm
Sun Feb 28 23:51:31 2010 +0100 (2010-02-28)
changeset 354101ea89d2a1bd4
parent 35409 5c5bb83f2bae
child 35411 cafb74a131da
more antiquotations;
src/HOL/Groebner_Basis.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Feb 28 22:30:51 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Feb 28 23:51:31 2010 +0100
     1.3 @@ -510,7 +510,7 @@
     1.4      let
     1.5        val z = instantiate_cterm ([(zT,T)],[]) zr
     1.6        val eq = instantiate_cterm ([(eqT,T)],[]) geq
     1.7 -      val th = Simplifier.rewrite (ss addsimps simp_thms)
     1.8 +      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
     1.9             (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
    1.10                    (Thm.capply (Thm.capply eq t) z)))
    1.11      in equal_elim (symmetric th) TrueI
    1.12 @@ -640,7 +640,7 @@
    1.13  
    1.14  val comp_conv = (Simplifier.rewrite
    1.15  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
    1.16 -              addsimps ths addsimps simp_thms
    1.17 +              addsimps ths addsimps @{thms simp_thms}
    1.18                addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
    1.19                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
    1.20                              ord_frac_simproc]
     2.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Feb 28 22:30:51 2010 +0100
     2.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Feb 28 23:51:31 2010 +0100
     2.3 @@ -76,7 +76,7 @@
     2.4  
     2.5  val string_eq_simp_tac = simp_tac (HOL_basic_ss 
     2.6    addsimps (@{thms list.inject} @ @{thms char.inject}
     2.7 -    @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms)
     2.8 +    @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
     2.9    addsimprocs [lazy_conj_simproc]
    2.10    addcongs [@{thm block_conj_cong}])
    2.11  
    2.12 @@ -84,7 +84,7 @@
    2.13  
    2.14  val lookup_ss = (HOL_basic_ss 
    2.15    addsimps (@{thms list.inject} @ @{thms char.inject}
    2.16 -    @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms
    2.17 +    @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}
    2.18      @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
    2.19        @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
    2.20    addsimprocs [lazy_conj_simproc]
     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 28 22:30:51 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Feb 28 23:51:31 2010 +0100
     3.3 @@ -481,7 +481,7 @@
     3.4          (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
     3.5             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     3.6              REPEAT (rtac TrueI 1),
     3.7 -            rewrite_goals_tac (mk_meta_eq choice_eq ::
     3.8 +            rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
     3.9                symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    3.10              rewrite_goals_tac (map symmetric range_eqs),
    3.11              REPEAT (EVERY
     4.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Feb 28 22:30:51 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Feb 28 23:51:31 2010 +0100
     4.3 @@ -210,13 +210,13 @@
     4.4            (map cert insts)) induct;
     4.5          val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
     4.6             (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
     4.7 -              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
     4.8 +              THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
     4.9  
    4.10        in split_conj_thm (Skip_Proof.prove_global thy1 [] []
    4.11          (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
    4.12        end;
    4.13  
    4.14 -    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
    4.15 +    val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
    4.16  
    4.17      (* define primrec combinators *)
    4.18  
    4.19 @@ -250,7 +250,7 @@
    4.20      val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
    4.21        (fn _ => EVERY
    4.22          [rewrite_goals_tac reccomb_defs,
    4.23 -         rtac the1_equality 1,
    4.24 +         rtac @{thm the1_equality} 1,
    4.25           resolve_tac rec_unique_thms 1,
    4.26           resolve_tac rec_intrs 1,
    4.27           REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
     5.1 --- a/src/HOL/Tools/Function/function.ML	Sun Feb 28 22:30:51 2010 +0100
     5.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Feb 28 23:51:31 2010 +0100
     5.3 @@ -146,7 +146,7 @@
     5.4          let
     5.5            val totality = Thm.close_derivation totality
     5.6            val remove_domain_condition =
     5.7 -            full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
     5.8 +            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
     5.9            val tsimps = map remove_domain_condition psimps
    5.10            val tinduct = map remove_domain_condition pinducts
    5.11  
     6.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Feb 28 22:30:51 2010 +0100
     6.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Feb 28 23:51:31 2010 +0100
     6.3 @@ -447,7 +447,8 @@
     6.4  val initial_conv =
     6.5      Simplifier.rewrite
     6.6       (HOL_basic_ss addsimps nnf_simps
     6.7 -     addsimps [not_all, not_ex] addsimps map (fn th => th RS sym) (ex_simps @ all_simps));
     6.8 +       addsimps [not_all, not_ex]
     6.9 +       addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}));
    6.10  
    6.11  val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    6.12  
    6.13 @@ -820,7 +821,7 @@
    6.14     in make_simproc {lhss = [Thm.lhs_of idl_sub], 
    6.15                  name = "poly_eq_simproc", proc = proc, identifier = []}
    6.16     end;
    6.17 -  val poly_eq_ss = HOL_basic_ss addsimps simp_thms 
    6.18 +  val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms}
    6.19                          addsimprocs [poly_eq_simproc]
    6.20  
    6.21   local
     7.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sun Feb 28 22:30:51 2010 +0100
     7.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sun Feb 28 23:51:31 2010 +0100
     7.3 @@ -60,7 +60,7 @@
     7.4    (Simplifier.rewrite 
     7.5      (HOL_basic_ss 
     7.6         addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
     7.7 -             @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc},
     7.8 +             @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
     7.9                   @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
    7.10               @ map (fn th => th RS sym) @{thms numerals}));
    7.11  
    7.12 @@ -632,9 +632,9 @@
    7.13   end
    7.14  end;
    7.15  
    7.16 -val nat_arith = @{thms "nat_arith"};
    7.17 -val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
    7.18 -                              addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
    7.19 +val nat_exp_ss =
    7.20 +  HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
    7.21 +    addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
    7.22  
    7.23  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
    7.24  
     8.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Feb 28 22:30:51 2010 +0100
     8.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Feb 28 23:51:31 2010 +0100
     8.3 @@ -16,7 +16,7 @@
     8.4  
     8.5  exception COOPER of string * exn;
     8.6  fun simp_thms_conv ctxt =
     8.7 -  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps simp_thms);
     8.8 +  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
     8.9  val FWD = Drule.implies_elim_list;
    8.10  
    8.11  val true_tm = @{cterm "True"};
    8.12 @@ -514,8 +514,8 @@
    8.13  
    8.14  local
    8.15   val pcv = Simplifier.rewrite
    8.16 -     (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
    8.17 -                      @ [not_all,all_not_ex, ex_disj_distrib]))
    8.18 +     (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
    8.19 +                      @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
    8.20   val postcv = Simplifier.rewrite presburger_ss
    8.21   fun conv ctxt p =
    8.22    let val _ = ()
     9.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sun Feb 28 22:30:51 2010 +0100
     9.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sun Feb 28 23:51:31 2010 +0100
     9.3 @@ -109,7 +109,7 @@
     9.4  
     9.5  local
     9.6  val ss1 = comp_ss
     9.7 -  addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
     9.8 +  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
     9.9        @ map (fn r => r RS sym) 
    9.10          [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
    9.11           @{thm "zmult_int"}]
    9.12 @@ -120,7 +120,7 @@
    9.13              @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
    9.14              @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
    9.15    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    9.16 -val div_mod_ss = HOL_basic_ss addsimps simp_thms 
    9.17 +val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
    9.18    @ map (symmetric o mk_meta_eq) 
    9.19      [@{thm "dvd_eq_mod_eq_0"},
    9.20       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    10.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sun Feb 28 22:30:51 2010 +0100
    10.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Feb 28 23:51:31 2010 +0100
    10.3 @@ -55,9 +55,10 @@
    10.4  (* Instantiation of some parameter for most common cases *)
    10.5  
    10.6  local
    10.7 -val pcv = Simplifier.rewrite
    10.8 -                 (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
    10.9 -                     @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]);
   10.10 +val pcv =
   10.11 +  Simplifier.rewrite
   10.12 +    (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @
   10.13 +        [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));
   10.14  
   10.15  in fun standard_qelim_conv atcv ncv qcv p =
   10.16        gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p
    11.1 --- a/src/HOL/Tools/arith_data.ML	Sun Feb 28 22:30:51 2010 +0100
    11.2 +++ b/src/HOL/Tools/arith_data.ML	Sun Feb 28 23:51:31 2010 +0100
    11.3 @@ -120,7 +120,7 @@
    11.4    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    11.5  
    11.6  fun simplify_meta_eq rules =
    11.7 -  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    11.8 +  let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules
    11.9    in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
   11.10  
   11.11  fun trans_tac NONE  = all_tac
    12.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Feb 28 22:30:51 2010 +0100
    12.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Feb 28 23:51:31 2010 +0100
    12.3 @@ -42,7 +42,7 @@
    12.4  val not_lessD = @{thm linorder_not_less} RS iffD1;
    12.5  val not_leD = @{thm linorder_not_le} RS iffD1;
    12.6  
    12.7 -fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
    12.8 +fun mk_Eq thm = thm RS @{thm Eq_FalseI} handle THM _ => thm RS @{thm Eq_TrueI};
    12.9  
   12.10  val mk_Trueprop = HOLogic.mk_Trueprop;
   12.11  
   12.12 @@ -703,8 +703,8 @@
   12.13    val nnf_simpset =
   12.14      empty_ss setmkeqTrue mk_eq_True
   12.15      setmksimps (mksimps mksimps_pairs)
   12.16 -    addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
   12.17 -      not_all, not_ex, not_not]
   12.18 +    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
   12.19 +      @{thm de_Morgan_conj}, not_all, not_ex, not_not]
   12.20    fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
   12.21  in
   12.22  
   12.23 @@ -823,7 +823,7 @@
   12.24        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   12.25         (*abel_cancel helps it work in abstract algebraic domains*)
   12.26        addsimprocs Nat_Arith.nat_cancel_sums_add
   12.27 -      addcongs [if_weak_cong],
   12.28 +      addcongs [@{thm if_weak_cong}],
   12.29      number_of = number_of}) #>
   12.30    add_discrete_type @{type_name nat};
   12.31  
    13.1 --- a/src/HOL/Tools/meson.ML	Sun Feb 28 22:30:51 2010 +0100
    13.2 +++ b/src/HOL/Tools/meson.ML	Sun Feb 28 23:51:31 2010 +0100
    13.3 @@ -517,10 +517,10 @@
    13.4    nnf_ss also includes the one-point simprocs,
    13.5    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    13.6  val nnf_simps =
    13.7 -     [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
    13.8 -      if_False, if_cancel, if_eq_cancel, cases_simp];
    13.9 +  [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm  Bex_def}, @{thm if_True},
   13.10 +    @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
   13.11  val nnf_extra_simps =
   13.12 -      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
   13.13 +  @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
   13.14  
   13.15  val nnf_ss =
   13.16    HOL_basic_ss addsimps nnf_extra_simps
   13.17 @@ -685,7 +685,7 @@
   13.18  
   13.19  (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   13.20    double-negations.*)
   13.21 -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   13.22 +val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
   13.23  
   13.24  (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   13.25  fun select_literal i cl = negate_head (make_last i cl);
    14.1 --- a/src/HOL/Tools/record.ML	Sun Feb 28 22:30:51 2010 +0100
    14.2 +++ b/src/HOL/Tools/record.ML	Sun Feb 28 23:51:31 2010 +0100
    14.3 @@ -1416,7 +1416,7 @@
    14.4          | name =>
    14.5              (case get_equalities thy name of
    14.6                NONE => NONE
    14.7 -            | SOME thm => SOME (thm RS Eq_TrueI)))
    14.8 +            | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
    14.9        | _ => NONE));
   14.10  
   14.11  
   14.12 @@ -1462,7 +1462,7 @@
   14.13          fun prove prop =
   14.14            prove_global true thy [] prop
   14.15              (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
   14.16 -                addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
   14.17 +                addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1);
   14.18  
   14.19          fun mkeq (lr, Teq, (sel, Tsel), x) i =
   14.20            if is_selector thy sel then