--- a/src/HOL/Probability/Borel.thy Wed Mar 10 15:38:33 2010 -0800
+++ b/src/HOL/Probability/Borel.thy Wed Mar 10 15:57:01 2010 -0800
@@ -186,20 +186,20 @@
definition
nat_to_rat_surj :: "nat \<Rightarrow> rat" where
- "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
- in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
+ "nat_to_rat_surj n = (let (i,j) = prod_decode n
+ in Fract (int_decode i) (int_decode j))"
lemma nat_to_rat_surj: "surj nat_to_rat_surj"
proof (auto simp add: surj_def nat_to_rat_surj_def)
fix y
- show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
+ show "\<exists>x. y = (\<lambda>(i, j). Fract (int_decode i) (int_decode j)) (prod_decode x)"
proof (cases y)
case (Fract a b)
- obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
+ obtain i where i: "int_decode i = a" using surj_int_decode
by (metis surj_def)
- obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
+ obtain j where j: "int_decode j = b" using surj_int_decode
by (metis surj_def)
- obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
+ obtain n where n: "prod_decode n = (i,j)" using surj_prod_decode
by (metis surj_def)
from Fract i j n show ?thesis
--- a/src/HOL/Probability/Caratheodory.thy Wed Mar 10 15:38:33 2010 -0800
+++ b/src/HOL/Probability/Caratheodory.thy Wed Mar 10 15:57:01 2010 -0800
@@ -816,9 +816,9 @@
by (simp add: eqe)
finally show ?thesis using Series.summable_le2 [OF 1 2] by auto
qed
- def C \<equiv> "(split BB) o nat_to_nat2"
+ def C \<equiv> "(split BB) o prod_decode"
have C: "!!n. C n \<in> sets M"
- apply (rule_tac p="nat_to_nat2 n" in PairE)
+ apply (rule_tac p="prod_decode n" in PairE)
apply (simp add: C_def)
apply (metis BB subsetD rangeI)
done
@@ -828,11 +828,10 @@
assume x: "x \<in> A i"
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
- thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
- by (metis nat_to_nat2_surj internal_split_def prod.cases
- prod_case_split surj_f_inv_f)
+ thus "\<exists>i. x \<in> split BB (prod_decode i)"
+ by (metis prod_encode_inverse prod.cases prod_case_split)
qed
- have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
+ have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
also have "... sums suminf ll"
proof (rule suminf_2dimen)
--- a/src/HOL/Probability/SeriesPlus.thy Wed Mar 10 15:38:33 2010 -0800
+++ b/src/HOL/Probability/SeriesPlus.thy Wed Mar 10 15:57:01 2010 -0800
@@ -1,5 +1,5 @@
theory SeriesPlus
- imports Complex_Main Nat_Int_Bij
+ imports Complex_Main Nat_Bijection
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -16,7 +16,7 @@
assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
and sumg: "summable g"
- shows "(f o nat_to_nat2) sums suminf g"
+ shows "(f o prod_decode) sums suminf g"
proof (simp add: sums_def)
{
fix x
@@ -31,18 +31,18 @@
thus "0 \<le> g m" using fsums [of m]
by (auto simp add: sums_iff)
qed
- show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
+ show "(\<lambda>n. \<Sum>x = 0..<n. f (prod_decode x)) ----> suminf g"
proof (rule increasing_LIMSEQ, simp add: f_nneg)
fix n
- def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
- def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
- have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
+ def i \<equiv> "Max (Domain (prod_decode ` {0..<n}))"
+ def j \<equiv> "Max (Range (prod_decode ` {0..<n}))"
+ have ij: "prod_decode ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
by (force simp add: i_def j_def
intro: finite_imageI Max_ge finite_Domain finite_Range)
- have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})"
- using setsum_reindex [of nat_to_nat2 "{0..<n}" f]
+ have "(\<Sum>x = 0..<n. f (prod_decode x)) = setsum f (prod_decode ` {0..<n})"
+ using setsum_reindex [of prod_decode "{0..<n}" f]
by (simp add: o_def)
- (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj)
+ (metis inj_prod_decode inj_prod_decode)
also have "... \<le> setsum f ({0..i} \<times> {0..j})"
by (rule setsum_mono2) (auto simp add: ij)
also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
@@ -56,10 +56,10 @@
by (auto simp add: sums_iff)
(metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
qed
- finally have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
+ finally have "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> setsum g {0..<Suc i}" .
also have "... \<le> suminf g"
by (rule series_pos_le [OF sumg]) (simp add: g_nneg)
- finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
+ finally show "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> suminf g" .
next
fix e :: real
assume e: "0 < e"
@@ -99,26 +99,25 @@
by auto
have finite_IJ: "finite IJ"
by (simp add: IJ_def)
- def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
- have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
+ def NIJ \<equiv> "Max (prod_decode -` IJ)"
+ have IJsb: "IJ \<subseteq> prod_decode ` {0..NIJ}"
proof (auto simp add: NIJ_def)
fix i j
assume ij:"(i,j) \<in> IJ"
- hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
- by (metis nat_to_nat2_surj surj_f_inv_f)
- thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+ hence "(i,j) = prod_decode (prod_encode (i,j))"
+ by simp
+ thus "(i,j) \<in> prod_decode ` {0..Max (prod_decode -` IJ)}"
by (rule image_eqI)
- (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
- nat_to_nat2_surj surj_f_inv_f)
+ (simp add: ij finite_vimageI [OF finite_IJ inj_prod_decode])
qed
- have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
+ have "setsum f IJ \<le> setsum f (prod_decode `{0..NIJ})"
by (rule setsum_mono2) (auto simp add: IJsb)
- also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
- by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV])
- also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
+ also have "... = (\<Sum>k = 0..NIJ. f (prod_decode k))"
+ by (simp add: setsum_reindex inj_prod_decode)
+ also have "... = (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))"
by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
- finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
- thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
+ finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))" .
+ thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (prod_decode x)) + e" using glessf
by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
qed
qed