--- a/Admin/CHECKLIST Tue Feb 28 15:54:51 2012 +0100
+++ b/Admin/CHECKLIST Tue Feb 28 21:58:59 2012 +0100
@@ -34,6 +34,10 @@
etc/components
lib/html/library_index_content.template
+- test contrib components:
+ x86_64-linux without 32bit C/C++ libraries
+ Mac OS X Leopard
+
Packaging
=========
--- a/src/HOL/Library/Char_nat.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Library/Char_nat.thy Tue Feb 28 21:58:59 2012 +0100
@@ -159,7 +159,7 @@
show ?thesis
by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
nat_of_nibble_of_nat mod_mult_distrib
- n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
+ n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
qed
lemma nibble_pair_of_nat_char:
--- a/src/HOL/Library/Multiset.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Feb 28 21:58:59 2012 +0100
@@ -208,11 +208,12 @@
by auto
lemma union_is_single:
- "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
+ "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
+proof
assume ?rhs then show ?lhs by auto
next
- assume ?lhs thus ?rhs
- by(simp add: multiset_eq_iff split:if_splits) (metis add_is_1)
+ assume ?lhs then show ?rhs
+ by (simp add: multiset_eq_iff split:if_splits) (metis add_is_1)
qed
lemma single_is_union:
@@ -392,7 +393,7 @@
by (simp add: multiset_inter_def multiset_typedef)
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
- by (rule multiset_eqI) (auto simp add: multiset_inter_count)
+ by (rule multiset_eqI) auto
lemma multiset_union_diff_commute:
assumes "B #\<inter> C = {#}"
@@ -400,7 +401,7 @@
proof (rule multiset_eqI)
fix x
from assms have "min (count B x) (count C x) = 0"
- by (auto simp add: multiset_inter_count multiset_eq_iff)
+ by (auto simp add: multiset_eq_iff)
then have "count B x = 0 \<or> count C x = 0"
by auto
then show "count (A + B - C) x = count (A - C + B) x"
@@ -948,15 +949,17 @@
note *** = this [of "op <"] this [of "op >"] this [of "op ="]
show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
- case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
- ultimately show ?thesis
+ case less
+ then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
+ with less show ?thesis
by (simp add: filter_sort [symmetric] ** ***)
next
case equal then show ?thesis
by (simp add: * less_le)
next
- case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
- ultimately show ?thesis
+ case greater
+ then have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
+ with greater show ?thesis
by (simp add: filter_sort [symmetric] ** ***)
qed
qed
@@ -1200,7 +1203,7 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
- by (auto simp add: mset_le_def count_Bag)
+ by (auto simp add: mset_le_def)
next
assume ?rhs
show ?lhs
@@ -1209,7 +1212,7 @@
from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
then show "count (Bag xs) x \<le> count A x"
- by (simp add: mset_le_def count_Bag)
+ by (simp add: mset_le_def)
qed
qed
@@ -1511,15 +1514,13 @@
qed (auto simp add: le_multiset_def irrefl dest: trans)
qed
-lemma mult_less_irrefl [elim!]:
- "M \<subset># (M::'a::order multiset) ==> R"
- by (simp add: multiset_order.less_irrefl)
+lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
+ by simp
subsubsection {* Monotonicity of multiset union *}
-lemma mult1_union:
- "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
+lemma mult1_union: "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
apply (unfold mult1_def)
apply auto
apply (rule_tac x = a in exI)
@@ -1625,9 +1626,9 @@
from MBb have BsubM: "B < M" by simp
show ?case
proof cases
- assume "b=c"
- then moreover have "B = C" using MBb MCc by auto
- ultimately show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
+ assume *: "b = c"
+ then have "B = C" using MBb MCc by auto
+ with * show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
next
assume diff: "b \<noteq> c"
let ?D = "B - {#c#}"
@@ -1780,7 +1781,8 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
-enriched_type image_mset: image_mset proof -
+enriched_type image_mset: image_mset
+proof -
fix f g
show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
proof
--- a/src/HOL/Library/Univ_Poly.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Library/Univ_Poly.thy Tue Feb 28 21:58:59 2012 +0100
@@ -103,7 +103,7 @@
lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp
end
-lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct "t", auto)
+lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct t) auto
lemma (in semiring_0) poly_simple_add_Cons[simp]: "[a] +++ ((0)#t) = (a#t)"
by simp
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -170,7 +170,7 @@
assumes Q: "Q \<in> sets P"
shows "(\<lambda>(x,y). (y, x)) -` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q")
proof -
- let "?f Q" = "(\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
+ let ?f = "\<lambda>Q. (\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
have *: "(\<lambda>(x,y). (y, x)) -` Q = ?f Q"
using sets_into_space[OF Q] by (auto simp: space_pair_measure)
have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))"
@@ -325,7 +325,7 @@
have M1: "sigma_finite_measure M1" by default
from M2.disjoint_sigma_finite guess F .. note F = this
then have F_sets: "\<And>i. F i \<in> sets M2" by auto
- let "?C x i" = "F i \<inter> Pair x -` Q"
+ let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
{ fix i
let ?R = "M2.restricted_space (F i)"
have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
@@ -607,8 +607,8 @@
proof -
have f_borel: "f \<in> borel_measurable P"
using f(1) by (rule borel_measurable_simple_function)
- let "?F z" = "f -` {z} \<inter> space P"
- let "?F' x z" = "Pair x -` ?F z"
+ let ?F = "\<lambda>z. f -` {z} \<inter> space P"
+ let ?F' = "\<lambda>x z. Pair x -` ?F z"
{ fix x assume "x \<in> space M1"
have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
by (auto simp: indicator_def)
@@ -819,7 +819,7 @@
shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE")
and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT")
proof -
- let "?pf x" = "ereal (f x)" and "?nf x" = "ereal (- f x)"
+ let ?pf = "\<lambda>x. ereal (f x)" and ?nf = "\<lambda>x. ereal (- f x)"
have
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and
int: "integral\<^isup>P P ?nf \<noteq> \<infinity>" "integral\<^isup>P P ?pf \<noteq> \<infinity>"
--- a/src/HOL/Probability/Borel_Space.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Feb 28 21:58:59 2012 +0100
@@ -521,7 +521,8 @@
finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
apply (simp only:)
apply (safe intro!: countable_UN Diff)
- by (auto simp: sets_sigma intro!: sigma_sets.Basic)
+ apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
+ done
next
fix a i assume "\<not> i < DIM('a)"
then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
@@ -556,7 +557,8 @@
finally show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
apply (simp only:)
apply (safe intro!: countable_UN Diff)
- by (auto simp: sets_sigma intro!: sigma_sets.Basic)
+ apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
+ done
next
fix a i assume "\<not> i < DIM('a)"
then show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
@@ -653,7 +655,8 @@
have "M \<in> sets ?SIGMA"
apply (subst open_UNION[OF `open M`])
apply (safe intro!: countable_UN)
- by (auto simp add: sigma_def intro!: sigma_sets.Basic) }
+ apply (auto simp add: sigma_def intro!: sigma_sets.Basic)
+ done }
then show ?thesis
unfolding borel_def by (intro sets_sigma_subset) auto
qed
@@ -1156,7 +1159,7 @@
assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"
have "f -` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f -` {-\<infinity>} \<inter> space M = {x\<in>space M. f x = -\<infinity>}" by auto
with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = -\<infinity>} \<in> sets M" by simp_all
- let "?f x" = "if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
+ let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
finally show "f \<in> borel_measurable M" .
@@ -1469,7 +1472,7 @@
shows "u' \<in> borel_measurable M"
proof -
have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)"
- using u' by (simp add: lim_imp_Liminf trivial_limit_sequentially lim_ereal)
+ using u' by (simp add: lim_imp_Liminf)
moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M"
by auto
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
--- a/src/HOL/Probability/Caratheodory.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Feb 28 21:58:59 2012 +0100
@@ -223,7 +223,7 @@
by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
moreover
have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
- by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
+ by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
ultimately show ?thesis
by (metis lambda_system_Compl lambda_system_Int xl yl)
qed
@@ -666,7 +666,7 @@
(\<lambda>x. Inf (measure_set M f x))"
proof (simp add: countably_subadditive_def, safe)
fix A :: "nat \<Rightarrow> 'a set"
- let "?outer B" = "Inf (measure_set M f B)"
+ let ?outer = "\<lambda>B. Inf (measure_set M f B)"
assume A: "range A \<subseteq> Pow (space M)"
and disj: "disjoint_family A"
and sb: "(\<Union>i. A i) \<subseteq> space M"
--- a/src/HOL/Probability/Complete_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -203,7 +203,7 @@
assumes f: "simple_function completion f"
shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
proof -
- let "?F x" = "f -` {x} \<inter> space M"
+ let ?F = "\<lambda>x. f -` {x} \<inter> space M"
have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
using completion.simple_functionD[OF f]
completion.simple_functionD[OF f] by simp_all
@@ -211,7 +211,8 @@
using F null_part by auto
from choice[OF this] obtain N where
N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
- let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
+ let ?N = "\<Union>x\<in>f`space M. N x"
+ let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
show ?thesis unfolding simple_function_def
proof (safe intro!: exI[of _ ?f'])
--- a/src/HOL/Probability/Conditional_Probability.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Conditional_Probability.thy Tue Feb 28 21:58:59 2012 +0100
@@ -25,8 +25,8 @@
interpret P: prob_space N
using prob_space_subalgebra[OF N] .
- let "?f A" = "\<lambda>x. X x * indicator A x"
- let "?Q A" = "integral\<^isup>P M (?f A)"
+ let ?f = "\<lambda>A x. X x * indicator A x"
+ let ?Q = "\<lambda>A. integral\<^isup>P M (?f A)"
from measure_space_density[OF borel]
have Q: "measure_space (N\<lparr> measure := ?Q \<rparr>)"
@@ -146,7 +146,7 @@
by auto
from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this
from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this
- let "?g x" = "p x - n x"
+ let ?g = "\<lambda>x. p x - n x"
show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
proof (intro bexI ballI)
show "?g \<in> borel_measurable M'" using p n by auto
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -627,7 +627,7 @@
by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
show ?case
proof (intro exI[of _ ?\<nu>] conjI ballI)
- let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
+ let ?m = "\<lambda>A. measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
{ fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
@@ -648,7 +648,7 @@
"(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
"\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
by blast+
- let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
+ let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
(\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
proof (intro exI[of _ ?F] conjI allI)
@@ -727,7 +727,7 @@
interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
interpret P: pair_sigma_finite I.P J.P by default
let ?g = "\<lambda>(x,y). merge I x J y"
- let "?X S" = "?g -` S \<inter> space P.P"
+ let ?X = "\<lambda>S. ?g -` S \<inter> space P.P"
from IJ.sigma_finite_pairs obtain F where
F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
"incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
@@ -839,7 +839,7 @@
unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
fix x assume x: "x \<in> space I.P"
- let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+ let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
have f'_eq: "\<And>y. ?f y = f (x(i := y))"
using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
show "?f \<in> borel_measurable (M i)" unfolding f'_eq
@@ -930,7 +930,7 @@
unfolding product_integral_fold[OF IJ, simplified, OF f]
proof (rule I.integral_cong, subst product_integral_singleton)
fix x assume x: "x \<in> space I.P"
- let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+ let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
have f'_eq: "\<And>y. ?f y = f (x(i := y))"
using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
--- a/src/HOL/Probability/Independent_Family.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Tue Feb 28 21:58:59 2012 +0100
@@ -142,7 +142,7 @@
with indep have "indep_sets F J"
by (subst (asm) indep_sets_finite_index_sets) auto
{ fix J K assume "indep_sets F K"
- let "?G S i" = "if i \<in> S then ?F i else F i"
+ let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i"
assume "finite J" "J \<subseteq> K"
then have "indep_sets (?G J) K"
proof induct
@@ -384,7 +384,7 @@
assumes disjoint: "disjoint_family_on I J"
shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J"
proof -
- let "?E j" = "{\<Inter>k\<in>K. E' k| E' K. finite K \<and> K \<noteq> {} \<and> K \<subseteq> I j \<and> (\<forall>k\<in>K. E' k \<in> E k) }"
+ let ?E = "\<lambda>j. {\<Inter>k\<in>K. E' k| E' K. finite K \<and> K \<noteq> {} \<and> K \<subseteq> I j \<and> (\<forall>k\<in>K. E' k \<in> E k) }"
from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events"
unfolding indep_sets_def by auto
@@ -447,7 +447,7 @@
with * L_inj show "k = j" by auto
qed (insert *, simp) }
note k_simp[simp] = this
- let "?E' l" = "E' (k l) l"
+ let ?E' = "\<lambda>l. E' (k l) l"
have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)"
by (auto simp: A intro!: arg_cong[where f=prob])
also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
@@ -658,7 +658,7 @@
fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>"
unfolding Int_stable_def by simp
qed
- let "?Q n" = "\<Union>i\<in>{n..}. F i"
+ let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i"
show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
unfolding terminal_events_def
proof
@@ -691,7 +691,7 @@
proof (rule indep_setsI[OF F(1)])
fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
assume A: "\<forall>j\<in>J. A j \<in> F j"
- let "?A j" = "if j \<in> J then A j else space M"
+ let ?A = "\<lambda>j. if j \<in> J then A j else space M"
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
using subset_trans[OF F(1) space_closed] J A
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -52,7 +52,7 @@
from J.sigma_finite_pairs guess F .. note F = this
then have [simp,intro]: "\<And>k i. k \<in> J \<Longrightarrow> F k i \<in> sets (M k)"
by auto
- let "?F i" = "\<Pi>\<^isub>E k\<in>J. F k i"
+ let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. F k i"
let ?J = "product_algebra_generator J M \<lparr> measure := measure (Pi\<^isub>M J M) \<rparr>"
have "?R \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (sigma ?J)"
proof (rule K.measure_preserving_Int_stable)
@@ -448,7 +448,7 @@
"K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = measure (Pi\<^isub>M K M) X"
by (auto simp: subset_insertI)
- let "?M y" = "merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
+ let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
{ fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
moreover
@@ -487,7 +487,7 @@
by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
note le_1 = this
- let "?q y" = "\<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
+ let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
unfolding `Z = emb I K X` using J K merge_in_G(3)
by (simp add: merge_in_G \<mu>G_eq measure_fold_measurable
@@ -536,15 +536,15 @@
using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
by (auto intro!: INF_lower2[of 0] J.measure_le_1)
- let "?M K Z y" = "merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
+ let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
{ fix Z k assume Z: "range Z \<subseteq> sets ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
then have Z_sets: "\<And>n. Z n \<in> sets ?G" by auto
fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
interpret J': finite_product_prob_space M J' by default fact+
- let "?q n y" = "\<mu>G (?M J' (Z n) y)"
- let "?Q n" = "?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
+ let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
+ let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
{ fix n
have "?q n \<in> borel_measurable (Pi\<^isub>M J' M)"
using Z J' by (intro fold(1)) auto
@@ -599,13 +599,14 @@
then have "\<exists>w\<in>space (Pi\<^isub>M J' M). \<forall>n. ?a / 2 ^ (k + 1) \<le> ?q n w" by auto }
note Ex_w = this
- let "?q k n y" = "\<mu>G (?M (J k) (A n) y)"
+ let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
- let "?P k wk w" =
- "w \<in> space (Pi\<^isub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and> (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
+ let ?P =
+ "\<lambda>k wk w. w \<in> space (Pi\<^isub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
+ (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
{ fix k have w: "w k \<in> space (Pi\<^isub>M (J k) M) \<and>
@@ -1015,7 +1016,7 @@
fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
proof -
- let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
+ let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
{ fix n :: nat
interpret n: finite_product_prob_space M "{..n}" by default auto
have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
--- a/src/HOL/Probability/Information.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Information.thy Tue Feb 28 21:58:59 2012 +0100
@@ -748,8 +748,8 @@
proof -
interpret MX: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"
using MX by (rule distribution_finite_prob_space)
- let "?X x" = "distribution X {x}"
- let "?XX x y" = "joint_distribution X X {(x, y)}"
+ let ?X = "\<lambda>x. distribution X {x}"
+ let ?XX = "\<lambda>x y. joint_distribution X X {(x, y)}"
{ fix x y :: 'c
{ assume "x \<noteq> y"
@@ -803,7 +803,7 @@
assumes X: "simple_function M X"
shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))"
proof -
- let "?p x" = "distribution X {x}"
+ let ?p = "\<lambda>x. distribution X {x}"
have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"
unfolding entropy_eq[OF X] setsum_negf[symmetric]
by (auto intro!: setsum_cong simp: log_simps)
@@ -1117,10 +1117,10 @@
proof -
interpret MX: finite_sigma_algebra MX using MX by simp
interpret MZ: finite_sigma_algebra MZ using MZ by simp
- let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
- let "?XZ x z" = "joint_distribution X Z {(x, z)}"
- let "?Z z" = "distribution Z {z}"
- let "?f x y z" = "log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
+ let ?XXZ = "\<lambda>x y z. joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
+ let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
+ let ?Z = "\<lambda>z. distribution Z {z}"
+ let ?f = "\<lambda>x y z. log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
{ fix x z have "?XXZ x x z = ?XZ x z"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) }
note this[simp]
@@ -1183,9 +1183,9 @@
assumes X: "simple_function M X" and Z: "simple_function M Z"
shows "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
proof -
- let "?XZ x z" = "joint_distribution X Z {(x, z)}"
- let "?Z z" = "distribution Z {z}"
- let "?X x" = "distribution X {x}"
+ let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
+ let ?Z = "\<lambda>z. distribution Z {z}"
+ let ?X = "\<lambda>x. distribution X {x}"
note fX = X[THEN simple_function_imp_finite_random_variable]
note fZ = Z[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fZ, simp]
@@ -1214,9 +1214,9 @@
assumes X: "simple_function M X" and Y: "simple_function M Y"
shows "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
proof -
- let "?XY x y" = "joint_distribution X Y {(x, y)}"
- let "?Y y" = "distribution Y {y}"
- let "?X x" = "distribution X {x}"
+ let ?XY = "\<lambda>x y. joint_distribution X Y {(x, y)}"
+ let ?Y = "\<lambda>y. distribution Y {y}"
+ let ?X = "\<lambda>x. distribution X {x}"
note fX = X[THEN simple_function_imp_finite_random_variable]
note fY = Y[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fY, simp]
@@ -1352,9 +1352,9 @@
assumes svi: "subvimage (space M) X P"
shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
proof -
- let "?XP x p" = "joint_distribution X P {(x, p)}"
- let "?X x" = "distribution X {x}"
- let "?P p" = "distribution P {p}"
+ let ?XP = "\<lambda>x p. joint_distribution X P {(x, p)}"
+ let ?X = "\<lambda>x. distribution X {x}"
+ let ?P = "\<lambda>p. distribution P {p}"
note fX = sf(1)[THEN simple_function_imp_finite_random_variable]
note fP = sf(2)[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fP, simp]
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Feb 28 21:58:59 2012 +0100
@@ -331,7 +331,7 @@
"\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"
unfolding f_def by auto
- let "?g j x" = "real (f x j) / 2^j :: ereal"
+ let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
show ?thesis
proof (intro exI[of _ ?g] conjI allI ballI)
fix i
@@ -567,7 +567,7 @@
shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
(is "_ = setsum _ (?p ` space M)")
proof-
- let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
+ let ?sub = "\<lambda>x. ?p ` (f -` {x} \<inter> space M)"
let ?SIGMA = "Sigma (f`space M) ?sub"
have [intro]:
@@ -659,7 +659,7 @@
and mono: "AE x. f x \<le> g x"
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
proof -
- let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
+ let ?S = "\<lambda>x. (g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
"\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
show ?thesis
@@ -899,7 +899,7 @@
let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
note gM = g(1)[THEN borel_measurable_simple_function]
have \<mu>G_pos: "0 \<le> \<mu> ?G" using gM by auto
- let "?g y x" = "if g x = \<infinity> then y else max 0 (g x)"
+ let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
apply (safe intro!: simple_function_max simple_function_If)
apply (force simp: max_def le_fun_def split: split_if_asm)+
@@ -941,7 +941,7 @@
fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
from ae[THEN AE_E] guess N . note N = this
then have ae_N: "AE x. x \<notin> N" by (auto intro: AE_not_in)
- let "?n x" = "n x * indicator (space M - N) x"
+ let ?n = "\<lambda>x. n x * indicator (space M - N) x"
have "AE x. n x \<le> ?n x" "simple_function M ?n"
using n N ae_N by auto
moreover
@@ -974,7 +974,7 @@
lemma (in measure_space) positive_integral_eq_simple_integral:
assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
proof -
- let "?f x" = "f x * indicator (space M) x"
+ let ?f = "\<lambda>x. f x * indicator (space M) x"
have f': "simple_function M ?f" using f by auto
with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
by (auto simp: fun_eq_iff max_def split: split_indicator)
@@ -1010,11 +1010,11 @@
using u(3) by auto
fix a :: ereal assume "0 < a" "a < 1"
hence "a \<noteq> 0" by auto
- let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
+ let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
have B: "\<And>i. ?B i \<in> sets M"
using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
- let "?uB i x" = "u x * indicator (?B i) x"
+ let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
{ fix i have "?B i \<subseteq> ?B (Suc i)"
proof safe
@@ -1027,7 +1027,7 @@
note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
- let "?B' i n" = "(u -` {i} \<inter> space M) \<inter> ?B n"
+ let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
have measure_conv: "\<And>i. \<mu> (u -` {i} \<inter> space M) = (SUP n. \<mu> (?B' i n))"
proof -
fix i
@@ -1126,7 +1126,7 @@
from f have "AE x. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
by (simp add: AE_all_countable)
from this[THEN AE_E] guess N . note N = this
- let "?f i x" = "if x \<in> space M - N then f i x else 0"
+ let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
have f_eq: "AE x. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ N])
then have "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP i. ?f i x) \<partial>M)"
by (auto intro!: positive_integral_cong_AE)
@@ -1202,7 +1202,7 @@
interpret T: measure_space M' by (rule measure_space_vimage[OF T])
from T.borel_measurable_implies_simple_function_sequence'[OF f]
guess f' . note f' = this
- let "?f i x" = "f' i (T x)"
+ let ?f = "\<lambda>i x. f' i (T x)"
have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
using f'(4) .
@@ -1225,7 +1225,7 @@
note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
- let "?L' i x" = "a * u i x + v i x"
+ let ?L' = "\<lambda>i x. a * u i x + v i x"
have "?L \<in> borel_measurable M" using assms by auto
from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
@@ -1494,7 +1494,7 @@
from G(4) g(2) have G_M': "AE x in M'. (SUP i. G i x) = g x"
by (auto intro!: ac split: split_max)
{ fix i
- let "?I y x" = "indicator (G i -` {y} \<inter> space M) x"
+ let ?I = "\<lambda>y x. indicator (G i -` {y} \<inter> space M) x"
{ fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
from * G' G have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * (\<Sum>y\<in>G i`space M. (y * ?I y x))"
@@ -1546,7 +1546,7 @@
then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
note gt_1 = this
assume *: "integral\<^isup>P M u = 0"
- let "?M n" = "{x \<in> space M. 1 \<le> real (n::nat) * u x}"
+ let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
proof -
{ fix n :: nat
@@ -1618,7 +1618,7 @@
proof -
interpret R: measure_space ?R
by (rule restricted_measure_space) fact
- let "?I g x" = "g x * indicator A x :: ereal"
+ let ?I = "\<lambda>g x. g x * indicator A x :: ereal"
show ?thesis
unfolding positive_integral_def
unfolding simple_function_restricted[OF A]
@@ -1846,10 +1846,10 @@
and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x"
shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
proof -
- let "?f x" = "max 0 (ereal (f x))"
- let "?mf x" = "max 0 (ereal (- f x))"
- let "?u x" = "max 0 (ereal (u x))"
- let "?v x" = "max 0 (ereal (v x))"
+ let ?f = "\<lambda>x. max 0 (ereal (f x))"
+ let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
+ let ?u = "\<lambda>x. max 0 (ereal (u x))"
+ let ?v = "\<lambda>x. max 0 (ereal (v x))"
from borel_measurable_diff[of u v] integrable
have f_borel: "?f \<in> borel_measurable M" and
@@ -1886,12 +1886,12 @@
shows "integrable M (\<lambda>t. a * f t + g t)"
and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" (is ?EQ)
proof -
- let "?f x" = "max 0 (ereal (f x))"
- let "?g x" = "max 0 (ereal (g x))"
- let "?mf x" = "max 0 (ereal (- f x))"
- let "?mg x" = "max 0 (ereal (- g x))"
- let "?p t" = "max 0 (a * f t) + max 0 (g t)"
- let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
+ let ?f = "\<lambda>x. max 0 (ereal (f x))"
+ let ?g = "\<lambda>x. max 0 (ereal (g x))"
+ let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
+ let ?mg = "\<lambda>x. max 0 (ereal (- g x))"
+ let ?p = "\<lambda>t. max 0 (a * f t) + max 0 (g t)"
+ let ?n = "\<lambda>t. max 0 (- (a * f t)) + max 0 (- g t)"
from assms have linear:
"(\<integral>\<^isup>+ x. ereal a * ?f x + ?g x \<partial>M) = ereal a * integral\<^isup>P M ?f + integral\<^isup>P M ?g"
@@ -2353,7 +2353,7 @@
show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
qed
- let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>"
+ let ?diff = "\<lambda>n x. 2 * w x - \<bar>u n x - u' x\<bar>"
have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
using w u `integrable M u'`
by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
@@ -2468,7 +2468,7 @@
from bchoice[OF this]
obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
- let "?w y" = "if y \<in> space M then w y else 0"
+ let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
using sums unfolding summable_def ..
@@ -2484,8 +2484,8 @@
have 3: "integrable M ?w"
proof (rule integral_monotone_convergence(1))
- let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
- let "?w' n y" = "if y \<in> space M then ?F n y else 0"
+ let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
+ let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
have "\<And>n. integrable M (?F n)"
using borel by (auto intro!: integral_setsum integrable_abs)
thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
@@ -2522,8 +2522,8 @@
shows "integrable M f"
and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums)
proof -
- let "?A r" = "f -` {enum r} \<inter> space M"
- let "?F r x" = "enum r * indicator (?A r) x"
+ let ?A = "\<lambda>r. f -` {enum r} \<inter> space M"
+ let ?F = "\<lambda>r x. enum r * indicator (?A r) x"
have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)"
using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
@@ -2579,8 +2579,8 @@
and "(\<integral>x. f x \<partial>M) =
(\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
proof -
- let "?A r" = "f -` {r} \<inter> space M"
- let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x"
+ let ?A = "\<lambda>r. f -` {r} \<inter> space M"
+ let ?S = "\<lambda>x. \<Sum>r\<in>f`space M. r * indicator (?A r) x"
{ fix x assume "x \<in> space M"
have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -133,8 +133,8 @@
fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A"
then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
by (auto dest: lebesgueD)
- let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
- let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
+ let ?m = "\<lambda>n i. integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
+ let ?M = "\<lambda>n I. integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg)
assume "(\<Union>i. A i) \<in> sets lebesgue"
then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
@@ -560,8 +560,8 @@
shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV"
unfolding simple_integral_def space_lebesgue
proof (subst lebesgue_simple_function_indicator)
- let "?M x" = "lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
- let "?F x" = "indicator (f -` {x})"
+ let ?M = "\<lambda>x. lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
+ let ?F = "\<lambda>x. indicator (f -` {x})"
{ fix x y assume "y \<in> range f"
from subsetD[OF f' this] have "y * ?F y x = ereal (real y * ?F y x)"
by (cases rule: ereal2_cases[of y "?F y x"])
@@ -637,7 +637,7 @@
guess u . note u = this
have SUP_eq: "\<And>x. (SUP i. u i x) = f x"
using u(4) f(2)[THEN subsetD] by (auto split: split_max)
- let "?u i x" = "real (u i x)"
+ let ?u = "\<lambda>i x. real (u i x)"
note u_eq = lebesgue.positive_integral_eq_simple_integral[OF u(1,5), symmetric]
{ fix i
note u_eq
@@ -986,7 +986,7 @@
(is "_ = ?\<nu> X")
proof -
let ?E = "\<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::real .. b})\<rparr> :: real algebra"
- let "?M \<nu>" = "\<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
+ let ?M = "\<lambda>\<nu>. \<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
have *: "?M (measure lebesgue) = lborel"
unfolding borel_eq_atLeastAtMost[symmetric]
by (simp add: lborel_def lebesgue_def)
--- a/src/HOL/Probability/Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -439,7 +439,7 @@
shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
using assms proof induct
case (insert i I)
- then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
+ then have "(\<Union>i\<in>I. A i) \<in> sets M" by auto
then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
using insert by (simp add: measure_subadditive)
also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
@@ -458,7 +458,7 @@
by (simp add: disjoint_family_disjointed comp_def)
also have "\<dots> \<le> (\<Sum>i. \<mu> (f i))"
using range_disjointed_sets[OF assms] assms
- by (auto intro!: suminf_le_pos measure_mono positive_measure disjointed_subset)
+ by (auto intro!: suminf_le_pos measure_mono disjointed_subset)
finally show ?thesis .
qed
@@ -509,7 +509,7 @@
assumes "X \<in> sets (sigma E)"
shows "\<mu> X = \<nu> X"
proof -
- let "?D F" = "{D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
+ let ?D = "\<lambda>F. {D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
interpret M: measure_space ?M
where "space ?M = space E" and "sets ?M = sets (sigma E)" and "measure ?M = \<mu>" by (simp_all add: M)
interpret N: measure_space ?N
@@ -559,7 +559,7 @@
have "\<And>D. D \<in> sets (sigma E) \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)"
by (subst (asm) *) auto }
note * = this
- let "?A i" = "A i \<inter> X"
+ let ?A = "\<lambda>i. A i \<inter> X"
have A': "range ?A \<subseteq> sets (sigma E)" "incseq ?A"
using A(1,2) `X \<in> sets (sigma E)` by (auto simp: incseq_def)
{ fix i have "\<mu> (?A i) = \<nu> (?A i)"
@@ -1015,7 +1015,7 @@
proof (rule measure_unique_Int_stable[OF E A(1,2,3) _ _ eq _ X])
interpret M: measure_space M by fact
interpret N: measure_space N by fact
- let "?T X" = "T -` X \<inter> space N"
+ let ?T = "\<lambda>X. T -` X \<inter> space N"
show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
by (rule M.measure_space_cong) (auto simp: M)
show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
@@ -1397,7 +1397,7 @@
lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
using measure_setsum[of "space M" "\<lambda>i. {i}"]
- by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
+ by (simp add: disjoint_family_on_def finite_space)
lemma (in finite_measure_space) finite_measure_singleton:
assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
--- a/src/HOL/Probability/Probability_Measure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -380,7 +380,7 @@
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
proof -
- let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
+ let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
from not_empty X(2) have "I \<noteq> {}" by auto
from I have "open I" by auto
@@ -741,7 +741,7 @@
proof (subst finite_measure_finite_Union[symmetric])
interpret MX: finite_sigma_algebra MX using X by auto
show "finite (space MX)" using MX.finite_space .
- let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
+ let ?d = "\<lambda>i. (\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
{ fix i assume "i \<in> space MX"
moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
ultimately show "?d i \<in> events"
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Feb 28 21:58:59 2012 +0100
@@ -17,7 +17,7 @@
measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>" and
disjoint: "disjoint_family A"
using disjoint_sigma_finite by auto
- let "?B i" = "2^Suc i * \<mu> (A i)"
+ let ?B = "\<lambda>i. 2^Suc i * \<mu> (A i)"
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
fix i have Ai: "A i \<in> sets M" using range by auto
@@ -28,7 +28,7 @@
from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
"\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
{ fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this
- let "?h x" = "\<Sum>i. n i * indicator (A i) x"
+ let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x"
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
have "\<And>i. A i \<in> sets M"
@@ -132,8 +132,8 @@
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < \<mu>' B - finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)"
proof -
interpret M': finite_measure "M\<lparr>measure := \<nu>\<rparr>" by fact
- let "?d A" = "\<mu>' A - M'.\<mu>' A"
- let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
+ let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
+ let ?A = "\<lambda>A. if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
then {}
else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
@@ -247,9 +247,9 @@
proof -
interpret M': finite_measure ?M' where
"space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" by fact auto
- let "?d A" = "\<mu>' A - M'.\<mu>' A"
- let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
- let "?r S" = "restricted_space S"
+ let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
+ let ?P = "\<lambda>A B n. A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
+ let ?r = "\<lambda>S. restricted_space S"
{ fix S n assume S: "S \<in> sets M"
note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S
then have "finite_measure (?r S)" "0 < 1 / real (Suc n)"
@@ -342,7 +342,7 @@
(\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
(\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
using f g sets unfolding G_def
- by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
+ by (auto cong: positive_integral_cong intro!: positive_integral_add)
also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
using f g sets unfolding G_def by (auto intro!: add_mono)
also have "\<dots> = \<nu> A"
@@ -388,9 +388,9 @@
qed
from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^isup>P M (gs n) = ys n" by auto
hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto
- let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
+ let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
def f \<equiv> "\<lambda>x. SUP i. ?g i x"
- let "?F A x" = "f x * indicator A x"
+ let ?F = "\<lambda>A x. f x * indicator A x"
have gs_not_empty: "\<And>i x. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
{ fix i have "?g i \<in> G"
proof (induct i)
@@ -420,7 +420,7 @@
have "\<And>x. 0 \<le> f x"
unfolding f_def using `\<And>i. gs i \<in> G`
by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
- let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
+ let ?t = "\<lambda>A. \<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
let ?M = "M\<lparr> measure := ?t\<rparr>"
interpret M: sigma_algebra ?M
by (intro sigma_algebra_cong) auto
@@ -522,7 +522,7 @@
using M'.finite_measure b finite_measure M.positive_measure[OF B(1)]
by (cases rule: ereal2_cases[of "?t B" "b * \<mu> B"]) auto }
note bM_le_t = this
- let "?f0 x" = "f x + b * indicator A0 x"
+ let ?f0 = "\<lambda>x. f x + b * indicator A0 x"
{ fix A assume A: "A \<in> sets M"
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) =
@@ -550,8 +550,7 @@
by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "\<nu> A") auto
finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> \<nu> A" . }
hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
- by (auto intro!: borel_measurable_indicator borel_measurable_ereal_add
- borel_measurable_ereal_times ereal_add_nonneg_nonneg)
+ by (auto intro!: ereal_add_nonneg_nonneg)
have real: "?t (space M) \<noteq> \<infinity>" "?t A0 \<noteq> \<infinity>"
"b * \<mu> (space M) \<noteq> \<infinity>" "b * \<mu> A0 \<noteq> \<infinity>"
using `A0 \<in> sets M` b
@@ -633,7 +632,7 @@
have "{} \<in> ?Q" using v.empty_measure by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
have "?a \<le> \<mu> (space M)" using sets_into_space
- by (auto intro!: SUP_least measure_mono top)
+ by (auto intro!: SUP_least measure_mono)
then have "?a \<noteq> \<infinity>" using finite_measure_of_space
by auto
from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
@@ -643,7 +642,7 @@
from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
by auto
then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
- let "?O n" = "\<Union>i\<le>n. Q' i"
+ let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
proof (rule continuity_from_below[of ?O])
show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
@@ -675,7 +674,7 @@
using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
qed
qed
- let "?O_0" = "(\<Union>i. ?O i)"
+ let ?O_0 = "(\<Union>i. ?O i)"
have "?O_0 \<in> sets M" using Q' by auto
def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
{ fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
@@ -710,10 +709,9 @@
fix i have "?O i \<union> A \<in> ?Q"
proof (safe del: notI)
show "?O i \<union> A \<in> sets M" using O_sets A by auto
- from O_in_G[of i]
- moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
+ from O_in_G[of i] have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
using v.measure_subadditive[of "?O i" A] A O_sets by auto
- ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
+ with O_in_G[of i] show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
using `\<nu> A \<noteq> \<infinity>` by auto
qed
then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
@@ -800,7 +798,7 @@
and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
\<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)"
by auto
- let "?f x" = "(\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
+ let ?f = "\<lambda>x. (\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
show ?thesis
proof (safe intro!: bexI[of _ ?f])
show "?f \<in> borel_measurable M" using Q0 borel Q_sets
@@ -850,7 +848,7 @@
nn: "\<And>x. 0 \<le> h x" and
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
"\<And>x. x \<in> space M \<Longrightarrow> h x < \<infinity>" by auto
- let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
+ let ?T = "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
let ?MT = "M\<lparr> measure := ?T \<rparr>"
interpret T: finite_measure ?MT
where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
@@ -872,7 +870,7 @@
show ?thesis
proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
- using borel f_borel by (auto intro: borel_measurable_ereal_times)
+ using borel f_borel by auto
show "\<And>x. 0 \<le> h x * f x" using nn f_borel by auto
fix A assume "A \<in> sets M"
then show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x \<partial>M)"
@@ -933,8 +931,8 @@
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
shows "AE x. f x = f' x"
proof -
- let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
- let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
+ let ?\<nu> = "\<lambda>A. ?P f A" and ?\<nu>' = "\<lambda>A. ?P f' A"
+ let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
interpret M: measure_space "M\<lparr> measure := ?\<nu>\<rparr>"
using borel(1) pos(1) by (rule measure_space_density) simp
have ac: "absolutely_continuous ?\<nu>"
@@ -957,7 +955,7 @@
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
- let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
+ let ?A = "\<lambda>i. Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
have "(\<Union>i. ?A i) \<in> null_sets"
proof (rule null_sets_UN)
fix i ::nat have "?A i \<in> sets M"
@@ -1079,7 +1077,7 @@
apply (rule_tac Int)
by (cases i) (auto intro: measurable_sets[OF f(1)]) }
note A_in_sets = this
- let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
+ let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
show "sigma_finite_measure ?N"
proof (default, intro exI conjI subsetI allI)
fix x assume "x \<in> range ?A"
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Feb 28 21:58:59 2012 +0100
@@ -214,7 +214,7 @@
then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
by auto
also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
- using `finite (sets M)` by (auto intro: finite_UN)
+ using `finite (sets M)` by auto
finally show "(\<Union>i. A i) \<in> sets M" .
qed
@@ -243,7 +243,7 @@
assumes "A`X \<subseteq> sets M"
shows "(\<Union>x\<in>X. A x) \<in> sets M"
proof -
- let "?A i" = "if i \<in> X then A i else {}"
+ let ?A = "\<lambda>i. if i \<in> X then A i else {}"
from assms have "range ?A \<subseteq> sets M" by auto
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
have "(\<Union>x. ?A x) \<in> sets M" by auto
@@ -1563,7 +1563,7 @@
unfolding sigma_algebra_eq_Int_stable Int_stable_def
proof (intro ballI)
fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
- let "?D E" = "\<lparr> space = space M,
+ let ?D = "\<lambda>E. \<lparr> space = space M,
sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
have "sets M \<subseteq> sets (?D B)"
proof
@@ -1637,7 +1637,7 @@
next
fix S assume "S \<subseteq> space (image_space X)"
then obtain S' where "S = X`S'" "S'\<in>sets M"
- by (auto simp: subset_image_iff sets_eq_Pow image_space_def)
+ by (auto simp: subset_image_iff image_space_def)
then show "S \<in> sets (image_space X)"
by (auto simp: image_space_def)
qed
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Feb 28 21:58:59 2012 +0100
@@ -82,7 +82,7 @@
assumes "dc \<in> dining_cryptographers"
shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
proof -
- let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])"
+ let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])"
have foldl_coin:
"\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
@@ -306,8 +306,8 @@
assumes "xs \<in> inversion ` dc_crypto"
shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
proof -
- let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
- let "?sets" = "{?set i | i. i < n}"
+ let ?set = "\<lambda>i. {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
+ let ?sets = "{?set i | i. i < n}"
have [simp]: "length xs = n" using assms
by (auto simp: dc_crypto inversion_def_raw)
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 28 21:58:59 2012 +0100
@@ -333,7 +333,7 @@
using `K k \<noteq> 0` by auto }
note t_eq_imp = this
- let "?S obs" = "t -`{t obs} \<inter> OB`msgs"
+ let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs"
{ fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
(\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
@@ -378,8 +378,8 @@
finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
note CP_T_eq_CP_O = this
- let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
- let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
+ let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
+ let ?Ht = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
{ fix obs assume obs: "obs \<in> OB`msgs"
have "?H obs = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"
--- a/src/Pure/Isar/element.ML Tue Feb 28 15:54:51 2012 +0100
+++ b/src/Pure/Isar/element.ML Tue Feb 28 21:58:59 2012 +0100
@@ -287,8 +287,8 @@
fun proof_local cmd goal_ctxt int after_qed' propss =
Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
- cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+ Proof.local_goal (Proof_Display.print_results Isabelle_Markup.state int) (K I)
+ Proof_Context.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
in
--- a/src/Pure/Isar/obtain.ML Tue Feb 28 15:54:51 2012 +0100
+++ b/src/Pure/Isar/obtain.ML Tue Feb 28 21:58:59 2012 +0100
@@ -299,7 +299,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results Isabelle_Markup.state int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
--- a/src/Pure/Isar/proof.ML Tue Feb 28 15:54:51 2012 +0100
+++ b/src/Pure/Isar/proof.ML Tue Feb 28 21:58:59 2012 +0100
@@ -991,7 +991,8 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
+ local_goal (Proof_Display.print_results Isabelle_Markup.state int)
+ prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
let
@@ -1003,7 +1004,8 @@
|> cat_lines;
fun print_results ctxt res =
- if ! testing then () else Proof_Display.print_results int ctxt res;
+ if ! testing then ()
+ else Proof_Display.print_results Isabelle_Markup.state int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
--- a/src/Pure/Isar/proof_display.ML Tue Feb 28 15:54:51 2012 +0100
+++ b/src/Pure/Isar/proof_display.ML Tue Feb 28 21:58:59 2012 +0100
@@ -17,7 +17,8 @@
val pretty_full_theory: bool -> theory -> Pretty.T
val print_theory: theory -> unit
val string_of_rule: Proof.context -> string -> thm -> string
- val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
+ val print_results: Markup.T -> bool -> Proof.context ->
+ ((string * string) * (string * thm list) list) -> unit
val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
end
@@ -100,16 +101,18 @@
in
-fun print_results do_print ctxt ((kind, name), facts) =
+fun print_results markup do_print ctxt ((kind, name), facts) =
if not do_print orelse kind = "" then ()
else if name = "" then
- Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
- else Pretty.writeln
- (case facts of
- [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
- Proof_Context.pretty_fact_aux ctxt false fact])
- | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
- Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
+ (Pretty.writeln o Pretty.mark markup)
+ (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+ else
+ (Pretty.writeln o Pretty.mark markup)
+ (case facts of
+ [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+ Proof_Context.pretty_fact_aux ctxt false fact])
+ | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+ Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
end;
--- a/src/Pure/Isar/specification.ML Tue Feb 28 15:54:51 2012 +0100
+++ b/src/Pure/Isar/specification.ML Tue Feb 28 21:58:59 2012 +0100
@@ -300,7 +300,7 @@
|> Attrib.partial_evaluation ctxt'
|> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
- val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
+ val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
in (res, lthy') end;
in
@@ -399,12 +399,12 @@
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
val lthy'' =
if Attrib.is_empty_binding (name, atts) then
- (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
+ (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
else
let
val ([(res_name, _)], lthy'') =
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
- val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
+ val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
in lthy'' end;
in after_qed results' lthy'' end;
in