--- 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
--- 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)"
--- 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)
--- 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. *}
--- 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]
--- 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]:
--- 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"
--- 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)
--- 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"
--- 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:
--- 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]
--- 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
--- 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
--- 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)
--- 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