more antiquotations;
authorwenzelm
Sun Nov 27 23:10:19 2011 +0100 (2011-11-27)
changeset 45654cf10bde35973
parent 45653 63ed1be524eb
child 45657 862d68ee10f3
more antiquotations;
src/FOL/FOL.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Library/positivstellensatz.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Prolog/prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Qelim/qelim.ML
     1.1 --- a/src/FOL/FOL.thy	Sun Nov 27 23:06:59 2011 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sun Nov 27 23:10:19 2011 +0100
     1.3 @@ -337,12 +337,12 @@
     1.4  (*intuitionistic simprules only*)
     1.5  val IFOL_ss =
     1.6    FOL_basic_ss
     1.7 -  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
     1.8 +  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
     1.9    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
    1.10    |> Simplifier.add_cong @{thm imp_cong};
    1.11  
    1.12  (*classical simprules too*)
    1.13 -val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
    1.14 +val FOL_ss = IFOL_ss addsimps @{thms cla_simps cla_ex_simps cla_all_simps};
    1.15  *}
    1.16  
    1.17  setup {* Simplifier.map_simpset_global (K FOL_ss) *}
     2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:06:59 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:10:19 2011 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5  val nT = HOLogic.natT;
     2.6  val binarith = @{thms normalize_bin_simps};
     2.7 -val comp_arith = binarith @ simp_thms
     2.8 +val comp_arith = binarith @ @{thms simp_thms};
     2.9  
    2.10  val zdvd_int = @{thm zdvd_int};
    2.11  val zdiff_int_split = @{thm zdiff_int_split};
     3.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 27 23:06:59 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 27 23:10:19 2011 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  val binarith =
     3.5    @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
     3.6    @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
     3.7 -val comp_arith = binarith @ simp_thms
     3.8 +val comp_arith = binarith @ @{thms simp_thms};
     3.9  
    3.10  val zdvd_int = @{thm zdvd_int};
    3.11  val zdiff_int_split = @{thm zdiff_int_split};
     4.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:06:59 2011 +0100
     4.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:10:19 2011 +0100
     4.3 @@ -163,7 +163,7 @@
     4.4                          qe))
     4.5                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
     4.6      val bex_conv =
     4.7 -      Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
     4.8 +      Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)})
     4.9      val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
    4.10     in result_th
    4.11     end
    4.12 @@ -200,8 +200,8 @@
    4.13   let
    4.14     val ss = simpset
    4.15     val ss' =
    4.16 -     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
    4.17 -              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
    4.18 +     merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps
    4.19 +                not_all all_not_ex ex_disj_distrib}, ss)
    4.20       |> Simplifier.inherit_context ss
    4.21     val pcv = Simplifier.rewrite ss'     
    4.22     val postcv = Simplifier.rewrite ss
     5.1 --- a/src/HOL/Decision_Procs/langford.ML	Sun Nov 27 23:06:59 2011 +0100
     5.2 +++ b/src/HOL/Decision_Procs/langford.ML	Sun Nov 27 23:10:19 2011 +0100
     5.3 @@ -26,7 +26,9 @@
     5.4                                       (Thm.cprop_of th), SOME x] th1) th
     5.5  in fold ins u th0 end;
     5.6  
     5.7 -val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
     5.8 +val simp_rule =
     5.9 +  Conv.fconv_rule
    5.10 +    (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms ball_simps simp_thms})));
    5.11  
    5.12  fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
    5.13   case term_of ep of 
    5.14 @@ -138,16 +140,14 @@
    5.15                   (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
    5.16             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
    5.17             |> Conv.fconv_rule (Conv.arg_conv 
    5.18 -                   (Simplifier.rewrite 
    5.19 -                      (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
    5.20 +                   (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
    5.21             |> SOME
    5.22            end
    5.23      | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
    5.24                   (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
    5.25             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
    5.26             |> Conv.fconv_rule (Conv.arg_conv 
    5.27 -                   (Simplifier.rewrite 
    5.28 -                (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
    5.29 +                   (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
    5.30             |> SOME
    5.31     end
    5.32   | _ => NONE;
    5.33 @@ -162,9 +162,9 @@
    5.34   let 
    5.35    val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
    5.36    val dnfex_conv = Simplifier.rewrite ss
    5.37 -   val pcv = Simplifier.rewrite
    5.38 -               (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
    5.39 -                @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
    5.40 +  val pcv =
    5.41 +    Simplifier.rewrite
    5.42 +      (dlo_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
    5.43   in fn p => 
    5.44     Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
    5.45                    (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
     6.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 27 23:06:59 2011 +0100
     6.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 27 23:10:19 2011 +0100
     6.3 @@ -37,7 +37,7 @@
     6.4               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
     6.5               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
     6.6               @{thm "diff_minus"}, @{thm "minus_divide_left"}]
     6.7 -val comp_ths = ths @ comp_arith @ simp_thms 
     6.8 +val comp_ths = ths @ comp_arith @ @{thms simp_thms};
     6.9  
    6.10  
    6.11  val zdvd_int = @{thm "zdvd_int"};
    6.12 @@ -89,7 +89,7 @@
    6.13  
    6.14  fun mir_tac ctxt q = 
    6.15      Object_Logic.atomize_prems_tac
    6.16 -        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms)
    6.17 +        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
    6.18          THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    6.19          THEN' SUBGOAL (fn (g, i) =>
    6.20    let
     7.1 --- a/src/HOL/HOL.thy	Sun Nov 27 23:06:59 2011 +0100
     7.2 +++ b/src/HOL/HOL.thy	Sun Nov 27 23:10:19 2011 +0100
     7.3 @@ -2011,15 +2011,8 @@
     7.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
     7.5  end;
     7.6  
     7.7 -val all_conj_distrib = @{thm all_conj_distrib};
     7.8 -val all_simps = @{thms all_simps};
     7.9 -val atomize_not = @{thm atomize_not};
    7.10  val case_split = @{thm case_split};
    7.11 -val cases_simp = @{thm cases_simp};
    7.12 -val choice_eq = @{thm choice_eq};
    7.13  val cong = @{thm cong};
    7.14 -val conj_comms = @{thms conj_comms};
    7.15 -val conj_cong = @{thm conj_cong};
    7.16  val de_Morgan_conj = @{thm de_Morgan_conj};
    7.17  val de_Morgan_disj = @{thm de_Morgan_disj};
    7.18  val disj_assoc = @{thm disj_assoc};
    7.19 @@ -2045,15 +2038,11 @@
    7.20  val imp_conjL = @{thm imp_conjL};
    7.21  val imp_conjR = @{thm imp_conjR};
    7.22  val imp_conv_disj = @{thm imp_conv_disj};
    7.23 -val simp_implies_def = @{thm simp_implies_def};
    7.24 -val simp_thms = @{thms simp_thms};
    7.25  val split_if = @{thm split_if};
    7.26  val the1_equality = @{thm the1_equality};
    7.27  val theI = @{thm theI};
    7.28  val theI' = @{thm theI'};
    7.29 -val True_implies_equals = @{thm True_implies_equals};
    7.30 -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
    7.31 -
    7.32 +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
    7.33  *}
    7.34  
    7.35  hide_const (open) eq equal
     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Nov 27 23:06:59 2011 +0100
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Nov 27 23:10:19 2011 +0100
     8.3 @@ -64,13 +64,13 @@
     8.4  
     8.5  (************************** miscellaneous functions ***************************)
     8.6  
     8.7 -val simple_ss = HOL_basic_ss addsimps simp_thms
     8.8 +val simple_ss = HOL_basic_ss addsimps @{thms simp_thms}
     8.9  
    8.10  val beta_rules =
    8.11    @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
    8.12    @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
    8.13  
    8.14 -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
    8.15 +val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules)
    8.16  
    8.17  fun define_consts
    8.18      (specs : (binding * term * mixfix) list)
     9.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:06:59 2011 +0100
     9.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:10:19 2011 +0100
     9.3 @@ -156,7 +156,7 @@
     9.4            fun con_thm p (con, args) =
     9.5              let
     9.6                val subgoal = con_assm false p (con, args)
     9.7 -              val rules = prems @ con_rews @ simp_thms
     9.8 +              val rules = prems @ con_rews @ @{thms simp_thms}
     9.9                val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
    9.10                fun arg_tac (lazy, _) =
    9.11                    rtac (if lazy then allI else case_UU_allI) 1
    10.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 27 23:06:59 2011 +0100
    10.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 27 23:10:19 2011 +0100
    10.3 @@ -36,7 +36,7 @@
    10.4  struct
    10.5  
    10.6  val beta_ss =
    10.7 -  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
    10.8 +  HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
    10.9  
   10.10  fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
   10.11  
    11.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Nov 27 23:06:59 2011 +0100
    11.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Nov 27 23:10:19 2011 +0100
    11.3 @@ -108,7 +108,7 @@
    11.4    }
    11.5  
    11.6  val beta_ss =
    11.7 -  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
    11.8 +  HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
    11.9  
   11.10  (******************************************************************************)
   11.11  (******************************** theory data *********************************)
    12.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 27 23:06:59 2011 +0100
    12.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 27 23:10:19 2011 +0100
    12.3 @@ -381,7 +381,7 @@
    12.4    @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
    12.5    @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
    12.6  
    12.7 -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
    12.8 +val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules);
    12.9  
   12.10  fun define_consts
   12.11      (specs : (binding * term * mixfix) list)
    13.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:06:59 2011 +0100
    13.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:10:19 2011 +0100
    13.3 @@ -200,7 +200,7 @@
    13.4  val pth_square = @{lemma "x * x >= (0::real)"  by simp};
    13.5  
    13.6  val weak_dnf_simps =
    13.7 -  List.take (simp_thms, 34) @
    13.8 +  List.take (@{thms simp_thms}, 34) @
    13.9      @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
   13.10        "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
   13.11  
   13.12 @@ -351,7 +351,8 @@
   13.13         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
   13.14         absconv1,absconv2,prover) = 
   13.15  let
   13.16 - val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
   13.17 + val pre_ss = HOL_basic_ss addsimps
   13.18 +  @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
   13.19   val prenex_ss = HOL_basic_ss addsimps prenex_simps
   13.20   val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
   13.21   val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
    14.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 27 23:06:59 2011 +0100
    14.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 27 23:10:19 2011 +0100
    14.3 @@ -1018,7 +1018,7 @@
    14.4              (fn _ =>
    14.5                simp_tac (HOL_basic_ss addsimps (supp_def ::
    14.6                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    14.7 -                 Collect_False_empty :: finite_emptyI :: simp_thms @
    14.8 +                 Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
    14.9                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
   14.10          in
   14.11            (supp_thm,
    15.1 --- a/src/HOL/Prolog/prolog.ML	Sun Nov 27 23:06:59 2011 +0100
    15.2 +++ b/src/HOL/Prolog/prolog.ML	Sun Nov 27 23:10:19 2011 +0100
    15.3 @@ -62,7 +62,7 @@
    15.4    (Simplifier.global_context @{theory} empty_ss
    15.5      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
    15.6    addsimps [
    15.7 -        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    15.8 +        @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    15.9          imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
   15.10          imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
   15.11          imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 27 23:06:59 2011 +0100
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 27 23:10:19 2011 +0100
    16.3 @@ -38,7 +38,7 @@
    16.4  
    16.5  
    16.6  (** special setup for simpset **)
    16.7 -val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
    16.8 +val HOL_basic_ss' = HOL_basic_ss addsimps @{thms simp_thms Pair_eq}
    16.9    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   16.10    setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
   16.11  
   16.12 @@ -206,7 +206,7 @@
   16.13          preds
   16.14    in 
   16.15      simp_tac (HOL_basic_ss addsimps
   16.16 -      (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 
   16.17 +      (@{thms HOL.simp_thms eval_pred} @ defs)) 1 
   16.18      (* need better control here! *)
   16.19    end
   16.20  
    17.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sun Nov 27 23:06:59 2011 +0100
    17.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Nov 27 23:10:19 2011 +0100
    17.3 @@ -55,8 +55,7 @@
    17.4  local
    17.5  val pcv =
    17.6    Simplifier.rewrite
    17.7 -    (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @
    17.8 -        [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));
    17.9 +    (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib});
   17.10  
   17.11  in fun standard_qelim_conv atcv ncv qcv p =
   17.12        gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p