# HG changeset patch
# User huffman
# Date 1268265421 28800
# Node ID 5007843dae335a830f60aab07fec35b583dd26d5
# Parent  29cb504abbb540e824ebcd8f8a4a1b11e93eb1bc
convert HOL-Probability to use Nat_Bijection library

diff -r 29cb504abbb5 -r 5007843dae33 src/HOL/Probability/Borel.thy
--- 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
diff -r 29cb504abbb5 -r 5007843dae33 src/HOL/Probability/Caratheodory.thy
--- 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)
diff -r 29cb504abbb5 -r 5007843dae33 src/HOL/Probability/SeriesPlus.thy
--- 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