prefer abs_def over def_raw;
authorwenzelm
Tue Mar 13 16:40:06 2012 +0100 (2012-03-13)
changeset 46904f30e941b4512
parent 46903 3d44892ac0d6
child 46905 6b1c0a80a57a
prefer abs_def over def_raw;
src/HOL/Big_Operators.thy
src/HOL/Series.thy
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Mar 13 16:22:18 2012 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Mar 13 16:40:06 2012 +0100
     1.3 @@ -1537,11 +1537,11 @@
     1.4  
     1.5  lemma dual_max:
     1.6    "ord.max (op \<ge>) = min"
     1.7 -  by (auto simp add: ord.max_def_raw min_def fun_eq_iff)
     1.8 +  by (auto simp add: ord.max_def min_def fun_eq_iff)
     1.9  
    1.10  lemma dual_min:
    1.11    "ord.min (op \<ge>) = max"
    1.12 -  by (auto simp add: ord.min_def_raw max_def fun_eq_iff)
    1.13 +  by (auto simp add: ord.min_def max_def fun_eq_iff)
    1.14  
    1.15  lemma strict_below_fold1_iff:
    1.16    assumes "finite A" and "A \<noteq> {}"
     2.1 --- a/src/HOL/Series.thy	Tue Mar 13 16:22:18 2012 +0100
     2.2 +++ b/src/HOL/Series.thy	Tue Mar 13 16:40:06 2012 +0100
     2.3 @@ -87,10 +87,13 @@
     2.4    by (simp add: sums_def summable_def, blast)
     2.5  
     2.6  lemma summable_sums:
     2.7 -  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" assumes "summable f" shows "f sums (suminf f)"
     2.8 +  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
     2.9 +  assumes "summable f"
    2.10 +  shows "f sums (suminf f)"
    2.11  proof -
    2.12 -  from assms guess s unfolding summable_def sums_def_raw .. note s = this
    2.13 -  then show ?thesis unfolding sums_def_raw suminf_def
    2.14 +  from assms obtain s where s: "(\<lambda>n. setsum f {0..<n}) ----> s"
    2.15 +    unfolding summable_def sums_def [abs_def] ..
    2.16 +  then show ?thesis unfolding sums_def [abs_def] suminf_def
    2.17      by (rule theI, auto intro!: tendsto_unique[OF trivial_limit_sequentially])
    2.18  qed
    2.19  
     3.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:22:18 2012 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 13 16:40:06 2012 +0100
     3.3 @@ -476,11 +476,11 @@
     3.4      pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
     3.5  
     3.6  val combinator_table =
     3.7 -  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
     3.8 -   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
     3.9 -   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
    3.10 -   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
    3.11 -   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
    3.12 +  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
    3.13 +   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
    3.14 +   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
    3.15 +   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
    3.16 +   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
    3.17  
    3.18  fun uncombine_term thy =
    3.19    let
     4.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:22:18 2012 +0100
     4.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:40:06 2012 +0100
     4.3 @@ -560,7 +560,7 @@
     4.4  val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
     4.5  
     4.6  (* FIXME: "let_simp" is probably redundant now that we also rewrite with
     4.7 -  "Let_def_raw". *)
     4.8 +  "Let_def [abs_def]". *)
     4.9  val nnf_ss =
    4.10    HOL_basic_ss addsimps nnf_extra_simps
    4.11      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    4.12 @@ -574,7 +574,7 @@
    4.13  val presimplify =
    4.14    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    4.15    #> simplify nnf_ss
    4.16 -  #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    4.17 +  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
    4.18  
    4.19  fun make_nnf ctxt th = case prems_of th of
    4.20      [] => th |> presimplify |> make_nnf1 ctxt
     5.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Mar 13 16:22:18 2012 +0100
     5.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Mar 13 16:40:06 2012 +0100
     5.3 @@ -188,8 +188,6 @@
     5.4        in  c_variant_abs_multi (ct, cv::vars)  end
     5.5        handle CTERM _ => (ct0, rev vars);
     5.6  
     5.7 -val skolem_def_raw = @{thms skolem_def_raw}
     5.8 -
     5.9  (* Given the definition of a Skolem function, return a theorem to replace
    5.10     an existential formula by a use of that function.
    5.11     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    5.12 @@ -210,8 +208,8 @@
    5.13        Drule.list_comb (rhs, frees)
    5.14        |> Drule.beta_conv cabs |> Thm.apply cTrueprop
    5.15      fun tacf [prem] =
    5.16 -      rewrite_goals_tac skolem_def_raw
    5.17 -      THEN rtac ((prem |> rewrite_rule skolem_def_raw)
    5.18 +      rewrite_goals_tac @{thms skolem_def [abs_def]}
    5.19 +      THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
    5.20                   RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
    5.21    in
    5.22      Goal.prove_internal [ex_tm] conc tacf
     6.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 13 16:22:18 2012 +0100
     6.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 13 16:40:06 2012 +0100
     6.3 @@ -62,7 +62,7 @@
     6.4  fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
     6.5    let
     6.6      val thy = Proof_Context.theory_of ctxt
     6.7 -    val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
     6.8 +    val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
     6.9      val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
    6.10      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    6.11    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end