diff -r 5dd7b89a16de -r 59b574c6f803 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 16:35:07 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 16:35:07 2013 +0100
@@ -76,9 +76,8 @@
 
 lemma finmap_of_eq_iff[simp]:
   assumes "finite i" "finite j"
-  shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> restrict m i = restrict n i"
-  using assms
-  apply (auto simp: finmap_eq_iff restrict_def) by metis
+  shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> (\<forall>k\<in>i. m k= n k)"
+  using assms by (auto simp: finmap_eq_iff)
 
 lemma finmap_of_inj_on_extensional_finite:
   assumes "finite K"
@@ -169,16 +168,7 @@
 begin
 
 definition dist_finmap where
-  "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
-    card ((domain P - domain Q) \<union> (domain Q - domain P))"
-
-lemma dist_finmap_extend:
-  assumes "finite X"
-  shows "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q \<union> X. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
-    card ((domain P - domain Q) \<union> (domain Q - domain P))"
-    unfolding dist_finmap_def add_right_cancel
-    using assms extensional_arb[of "(P)\<^isub>F"] extensional_arb[of "(Q)\<^isub>F" "domain Q"]
-    by (intro setsum_mono_zero_cong_left) auto
+  "dist P Q = Max (range (\<lambda>i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i))) + (if domain P = domain Q then 0 else 1)"
 
 definition open_finmap :: "('a \<Rightarrow>\<^isub>F 'b) set \<Rightarrow> bool" where
   "open_finmap S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
@@ -189,25 +179,45 @@
   shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
 using assms by auto
 
-lemma dist_le_1_imp_domain_eq:
-  assumes "dist P Q < 1"
-  shows "domain P = domain Q"
+lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^isub>F ` S)"
+  by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
+
+lemma finite_proj_image: "finite ((P)\<^isub>F ` S)"
+ by (cases "\<exists>x. x \<notin> domain P") (auto intro: finite_proj_image' finite_subset[where B="domain P"])
+
+lemma finite_proj_diag: "finite ((\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S)"
 proof -
-  have "0 \<le> (\<Sum>i\<in>domain P \<union> domain Q. dist (P i) (Q i))"
-    by (simp add: setsum_nonneg)
-  with assms have "card (domain P - domain Q \<union> (domain Q - domain P)) = 0"
-    unfolding dist_finmap_def by arith
-  thus "domain P = domain Q" by auto
+  have "(\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S = (\<lambda>(i, j). d i j) ` ((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S)" by auto
+  moreover have "((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S) \<subseteq> (\<lambda>i. (P)\<^isub>F i) ` S \<times> (\<lambda>i. (Q)\<^isub>F i) ` S" by auto
+  moreover have "finite \<dots>" using finite_proj_image[of P S] finite_proj_image[of Q S]
+    by (intro finite_cartesian_product) simp_all
+  ultimately show ?thesis by (simp add: finite_subset)
 qed
 
+lemma dist_le_1_imp_domain_eq:
+  shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
+  by (simp add: dist_finmap_def finite_proj_diag split: split_if_asm)
+
 lemma dist_proj:
   shows "dist ((x)\<^isub>F i) ((y)\<^isub>F i) \<le> dist x y"
 proof -
-  have "dist (x i) (y i) = (\<Sum>i\<in>{i}. dist (x i) (y i))" by simp
-  also have "\<dots> \<le> (\<Sum>i\<in>domain x \<union> domain y \<union> {i}. dist (x i) (y i))"
-    by (intro setsum_mono2) auto
-  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_extend[of "{i}"])
-  finally show ?thesis by simp
+  have "dist (x i) (y i) \<le> Max (range (\<lambda>i. dist (x i) (y i)))"
+    by (simp add: Max_ge_iff finite_proj_diag)
+  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_def)
+  finally show ?thesis .
+qed
+
+lemma dist_finmap_lessI:
+  assumes "domain P = domain Q" "0 < e" "\<And>i. i \<in> domain P \<Longrightarrow> dist (P i) (Q i) < e"
+  shows "dist P Q < e"
+proof -
+  have "dist P Q = Max (range (\<lambda>i. dist (P i) (Q i)))"
+    using assms by (simp add: dist_finmap_def finite_proj_diag)
+  also have "\<dots> < e"
+  proof (subst Max_less_iff, safe)
+    fix i show "dist ((P)\<^isub>F i) ((Q)\<^isub>F i) < e" using assms by (cases "i \<in> domain P") simp_all
+  qed (simp add: finite_proj_diag)
+  finally show ?thesis .
 qed
 
 lemma open_Pi'I:
@@ -266,24 +276,25 @@
     unfolding open_finmap_def ..
 next
   fix P Q::"'a \<Rightarrow>\<^isub>F 'b"
+  have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
+    by (metis Max.in_idem Max_in max_def min_max.sup.commute order_refl)
   show "dist P Q = 0 \<longleftrightarrow> P = Q"
-    by (auto simp: finmap_eq_iff dist_finmap_def setsum_nonneg setsum_nonneg_eq_0_iff)
+    by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+      intro!: Max_eqI image_eqI[where x=undefined])
 next
   fix P Q R::"'a \<Rightarrow>\<^isub>F 'b"
-  let ?symdiff = "\<lambda>a b. domain a - domain b \<union> (domain b - domain a)"
-  def E \<equiv> "domain P \<union> domain Q \<union> domain R"
-  hence "finite E" by (simp add: E_def)
-  have "card (?symdiff P Q) \<le> card (?symdiff P R \<union> ?symdiff Q R)"
-    by (auto intro: card_mono)
-  also have "\<dots> \<le> card (?symdiff P R) + card (?symdiff Q R)"
-    by (subst card_Un_Int) auto
-  finally have "dist P Q \<le> (\<Sum>i\<in>E. dist (P i) (R i) + dist (Q i) (R i)) +
-    real (card (?symdiff P R) + card (?symdiff Q R))"
-    unfolding dist_finmap_extend[OF `finite E`]
-    by (intro add_mono) (auto simp: E_def intro: setsum_mono dist_triangle_le)
-  also have "\<dots> \<le> dist P R + dist Q R"
-    unfolding dist_finmap_extend[OF `finite E`] by (simp add: ac_simps E_def setsum_addf[symmetric])
-  finally show "dist P Q \<le> dist P R + dist Q R" by simp
+  let ?dists = "\<lambda>P Q i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)"
+  let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R"
+  let ?dom = "\<lambda>P Q. (if domain P = domain Q then 0 else 1::real)"
+  have "dist P Q = Max (range ?dpq) + ?dom P Q"
+    by (simp add: dist_finmap_def)
+  also obtain t where "t \<in> range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag)
+  then obtain i where "Max (range ?dpq) = ?dpq i" by auto
+  also have "?dpq i \<le> ?dpr i + ?dqr i" by (rule dist_triangle2)
+  also have "?dpr i \<le> Max (range ?dpr)" by (simp add: finite_proj_diag)
+  also have "?dqr i \<le> Max (range ?dqr)" by (simp add: finite_proj_diag)
+  also have "?dom P Q \<le> ?dom P R + ?dom Q R" by simp
+  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps)
 qed
 
 end
@@ -353,26 +364,27 @@
 
 subsection {* Complete Space of Finite Maps *}
 
-lemma tendsto_dist_zero:
-  assumes "(\<lambda>i. dist (f i) g) ----> 0"
-  shows "f ----> g"
-  using assms by (auto simp: tendsto_iff dist_real_def)
-
-lemma tendsto_dist_zero':
-  assumes "(\<lambda>i. dist (f i) g) ----> x"
-  assumes "0 = x"
-  shows "f ----> g"
-  using assms tendsto_dist_zero by simp
-
 lemma tendsto_finmap:
   fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^isub>F ('a::metric_space))"
   assumes ind_f:  "\<And>n. domain (f n) = domain g"
   assumes proj_g:  "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i"
   shows "f ----> g"
-  apply (rule tendsto_dist_zero')
-  unfolding dist_finmap_def assms
-  apply (rule tendsto_intros proj_g | simp)+
-  done
+  unfolding tendsto_iff
+proof safe
+  fix e::real assume "0 < e"
+  let ?dists = "\<lambda>x i. dist ((f x)\<^isub>F i) ((g)\<^isub>F i)"
+  have "eventually (\<lambda>x. \<forall>i\<in>domain g. ?dists x i < e) sequentially"
+    using finite_domain[of g] proj_g
+  proof induct
+    case (insert i G)
+    with `0 < e` have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff)
+    moreover
+    from insert have "eventually (\<lambda>x. \<forall>i\<in>G. dist ((f x)\<^isub>F i) ((g)\<^isub>F i) < e) sequentially" by simp
+    ultimately show ?case by eventually_elim auto
+  qed simp
+  thus "eventually (\<lambda>x. dist (f x) g < e) sequentially"
+    by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f `0 < e`)
+qed
 
 instance finmap :: (type, complete_space) complete_space
 proof
@@ -412,34 +424,27 @@
   have "P ----> Q"
   proof (rule metric_LIMSEQ_I)
     fix e::real assume "0 < e"
-    def e' \<equiv> "min 1 (e / (card d + 1))"
-    hence "0 < e'" using `0 < e` by (auto simp: e'_def intro: divide_pos_pos)
-    have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e'"
+    have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e"
     proof (safe intro!: bchoice)
       fix i assume "i \<in> d"
-      from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e'`]
-      show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e'" .
+      from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e`]
+      show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" .
     qed then guess ni .. note ni = this
     def N \<equiv> "max Nd (Max (ni ` d))"
     show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e"
     proof (safe intro!: exI[where x="N"])
       fix n assume "N \<le> n"
-      hence "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
+      hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
         using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse)
-      hence "dist (P n) Q = (\<Sum>i\<in>d. dist ((P n) i) (Q i))" by (simp add: dist_finmap_def)
-      also have "\<dots> \<le> (\<Sum>i\<in>d. e')"
-      proof (intro setsum_mono less_imp_le)
-        fix i assume "i \<in> d"
-        hence "ni i \<le> Max (ni ` d)" by simp
+      show "dist (P n) Q < e"
+      proof (rule dist_finmap_lessI[OF dom(3) `0 < e`])
+        fix i
+        assume "i \<in> domain (P n)"
+        hence "ni i \<le> Max (ni ` d)" using dom by simp
         also have "\<dots> \<le> N" by (simp add: N_def)
-        also have "\<dots> \<le> n" using `N \<le> n` .
-        finally
-        show "dist ((P n) i) (Q i) < e'"
-          using ni `i \<in> d` by (auto simp: p_def q N_def)
+        finally show "dist ((P n)\<^isub>F i) ((Q)\<^isub>F i) < e" using ni `i \<in> domain (P n)` `N \<le> n` dom
+          by (auto simp: p_def q N_def less_imp_le)
       qed
-      also have "\<dots> = card d * e'" by (simp add: real_eq_of_nat)
-      also have "\<dots> < e" using `0 < e` by (simp add: e'_def field_simps min_def)
-      finally show "dist (P n) Q < e" .
     qed
   qed
   thus "convergent P" by (auto simp: convergent_def)
@@ -489,16 +494,14 @@
   fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
   assume "open O'" "x \<in> O'"
   then obtain e where e: "e > 0" "\<And>y. dist y x < e \<Longrightarrow> y \<in> O'"  unfolding open_dist by blast
-  def e' \<equiv> "e / (card (domain x) + 1)"
-
   have "\<exists>B.
-    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> ball (x i) e' \<and> B i \<in> union_closed_basis)"
+    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> ball (x i) e \<and> B i \<in> union_closed_basis)"
   proof (rule bchoice, safe)
     fix i assume "i \<in> domain x"
-    have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
-      by (auto simp add: e'_def intro!: divide_pos_pos)
+    have "open (ball (x i) e)" "x i \<in> ball (x i) e" using e
+      by (auto simp add: intro!: divide_pos_pos)
     from topological_basisE[OF basis_union_closed_basis this] guess b' .
-    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
+    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e \<and> y \<in> union_closed_basis" by auto
   qed
   then guess B .. note B = this
   def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
@@ -507,24 +510,16 @@
   moreover have "x \<in> B'" unfolding B'_def using B by auto
   moreover have "B' \<subseteq> O'"
   proof
-    fix y assume "y \<in> B'" with B have "domain y = domain x" unfolding B'_def
+    fix y assume "y \<in> B'" with B have dom: "domain y = domain x" unfolding B'_def
       by (simp add: Pi'_def)
     show "y \<in> O'"
-    proof (rule e)
-      have "dist y x = (\<Sum>i \<in> domain x. dist (y i) (x i))"
-        using `domain y = domain x` by (simp add: dist_finmap_def)
-      also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
-      proof (rule setsum_mono)
-        fix i assume "i \<in> domain x"
-        with `y \<in> B'` B have "y i \<in> B i"
-          by (simp add: Pi'_def B'_def)
-        hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
-          by force
-        thus "dist (y i) (x i) \<le> e'" by (simp add: dist_commute)
-      qed
-      also have "\<dots> = card (domain x) * e'" by (simp add: real_eq_of_nat)
-      also have "\<dots> < e" using e by (simp add: e'_def field_simps)
-      finally show "dist y x < e" .
+    proof (rule e, rule dist_finmap_lessI[OF dom `0 < e`])
+      fix i assume "i \<in> domain y"
+      with `y \<in> B'` B have "y i \<in> B i"
+        by (simp add: Pi'_def B'_def)
+      hence "y i \<in> ball (x i) e" using B `domain y = domain x` `i \<in> domain y`
+        by force
+      thus "dist (y i) (x i) < e" by (simp add: dist_commute)
     qed
   qed
   ultimately