# HG changeset patch
# User wenzelm
# Date 1331654216 -3600
# Node ID 6b1c0a80a57a58c9c34f3eccb8a12fa64d73d209
# Parent  f30e941b451224dbe3f4e8cb327b51484e6778d9
prefer abs_def over def_raw;

diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Import/HOL_Light/Compatibility.thy
--- a/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -272,7 +272,7 @@
 
 lemma DEF_DISJOINT:
   "DISJOINT = (%u ua. u \<inter> ua = {})"
-  by (auto simp add: DISJOINT_def_raw)
+  by (auto simp add: DISJOINT_def [abs_def])
 
 lemma DEF_DIFF:
   "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
@@ -282,7 +282,7 @@
 
 lemma DEF_DELETE:
   "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
-  by (auto simp add: DELETE_def_raw)
+  by (auto simp add: DELETE_def [abs_def])
 
 lemma COND_DEF:
   "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
@@ -344,7 +344,7 @@
 definition [import_rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
 
 lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
-  by (simp add: INFINITE_def_raw)
+  by (simp add: INFINITE_def [abs_def])
 
 end
 
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Import/HOL_Light/HOLLightInt.thy
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -90,7 +90,7 @@
 
 lemma int_mod_def':
   "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
-  by (simp add: int_mod_def_raw)
+  by (simp add: int_mod_def [abs_def])
 
 lemma int_congruent:
   "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -7,9 +7,9 @@
 declare HOL.if_bool_eq_disj[code_pred_inline]
 
 declare bool_diff_def[code_pred_inline]
-declare inf_bool_def_raw[code_pred_inline]
-declare less_bool_def_raw[code_pred_inline]
-declare le_bool_def_raw[code_pred_inline]
+declare inf_bool_def[abs_def, code_pred_inline]
+declare less_bool_def[abs_def, code_pred_inline]
+declare le_bool_def[abs_def, code_pred_inline]
 
 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -2762,12 +2762,24 @@
 
 lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
   apply safe defer apply(subst negligible_def)
-proof- fix t::"'a set" assume as:"negligible s"
-  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)  
-  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
-    apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
-    apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
-    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
+proof -
+  fix t::"'a set" assume as:"negligible s"
+  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 auto
+  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
+    apply(subst has_integral_alt)
+    apply(cases,subst if_P,assumption)
+    unfolding if_not_P
+    apply(safe,rule as[unfolded negligible_def,rule_format])
+    apply(rule_tac x=1 in exI)
+    apply(safe,rule zero_less_one)
+    apply(rule_tac x=0 in exI)
+    using negligible_subset[OF as,of "s \<inter> t"]
+    unfolding negligible_def indicator_def [abs_def]
+    unfolding *
+    apply auto
+    done
+qed auto
 
 subsection {* Finite case of the spike theorem is quite commonly needed. *}
 
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -149,7 +149,7 @@
 
 lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
 nitpick [expect = none]
-by (rule Zero_nat_def_raw)
+by (rule Zero_nat_def [abs_def])
 
 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
 nitpick [expect = none]
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -32,7 +32,7 @@
 lemma [code_pred_def]:
   "cardsp [] g k = False"
   "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)"
-unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
+unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
 
 definition
   "isinp evs r g = (g \<in> isin evs r)"
@@ -44,7 +44,7 @@
    in case e of Check_in g' r c => G g
     | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
     | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
-unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
+unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)
 
 declare hotel.simps(1)[code_pred_def]
 lemma [code_pred_def]:
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -90,7 +90,7 @@
 lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
-  unfolding indicator_def_raw using A
+  unfolding indicator_def [abs_def] using A
   by (auto intro!: measurable_If_set borel_measurable_const)
 
 lemma (in sigma_algebra) borel_measurable_indicator_iff:
@@ -101,7 +101,7 @@
   then have "?I -` {1} \<inter> space M \<in> sets M"
     unfolding measurable_def by auto
   also have "?I -` {1} \<inter> space M = A \<inter> space M"
-    unfolding indicator_def_raw by auto
+    unfolding indicator_def [abs_def] by auto
   finally show "A \<inter> space M \<in> sets M" .
 next
   assume "A \<inter> space M \<in> sets M"
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -706,7 +706,7 @@
   have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
     using assms by (subst measure_times) auto
   then show ?thesis
-    unfolding positive_integral_def simple_function_def simple_integral_def_raw
+    unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
   proof (simp add: P_empty, intro antisym)
     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
       by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -874,7 +874,7 @@
       by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
     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)))"
       using J M.sets_into_space
-      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
+      by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
     also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
       using J by (intro sigma_sets_mono') auto
     finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -823,7 +823,7 @@
   interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
     using distribution_prob_space[OF X] .
   from A show "S.\<mu>' A = distribution X A"
-    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
+    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
 qed
 
 lemma (in information_space) entropy_uniform_max:
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -247,7 +247,7 @@
   hence "finite ?S" by (rule finite_subset) simp
   moreover have "- A \<inter> space M = space M - A" by auto
   ultimately show ?thesis unfolding simple_function_def
-    using assms by (auto simp: indicator_def_raw)
+    using assms by (auto simp: indicator_def [abs_def])
 qed
 
 lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
@@ -821,7 +821,7 @@
 lemma (in measure_space) simple_integral_subalgebra:
   assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
   shows "integral\<^isup>S N = integral\<^isup>S M"
-  unfolding simple_integral_def_raw by simp
+  unfolding simple_integral_def [abs_def] by simp
 
 lemma (in measure_space) simple_integral_vimage:
   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
@@ -1482,7 +1482,7 @@
   have borel[simp]:
     "borel_measurable M' = borel_measurable M"
     "simple_function M' = simple_function M"
-    unfolding measurable_def simple_function_def_raw by (auto simp: M')
+    unfolding measurable_def simple_function_def [abs_def] by (auto simp: M')
   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
   note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
   note G'(2)[simp]
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -48,7 +48,7 @@
 qed
 
 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
-  unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
+  unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
 
 subsection {* Lebesgue measure *} 
 
@@ -95,7 +95,7 @@
     using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
 next
   fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
-    by (auto simp: cube_def indicator_def_raw)
+    by (auto simp: cube_def indicator_def [abs_def])
 next
   fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
   then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
@@ -193,7 +193,7 @@
   have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
     unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
-    unfolding indicator_def_raw has_integral_restrict_univ ..
+    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
   finally show ?thesis
     using has_integral_const[of "1::real" "?N" "?P"] by simp
 qed
@@ -437,9 +437,9 @@
   shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})"
 proof -
   have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
-    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
+    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def])
   from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
-    by (simp add: indicator_def_raw)
+    by (simp add: indicator_def [abs_def])
 qed
 
 lemma atLeastAtMost_singleton_euclidean[simp]:
@@ -504,7 +504,7 @@
   and sets_lborel[simp]: "sets lborel = sets borel"
   and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>"
   and measurable_lborel[simp]: "measurable lborel = measurable borel"
-  by (simp_all add: measurable_def_raw lborel_def)
+  by (simp_all add: measurable_def [abs_def] lborel_def)
 
 interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space"
   where "space lborel = UNIV"
@@ -871,7 +871,7 @@
 
   let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   show "Int_stable ?E" using Int_stable_cuboids .
-  show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
+  show "range cube \<subseteq> sets ?E" unfolding cube_def [abs_def] by auto
   show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
   { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
   then show "(\<Union>i. cube i) = space ?E" by auto
@@ -1001,7 +1001,7 @@
     then show "(\<Union>i. cube i) = space ?E" by auto
     show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
     show "range cube \<subseteq> sets ?E"
-      unfolding cube_def_raw by auto
+      unfolding cube_def [abs_def] by auto
     show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
       by (simp add: cube_def)
     show "measure_space lborel" by default
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -260,7 +260,7 @@
 proof (rule prob_space_vimage)
   show "X \<in> measure_preserving M ?S"
     using X
-    unfolding measure_preserving_def distribution_def_raw
+    unfolding measure_preserving_def distribution_def [abs_def]
     by (auto simp: finite_measure_eq measurable_sets)
   show "sigma_algebra ?S" using X by simp
 qed
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -132,7 +132,7 @@
   have *: "{xs. length xs = n} \<noteq> {}"
     by (auto intro!: exI[of _ "replicate n undefined"])
   show ?thesis
-    unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
+    unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] ..
 qed
 
 lemma card_payer_and_inversion:
@@ -310,7 +310,7 @@
   let ?sets = "{?set i | i. i < n}"
 
   have [simp]: "length xs = n" using assms
-    by (auto simp: dc_crypto inversion_def_raw)
+    by (auto simp: dc_crypto inversion_def [abs_def])
 
   have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
     unfolding dc_crypto payer_def by auto
@@ -462,7 +462,7 @@
           {dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}"
         by (auto simp add: payer_def)
       moreover from x z obtain i where "z = Some i" and "i < n" by auto
-      moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto)
+      moreover from x have "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
       ultimately
       have "?dIP {(x, z)} = 2 / (real n * 2^n)" using x
         by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def)
@@ -490,7 +490,7 @@
       unfolding neg_equal_iff_equal
     proof (rule setsum_cong[OF refl])
       fix x assume x_inv: "x \<in> inversion ` dc_crypto"
-      hence "length x = n" by (auto simp: inversion_def_raw dc_crypto)
+      hence "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
       moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
       ultimately have "?dI {x} = 2 / 2^n" using `0 < n`
         by (auto simp: card_inversion[OF x_inv] card_dc_crypto distribution_def)
diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -115,7 +115,7 @@
 by (simp add: preal_def cut_of_rat)
 
 lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
-  unfolding preal_def cut_def_raw by blast
+  unfolding preal_def cut_def [abs_def] by blast
 
 lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   apply (drule preal_nonempty)
@@ -131,10 +131,10 @@
   done
 
 lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
-  unfolding preal_def cut_def_raw by blast
+  unfolding preal_def cut_def [abs_def] by blast
 
 lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
-  unfolding preal_def cut_def_raw by blast
+  unfolding preal_def cut_def [abs_def] by blast
 
 text{*Relaxing the final premise*}
 lemma preal_downwards_closed':
@@ -966,7 +966,7 @@
 
 lemma mem_diff_set:
      "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
-apply (unfold preal_def cut_def_raw)
+apply (unfold preal_def cut_def [abs_def])
 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
                      diff_set_lemma3 diff_set_lemma4)
 done
@@ -1135,7 +1135,7 @@
 
 lemma preal_sup:
      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
-apply (unfold preal_def cut_def_raw)
+apply (unfold preal_def cut_def [abs_def])
 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
                      preal_sup_set_lemma3 preal_sup_set_lemma4)
 done