prefer abs_def over def_raw;
authorwenzelm
Tue Mar 13 16:56:56 2012 +0100 (2012-03-13 ago)
changeset 469056b1c0a80a57a
parent 46904 f30e941b4512
child 46906 3c1787d46935
prefer abs_def over def_raw;
src/HOL/Import/HOL_Light/Compatibility.thy
src/HOL/Import/HOL_Light/HOLLightInt.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:40:06 2012 +0100
     1.2 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:56:56 2012 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  
     1.5  lemma DEF_DISJOINT:
     1.6    "DISJOINT = (%u ua. u \<inter> ua = {})"
     1.7 -  by (auto simp add: DISJOINT_def_raw)
     1.8 +  by (auto simp add: DISJOINT_def [abs_def])
     1.9  
    1.10  lemma DEF_DIFF:
    1.11    "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
    1.12 @@ -282,7 +282,7 @@
    1.13  
    1.14  lemma DEF_DELETE:
    1.15    "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
    1.16 -  by (auto simp add: DELETE_def_raw)
    1.17 +  by (auto simp add: DELETE_def [abs_def])
    1.18  
    1.19  lemma COND_DEF:
    1.20    "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
    1.21 @@ -344,7 +344,7 @@
    1.22  definition [import_rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
    1.23  
    1.24  lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
    1.25 -  by (simp add: INFINITE_def_raw)
    1.26 +  by (simp add: INFINITE_def [abs_def])
    1.27  
    1.28  end
    1.29  
     2.1 --- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:40:06 2012 +0100
     2.2 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:56:56 2012 +0100
     2.3 @@ -90,7 +90,7 @@
     2.4  
     2.5  lemma int_mod_def':
     2.6    "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
     2.7 -  by (simp add: int_mod_def_raw)
     2.8 +  by (simp add: int_mod_def [abs_def])
     2.9  
    2.10  lemma int_congruent:
    2.11    "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
     3.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:40:06 2012 +0100
     3.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:56:56 2012 +0100
     3.3 @@ -7,9 +7,9 @@
     3.4  declare HOL.if_bool_eq_disj[code_pred_inline]
     3.5  
     3.6  declare bool_diff_def[code_pred_inline]
     3.7 -declare inf_bool_def_raw[code_pred_inline]
     3.8 -declare less_bool_def_raw[code_pred_inline]
     3.9 -declare le_bool_def_raw[code_pred_inline]
    3.10 +declare inf_bool_def[abs_def, code_pred_inline]
    3.11 +declare less_bool_def[abs_def, code_pred_inline]
    3.12 +declare le_bool_def[abs_def, code_pred_inline]
    3.13  
    3.14  lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
    3.15  by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:40:06 2012 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:56:56 2012 +0100
     4.3 @@ -2762,12 +2762,24 @@
     4.4  
     4.5  lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
     4.6    apply safe defer apply(subst negligible_def)
     4.7 -proof- fix t::"'a set" assume as:"negligible s"
     4.8 -  have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)" by(rule ext,auto)  
     4.9 -  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
    4.10 -    apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
    4.11 -    apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
    4.12 -    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
    4.13 +proof -
    4.14 +  fix t::"'a set" assume as:"negligible s"
    4.15 +  have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
    4.16 +    by auto
    4.17 +  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
    4.18 +    apply(subst has_integral_alt)
    4.19 +    apply(cases,subst if_P,assumption)
    4.20 +    unfolding if_not_P
    4.21 +    apply(safe,rule as[unfolded negligible_def,rule_format])
    4.22 +    apply(rule_tac x=1 in exI)
    4.23 +    apply(safe,rule zero_less_one)
    4.24 +    apply(rule_tac x=0 in exI)
    4.25 +    using negligible_subset[OF as,of "s \<inter> t"]
    4.26 +    unfolding negligible_def indicator_def [abs_def]
    4.27 +    unfolding *
    4.28 +    apply auto
    4.29 +    done
    4.30 +qed auto
    4.31  
    4.32  subsection {* Finite case of the spike theorem is quite commonly needed. *}
    4.33  
     5.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:40:06 2012 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:56:56 2012 +0100
     5.3 @@ -149,7 +149,7 @@
     5.4  
     5.5  lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
     5.6  nitpick [expect = none]
     5.7 -by (rule Zero_nat_def_raw)
     5.8 +by (rule Zero_nat_def [abs_def])
     5.9  
    5.10  lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    5.11  nitpick [expect = none]
     6.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:40:06 2012 +0100
     6.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:56:56 2012 +0100
     6.3 @@ -32,7 +32,7 @@
     6.4  lemma [code_pred_def]:
     6.5    "cardsp [] g k = False"
     6.6    "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
     6.7 -unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
     6.8 +unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
     6.9  
    6.10  definition
    6.11    "isinp evs r g = (g \<in> isin evs r)"
    6.12 @@ -44,7 +44,7 @@
    6.13     in case e of Check_in g' r c => G g
    6.14      | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
    6.15      | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
    6.16 -unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
    6.17 +unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)
    6.18  
    6.19  declare hotel.simps(1)[code_pred_def]
    6.20  lemma [code_pred_def]:
     7.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:40:06 2012 +0100
     7.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:56:56 2012 +0100
     7.3 @@ -90,7 +90,7 @@
     7.4  lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
     7.5    assumes A: "A \<in> sets M"
     7.6    shows "indicator A \<in> borel_measurable M"
     7.7 -  unfolding indicator_def_raw using A
     7.8 +  unfolding indicator_def [abs_def] using A
     7.9    by (auto intro!: measurable_If_set borel_measurable_const)
    7.10  
    7.11  lemma (in sigma_algebra) borel_measurable_indicator_iff:
    7.12 @@ -101,7 +101,7 @@
    7.13    then have "?I -` {1} \<inter> space M \<in> sets M"
    7.14      unfolding measurable_def by auto
    7.15    also have "?I -` {1} \<inter> space M = A \<inter> space M"
    7.16 -    unfolding indicator_def_raw by auto
    7.17 +    unfolding indicator_def [abs_def] by auto
    7.18    finally show "A \<inter> space M \<in> sets M" .
    7.19  next
    7.20    assume "A \<inter> space M \<in> sets M"
     8.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
     8.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
     8.3 @@ -706,7 +706,7 @@
     8.4    have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
     8.5      using assms by (subst measure_times) auto
     8.6    then show ?thesis
     8.7 -    unfolding positive_integral_def simple_function_def simple_integral_def_raw
     8.8 +    unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
     8.9    proof (simp add: P_empty, intro antisym)
    8.10      show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
    8.11        by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
     9.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
     9.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
     9.3 @@ -874,7 +874,7 @@
     9.4        by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
     9.5      also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
     9.6        using J M.sets_into_space
     9.7 -      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
     9.8 +      by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
     9.9      also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
    9.10        using J by (intro sigma_sets_mono') auto
    9.11      finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
    10.1 --- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
    10.2 +++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
    10.3 @@ -823,7 +823,7 @@
    10.4    interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
    10.5      using distribution_prob_space[OF X] .
    10.6    from A show "S.\<mu>' A = distribution X A"
    10.7 -    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
    10.8 +    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
    10.9  qed
   10.10  
   10.11  lemma (in information_space) entropy_uniform_max:
    11.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:40:06 2012 +0100
    11.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:56:56 2012 +0100
    11.3 @@ -247,7 +247,7 @@
    11.4    hence "finite ?S" by (rule finite_subset) simp
    11.5    moreover have "- A \<inter> space M = space M - A" by auto
    11.6    ultimately show ?thesis unfolding simple_function_def
    11.7 -    using assms by (auto simp: indicator_def_raw)
    11.8 +    using assms by (auto simp: indicator_def [abs_def])
    11.9  qed
   11.10  
   11.11  lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
   11.12 @@ -821,7 +821,7 @@
   11.13  lemma (in measure_space) simple_integral_subalgebra:
   11.14    assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
   11.15    shows "integral\<^isup>S N = integral\<^isup>S M"
   11.16 -  unfolding simple_integral_def_raw by simp
   11.17 +  unfolding simple_integral_def [abs_def] by simp
   11.18  
   11.19  lemma (in measure_space) simple_integral_vimage:
   11.20    assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
   11.21 @@ -1482,7 +1482,7 @@
   11.22    have borel[simp]:
   11.23      "borel_measurable M' = borel_measurable M"
   11.24      "simple_function M' = simple_function M"
   11.25 -    unfolding measurable_def simple_function_def_raw by (auto simp: M')
   11.26 +    unfolding measurable_def simple_function_def [abs_def] by (auto simp: M')
   11.27    from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
   11.28    note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
   11.29    note G'(2)[simp]
    12.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
    12.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
    12.3 @@ -48,7 +48,7 @@
    12.4  qed
    12.5  
    12.6  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
    12.7 -  unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
    12.8 +  unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
    12.9  
   12.10  subsection {* Lebesgue measure *} 
   12.11  
   12.12 @@ -95,7 +95,7 @@
   12.13      using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
   12.14  next
   12.15    fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
   12.16 -    by (auto simp: cube_def indicator_def_raw)
   12.17 +    by (auto simp: cube_def indicator_def [abs_def])
   12.18  next
   12.19    fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
   12.20    then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
   12.21 @@ -193,7 +193,7 @@
   12.22    have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
   12.23      unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
   12.24    also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
   12.25 -    unfolding indicator_def_raw has_integral_restrict_univ ..
   12.26 +    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
   12.27    finally show ?thesis
   12.28      using has_integral_const[of "1::real" "?N" "?P"] by simp
   12.29  qed
   12.30 @@ -437,9 +437,9 @@
   12.31    shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})"
   12.32  proof -
   12.33    have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
   12.34 -    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
   12.35 +    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def])
   12.36    from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
   12.37 -    by (simp add: indicator_def_raw)
   12.38 +    by (simp add: indicator_def [abs_def])
   12.39  qed
   12.40  
   12.41  lemma atLeastAtMost_singleton_euclidean[simp]:
   12.42 @@ -504,7 +504,7 @@
   12.43    and sets_lborel[simp]: "sets lborel = sets borel"
   12.44    and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>"
   12.45    and measurable_lborel[simp]: "measurable lborel = measurable borel"
   12.46 -  by (simp_all add: measurable_def_raw lborel_def)
   12.47 +  by (simp_all add: measurable_def [abs_def] lborel_def)
   12.48  
   12.49  interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space"
   12.50    where "space lborel = UNIV"
   12.51 @@ -871,7 +871,7 @@
   12.52  
   12.53    let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   12.54    show "Int_stable ?E" using Int_stable_cuboids .
   12.55 -  show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
   12.56 +  show "range cube \<subseteq> sets ?E" unfolding cube_def [abs_def] by auto
   12.57    show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
   12.58    { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
   12.59    then show "(\<Union>i. cube i) = space ?E" by auto
   12.60 @@ -1001,7 +1001,7 @@
   12.61      then show "(\<Union>i. cube i) = space ?E" by auto
   12.62      show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
   12.63      show "range cube \<subseteq> sets ?E"
   12.64 -      unfolding cube_def_raw by auto
   12.65 +      unfolding cube_def [abs_def] by auto
   12.66      show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
   12.67        by (simp add: cube_def)
   12.68      show "measure_space lborel" by default
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
    13.3 @@ -260,7 +260,7 @@
    13.4  proof (rule prob_space_vimage)
    13.5    show "X \<in> measure_preserving M ?S"
    13.6      using X
    13.7 -    unfolding measure_preserving_def distribution_def_raw
    13.8 +    unfolding measure_preserving_def distribution_def [abs_def]
    13.9      by (auto simp: finite_measure_eq measurable_sets)
   13.10    show "sigma_algebra ?S" using X by simp
   13.11  qed
    14.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:40:06 2012 +0100
    14.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:56:56 2012 +0100
    14.3 @@ -132,7 +132,7 @@
    14.4    have *: "{xs. length xs = n} \<noteq> {}"
    14.5      by (auto intro!: exI[of _ "replicate n undefined"])
    14.6    show ?thesis
    14.7 -    unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
    14.8 +    unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] ..
    14.9  qed
   14.10  
   14.11  lemma card_payer_and_inversion:
   14.12 @@ -310,7 +310,7 @@
   14.13    let ?sets = "{?set i | i. i < n}"
   14.14  
   14.15    have [simp]: "length xs = n" using assms
   14.16 -    by (auto simp: dc_crypto inversion_def_raw)
   14.17 +    by (auto simp: dc_crypto inversion_def [abs_def])
   14.18  
   14.19    have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
   14.20      unfolding dc_crypto payer_def by auto
   14.21 @@ -462,7 +462,7 @@
   14.22            {dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}"
   14.23          by (auto simp add: payer_def)
   14.24        moreover from x z obtain i where "z = Some i" and "i < n" by auto
   14.25 -      moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto)
   14.26 +      moreover from x have "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
   14.27        ultimately
   14.28        have "?dIP {(x, z)} = 2 / (real n * 2^n)" using x
   14.29          by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def)
   14.30 @@ -490,7 +490,7 @@
   14.31        unfolding neg_equal_iff_equal
   14.32      proof (rule setsum_cong[OF refl])
   14.33        fix x assume x_inv: "x \<in> inversion ` dc_crypto"
   14.34 -      hence "length x = n" by (auto simp: inversion_def_raw dc_crypto)
   14.35 +      hence "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
   14.36        moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
   14.37        ultimately have "?dI {x} = 2 / 2^n" using `0 < n`
   14.38          by (auto simp: card_inversion[OF x_inv] card_dc_crypto distribution_def)
    15.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:40:06 2012 +0100
    15.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:56:56 2012 +0100
    15.3 @@ -115,7 +115,7 @@
    15.4  by (simp add: preal_def cut_of_rat)
    15.5  
    15.6  lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
    15.7 -  unfolding preal_def cut_def_raw by blast
    15.8 +  unfolding preal_def cut_def [abs_def] by blast
    15.9  
   15.10  lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   15.11    apply (drule preal_nonempty)
   15.12 @@ -131,10 +131,10 @@
   15.13    done
   15.14  
   15.15  lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   15.16 -  unfolding preal_def cut_def_raw by blast
   15.17 +  unfolding preal_def cut_def [abs_def] by blast
   15.18  
   15.19  lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   15.20 -  unfolding preal_def cut_def_raw by blast
   15.21 +  unfolding preal_def cut_def [abs_def] by blast
   15.22  
   15.23  text{*Relaxing the final premise*}
   15.24  lemma preal_downwards_closed':
   15.25 @@ -966,7 +966,7 @@
   15.26  
   15.27  lemma mem_diff_set:
   15.28       "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
   15.29 -apply (unfold preal_def cut_def_raw)
   15.30 +apply (unfold preal_def cut_def [abs_def])
   15.31  apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
   15.32                       diff_set_lemma3 diff_set_lemma4)
   15.33  done
   15.34 @@ -1135,7 +1135,7 @@
   15.35  
   15.36  lemma preal_sup:
   15.37       "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
   15.38 -apply (unfold preal_def cut_def_raw)
   15.39 +apply (unfold preal_def cut_def [abs_def])
   15.40  apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
   15.41                       preal_sup_set_lemma3 preal_sup_set_lemma4)
   15.42  done