# HG changeset patch
# User wenzelm
# Date 1272977070 -7200
# Node ID 30bd207ec222863d36e723f010680c76750f3bbd
# Parent  4482c4a2cb727ffe16b02db3c68c9f38a4df86a6# Parent  2fd4e2c766366b47817634c23688358969fdf2c6
merged

diff -r 2fd4e2c76636 -r 30bd207ec222 NEWS
--- a/NEWS	Tue May 04 14:38:59 2010 +0200
+++ b/NEWS	Tue May 04 14:44:30 2010 +0200
@@ -89,6 +89,9 @@
 
 *** Pure ***
 
+* Predicates of locales introduces by classes carry a mandatory "class"
+prefix.  INCOMPATIBILITY.
+
 * 'code_reflect' allows to incorporate generated ML code into
 runtime environment;  replaces immature code_datatype antiquotation.
 INCOMPATIBILITY.
@@ -137,6 +140,9 @@
 
 *** HOL ***
 
+* Theory 'Finite_Set': various folding_* locales facilitate the application
+of the various fold combinators on finite sets.
+
 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
 provides abstract red-black tree type which is backed by RBT_Impl
 as implementation.  INCOMPATIBILTY.
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Tue May 04 14:44:30 2010 +0200
@@ -9,8 +9,6 @@
 
 section "error free"
  
-hide_const field
-
 lemma error_free_halloc:
   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
           error_free_s0: "error_free s0"
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Tue May 04 14:44:30 2010 +0200
@@ -33,7 +33,7 @@
 text {* for ad-hoc proofs for @{const fold_image} *}
 
 lemma (in comm_monoid_add) comm_monoid_mult:
-  "comm_monoid_mult (op +) 0"
+  "class.comm_monoid_mult (op +) 0"
 proof qed (auto intro: add_assoc add_commute)
 
 notation times (infixl "*" 70)
@@ -554,6 +554,26 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
+lemma setsum_nonneg_leq_bound:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
+  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
+  shows "f i \<le> B"
+proof -
+  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
+    using assms by (auto intro!: setsum_nonneg)
+  moreover
+  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
+    using assms by (simp add: setsum_diff1)
+  ultimately show ?thesis by auto
+qed
+
+lemma setsum_nonneg_0:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
+  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
+  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
+  shows "f i = 0"
+  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
+
 lemma setsum_mono2:
 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
@@ -1180,7 +1200,8 @@
 context semilattice_inf
 begin
 
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+  "class.ab_semigroup_idem_mult inf"
 proof qed (rule inf_assoc inf_commute inf_idem)+
 
 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1250,7 +1271,7 @@
 context semilattice_sup
 begin
 
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
 
 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1470,15 +1491,15 @@
   using assms by (rule Max.hom_commute)
 
 lemma ab_semigroup_idem_mult_min:
-  "ab_semigroup_idem_mult min"
+  "class.ab_semigroup_idem_mult min"
   proof qed (auto simp add: min_def)
 
 lemma ab_semigroup_idem_mult_max:
-  "ab_semigroup_idem_mult max"
+  "class.ab_semigroup_idem_mult max"
   proof qed (auto simp add: max_def)
 
 lemma max_lattice:
-  "semilattice_inf (op \<ge>) (op >) max"
+  "class.semilattice_inf (op \<ge>) (op >) max"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max:
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue May 04 14:44:30 2010 +0200
@@ -33,8 +33,8 @@
 begin
 
 lemma dual_complete_lattice:
-  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+  "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
     (unfold_locales, (fact bot_least top_greatest
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 14:44:30 2010 +0200
@@ -265,7 +265,7 @@
 lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
 lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Divides.thy	Tue May 04 14:44:30 2010 +0200
@@ -379,6 +379,8 @@
 class ring_div = semiring_div + comm_ring_1
 begin
 
+subclass ring_1_no_zero_divisors ..
+
 text {* Negation respects modular equivalence. *}
 
 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 04 14:44:30 2010 +0200
@@ -509,13 +509,8 @@
 
 subsection {* Class @{text finite}  *}
 
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
 begin
 
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
@@ -1734,12 +1729,10 @@
 qed
 
 lemma insert [simp]:
-  assumes "finite A" and "x \<notin> A"
-  shows "F (insert x A) = (if A = {} then x else x * F A)"
-proof (cases "A = {}")
-  case True then show ?thesis by simp
-next
-  case False then obtain b where "b \<in> A" by blast
+  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
+  shows "F (insert x A) = x * F A"
+proof -
+  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
   with `finite A` have "finite B" by simp
   interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
@@ -1833,8 +1826,6 @@
     (simp_all add: assoc in_idem `finite A`)
 qed
 
-declare insert [simp del]
-
 lemma eq_fold_idem':
   assumes "finite A"
   shows "F (insert a A) = fold (op *) a A"
@@ -1844,13 +1835,13 @@
 qed
 
 lemma insert_idem [simp]:
-  assumes "finite A"
-  shows "F (insert x A) = (if A = {} then x else x * F A)"
+  assumes "finite A" and "A \<noteq> {}"
+  shows "F (insert x A) = x * F A"
 proof (cases "x \<in> A")
-  case False with `finite A` show ?thesis by (rule insert)
+  case False from `finite A` `x \<notin> A` `A \<noteq> {}` show ?thesis by (rule insert)
 next
-  case True then have "A \<noteq> {}" by auto
-  with `finite A` show ?thesis by (simp add: in_idem insert_absorb True)
+  case True
+  from `finite A` `A \<noteq> {}` show ?thesis by (simp add: in_idem insert_absorb True)
 qed
   
 lemma union_idem:
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/HOL.thy	Tue May 04 14:44:30 2010 +0200
@@ -1493,7 +1493,7 @@
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
-        @{thms induct_rulify_fallback induct_true_def induct_false_def})))
+        @{thms induct_rulify_fallback})))
     addsimprocs
       [Simplifier.simproc @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
@@ -1886,7 +1886,6 @@
 *}
 
 hide_const (open) eq
-hide_const eq
 
 text {* Cases *}
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 14:44:30 2010 +0200
@@ -27,18 +27,19 @@
 
 types 'a sem = "'a => 'a => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (%s s'. s ~: b & (s=s'))"
-"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) s (f s)"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) s s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (s' = f s)"
-"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s  : b --> Sem c1 s s') &
-                                      (s ~: b --> Sem c2 s s'))"
-"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
@@ -209,19 +210,18 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (auto simp:Valid_def)
 
-lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+    s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply (clarsimp simp:Valid_def)
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 14:44:30 2010 +0200
@@ -25,22 +25,23 @@
 
 types 'a sem = "'a option => 'a option => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
-"iter (Suc n) b S =
-  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) None None"
+| "Sem (Basic f) (Some s) (Some (f s))"
+| "Sem Abort s None"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "Sem (IF b THEN c1 ELSE c2 FI) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem (While b x c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) (Some s) s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
-"Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' =
- (case s of None \<Rightarrow> s' = None
-  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
-"Sem(While b x c) s s' =
- (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
@@ -212,23 +213,20 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastsimp simp:Valid_def image_def)
 
-lemma iter_aux:
- "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
-  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
-apply(unfold image_def)
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+    s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply(simp add:Valid_def)
 apply(simp (no_asm) add:image_def)
 apply clarify
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 14:44:30 2010 +0200
@@ -216,6 +216,9 @@
   and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
 unfolding noteq_refs_def noteq_arrs_def by auto
 
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+  unfolding noteq_refs_def by auto
+
 lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
   by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Lattices.thy	Tue May 04 14:44:30 2010 +0200
@@ -67,8 +67,8 @@
 text {* Dual lattice *}
 
 lemma dual_semilattice:
-  "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+  "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
 
 end
@@ -235,8 +235,8 @@
 begin
 
 lemma dual_lattice:
-  "lattice (op \<ge>) (op >) sup inf"
-  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+  "class.lattice (op \<ge>) (op >) sup inf"
+  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -347,8 +347,8 @@
 by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
-  "distrib_lattice (op \<ge>) (op >) sup inf"
-  by (rule distrib_lattice.intro, rule dual_lattice)
+  "class.distrib_lattice (op \<ge>) (op >) sup inf"
+  by (rule class.distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
 lemmas sup_inf_distrib =
@@ -419,7 +419,7 @@
 begin
 
 lemma dual_bounded_lattice:
-  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
 
 end
@@ -431,8 +431,8 @@
 begin
 
 lemma dual_boolean_algebra:
-  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
 lemma compl_inf_bot:
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Library/Convex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Convex.thy	Tue May 04 14:44:30 2010 +0200
@@ -0,0 +1,610 @@
+theory Convex
+imports Product_Vector
+begin
+
+subsection {* Convexity. *}
+
+definition
+  convex :: "'a::real_vector set \<Rightarrow> bool" where
+  "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
+
+lemma convex_alt:
+  "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
+  (is "_ \<longleftrightarrow> ?alt")
+proof
+  assume alt[rule_format]: ?alt
+  { fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s"
+    assume "0 \<le> u" "0 \<le> v" "u + v = 1"
+    moreover hence "u = 1 - v" by auto
+    ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto }
+  thus "convex s" unfolding convex_def by auto
+qed (auto simp: convex_def)
+
+lemma mem_convex:
+  assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
+  shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
+  using assms unfolding convex_alt by auto
+
+lemma convex_empty[intro]: "convex {}"
+  unfolding convex_def by simp
+
+lemma convex_singleton[intro]: "convex {a}"
+  unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric])
+
+lemma convex_UNIV[intro]: "convex UNIV"
+  unfolding convex_def by auto
+
+lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
+  unfolding convex_def by auto
+
+lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
+  unfolding convex_def by auto
+
+lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
+  unfolding convex_def
+  by (auto simp: inner_add inner_scaleR intro!: convex_bound_le)
+
+lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
+proof -
+  have *:"{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
+  show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
+qed
+
+lemma convex_hyperplane: "convex {x. inner a x = b}"
+proof-
+  have *:"{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
+  show ?thesis using convex_halfspace_le convex_halfspace_ge
+    by (auto intro!: convex_Int simp: *)
+qed
+
+lemma convex_halfspace_lt: "convex {x. inner a x < b}"
+  unfolding convex_def
+  by (auto simp: convex_bound_lt inner_add)
+
+lemma convex_halfspace_gt: "convex {x. inner a x > b}"
+   using convex_halfspace_lt[of "-a" "-b"] by auto
+
+lemma convex_real_interval:
+  fixes a b :: "real"
+  shows "convex {a..}" and "convex {..b}"
+  and "convex {a<..}" and "convex {..<b}"
+  and "convex {a..b}" and "convex {a<..b}"
+  and "convex {a..<b}" and "convex {a<..<b}"
+proof -
+  have "{a..} = {x. a \<le> inner 1 x}" by auto
+  thus 1: "convex {a..}" by (simp only: convex_halfspace_ge)
+  have "{..b} = {x. inner 1 x \<le> b}" by auto
+  thus 2: "convex {..b}" by (simp only: convex_halfspace_le)
+  have "{a<..} = {x. a < inner 1 x}" by auto
+  thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt)
+  have "{..<b} = {x. inner 1 x < b}" by auto
+  thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt)
+  have "{a..b} = {a..} \<inter> {..b}" by auto
+  thus "convex {a..b}" by (simp only: convex_Int 1 2)
+  have "{a<..b} = {a<..} \<inter> {..b}" by auto
+  thus "convex {a<..b}" by (simp only: convex_Int 3 2)
+  have "{a..<b} = {a..} \<inter> {..<b}" by auto
+  thus "convex {a..<b}" by (simp only: convex_Int 1 4)
+  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
+  thus "convex {a<..<b}" by (simp only: convex_Int 3 4)
+qed
+
+subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
+
+lemma convex_setsum:
+  fixes C :: "'a::real_vector set"
+  assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
+  shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C"
+using assms
+proof (induct s arbitrary:a rule:finite_induct)
+  case empty thus ?case by auto
+next
+  case (insert i s) note asms = this
+  { assume "a i = 1"
+    hence "(\<Sum> j \<in> s. a j) = 0"
+      using asms by auto
+    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
+      using setsum_nonneg_0[where 'b=real] asms by fastsimp
+    hence ?case using asms by auto }
+  moreover
+  { assume asm: "a i \<noteq> 1"
+    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
+    have fis: "finite (insert i s)" using asms by auto
+    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp
+    hence "a i < 1" using asm by auto
+    hence i0: "1 - a i > 0" by auto
+    let "?a j" = "a j / (1 - a i)"
+    { fix j assume "j \<in> s"
+      hence "?a j \<ge> 0"
+        using i0 asms divide_nonneg_pos
+        by fastsimp } note a_nonneg = this
+    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
+    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    from this asms
+    have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
+    hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
+      using asms[unfolded convex_def, rule_format] yai ai1 by auto
+    hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C"
+      using scaleR_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j *\<^sub>R y j" s] by auto
+    hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" using i0 by auto
+    hence ?case using setsum.insert asms by auto }
+  ultimately show ?case by auto
+qed
+
+lemma convex:
+  shows "convex s \<longleftrightarrow> (\<forall>(k::nat) u x. (\<forall>i. 1\<le>i \<and> i\<le>k \<longrightarrow> 0 \<le> u i \<and> x i \<in>s) \<and> (setsum u {1..k} = 1)
+           \<longrightarrow> setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)"
+proof safe
+  fix k :: nat fix u :: "nat \<Rightarrow> real" fix x
+  assume "convex s"
+    "\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s"
+    "setsum u {1..k} = 1"
+  from this convex_setsum[of "{1 .. k}" s]
+  show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto
+next
+  assume asm: "\<forall>k u x. (\<forall> i :: nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1
+    \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s"
+  { fix \<mu> :: real fix x y :: 'a assume xy: "x \<in> s" "y \<in> s" assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1"
+    let "?u i" = "if (i :: nat) = 1 then \<mu> else 1 - \<mu>"
+    let "?x i" = "if (i :: nat) = 1 then x else y"
+    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}" by auto
+    hence card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1" by simp
+    hence "setsum ?u {1 .. 2} = 1"
+      using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
+      by auto
+    from this asm[rule_format, of "2" ?u ?x]
+    have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s"
+      using mu xy by auto
+    have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
+      using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
+    from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
+    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y" by auto
+    hence "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute) }
+  thus "convex s" unfolding convex_alt by auto
+qed
+
+
+lemma convex_explicit:
+  fixes s :: "'a::real_vector set"
+  shows "convex s \<longleftrightarrow>
+  (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"
+proof safe
+  fix t fix u :: "'a \<Rightarrow> real"
+  assume "convex s" "finite t"
+    "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
+  thus "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+    using convex_setsum[of t s u "\<lambda> x. x"] by auto
+next
+  assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x)
+    \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+  show "convex s"
+    unfolding convex_alt
+  proof safe
+    fix x y fix \<mu> :: real
+    assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1"
+    { assume "x \<noteq> y"
+      hence "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
+        using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"]
+          asm by auto }
+    moreover
+    { assume "x = y"
+      hence "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
+        using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"]
+          asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) }
+    ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast
+  qed
+qed
+
+lemma convex_finite: assumes "finite s"
+  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
+                      \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
+  unfolding convex_explicit
+proof (safe elim!: conjE)
+  fix t u assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
+    and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
+  have *:"s \<inter> t = t" using as(2) by auto
+  have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)" by simp
+  show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+   using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as *
+   by (auto simp: assms setsum_cases if_distrib if_distrib_arg)
+qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
+
+definition
+  convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
+  "convex_on s f \<longleftrightarrow>
+  (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
+
+lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
+  unfolding convex_on_def by auto
+
+lemma convex_add[intro]:
+  assumes "convex_on s f" "convex_on s g"
+  shows "convex_on s (\<lambda>x. f x + g x)"
+proof-
+  { fix x y assume "x\<in>s" "y\<in>s" moreover
+    fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
+    ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)"
+      using assms unfolding convex_on_def by (auto simp add:add_mono)
+    hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps)  }
+  thus ?thesis unfolding convex_on_def by auto
+qed
+
+lemma convex_cmul[intro]:
+  assumes "0 \<le> (c::real)" "convex_on s f"
+  shows "convex_on s (\<lambda>x. c * f x)"
+proof-
+  have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
+  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
+qed
+
+lemma convex_lower:
+  assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"
+  shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
+proof-
+  let ?m = "max (f x) (f y)"
+  have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
+    using assms(4,5) by(auto simp add: mult_mono1 add_mono)
+  also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
+  finally show ?thesis
+    using assms unfolding convex_on_def by fastsimp
+qed
+
+lemma convex_distance[intro]:
+  fixes s :: "'a::real_normed_vector set"
+  shows "convex_on s (\<lambda>x. dist a x)"
+proof(auto simp add: convex_on_def dist_norm)
+  fix x y assume "x\<in>s" "y\<in>s"
+  fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
+  have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp
+  hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
+    by (auto simp add: algebra_simps)
+  show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
+    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
+    using `0 \<le> u` `0 \<le> v` by auto
+qed
+
+subsection {* Arithmetic operations on sets preserve convexity. *}
+lemma convex_scaling:
+  assumes "convex s"
+  shows"convex ((\<lambda>x. c *\<^sub>R x) ` s)"
+using assms unfolding convex_def image_iff
+proof safe
+  fix x xa y xb :: "'a::real_vector" fix u v :: real
+  assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
+    "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  show "\<exists>x\<in>s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x"
+    using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps)
+qed
+
+lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"
+using assms unfolding convex_def image_iff
+proof safe
+  fix x xa y xb :: "'a::real_vector" fix u v :: real
+  assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
+    "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  show "\<exists>x\<in>s. u *\<^sub>R - xa + v *\<^sub>R - xb = - x"
+    using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto
+qed
+
+lemma convex_sums:
+  assumes "convex s" "convex t"
+  shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
+using assms unfolding convex_def image_iff
+proof safe
+  fix xa xb ya yb assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"
+  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
+  show "\<exists>x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \<and> x \<in> s \<and> y \<in> t"
+    using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"]
+      assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib)
+qed
+
+lemma convex_differences:
+  assumes "convex s" "convex t"
+  shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
+proof -
+  have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
+  proof safe
+    fix x x' y assume "x' \<in> s" "y \<in> t"
+    thus "\<exists>x y'. x' - y = x + y' \<and> x \<in> s \<and> y' \<in> uminus ` t"
+      using exI[of _ x'] exI[of _ "-y"] by auto
+  next
+    fix x x' y y' assume "x' \<in> s" "y' \<in> t"
+    thus "\<exists>x y. x' + - y' = x - y \<and> x \<in> s \<and> y \<in> t"
+      using exI[of _ x'] exI[of _ y'] by auto
+  qed
+  thus ?thesis using convex_sums[OF assms(1)  convex_negations[OF assms(2)]] by auto
+qed
+
+lemma convex_translation: assumes "convex s" shows "convex ((\<lambda>x. a + x) ` s)"
+proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
+  thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed
+
+lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
+  thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
+
+lemma convex_linear_image:
+  assumes c:"convex s" and l:"bounded_linear f"
+  shows "convex(f ` s)"
+proof(auto simp add: convex_def)
+  interpret f: bounded_linear f by fact
+  fix x y assume xy:"x \<in> s" "y \<in> s"
+  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
+  show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
+    using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR
+      c[unfolded convex_def] xy uv by auto
+qed
+
+
+lemma pos_is_convex:
+  shows "convex {0 :: real <..}"
+unfolding convex_alt
+proof safe
+  fix y x \<mu> :: real
+  assume asms: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
+  { assume "\<mu> = 0"
+    hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y" by simp
+    hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+  moreover
+  { assume "\<mu> = 1"
+    hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms by simp }
+  moreover
+  { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
+    hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
+    hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
+      using add_nonneg_pos[of "\<mu> *\<^sub>R x" "(1 - \<mu>) *\<^sub>R y"]
+        real_mult_order by auto fastsimp }
+  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
+qed
+
+lemma convex_on_setsum:
+  fixes a :: "'a \<Rightarrow> real"
+  fixes y :: "'a \<Rightarrow> 'b::real_vector"
+  fixes f :: "'b \<Rightarrow> real"
+  assumes "finite s" "s \<noteq> {}"
+  assumes "convex_on C f"
+  assumes "convex C"
+  assumes "(\<Sum> i \<in> s. a i) = 1"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
+  shows "f (\<Sum> i \<in> s. a i *\<^sub>R y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
+using assms
+proof (induct s arbitrary:a rule:finite_ne_induct)
+  case (singleton i)
+  hence ai: "a i = 1" by auto
+  thus ?case by auto
+next
+  case (insert i s) note asms = this
+  hence "convex_on C f" by simp
+  from this[unfolded convex_on_def, rule_format]
+  have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk>
+  \<Longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+    by simp
+  { assume "a i = 1"
+    hence "(\<Sum> j \<in> s. a j) = 0"
+      using asms by auto
+    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
+      using setsum_nonneg_0[where 'b=real] asms by fastsimp
+    hence ?case using asms by auto }
+  moreover
+  { assume asm: "a i \<noteq> 1"
+    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
+    have fis: "finite (insert i s)" using asms by auto
+    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp
+    hence "a i < 1" using asm by auto
+    hence i0: "1 - a i > 0" by auto
+    let "?a j" = "a j / (1 - a i)"
+    { fix j assume "j \<in> s"
+      hence "?a j \<ge> 0"
+        using i0 asms divide_nonneg_pos
+        by fastsimp } note a_nonneg = this
+    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
+    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    have "convex C" using asms by auto
+    hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
+      using asms convex_setsum[OF `finite s`
+        `convex C` a1 a_nonneg] by auto
+    have asum_le: "f (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))"
+      using a_nonneg a1 asms by blast
+    have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) = f ((\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
+      using setsum.insert[of s i "\<lambda> j. a j *\<^sub>R y j", OF `finite s` `i \<notin> s`] asms
+      by (auto simp only:add_commute)
+    also have "\<dots> = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
+      using i0 by auto
+    also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
+      using scaleR_right.setsum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps)
+    also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
+      by (auto simp:real_divide_def)
+    also have "\<dots> \<le> (1 - a i) *\<^sub>R f ((\<Sum> j \<in> s. ?a j *\<^sub>R y j)) + a i * f (y i)"
+      using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
+      by (auto simp add:add_commute)
+    also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
+      using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
+        OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
+    also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
+      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
+    also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
+    also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
+    finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
+      by simp }
+  ultimately show ?case by auto
+qed
+
+lemma convex_on_alt:
+  fixes C :: "'a::real_vector set"
+  assumes "convex C"
+  shows "convex_on C f =
+  (\<forall> x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1
+      \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
+proof safe
+  fix x y fix \<mu> :: real
+  assume asms: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
+  from this[unfolded convex_on_def, rule_format]
+  have "\<And> u v. \<lbrakk>0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" by auto
+  from this[of "\<mu>" "1 - \<mu>", simplified] asms
+  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y)
+          \<le> \<mu> * f x + (1 - \<mu>) * f y" by auto
+next
+  assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+  {fix x y fix u v :: real
+    assume lasm: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
+    hence[simp]: "1 - u = v" by auto
+    from asm[rule_format, of x y u]
+    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using lasm by auto }
+  thus "convex_on C f" unfolding convex_on_def by auto
+qed
+
+
+lemma pos_convex_function:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "convex C"
+  assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
+  shows "convex_on C f"
+unfolding convex_on_alt[OF assms(1)]
+using assms
+proof safe
+  fix x y \<mu> :: real
+  let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
+  assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
+  hence "1 - \<mu> \<ge> 0" by auto
+  hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
+  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
+            \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
+    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
+      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+  hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
+    by (auto simp add:field_simps)
+  thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
+    using convex_on_alt by auto
+qed
+
+lemma atMostAtLeast_subset_convex:
+  fixes C :: "real set"
+  assumes "convex C"
+  assumes "x \<in> C" "y \<in> C" "x < y"
+  shows "{x .. y} \<subseteq> C"
+proof safe
+  fix z assume zasm: "z \<in> {x .. y}"
+  { assume asm: "x < z" "z < y"
+    let "?\<mu>" = "(y - z) / (y - x)"
+    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps)
+    hence comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
+      using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>] by (simp add:algebra_simps)
+    have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
+      by (auto simp add:field_simps)
+    also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
+      using assms unfolding add_divide_distrib by (auto simp:field_simps)
+    also have "\<dots> = z"
+      using assms by (auto simp:field_simps)
+    finally have "z \<in> C"
+      using comb by auto } note less = this
+  show "z \<in> C" using zasm less assms
+    unfolding atLeastAtMost_iff le_less by auto
+qed
+
+lemma f''_imp_f':
+  fixes f :: "real \<Rightarrow> real"
+  assumes "convex C"
+  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
+  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
+  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
+  assumes "x \<in> C" "y \<in> C"
+  shows "f' x * (y - x) \<le> f y - f x"
+using assms
+proof -
+  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x"
+    hence ge: "y - x > 0" "y - x \<ge> 0" by auto
+    from asm have le: "x - y < 0" "x - y \<le> 0" by auto
+    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
+      using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `y \<in> C` `x < y`],
+        THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
+      by auto
+    hence "z1 \<in> C" using atMostAtLeast_subset_convex
+      `convex C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
+    from z1 have z1': "f x - f y = (x - y) * f' z1"
+      by (simp add:field_simps)
+    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
+      using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `z1 \<in> C` `x < z1`],
+        THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
+      by auto
+    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
+      using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `z1 \<in> C` `y \<in> C` `z1 < y`],
+        THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
+      by auto
+    have "f' y - (f x - f y) / (x - y) = f' y - f' z1"
+      using asm z1' by auto
+    also have "\<dots> = (y - z1) * f'' z3" using z3 by auto
+    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
+    have A': "y - z1 \<ge> 0" using z1 by auto
+    have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
+      `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
+    hence B': "f'' z3 \<ge> 0" using assms by auto
+    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
+    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
+    from mult_right_mono_neg[OF this le(2)]
+    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
+      unfolding diff_def using real_add_mult_distrib by auto
+    hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
+    hence res: "f' y * (x - y) \<le> f x - f y" by auto
+    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
+      using asm z1 by auto
+    also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto
+    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
+    have A: "z1 - x \<ge> 0" using z1 by auto
+    have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
+      `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
+    hence B: "f'' z2 \<ge> 0" using assms by auto
+    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
+    from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
+    from mult_right_mono[OF this ge(2)]
+    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
+      unfolding diff_def using real_add_mult_distrib by auto
+    hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
+    hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
+      using res by auto } note less_imp = this
+  { fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y"
+    hence"f y - f x \<ge> f' x * (y - x)"
+    unfolding neq_iff using less_imp by auto } note neq_imp = this
+  moreover
+  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y"
+    hence "f y - f x \<ge> f' x * (y - x)" by auto }
+  ultimately show ?thesis using assms by blast
+qed
+
+lemma f''_ge0_imp_convex:
+  fixes f :: "real \<Rightarrow> real"
+  assumes conv: "convex C"
+  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
+  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
+  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
+  shows "convex_on C f"
+using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
+
+lemma minus_log_convex:
+  fixes b :: real
+  assumes "b > 1"
+  shows "convex_on {0 <..} (\<lambda> x. - log b x)"
+proof -
+  have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
+  hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
+    using DERIV_minus by auto
+  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
+    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
+  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
+  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
+    by auto
+  hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
+    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
+  have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
+    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
+  from f''_ge0_imp_convex[OF pos_is_convex,
+    unfolded greaterThan_iff, OF f' f''0 f''_ge0]
+  show ?thesis by auto
+qed
+
+end
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Tue May 04 14:44:30 2010 +0200
@@ -54,11 +54,6 @@
 
 subsection {* Addition *}
 
-lemma add_diff_add:
-  fixes a b c d :: "'a::ab_group_add"
-  shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
 lemma bounded_linear_add:
   assumes "bounded_linear f"
   assumes "bounded_linear g"
@@ -402,11 +397,6 @@
 
 subsection {* Inverse *}
 
-lemma inverse_diff_inverse:
-  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
-   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
-
 lemmas bounded_linear_mult_const =
   mult.bounded_linear_left [THEN bounded_linear_compose]
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 04 14:44:30 2010 +0200
@@ -1239,7 +1239,7 @@
   qed
   have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
   qed (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Library/Product_plus.thy	Tue May 04 14:44:30 2010 +0200
@@ -112,4 +112,10 @@
 instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   by default (simp_all add: expand_prod_eq)
 
+lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
+lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
 end
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Limits.thy	Tue May 04 14:44:30 2010 +0200
@@ -11,7 +11,7 @@
 subsection {* Nets *}
 
 text {*
-  A net is now defined simply as a filter.
+  A net is now defined simply as a filter on a set.
   The definition also allows non-proper filters.
 *}
 
@@ -53,6 +53,12 @@
 unfolding eventually_def
 by (rule is_filter.True [OF is_filter_Rep_net])
 
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
+proof -
+  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+  thus "eventually P net" by simp
+qed
+
 lemma eventually_mono:
   "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
 unfolding eventually_def
@@ -101,15 +107,15 @@
 
 subsection {* Finer-than relation *}
 
-text {* @{term "net \<le> net'"} means that @{term net'} is finer than
-@{term net}. *}
+text {* @{term "net \<le> net'"} means that @{term net} is finer than
+@{term net'}. *}
 
-instantiation net :: (type) "{order,top}"
+instantiation net :: (type) complete_lattice
 begin
 
 definition
   le_net_def [code del]:
-    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
+    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
 
 definition
   less_net_def [code del]:
@@ -117,12 +123,64 @@
 
 definition
   top_net_def [code del]:
-    "top = Abs_net (\<lambda>P. True)"
+    "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+
+definition
+  bot_net_def [code del]:
+    "bot = Abs_net (\<lambda>P. True)"
+
+definition
+  sup_net_def [code del]:
+    "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+
+definition
+  inf_net_def [code del]:
+    "inf a b = Abs_net
+      (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+
+definition
+  Sup_net_def [code del]:
+    "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+
+definition
+  Inf_net_def [code del]:
+    "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+
+lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
+unfolding top_net_def
+by (rule eventually_Abs_net, rule is_filter.intro, auto)
 
-lemma eventually_top [simp]: "eventually P top"
-unfolding top_net_def
+lemma eventually_bot [simp]: "eventually P bot"
+unfolding bot_net_def
 by (subst eventually_Abs_net, rule is_filter.intro, auto)
 
+lemma eventually_sup:
+  "eventually P (sup net net') \<longleftrightarrow> eventually P net \<and> eventually P net'"
+unfolding sup_net_def
+by (rule eventually_Abs_net, rule is_filter.intro)
+   (auto elim!: eventually_rev_mp)
+
+lemma eventually_inf:
+  "eventually P (inf a b) \<longleftrightarrow>
+   (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+unfolding inf_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (fast intro: eventually_True)
+apply clarify
+apply (intro exI conjI)
+apply (erule (1) eventually_conj)
+apply (erule (1) eventually_conj)
+apply simp
+apply auto
+done
+
+lemma eventually_Sup:
+  "eventually P (Sup A) \<longleftrightarrow> (\<forall>net\<in>A. eventually P net)"
+unfolding Sup_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (auto intro: eventually_conj elim!: eventually_rev_mp)
+done
+
 instance proof
   fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     by (rule less_net_def)
@@ -137,21 +195,49 @@
     unfolding le_net_def expand_net_eq by fast
 next
   fix x :: "'a net" show "x \<le> top"
+    unfolding le_net_def eventually_top by (simp add: always_eventually)
+next
+  fix x :: "'a net" show "bot \<le> x"
     unfolding le_net_def by simp
+next
+  fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
+    unfolding le_net_def eventually_sup by simp_all
+next
+  fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
+    unfolding le_net_def eventually_sup by simp
+next
+  fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
+    unfolding le_net_def eventually_inf by (auto intro: eventually_True)
+next
+  fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
+    unfolding le_net_def eventually_inf
+    by (auto elim!: eventually_mono intro: eventually_conj)
+next
+  fix x :: "'a net" and A assume "x \<in> A" thus "x \<le> Sup A"
+    unfolding le_net_def eventually_Sup by simp
+next
+  fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
+    unfolding le_net_def eventually_Sup by simp
+next
+  fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
+    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
+next
+  fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
+    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
 qed
 
 end
 
 lemma net_leD:
-  "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
+  "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
 unfolding le_net_def by simp
 
 lemma net_leI:
-  "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
+  "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
 unfolding le_net_def by simp
 
 lemma eventually_False:
-  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
+  "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
 unfolding expand_net_eq by (auto elim: eventually_rev_mp)
 
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/List.thy	Tue May 04 14:44:30 2010 +0200
@@ -3039,6 +3039,9 @@
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
 
+lemma Ex_list_of_length: "\<exists>xs. length xs = n"
+by (rule exI[of _ "replicate n undefined"]) simp
+
 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
 by (induct n) auto
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Log.thy	Tue May 04 14:44:30 2010 +0200
@@ -145,6 +145,21 @@
 apply (drule_tac a = "log a x" in powr_less_mono, auto)
 done
 
+lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
+proof (rule inj_onI, simp)
+  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
+  show "x = y"
+  proof (cases rule: linorder_cases)
+    assume "x < y" hence "log b x < log b y"
+      using log_less_cancel_iff[OF `1 < b`] pos by simp
+    thus ?thesis using * by simp
+  next
+    assume "y < x" hence "log b y < log b x"
+      using log_less_cancel_iff[OF `1 < b`] pos by simp
+    thus ?thesis using * by simp
+  qed simp
+qed
+
 lemma log_le_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
 by (simp add: linorder_not_less [symmetric])
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 04 14:44:30 2010 +0200
@@ -5,7 +5,7 @@
 header {* Convex sets, functions and related things. *}
 
 theory Convex_Euclidean_Space
-imports Topology_Euclidean_Space
+imports Topology_Euclidean_Space Convex
 begin
 
 
@@ -315,176 +315,6 @@
   shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
   using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
 
-subsection {* Convexity. *}
-
-definition
-  convex :: "'a::real_vector set \<Rightarrow> bool" where
-  "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
-
-lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
-proof- have *:"\<And>u v::real. u + v = 1 \<longleftrightarrow> u = 1 - v" by auto
-  show ?thesis unfolding convex_def apply auto
-    apply(erule_tac x=x in ballE) apply(erule_tac x=y in ballE) apply(erule_tac x="1 - u" in allE)
-    by (auto simp add: *) qed
-
-lemma mem_convex:
-  assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
-  shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
-  using assms unfolding convex_alt by auto
-
-lemma convex_empty[intro]: "convex {}"
-  unfolding convex_def by simp
-
-lemma convex_singleton[intro]: "convex {a}"
-  unfolding convex_def by (auto simp add:scaleR_left_distrib[THEN sym])
-
-lemma convex_UNIV[intro]: "convex UNIV"
-  unfolding convex_def by auto
-
-lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"
-  unfolding convex_def by auto
-
-lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
-  unfolding convex_def by auto
-
-lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
-  unfolding convex_def apply auto
-  unfolding inner_add inner_scaleR
-  by (metis real_convex_bound_le)
-
-lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
-proof- have *:"{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto
-  show ?thesis apply(unfold *) using convex_halfspace_le[of "-a" "-b"] by auto qed
-
-lemma convex_hyperplane: "convex {x. inner a x = b}"
-proof-
-  have *:"{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto
-  show ?thesis unfolding * apply(rule convex_Int)
-    using convex_halfspace_le convex_halfspace_ge by auto
-qed
-
-lemma convex_halfspace_lt: "convex {x. inner a x < b}"
-  unfolding convex_def
-  by(auto simp add: real_convex_bound_lt inner_add)
-
-lemma convex_halfspace_gt: "convex {x. inner a x > b}"
-   using convex_halfspace_lt[of "-a" "-b"] by auto
-
-lemma convex_real_interval:
-  fixes a b :: "real"
-  shows "convex {a..}" and "convex {..b}"
-  and "convex {a<..}" and "convex {..<b}"
-  and "convex {a..b}" and "convex {a<..b}"
-  and "convex {a..<b}" and "convex {a<..<b}"
-proof -
-  have "{a..} = {x. a \<le> inner 1 x}" by auto
-  thus 1: "convex {a..}" by (simp only: convex_halfspace_ge)
-  have "{..b} = {x. inner 1 x \<le> b}" by auto
-  thus 2: "convex {..b}" by (simp only: convex_halfspace_le)
-  have "{a<..} = {x. a < inner 1 x}" by auto
-  thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt)
-  have "{..<b} = {x. inner 1 x < b}" by auto
-  thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt)
-  have "{a..b} = {a..} \<inter> {..b}" by auto
-  thus "convex {a..b}" by (simp only: convex_Int 1 2)
-  have "{a<..b} = {a<..} \<inter> {..b}" by auto
-  thus "convex {a<..b}" by (simp only: convex_Int 3 2)
-  have "{a..<b} = {a..} \<inter> {..<b}" by auto
-  thus "convex {a..<b}" by (simp only: convex_Int 1 4)
-  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
-  thus "convex {a<..<b}" by (simp only: convex_Int 3 4)
-qed
-
-lemma convex_box:
-  assumes "\<And>i. convex {x. P i x}"
-  shows "convex {x. \<forall>i. P i (x$i)}"
-using assms unfolding convex_def by auto
-
-lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
-by (rule convex_box, simp add: atLeast_def [symmetric] convex_real_interval)
-
-subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
-
-lemma convex: "convex s \<longleftrightarrow>
-  (\<forall>(k::nat) u x. (\<forall>i. 1\<le>i \<and> i\<le>k \<longrightarrow> 0 \<le> u i \<and> x i \<in>s) \<and> (setsum u {1..k} = 1)
-           \<longrightarrow> setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)"
-  unfolding convex_def apply rule apply(rule allI)+ defer apply(rule ballI)+ apply(rule allI)+ proof(rule,rule,rule,rule)
-  fix x y u v assume as:"\<forall>(k::nat) u x. (\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R x i) \<in> s"
-    "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
-  show "u *\<^sub>R x + v *\<^sub>R y \<in> s" using as(1)[THEN spec[where x=2], THEN spec[where x="\<lambda>n. if n=1 then u else v"], THEN spec[where x="\<lambda>n. if n=1 then x else y"]] and as(2-)
-    by (auto simp add: setsum_head_Suc) 
-next
-  fix k u x assume as:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" 
-  show "(\<forall>i::nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R x i) \<in> s" apply(rule,erule conjE) proof(induct k arbitrary: u)
-  case (Suc k) show ?case proof(cases "u (Suc k) = 1")
-    case True hence "(\<Sum>i = Suc 0..k. u i *\<^sub>R x i) = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-
-      fix i assume i:"i \<in> {Suc 0..k}" "u i *\<^sub>R x i \<noteq> 0"
-      hence ui:"u i \<noteq> 0" by auto
-      hence "setsum (\<lambda>k. if k=i then u i else 0) {1 .. k} \<le> setsum u {1 .. k}" apply(rule_tac setsum_mono) using Suc(2) by auto
-      hence "setsum u {1 .. k} \<ge> u i" using i(1) by(auto simp add: setsum_delta) 
-      hence "setsum u {1 .. k} > 0"  using ui apply(rule_tac less_le_trans[of _ "u i"]) using Suc(2)[THEN spec[where x=i]] and i(1) by auto
-      thus False using Suc(3) unfolding setsum_cl_ivl_Suc and True by simp qed
-    thus ?thesis unfolding setsum_cl_ivl_Suc using True and Suc(2) by auto
-  next
-    have *:"setsum u {1..k} = 1 - u (Suc k)" using Suc(3)[unfolded setsum_cl_ivl_Suc] by auto
-    have **:"u (Suc k) \<le> 1" unfolding not_le using Suc(3) using setsum_nonneg[of "{1..k}" u] using Suc(2) by auto
-    have ***:"\<And>i k. (u i / (1 - u (Suc k))) *\<^sub>R x i = (inverse (1 - u (Suc k))) *\<^sub>R (u i *\<^sub>R x i)" unfolding real_divide_def by (auto simp add: algebra_simps)
-    case False hence nn:"1 - u (Suc k) \<noteq> 0" by auto
-    have "(\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *\<^sub>R x i) \<in> s" apply(rule Suc(1)) unfolding setsum_divide_distrib[THEN sym] and *
-      apply(rule_tac allI) apply(rule,rule) apply(rule divide_nonneg_pos) using nn Suc(2) ** by auto
-    hence "(1 - u (Suc k)) *\<^sub>R (\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *\<^sub>R x i) + u (Suc k) *\<^sub>R x (Suc k) \<in> s"
-      apply(rule as[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using Suc(2)[THEN spec[where x="Suc k"]] and ** by auto
-    thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed
-
-
-lemma convex_explicit:
-  fixes s :: "'a::real_vector set"
-  shows "convex s \<longleftrightarrow>
-  (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"
-  unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof-
-  fix x y u v assume as:"\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
-  show "u *\<^sub>R x + v *\<^sub>R y \<in> s" proof(cases "x=y")
-    case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next
-    case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed
-next 
-  fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)"
-  (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)
-  from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct t rule:finite_induct)
-    prefer 2 apply (rule,rule) apply(erule conjE)+ proof-
-    fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s"
-    assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)"
-    show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1")
-      case True hence "setsum (\<lambda>x. u x *\<^sub>R x) f = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-
-        fix y assume y:"y \<in> f" "u y *\<^sub>R y \<noteq> 0"
-        hence uy:"u y \<noteq> 0" by auto
-        hence "setsum (\<lambda>k. if k=y then u y else 0) f \<le> setsum u f" apply(rule_tac setsum_mono) using as(4) by auto
-        hence "setsum u f \<ge> u y" using y(1) and as(1) by(auto simp add: setsum_delta) 
-        hence "setsum u f > 0" using uy apply(rule_tac less_le_trans[of _ "u y"]) using as(4) and y(1) by auto
-        thus False using as(2,5) unfolding setsum_clauses(2)[OF as(1)] and True by auto qed
-      thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2,3) unfolding True by auto
-    next
-      have *:"setsum u f = setsum u (insert x f) - u x" using as(2) unfolding setsum_clauses(2)[OF as(1)] by auto
-      have **:"u x \<le> 1" unfolding not_le using as(5)[unfolded setsum_clauses(2)[OF as(1)]] and as(2)
-        using setsum_nonneg[of f u] and as(4) by auto
-      case False hence "inverse (1 - u x) *\<^sub>R (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s" unfolding scaleR_right.setsum and scaleR_scaleR
-        apply(rule_tac ind[THEN spec, THEN mp]) apply rule defer apply rule apply rule apply(rule mult_nonneg_nonneg)
-        unfolding setsum_right_distrib[THEN sym] and * using as and ** by auto
-      hence "u x *\<^sub>R x + (1 - u x) *\<^sub>R ((inverse (1 - u x)) *\<^sub>R setsum (\<lambda>x. u x *\<^sub>R x) f) \<in>s" 
-        apply(rule_tac asm(1)[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using as and ** False by auto 
-      thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2) and False by auto qed
-  qed auto thus "t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" by auto
-qed
-
-lemma convex_finite: assumes "finite s"
-  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
-                      \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
-  unfolding convex_explicit apply(rule, rule, rule) defer apply(rule,rule,rule)apply(erule conjE)+ proof-
-  fix t u assume as:"\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s" " finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
-  have *:"s \<inter> t = t" using as(3) by auto
-  show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" using as(1)[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]]
-    unfolding if_smult and setsum_cases[OF assms] using as(2-) * by auto
-qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
-
 subsection {* Cones. *}
 
 definition
@@ -595,49 +425,15 @@
 lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
   by(simp add: convex_connected convex_UNIV)
 
-subsection {* Convex functions into the reals. *}
-
-definition
-  convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
-  "convex_on s f \<longleftrightarrow>
-  (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
-
-lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
-  unfolding convex_on_def by auto
+subsection {* Balls, being convex, are connected. *}
 
-lemma convex_add[intro]:
-  assumes "convex_on s f" "convex_on s g"
-  shows "convex_on s (\<lambda>x. f x + g x)"
-proof-
-  { fix x y assume "x\<in>s" "y\<in>s" moreover
-    fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
-    ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)"
-      using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
-      using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
-      apply - apply(rule add_mono) by auto
-    hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps)  }
-  thus ?thesis unfolding convex_on_def by auto 
-qed
+lemma convex_box:
+  assumes "\<And>i. convex {x. P i x}"
+  shows "convex {x. \<forall>i. P i (x$i)}"
+using assms unfolding convex_def by auto
 
-lemma convex_cmul[intro]:
-  assumes "0 \<le> (c::real)" "convex_on s f"
-  shows "convex_on s (\<lambda>x. c * f x)"
-proof-
-  have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
-  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
-qed
-
-lemma convex_lower:
-  assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"
-  shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
-proof-
-  let ?m = "max (f x) (f y)"
-  have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)" apply(rule add_mono) 
-    using assms(4,5) by(auto simp add: mult_mono1)
-  also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
-  finally show ?thesis using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
-    using assms(2-6) by auto 
-qed
+lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
+  by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
 
 lemma convex_local_global_minimum:
   fixes s :: "'a::real_normed_vector set"
@@ -661,76 +457,6 @@
   ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
 qed
 
-lemma convex_distance[intro]:
-  fixes s :: "'a::real_normed_vector set"
-  shows "convex_on s (\<lambda>x. dist a x)"
-proof(auto simp add: convex_on_def dist_norm)
-  fix x y assume "x\<in>s" "y\<in>s"
-  fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
-  have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp
-  hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
-    by (auto simp add: algebra_simps)
-  show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
-    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
-    using `0 \<le> u` `0 \<le> v` by auto
-qed
-
-subsection {* Arithmetic operations on sets preserve convexity. *}
-
-lemma convex_scaling: "convex s \<Longrightarrow> convex ((\<lambda>x. c *\<^sub>R x) ` s)"
-  unfolding convex_def and image_iff apply auto
-  apply (rule_tac x="u *\<^sub>R x+v *\<^sub>R y" in bexI) by (auto simp add: algebra_simps)
-
-lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"
-  unfolding convex_def and image_iff apply auto
-  apply (rule_tac x="u *\<^sub>R x+v *\<^sub>R y" in bexI) by auto
-
-lemma convex_sums:
-  assumes "convex s" "convex t"
-  shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
-proof(auto simp add: convex_def image_iff scaleR_right_distrib)
-  fix xa xb ya yb assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  show "\<exists>x y. u *\<^sub>R xa + u *\<^sub>R ya + (v *\<^sub>R xb + v *\<^sub>R yb) = x + y \<and> x \<in> s \<and> y \<in> t"
-    apply(rule_tac x="u *\<^sub>R xa + v *\<^sub>R xb" in exI) apply(rule_tac x="u *\<^sub>R ya + v *\<^sub>R yb" in exI)
-    using assms(1)[unfolded convex_def, THEN bspec[where x=xa], THEN bspec[where x=xb]]
-    using assms(2)[unfolded convex_def, THEN bspec[where x=ya], THEN bspec[where x=yb]]
-    using uv xy by auto
-qed
-
-lemma convex_differences: 
-  assumes "convex s" "convex t"
-  shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
-proof-
-  have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}" unfolding image_iff apply auto
-    apply(rule_tac x=xa in exI) apply(rule_tac x="-y" in exI) apply simp
-    apply(rule_tac x=xa in exI) apply(rule_tac x=xb in exI) by simp
-  thus ?thesis using convex_sums[OF assms(1)  convex_negations[OF assms(2)]] by auto
-qed
-
-lemma convex_translation: assumes "convex s" shows "convex ((\<lambda>x. a + x) ` s)"
-proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
-  thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed
-
-lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
-proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
-  thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
-
-lemma convex_linear_image:
-  assumes c:"convex s" and l:"bounded_linear f"
-  shows "convex(f ` s)"
-proof(auto simp add: convex_def)
-  interpret f: bounded_linear f by fact
-  fix x y assume xy:"x \<in> s" "y \<in> s"
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
-    apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI)
-    unfolding f.add f.scaleR
-    using c[unfolded convex_def] xy uv by auto
-qed
-
-subsection {* Balls, being convex, are connected. *}
-
 lemma convex_ball:
   fixes x :: "'a::real_normed_vector"
   shows "convex (ball x e)" 
@@ -739,7 +465,7 @@
   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
     using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto 
+  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto
 qed
 
 lemma convex_cball:
@@ -750,7 +476,7 @@
   fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
     using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto 
+  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto 
 qed
 
 lemma connected_ball:
@@ -2205,14 +1931,6 @@
 
 subsection {* Use this to derive general bound property of convex function. *}
 
-(* TODO: move *)
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
-(* TODO: move *)
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
 lemma convex_on:
   assumes "convex s"
   shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue May 04 14:44:30 2010 +0200
@@ -8,7 +8,7 @@
 imports
   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   Finite_Cartesian_Product Infinite_Set Numeral_Type
-  Inner_Product L2_Norm
+  Inner_Product L2_Norm Convex
 uses "positivstellensatz.ML" ("normarith.ML")
 begin
 
@@ -1411,40 +1411,6 @@
   done
 
 
-lemma real_convex_bound_lt:
-  assumes xa: "(x::real) < a" and ya: "y < a" and u: "0 <= u" and v: "0 <= v"
-  and uv: "u + v = 1"
-  shows "u * x + v * y < a"
-proof-
-  have uv': "u = 0 \<longrightarrow> v \<noteq> 0" using u v uv by arith
-  have "a = a * (u + v)" unfolding uv  by simp
-  hence th: "u * a + v * a = a" by (simp add: field_simps)
-  from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_strict_left_mono)
-  from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_strict_left_mono)
-  from xa ya u v have "u * x + v * y < u * a + v * a"
-    apply (cases "u = 0", simp_all add: uv')
-    apply(rule mult_strict_left_mono)
-    using uv' apply simp_all
-
-    apply (rule add_less_le_mono)
-    apply(rule mult_strict_left_mono)
-    apply simp_all
-    apply (rule mult_left_mono)
-    apply simp_all
-    done
-  thus ?thesis unfolding th .
-qed
-
-lemma real_convex_bound_le:
-  assumes xa: "(x::real) \<le> a" and ya: "y \<le> a" and u: "0 <= u" and v: "0 <= v"
-  and uv: "u + v = 1"
-  shows "u * x + v * y \<le> a"
-proof-
-  from xa ya u v have "u * x + v * y \<le> u * a + v * a" by (simp add: add_mono mult_left_mono)
-  also have "\<dots> \<le> (u + v) * a" by (simp add: field_simps)
-  finally show ?thesis unfolding uv by simp
-qed
-
 lemma infinite_enumerate: assumes fS: "infinite S"
   shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
 unfolding subseq_def
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 14:44:30 2010 +0200
@@ -6,7 +6,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Euclidean_Space Product_Vector Glbs
+imports SEQ Euclidean_Space Glbs
 begin
 
 subsection{* General notion of a topology *}
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Orderings.thy	Tue May 04 14:44:30 2010 +0200
@@ -106,7 +106,7 @@
 text {* Dual order *}
 
 lemma dual_preorder:
-  "preorder (op \<ge>) (op >)"
+  "class.preorder (op \<ge>) (op >)"
 proof qed (auto simp add: less_le_not_le intro: order_trans)
 
 end
@@ -186,7 +186,7 @@
 text {* Dual order *}
 
 lemma dual_order:
-  "order (op \<ge>) (op >)"
+  "class.order (op \<ge>) (op >)"
 by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
 
 end
@@ -257,8 +257,8 @@
 text {* Dual order *}
 
 lemma dual_linorder:
-  "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+  "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
 
 
 text {* min/max *}
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Probability/Information.thy	Tue May 04 14:44:30 2010 +0200
@@ -1,169 +1,264 @@
 theory Information
-imports Probability_Space Product_Measure
+imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex"
 begin
 
-lemma pos_neg_part_abs:
-  fixes f :: "'a \<Rightarrow> real"
-  shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
-unfolding real_abs_def pos_part_def neg_part_def by auto
+section "Convex theory"
 
-lemma pos_part_abs:
-  fixes f :: "'a \<Rightarrow> real"
-  shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
-unfolding pos_part_def real_abs_def by auto
-
-lemma neg_part_abs:
-  fixes f :: "'a \<Rightarrow> real"
-  shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
-unfolding neg_part_def real_abs_def by auto
+lemma log_setsum:
+  assumes "finite s" "s \<noteq> {}"
+  assumes "b > 1"
+  assumes "(\<Sum> i \<in> s. a i) = 1"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
+  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
+proof -
+  have "convex_on {0 <..} (\<lambda> x. - log b x)"
+    by (rule minus_log_convex[OF `b > 1`])
+  hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
+    using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastsimp
+  thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
+qed
 
-lemma (in measure_space) int_abs:
-  assumes "integrable f"
-  shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
-using assms
+lemma log_setsum':
+  assumes "finite s" "s \<noteq> {}"
+  assumes "b > 1"
+  assumes "(\<Sum> i \<in> s. a i) = 1"
+  assumes pos: "\<And> i. i \<in> s \<Longrightarrow> 0 \<le> a i"
+          "\<And> i. \<lbrakk> i \<in> s ; 0 < a i \<rbrakk> \<Longrightarrow> 0 < y i"
+  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
 proof -
-  from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"
-    unfolding integrable_def by auto
-  hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"
-    using nnfis_add by auto
-  hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp
-  thus ?thesis unfolding integrable_def
-    using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]
-      ext[OF neg_part_abs[of f], of "\<lambda> y. y"]
-    using nnfis_0 by auto
+  have "\<And>y. (\<Sum> i \<in> s - {i. a i = 0}. a i * y i) = (\<Sum> i \<in> s. a i * y i)"
+    using assms by (auto intro!: setsum_mono_zero_cong_left)
+  moreover have "log b (\<Sum> i \<in> s - {i. a i = 0}. a i * y i) \<ge> (\<Sum> i \<in> s - {i. a i = 0}. a i * log b (y i))"
+  proof (rule log_setsum)
+    have "setsum a (s - {i. a i = 0}) = setsum a s"
+      using assms(1) by (rule setsum_mono_zero_cong_left) auto
+    thus sum_1: "setsum a (s - {i. a i = 0}) = 1"
+      "finite (s - {i. a i = 0})" using assms by simp_all
+
+    show "s - {i. a i = 0} \<noteq> {}"
+    proof
+      assume *: "s - {i. a i = 0} = {}"
+      hence "setsum a (s - {i. a i = 0}) = 0" by (simp add: * setsum_empty)
+      with sum_1 show False by simp
+qed
+
+    fix i assume "i \<in> s - {i. a i = 0}"
+    hence "i \<in> s" "a i \<noteq> 0" by simp_all
+    thus "0 \<le> a i" "y i \<in> {0<..}" using pos[of i] by auto
+  qed fact+
+  ultimately show ?thesis by simp
 qed
 
-lemma (in measure_space) measure_mono:
-  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
-  shows "measure M a \<le> measure M b"
+section "Information theory"
+
+lemma (in finite_prob_space) sum_over_space_distrib:
+  "(\<Sum>x\<in>X`space M. distribution X {x}) = 1"
+  unfolding distribution_def prob_space[symmetric] using finite_space
+  by (subst measure_finitely_additive'')
+     (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob])
+
+locale finite_information_space = finite_prob_space +
+  fixes b :: real assumes b_gt_1: "1 < b"
+
+definition
+  "KL_divergence b M X Y =
+    measure_space.integral (M\<lparr>measure := X\<rparr>)
+                           (\<lambda>x. log b ((measure_space.RN_deriv (M \<lparr>measure := Y\<rparr> ) X) x))"
+
+lemma (in finite_prob_space) distribution_mono:
+  assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y"
+  shows "distribution X x \<le> distribution Y y"
+  unfolding distribution_def
+  using assms by (auto simp: sets_eq_Pow intro!: measure_mono)
+
+lemma (in prob_space) distribution_remove_const:
+  shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}"
+  and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}"
+  and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}"
+  and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}"
+  and "distribution (\<lambda>x. ()) {()} = 1"
+  unfolding prob_space[symmetric]
+  by (auto intro!: arg_cong[where f=prob] simp: distribution_def)
+
+
+context finite_information_space
+begin
+
+lemma distribution_mono_gt_0:
+  assumes gt_0: "0 < distribution X x"
+  assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y"
+  shows "0 < distribution Y y"
+  by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *)
+
+lemma
+  assumes "0 \<le> A" and pos: "0 < A \<Longrightarrow> 0 < B" "0 < A \<Longrightarrow> 0 < C"
+  shows mult_log_mult: "A * log b (B * C) = A * log b B + A * log b C" (is "?mult")
+  and mult_log_divide: "A * log b (B / C) = A * log b B - A * log b C" (is "?div")
 proof -
-  have "b = a \<union> (b - a)" using assms by auto
-  moreover have "{} = a \<inter> (b - a)" by auto
-  ultimately have "measure M b = measure M a + measure M (b - a)"
-    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
-  moreover have "measure M (b - a) \<ge> 0" using positive assms by auto
-  ultimately show "measure M a \<le> measure M b" by auto
+  have "?mult \<and> ?div"
+proof (cases "A = 0")
+  case False
+  hence "0 < A" using `0 \<le> A` by auto
+    with pos[OF this] show "?mult \<and> ?div" using b_gt_1
+      by (auto simp: log_divide log_mult field_simps)
+qed simp
+  thus ?mult and ?div by auto
 qed
 
-lemma (in measure_space) integral_0:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"
-  shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"
-proof -
-  have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto
-  moreover
-  { fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"
-    hence "\<bar> f y \<bar> > 0" by auto
-    hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"
-      using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto
-    hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
-      by auto }
-  moreover
-  { fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
-    then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto
-    hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto
-    hence "\<bar>f y\<bar> > 0"
-      using real_of_nat_Suc_gt_zero
-        positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp
-    hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }
-  ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
-    by blast
-  { fix n
-    have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using int_abs assms by auto
-    have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M)
-           \<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"
-      using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto
-    hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"
-      using assms unfolding nonneg_def by auto
-    have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
-      apply (subst Int_commute) unfolding Int_def
-      using borel[unfolded borel_measurable_ge_iff] by simp
-    hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>
-      {x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
-      using positive le0 unfolding atLeast_def by fastsimp }
-  moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"
-    by auto
-  moreover
-  { fix n
-    have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"
-      using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp
-    hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)
-    hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M
-         \<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }
-  ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"
-    using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]
-    unfolding o_def by (simp del: of_nat_Suc)
-  hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"
-    using LIMSEQ_const[of 0] LIMSEQ_unique by simp
-  hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"
-    using assms unfolding nonneg_def by auto
-  thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp
+lemma split_pairs:
+  shows
+    "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
+    "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
+
+ML {*
+
+  (* tactic to solve equations of the form @{term "W * log b (X / (Y * Z)) = W * log b X - W * log b (Y * Z)"}
+     where @{term W} is a joint distribution of @{term X}, @{term Y}, and @{term Z}. *)
+
+  val mult_log_intros = [@{thm mult_log_divide}, @{thm mult_log_mult}]
+  val intros = [@{thm divide_pos_pos}, @{thm mult_pos_pos}, @{thm positive_distribution}]
+
+  val distribution_gt_0_tac = (rtac @{thm distribution_mono_gt_0}
+    THEN' assume_tac
+    THEN' clarsimp_tac (clasimpset_of @{context} addsimps2 @{thms split_pairs}))
+
+  val distr_mult_log_eq_tac = REPEAT_ALL_NEW (CHANGED o TRY o
+    (resolve_tac (mult_log_intros @ intros)
+      ORELSE' distribution_gt_0_tac
+      ORELSE' clarsimp_tac (clasimpset_of @{context})))
+
+  fun instanciate_term thy redex intro =
+    let
+      val intro_concl = Thm.concl_of intro
+
+      val lhs = intro_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
+
+      val m = SOME (Pattern.match thy (lhs, redex) (Vartab.empty, Vartab.empty))
+        handle Pattern.MATCH => NONE
+
+    in
+      Option.map (fn m => Envir.subst_term m intro_concl) m
+    end
+
+  fun mult_log_simproc simpset redex =
+  let
+    val ctxt = Simplifier.the_context simpset
+    val thy = ProofContext.theory_of ctxt
+    fun prove (SOME thm) = (SOME
+          (Goal.prove ctxt [] [] thm (K (distr_mult_log_eq_tac 1))
+           |> mk_meta_eq)
+            handle THM _ => NONE)
+      | prove NONE = NONE
+  in
+    get_first (instanciate_term thy (term_of redex) #> prove) mult_log_intros
+  end
+*}
+
+simproc_setup mult_log ("distribution X x * log b (A * B)" |
+                        "distribution X x * log b (A / B)") = {* K mult_log_simproc *}
+
+end
+
+lemma KL_divergence_eq_finite:
+  assumes u: "finite_measure_space (M\<lparr>measure := u\<rparr>)"
+  assumes v: "finite_measure_space (M\<lparr>measure := v\<rparr>)"
+  assumes u_0: "\<And>x. \<lbrakk> x \<in> space M ; v {x} = 0 \<rbrakk> \<Longrightarrow> u {x} = 0"
+  shows "KL_divergence b M u v = (\<Sum>x\<in>space M. u {x} * log b (u {x} / v {x}))" (is "_ = ?sum")
+proof (simp add: KL_divergence_def, subst finite_measure_space.integral_finite_singleton, simp_all add: u)
+  have ms_u: "measure_space (M\<lparr>measure := u\<rparr>)"
+    using u unfolding finite_measure_space_def by simp
+
+  show "(\<Sum>x \<in> space M. log b (measure_space.RN_deriv (M\<lparr>measure := v\<rparr>) u x) * u {x}) = ?sum"
+    apply (rule setsum_cong[OF refl])
+    apply simp
+    apply (safe intro!: arg_cong[where f="log b"] )
+    apply (subst finite_measure_space.RN_deriv_finite_singleton)
+    using assms ms_u by auto
 qed
 
-definition
-  "KL_divergence b M u v =
-    measure_space.integral (M\<lparr>measure := u\<rparr>)
-                           (\<lambda>x. log b ((measure_space.RN_deriv (M \<lparr>measure := v\<rparr> ) u) x))"
-
-lemma (in finite_prob_space) finite_measure_space:
-  shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
-    (is "finite_measure_space ?S")
-proof (rule finite_Pow_additivity_sufficient, simp_all)
-  show "finite (X ` space M)" using finite_space by simp
-
-  show "positive ?S (distribution X)" unfolding distribution_def
-    unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto
+lemma log_setsum_divide:
+  assumes "finite S" and "S \<noteq> {}" and "1 < b"
+  assumes "(\<Sum>x\<in>S. g x) = 1"
+  assumes pos: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
+  assumes g_pos: "\<And>x. \<lbrakk> x \<in> S ; 0 < g x \<rbrakk> \<Longrightarrow> 0 < f x"
+  shows "- (\<Sum>x\<in>S. g x * log b (g x / f x)) \<le> log b (\<Sum>x\<in>S. f x)"
+proof -
+  have log_mono: "\<And>x y. 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log b x \<le> log b y"
+    using `1 < b` by (subst log_le_cancel_iff) auto
 
-  show "additive ?S (distribution X)" unfolding additive_def distribution_def
-  proof (simp, safe)
-    fix x y
-    have x: "(X -` x) \<inter> space M \<in> sets M"
-      and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
-    assume "x \<inter> y = {}"
-    from additive[unfolded additive_def, rule_format, OF x y] this
-    have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) =
-      prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)"
-      apply (subst Int_Un_distrib2)
-      by auto
-    thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)"
-      by auto
+  have "- (\<Sum>x\<in>S. g x * log b (g x / f x)) = (\<Sum>x\<in>S. g x * log b (f x / g x))"
+  proof (unfold setsum_negf[symmetric], rule setsum_cong)
+    fix x assume x: "x \<in> S"
+    show "- (g x * log b (g x / f x)) = g x * log b (f x / g x)"
+    proof (cases "g x = 0")
+      case False
+      with pos[OF x] g_pos[OF x] have "0 < f x" "0 < g x" by simp_all
+      thus ?thesis using `1 < b` by (simp add: log_divide field_simps)
+    qed simp
+  qed rule
+  also have "... \<le> log b (\<Sum>x\<in>S. g x * (f x / g x))"
+  proof (rule log_setsum')
+    fix x assume x: "x \<in> S" "0 < g x"
+    with g_pos[OF x] show "0 < f x / g x" by (safe intro!: divide_pos_pos)
+  qed fact+
+  also have "... = log b (\<Sum>x\<in>S - {x. g x = 0}. f x)" using `finite S`
+    by (auto intro!: setsum_mono_zero_cong_right arg_cong[where f="log b"]
+        split: split_if_asm)
+  also have "... \<le> log b (\<Sum>x\<in>S. f x)"
+  proof (rule log_mono)
+    have "0 = (\<Sum>x\<in>S - {x. g x = 0}. 0)" by simp
+    also have "... < (\<Sum>x\<in>S - {x. g x = 0}. f x)" (is "_ < ?sum")
+    proof (rule setsum_strict_mono)
+      show "finite (S - {x. g x = 0})" using `finite S` by simp
+      show "S - {x. g x = 0} \<noteq> {}"
+      proof
+        assume "S - {x. g x = 0} = {}"
+        hence "(\<Sum>x\<in>S. g x) = 0" by (subst setsum_0') auto
+        with `(\<Sum>x\<in>S. g x) = 1` show False by simp
+      qed
+      fix x assume "x \<in> S - {x. g x = 0}"
+      thus "0 < f x" using g_pos[of x] pos(1)[of x] by auto
+    qed
+    finally show "0 < ?sum" .
+    show "(\<Sum>x\<in>S - {x. g x = 0}. f x) \<le> (\<Sum>x\<in>S. f x)"
+      using `finite S` pos by (auto intro!: setsum_mono2)
   qed
+  finally show ?thesis .
 qed
 
-lemma (in finite_prob_space) finite_prob_space:
-  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
-  (is "finite_prob_space ?S")
-  unfolding finite_prob_space_def prob_space_def prob_space_axioms_def
-proof safe
-  show "finite_measure_space ?S" by (rule finite_measure_space)
-  thus "measure_space ?S" by (simp add: finite_measure_space_def)
+lemma KL_divergence_positive_finite:
+  assumes u: "finite_prob_space (M\<lparr>measure := u\<rparr>)"
+  assumes v: "finite_prob_space (M\<lparr>measure := v\<rparr>)"
+  assumes u_0: "\<And>x. \<lbrakk> x \<in> space M ; v {x} = 0 \<rbrakk> \<Longrightarrow> u {x} = 0"
+  and "1 < b"
+  shows "0 \<le> KL_divergence b M u v"
+proof -
+  interpret u: finite_prob_space "M\<lparr>measure := u\<rparr>" using u .
+  interpret v: finite_prob_space "M\<lparr>measure := v\<rparr>" using v .
 
-  have "X -` X ` space M \<inter> space M = space M" by auto
-  thus "measure ?S (space ?S) = 1"
-    by (simp add: distribution_def prob_space)
-qed
+  have *: "space M \<noteq> {}" using u.not_empty by simp
 
-lemma (in finite_prob_space) finite_measure_space_image_prod:
-  "finite_measure_space \<lparr>space = X ` space M \<times> Y ` space M,
-    sets = Pow (X ` space M \<times> Y ` space M), measure_space.measure = distribution (\<lambda>x. (X x, Y x))\<rparr>"
-  (is "finite_measure_space ?Z")
-proof (rule finite_Pow_additivity_sufficient, simp_all)
-  show "finite (X ` space M \<times> Y ` space M)" using finite_space by simp
+  have "- (KL_divergence b M u v) \<le> log b (\<Sum>x\<in>space M. v {x})"
+  proof (subst KL_divergence_eq_finite, safe intro!: log_setsum_divide *)
+    show "finite_measure_space (M\<lparr>measure := u\<rparr>)"
+      "finite_measure_space (M\<lparr>measure := v\<rparr>)"
+       using u v unfolding finite_prob_space_eq by simp_all
 
-  let ?d = "distribution (\<lambda>x. (X x, Y x))"
+     show "finite (space M)" using u.finite_space by simp
+     show "1 < b" by fact
+     show "(\<Sum>x\<in>space M. u {x}) = 1" using u.sum_over_space_eq_1 by simp
 
-  show "positive ?Z ?d"
-    using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
+     fix x assume x: "x \<in> space M"
+     thus pos: "0 \<le> u {x}" "0 \<le> v {x}"
+       using u.positive u.sets_eq_Pow v.positive v.sets_eq_Pow by simp_all
 
-  show "additive ?Z ?d" unfolding additive_def
-  proof safe
-    fix x y assume "x \<in> sets ?Z" and "y \<in> sets ?Z"
-    assume "x \<inter> y = {}"
-    thus "?d (x \<union> y) = ?d x + ?d y"
-      apply (simp add: distribution_def)
-      apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
-      by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
+     { assume "v {x} = 0" from u_0[OF x this] show "u {x} = 0" . }
+     { assume "0 < u {x}"
+       hence "v {x} \<noteq> 0" using u_0[OF x] by auto
+       with pos show "0 < v {x}" by simp }
   qed
+  thus "0 \<le> KL_divergence b M u v" using v.sum_over_space_eq_1 by simp
 qed
 
 definition (in prob_space)
@@ -174,346 +269,142 @@
     in
       KL_divergence b prod_space (joint_distribution X Y) (measure prod_space)"
 
-abbreviation (in finite_prob_space)
-  finite_mutual_information ("\<I>\<^bsub>_\<^esub>'(_ ; _')") where
-  "\<I>\<^bsub>b\<^esub>(X ; Y) \<equiv> mutual_information b
+abbreviation (in finite_information_space)
+  finite_mutual_information ("\<I>'(_ ; _')") where
+  "\<I>(X ; Y) \<equiv> mutual_information b
     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
 
-abbreviation (in finite_prob_space)
-  finite_mutual_information_2 :: "('a \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd) \<Rightarrow> real" ("\<I>'(_ ; _')") where
-  "\<I>(X ; Y) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y)"
+lemma (in finite_measure_space) measure_spaceI: "measure_space M"
+  by unfold_locales
 
-lemma (in prob_space) mutual_information_cong:
-  assumes [simp]: "space S1 = space S3" "sets S1 = sets S3"
-    "space S2 = space S4" "sets S2 = sets S4"
-  shows "mutual_information b S1 S2 X Y = mutual_information b S3 S4 X Y"
-  unfolding mutual_information_def by simp
+lemma prod_measure_times_finite:
+  assumes fms: "finite_measure_space M" "finite_measure_space M'" and a: "a \<in> space M \<times> space M'"
+  shows "prod_measure M M' {a} = measure M {fst a} * measure M' {snd a}"
+proof (cases a)
+  case (Pair b c)
+  hence a_eq: "{a} = {b} \<times> {c}" by simp
 
-lemma (in prob_space) joint_distribution:
-  "joint_distribution X Y = distribution (\<lambda>x. (X x, Y x))"
-  unfolding joint_distribution_def_raw distribution_def_raw ..
+  with fms[THEN finite_measure_space.measure_spaceI]
+    fms[THEN finite_measure_space.sets_eq_Pow] a Pair
+  show ?thesis unfolding a_eq
+    by (subst prod_measure_times) simp_all
+qed
 
-lemma (in finite_prob_space) finite_mutual_information_reduce:
-  "\<I>\<^bsub>b\<^esub>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
-    distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /
-                                                   (distribution X {x} * distribution Y {y})))"
-  (is "_ = setsum ?log ?prod")
-  unfolding Let_def mutual_information_def KL_divergence_def
-proof (subst finite_measure_space.integral_finite_singleton, simp_all add: joint_distribution)
-  let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure_space.measure = distribution X\<rparr>"
-  let ?Y = "\<lparr>space = Y ` space M, sets = Pow (Y ` space M), measure_space.measure = distribution Y\<rparr>"
-  let ?P = "prod_measure_space ?X ?Y"
+lemma setsum_cartesian_product':
+  "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
+  unfolding setsum_cartesian_product by simp
 
-  interpret X: finite_measure_space "?X" by (rule finite_measure_space)
-  moreover interpret Y: finite_measure_space "?Y" by (rule finite_measure_space)
-  ultimately have ms_X: "measure_space ?X" and ms_Y: "measure_space ?Y" by unfold_locales
-
-  interpret P: finite_measure_space "?P" by (rule finite_measure_space_finite_prod_measure) (fact+)
-
-  let ?P' = "measure_update (\<lambda>_. distribution (\<lambda>x. (X x, Y x))) ?P"
-  from finite_measure_space_image_prod[of X Y]
-    sigma_prod_sets_finite[OF X.finite_space Y.finite_space]
-  show "finite_measure_space ?P'"
-    by (simp add: X.sets_eq_Pow Y.sets_eq_Pow joint_distribution finite_measure_space_def prod_measure_space_def)
+lemma (in finite_information_space)
+  assumes MX: "finite_prob_space \<lparr> space = space MX, sets = sets MX, measure = distribution X\<rparr>"
+    (is "finite_prob_space ?MX")
+  assumes MY: "finite_prob_space \<lparr> space = space MY, sets = sets MY, measure = distribution Y\<rparr>"
+    (is "finite_prob_space ?MY")
+  and X_space: "X ` space M \<subseteq> space MX" and Y_space: "Y ` space M \<subseteq> space MY"
+  shows mutual_information_eq_generic:
+    "mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY.
+      joint_distribution X Y {(x,y)} *
+      log b (joint_distribution X Y {(x,y)} /
+      (distribution X {x} * distribution Y {y})))"
+    (is "?equality")
+  and mutual_information_positive_generic:
+    "0 \<le> mutual_information b MX MY X Y" (is "?positive")
+proof -
+  let ?P = "prod_measure_space ?MX ?MY"
+  let ?measure = "joint_distribution X Y"
+  let ?P' = "measure_update (\<lambda>_. ?measure) ?P"
 
-  show "(\<Sum>x \<in> space ?P. log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x})
-    = setsum ?log ?prod"
-  proof (rule setsum_cong)
-    show "space ?P = ?prod" unfolding prod_measure_space_def by simp
-  next
-    fix x assume x: "x \<in> X ` space M \<times> Y ` space M"
-    then obtain d e where x_Pair: "x = (d, e)"
-      and d: "d \<in> X ` space M"
-      and e: "e \<in> Y ` space M" by auto
-
-    { fix x assume m_0: "measure ?P {x} = 0"
-      have "distribution (\<lambda>x. (X x, Y x)) {x} = 0"
-      proof (cases x)
-        case (Pair a b)
-        hence "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = (X -` {a} \<inter> space M) \<inter> (Y -` {b} \<inter> space M)"
-          and x_prod: "{x} = {a} \<times> {b}" by auto
+  interpret X: finite_prob_space "?MX" using MX .
+  moreover interpret Y: finite_prob_space "?MY" using MY .
+  ultimately have ms_X: "measure_space ?MX"
+    and ms_Y: "measure_space ?MY" by unfold_locales
 
-        let ?PROD = "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M"
+  have fms_P: "finite_measure_space ?P"
+      by (rule finite_measure_space_finite_prod_measure) fact+
+
+  have fms_P': "finite_measure_space ?P'"
+      using finite_product_measure_space[of "space MX" "space MY"]
+        X.finite_space Y.finite_space sigma_prod_sets_finite[OF X.finite_space Y.finite_space]
+        X.sets_eq_Pow Y.sets_eq_Pow
+      by (simp add: prod_measure_space_def)
 
-        show ?thesis
-        proof (cases "{a} \<subseteq> X ` space M \<and> {b} \<subseteq> Y ` space M")
-          case False
-          hence "?PROD = {}"
-            unfolding Pair by auto
-          thus ?thesis by (auto simp: distribution_def)
-        next
-          have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
-            using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
+  { fix x assume "x \<in> space ?P"
+    hence x_in_MX: "{fst x} \<in> sets MX" using X.sets_eq_Pow
+      by (auto simp: prod_measure_space_def)
+
+    assume "measure ?P {x} = 0"
+    with prod_measure_times[OF ms_X ms_Y, of "{fst x}" "{snd x}"] x_in_MX
+    have "distribution X {fst x} = 0 \<or> distribution Y {snd x} = 0"
+      by (simp add: prod_measure_space_def)
+
+    hence "joint_distribution X Y {x} = 0"
+      by (cases x) (auto simp: distribution_order) }
+  note measure_0 = this
 
-          case True
-          with prod_measure_times[OF ms_X ms_Y, simplified, of "{a}" "{b}"]
-          have "prob (X -` {a} \<inter> space M) = 0 \<or> prob (Y -` {b} \<inter> space M) = 0" (is "?X_0 \<or> ?Y_0") using m_0
-            by (simp add: prod_measure_space_def distribution_def Pair)
-          thus ?thesis
-          proof (rule disjE)
-            assume ?X_0
-            have "prob ?PROD \<le> prob (X -` {a} \<inter> space M)"
-              using sets_eq_Pow Pair by (auto intro!: measure_mono)
-            thus ?thesis using `?X_0` by (auto simp: distribution_def)
-          next
-            assume ?Y_0
-            have "prob ?PROD \<le> prob (Y -` {b} \<inter> space M)"
-              using sets_eq_Pow Pair by (auto intro!: measure_mono)
-            thus ?thesis using `?Y_0` by (auto simp: distribution_def)
-          qed
-        qed
-      qed }
-    note measure_zero_joint_distribution = this
+  show ?equality
+    unfolding Let_def mutual_information_def using fms_P fms_P' measure_0 MX MY
+    by (subst KL_divergence_eq_finite)
+       (simp_all add: prod_measure_space_def prod_measure_times_finite
+         finite_prob_space_eq setsum_cartesian_product')
 
-    show "log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x} = ?log x"
-    apply (cases "distribution (\<lambda>x. (X x, Y x)) {x} \<noteq> 0")
-    apply (subst P.RN_deriv_finite_singleton)
-    proof (simp_all add: x_Pair)
-      from `finite_measure_space ?P'` show "measure_space ?P'" by (simp add: finite_measure_space_def)
-    next
-      fix x assume m_0: "measure ?P {x} = 0" thus "distribution (\<lambda>x. (X x, Y x)) {x} = 0" by fact
-    next
-      show "(d,e) \<in> space ?P" unfolding prod_measure_space_def using x x_Pair by simp
-    next
-      assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
-      show "measure ?P {(d,e)} \<noteq> 0"
-      proof
-        assume "measure ?P {(d,e)} = 0"
-        from measure_zero_joint_distribution[OF this] jd_0
-        show False by simp
-      qed
-    next
-      assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
-      with prod_measure_times[OF ms_X ms_Y, simplified, of "{d}" "{e}"] d
-      show "log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / measure ?P {(d, e)}) =
-        log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / (distribution X {d} * distribution Y {e}))"
-        by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
-    qed
+  show ?positive
+    unfolding Let_def mutual_information_def using measure_0 b_gt_1
+  proof (safe intro!: KL_divergence_positive_finite, simp_all)
+    from ms_X ms_Y X.top Y.top X.prob_space Y.prob_space
+    have "measure ?P (space ?P) = 1"
+      by (simp add: prod_measure_space_def, subst prod_measure_times, simp_all)
+    with fms_P show "finite_prob_space ?P"
+      by (simp add: finite_prob_space_eq)
+
+    from ms_X ms_Y X.top Y.top X.prob_space Y.prob_space Y.not_empty X_space Y_space
+    have "measure ?P' (space ?P') = 1" unfolding prob_space[symmetric]
+      by (auto simp add: prod_measure_space_def distribution_def vimage_Times comp_def
+        intro!: arg_cong[where f=prob])
+    with fms_P' show "finite_prob_space ?P'"
+      by (simp add: finite_prob_space_eq)
   qed
 qed
 
-lemma (in finite_prob_space) distribution_log_split:
-  assumes "1 < b"
-  shows
-  "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
-                                                     (distribution X {X x} * distribution Z {z})) =
-   distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
-                                                     distribution Z {z}) -
-   distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution X {X x})"
-  (is "?lhs = ?rhs")
-proof (cases "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} = 0")
-  case True thus ?thesis by simp
-next
-  case False
-
-  let ?dZ = "distribution Z"
-  let ?dX = "distribution X"
-  let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
-
-  have dist_nneg: "\<And>x X. 0 \<le> distribution X x"
-    unfolding distribution_def using sets_eq_Pow by (auto intro: positive)
-
-  have "?lhs = ?dXZ {(X x, z)} * (log b (?dXZ {(X x, z)} / ?dZ {z}) - log b (?dX {X x}))"
-  proof -
-    have pos_dXZ: "0 < ?dXZ {(X x, z)}"
-      using False dist_nneg[of "\<lambda>x. (X x, Z x)" "{(X x, z)}"] by auto
-    moreover
-    have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (X -` {X x}) \<inter> space M" by auto
-    hence "?dXZ {(X x, z)} \<le> ?dX {X x}"
-      unfolding distribution_def
-      by (rule measure_mono) (simp_all add: sets_eq_Pow)
-    with pos_dXZ have "0 < ?dX {X x}" by (rule less_le_trans)
-    moreover
-    have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (Z -` {z}) \<inter> space M" by auto
-    hence "?dXZ {(X x, z)} \<le> ?dZ {z}"
-      unfolding distribution_def
-      by (rule measure_mono) (simp_all add: sets_eq_Pow)
-    with pos_dXZ have "0 < ?dZ {z}" by (rule less_le_trans)
-    moreover have "0 < b" by (rule less_trans[OF _ `1 < b`]) simp
-    moreover have "b \<noteq> 1" by (rule ccontr) (insert `1 < b`, simp)
-    ultimately show ?thesis
-      using pos_dXZ
-      apply (subst (2) mult_commute)
-      apply (subst divide_divide_eq_left[symmetric])
-      apply (subst log_divide)
-      by (auto intro: divide_pos_pos)
-  qed
-  also have "... = ?rhs"
-    by (simp add: field_simps)
-  finally show ?thesis .
-qed
-
-lemma (in finite_prob_space) finite_mutual_information_reduce_prod:
-  "mutual_information b
-    \<lparr> space = X ` space M, sets = Pow (X ` space M) \<rparr>
-    \<lparr> space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M) \<rparr>
-    X (\<lambda>x. (Y x,Z x)) =
-    (\<Sum> (x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.
-      distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} *
-      log b (distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} /
-              (distribution X {x} * distribution (\<lambda>x. (Y x,Z x)) {(y,z)})))" (is "_ = setsum ?log ?space")
-  unfolding Let_def mutual_information_def KL_divergence_def using finite_space
-proof (subst finite_measure_space.integral_finite_singleton,
-       simp_all add: prod_measure_space_def sigma_prod_sets_finite joint_distribution)
-  let ?sets = "Pow (X ` space M \<times> Y ` space M \<times> Z ` space M)"
-    and ?measure = "distribution (\<lambda>x. (X x, Y x, Z x))"
-  let ?P = "\<lparr> space = ?space, sets = ?sets, measure = ?measure\<rparr>"
-
-  show "finite_measure_space ?P"
-  proof (rule finite_Pow_additivity_sufficient, simp_all)
-    show "finite ?space" using finite_space by auto
-
-    show "positive ?P ?measure"
-      using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
-
-    show "additive ?P ?measure"
-    proof (simp add: additive_def distribution_def, safe)
-      fix x y assume "x \<subseteq> ?space" and "y \<subseteq> ?space"
-      assume "x \<inter> y = {}"
-      thus "prob (((\<lambda>x. (X x, Y x, Z x)) -` x \<union> (\<lambda>x. (X x, Y x, Z x)) -` y) \<inter> space M) =
-            prob ((\<lambda>x. (X x, Y x, Z x)) -` x \<inter> space M) + prob ((\<lambda>x. (X x, Y x, Z x)) -` y \<inter> space M)"
-        apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
-        by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
-    qed
-  qed
+lemma (in finite_information_space) mutual_information_eq:
+  "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
+    distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /
+                                                   (distribution X {x} * distribution Y {y})))"
+  by (subst mutual_information_eq_generic) (simp_all add: finite_prob_space_of_images)
 
-  let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
-  and ?YZ = "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M), measure = distribution (\<lambda>x. (Y x, Z x))\<rparr>"
-  let ?u = "prod_measure ?X ?YZ"
-
-  from finite_measure_space[of X] finite_measure_space_image_prod[of Y Z]
-  have ms_X: "measure_space ?X" and ms_YZ: "measure_space ?YZ"
-    by (simp_all add: finite_measure_space_def)
-
-  show "(\<Sum>x \<in> ?space. log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
-    (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x})
-    = setsum ?log ?space"
-  proof (rule setsum_cong)
-    fix x assume x: "x \<in> ?space"
-    then obtain d e f where x_Pair: "x = (d, e, f)"
-      and d: "d \<in> X ` space M"
-      and e: "e \<in> Y ` space M"
-      and f: "f \<in> Z ` space M" by auto
-
-    { fix x assume m_0: "?u {x} = 0"
-
-      let ?PROD = "(\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M"
-      obtain a b c where Pair: "x = (a, b, c)" by (cases x)
-      hence "?PROD = (X -` {a} \<inter> space M) \<inter> ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M)"
-        and x_prod: "{x} = {a} \<times> {(b, c)}" by auto
-
-      have "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0"
-      proof (cases "{a} \<subseteq> X ` space M")
-        case False
-        hence "?PROD = {}"
-          unfolding Pair by auto
-        thus ?thesis by (auto simp: distribution_def)
-      next
-        have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
-          using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
-
-        case True
-        with prod_measure_times[OF ms_X ms_YZ, simplified, of "{a}" "{(b,c)}"]
-        have "prob (X -` {a} \<inter> space M) = 0 \<or> prob ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M) = 0"
-          (is "prob ?X = 0 \<or> prob ?Y = 0") using m_0
-          by (simp add: prod_measure_space_def distribution_def Pair)
-        thus ?thesis
-        proof (rule disjE)
-          assume "prob ?X = 0"
-          have "prob ?PROD \<le> prob ?X"
-            using sets_eq_Pow Pair by (auto intro!: measure_mono)
-          thus ?thesis using `prob ?X = 0` by (auto simp: distribution_def)
-        next
-          assume "prob ?Y = 0"
-          have "prob ?PROD \<le> prob ?Y"
-            using sets_eq_Pow Pair by (auto intro!: measure_mono)
-          thus ?thesis using `prob ?Y = 0` by (auto simp: distribution_def)
-        qed
-      qed }
-    note measure_zero_joint_distribution = this
-
-    from x_Pair d e f finite_space
-    show "log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
-      (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x} = ?log x"
-    apply (cases "distribution (\<lambda>x. (X x, Y x, Z x)) {x} \<noteq> 0")
-    apply (subst finite_measure_space.RN_deriv_finite_singleton)
-    proof simp_all
-      show "measure_space ?P" using `finite_measure_space ?P` by (simp add: finite_measure_space_def)
-
-      from finite_measure_space_finite_prod_measure[OF finite_measure_space[of X]
-        finite_measure_space_image_prod[of Y Z]] finite_space
-      show "finite_measure_space \<lparr>space=?space, sets=?sets, measure=?u\<rparr>"
-        by (simp add: prod_measure_space_def sigma_prod_sets_finite)
-    next
-      fix x assume "?u {x} = 0" thus "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0" by fact
-    next
-      assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
-      show "?u {(d,e,f)} \<noteq> 0"
-      proof
-        assume "?u {(d, e, f)} = 0"
-        from measure_zero_joint_distribution[OF this] jd_0
-        show False by simp
-      qed
-    next
-      assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
-      with prod_measure_times[OF ms_X ms_YZ, simplified, of "{d}" "{(e,f)}"] d
-      show "log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / ?u {(d, e, f)}) =
-        log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / (distribution X {d} * distribution (\<lambda>x. (Y x, Z x)) {(e,f)}))"
-        by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
-    qed
-  qed simp
-qed
+lemma (in finite_information_space) mutual_information_positive: "0 \<le> \<I>(X;Y)"
+  by (subst mutual_information_positive_generic) (simp_all add: finite_prob_space_of_images)
 
 definition (in prob_space)
   "entropy b s X = mutual_information b s s X X"
 
-abbreviation (in finite_prob_space)
-  finite_entropy ("\<H>\<^bsub>_\<^esub>'(_')") where
-  "\<H>\<^bsub>b\<^esub>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
-
-abbreviation (in finite_prob_space)
-  finite_entropy_2 ("\<H>'(_')") where
-  "\<H>(X) \<equiv> \<H>\<^bsub>2\<^esub>(X)"
+abbreviation (in finite_information_space)
+  finite_entropy ("\<H>'(_')") where
+  "\<H>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
 
-lemma (in finite_prob_space) finite_entropy_reduce:
-  assumes "1 < b"
-  shows "\<H>\<^bsub>b\<^esub>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
+lemma (in finite_information_space) joint_distribution_remove[simp]:
+    "joint_distribution X X {(x, x)} = distribution X {x}"
+  unfolding distribution_def by (auto intro!: arg_cong[where f=prob])
+
+lemma (in finite_information_space) entropy_eq:
+  "\<H>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
 proof -
-  have fin: "finite (X ` space M)" using finite_space by simp
-
-  have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
-
+  { fix f
   { fix x y
     have "(\<lambda>x. (X x, X x)) -` {(x, y)} = (if x = y then X -` {x} else {})" by auto
-    hence "distribution (\<lambda>x. (X x, X x))  {(x,y)} = (if x = y then distribution X {x} else 0)"
+      hence "distribution (\<lambda>x. (X x, X x))  {(x,y)} * f x y = (if x = y then distribution X {x} * f x y else 0)"
       unfolding distribution_def by auto }
-  moreover
-  have "\<And>x. 0 \<le> distribution X x"
-    unfolding distribution_def using finite_space sets_eq_Pow by (auto intro: positive)
-  hence "\<And>x. distribution X x \<noteq> 0 \<Longrightarrow> 0 < distribution X x" by (auto simp: le_less)
-  ultimately
-  show ?thesis using `1 < b`
-    by (auto intro!: setsum_cong
-      simp: log_inverse If_mult_distr setsum_cases[OF fin] inverse_eq_divide[symmetric]
-        entropy_def setsum_negf[symmetric] joint_distribution finite_mutual_information_reduce
-        setsum_cartesian_product[symmetric])
+    hence "(\<Sum>(x, y) \<in> X ` space M \<times> X ` space M. joint_distribution X X {(x, y)} * f x y) =
+      (\<Sum>x \<in> X ` space M. distribution X {x} * f x x)"
+      unfolding setsum_cartesian_product' by (simp add: setsum_cases finite_space) }
+  note remove_cartesian_product = this
+
+  show ?thesis
+    unfolding entropy_def mutual_information_eq setsum_negf[symmetric] remove_cartesian_product
+    by (auto intro!: setsum_cong)
 qed
 
-lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
-proof (rule inj_onI, simp)
-  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
-  show "x = y"
-  proof (cases rule: linorder_cases)
-    assume "x < y" hence "log b x < log b y"
-      using log_less_cancel_iff[OF `1 < b`] pos by simp
-    thus ?thesis using * by simp
-  next
-    assume "y < x" hence "log b y < log b x"
-      using log_less_cancel_iff[OF `1 < b`] pos by simp
-    thus ?thesis using * by simp
-  qed simp
-qed
+lemma (in finite_information_space) entropy_positive: "0 \<le> \<H>(X)"
+  unfolding entropy_def using mutual_information_positive .
 
 definition (in prob_space)
   "conditional_mutual_information b s1 s2 s3 X Y Z \<equiv>
@@ -524,160 +415,181 @@
       mutual_information b s1 prod_space X (\<lambda>x. (Y x, Z x)) -
       mutual_information b s1 s3 X Z"
 
-abbreviation (in finite_prob_space)
-  finite_conditional_mutual_information ("\<I>\<^bsub>_\<^esub>'( _ ; _ | _ ')") where
-  "\<I>\<^bsub>b\<^esub>(X ; Y | Z) \<equiv> conditional_mutual_information b
+abbreviation (in finite_information_space)
+  finite_conditional_mutual_information ("\<I>'( _ ; _ | _ ')") where
+  "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr>
     \<lparr> space = Z`space M, sets = Pow (Z`space M) \<rparr>
     X Y Z"
 
-abbreviation (in finite_prob_space)
-  finite_conditional_mutual_information_2 ("\<I>'( _ ; _ | _ ')") where
-  "\<I>(X ; Y | Z) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y | Z)"
+lemma (in finite_information_space) setsum_distribution_gen:
+  assumes "Z -` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y -` {f x}) \<inter> space M"
+  and "inj_on f (X`space M)"
+  shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}"
+  unfolding distribution_def assms
+  using finite_space assms
+  by (subst measure_finitely_additive'')
+     (auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def
+      intro!: arg_cong[where f=prob])
+
+lemma (in finite_information_space) setsum_distribution:
+  "(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}"
+  "(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}"
+  "(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}"
+  "(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}"
+  "(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}"
+  by (auto intro!: inj_onI setsum_distribution_gen)
 
-lemma image_pair_eq_Sigma:
-  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
-proof (safe intro!: imageI vimageI, simp_all)
-  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
-  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" unfolding eq[symmetric]
-    using * by auto
+lemma (in finite_information_space) conditional_mutual_information_eq_sum:
+   "\<I>(X ; Y | Z) =
+     (\<Sum>(x, y, z)\<in>X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M.
+             distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
+             log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}/
+        distribution (\<lambda>x. (Y x, Z x)) {(y, z)})) -
+     (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
+        distribution (\<lambda>x. (X x, Z x)) {(x,z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(x,z)} / distribution Z {z}))"
+  (is "_ = ?rhs")
+proof -
+  have setsum_product:
+    "\<And>f x. (\<Sum>v\<in>(\<lambda>x. (Y x, Z x)) ` space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x,v)} * f v)
+      = (\<Sum>v\<in>Y ` space M \<times> Z ` space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x,v)} * f v)"
+  proof (safe intro!: setsum_mono_zero_cong_left imageI)
+    fix x y z f
+    assume *: "(Y y, Z z) \<notin> (\<lambda>x. (Y x, Z x)) ` space M" and "y \<in> space M" "z \<in> space M"
+    hence "(\<lambda>x. (X x, Y x, Z x)) -` {(x, Y y, Z z)} \<inter> space M = {}"
+    proof safe
+      fix x' assume x': "x' \<in> space M" and eq: "Y x' = Y y" "Z x' = Z z"
+      have "(Y y, Z z) \<in> (\<lambda>x. (Y x, Z x)) ` space M" using eq[symmetric] x' by auto
+      thus "x' \<in> {}" using * by auto
+    qed
+    thus "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, Y y, Z z)} * f (Y y) (Z z) = 0"
+      unfolding distribution_def by simp
+  qed (simp add: finite_space)
+
+  thus ?thesis
+    unfolding conditional_mutual_information_def Let_def mutual_information_eq
+    apply (subst mutual_information_eq_generic)
+    by (auto simp add: prod_measure_space_def sigma_prod_sets_finite finite_space
+        finite_prob_space_of_images finite_product_prob_space_of_images
+        setsum_cartesian_product' setsum_product setsum_subtractf setsum_addf
+        setsum_left_distrib[symmetric] setsum_distribution
+      cong: setsum_cong)
 qed
 
-lemma inj_on_swap: "inj_on (\<lambda>(x,y). (y,x)) A" by (auto intro!: inj_onI)
-
-lemma (in finite_prob_space) finite_conditional_mutual_information_reduce:
-  assumes "1 < b"
-  shows "\<I>\<^bsub>b\<^esub>(X ; Y | Z) =
-	- (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
-             distribution (\<lambda>x. (X x, Z x)) {(x,z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(x,z)} / distribution Z {z}))
-	+ (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
+lemma (in finite_information_space) conditional_mutual_information_eq:
+  "\<I>(X ; Y | Z) = (\<Sum>(x, y, z) \<in> X ` space M \<times> Y ` space M \<times> Z ` space M.
              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}/
-             distribution (\<lambda>x. (Y x, Z x)) {(y, z)}))" (is "_ = ?rhs")
-unfolding conditional_mutual_information_def Let_def using finite_space
-apply (simp add: prod_measure_space_def sigma_prod_sets_finite)
-apply (subst mutual_information_cong[of _ "\<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
-  _ "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M)\<rparr>"], simp_all)
-apply (subst finite_mutual_information_reduce_prod, simp_all)
-apply (subst finite_mutual_information_reduce, simp_all)
+    (joint_distribution X Z {(x, z)} * joint_distribution Y Z {(y,z)} / distribution Z {z})))"
+  unfolding conditional_mutual_information_def Let_def mutual_information_eq
+    apply (subst mutual_information_eq_generic)
+  by (auto simp add: prod_measure_space_def sigma_prod_sets_finite finite_space
+      finite_prob_space_of_images finite_product_prob_space_of_images
+      setsum_cartesian_product' setsum_product setsum_subtractf setsum_addf
+      setsum_left_distrib[symmetric] setsum_distribution setsum_commute[where A="Y`space M"]
+    cong: setsum_cong)
+
+lemma (in finite_information_space) conditional_mutual_information_eq_mutual_information:
+  "\<I>(X ; Y) = \<I>(X ; Y | (\<lambda>x. ()))"
+proof -
+  have [simp]: "(\<lambda>x. ()) ` space M = {()}" using not_empty by auto
+
+  show ?thesis
+    unfolding conditional_mutual_information_eq mutual_information_eq
+    by (simp add: setsum_cartesian_product' distribution_remove_const)
+qed
+
+lemma (in finite_information_space) conditional_mutual_information_positive:
+  "0 \<le> \<I>(X ; Y | Z)"
 proof -
   let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))"
-  let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
-  let ?dYZ = "distribution (\<lambda>x. (Y x, Z x))"
+  let ?dXZ = "joint_distribution X Z"
+  let ?dYZ = "joint_distribution Y Z"
   let ?dX = "distribution X"
-  let ?dY = "distribution Y"
   let ?dZ = "distribution Z"
+  let ?M = "X ` space M \<times> Y ` space M \<times> Z ` space M"
+
+  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: expand_fun_eq)
 
-  have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
-  { fix x y
-    have "(\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M =
-      (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then (\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M else {})" by auto
-    hence "?dXYZ {(X x, y)} = (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then ?dXYZ {(X x, y)} else 0)"
-      unfolding distribution_def by auto }
-  note split_measure = this
-
-  have sets: "Y ` space M \<times> Z ` space M \<inter> (\<lambda>x. (Y x, Z x)) ` space M = (\<lambda>x. (Y x, Z x)) ` space M" by auto
-
-  have cong: "\<And>A B C D. \<lbrakk> A = C ; B = D \<rbrakk> \<Longrightarrow> A + B = C + D" by auto
-
-  { fix A f have "setsum f A = setsum (\<lambda>(x, y). f (y, x)) ((\<lambda>(x, y). (y, x)) ` A)"
-    using setsum_reindex[OF inj_on_swap, of "\<lambda>(x, y). f (y, x)" A] by (simp add: split_twice) }
-  note setsum_reindex_swap = this
-
-  { fix A B f assume *: "finite A" "\<forall>x\<in>A. finite (B x)"
-    have "(\<Sum>x\<in>Sigma A B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) (B x))"
-      unfolding setsum_Sigma[OF *] by simp }
-  note setsum_Sigma = this
+  have "- (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
+    log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))
+    \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})"
+    unfolding split_beta
+  proof (rule log_setsum_divide)
+    show "?M \<noteq> {}" using not_empty by simp
+    show "1 < b" using b_gt_1 .
 
-  { fix x
-    have "(\<Sum>z\<in>Z ` space M. ?dXZ {(X x, z)}) = (\<Sum>yz\<in>(\<lambda>x. (Y x, Z x)) ` space M. ?dXYZ {(X x, yz)})"
-      apply (subst setsum_reindex_swap)
-      apply (simp add: image_image distribution_def)
-      unfolding image_pair_eq_Sigma
-      apply (subst setsum_Sigma)
-      using finite_space apply simp_all
-      apply (rule setsum_cong[OF refl])
-      apply (subst measure_finitely_additive'')
-      by (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) }
+    fix x assume "x \<in> ?M"
+    show "0 \<le> ?dXYZ {(fst x, fst (snd x), snd (snd x))}" using positive_distribution .
+    show "0 \<le> ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
+      by (auto intro!: mult_nonneg_nonneg positive_distribution simp: zero_le_divide_iff)
 
-  thus "(\<Sum>(x, y, z)\<in>X ` space M \<times> Y ` space M \<times> Z ` space M.
-      ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / (?dX {x} * ?dYZ {(y, z)}))) -
-    (\<Sum>(x, y)\<in>X ` space M \<times> Z ` space M.
-      ?dXZ {(x, y)} * log b (?dXZ {(x, y)} / (?dX {x} * ?dZ {y}))) =
-  - (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
-      ?dXZ {(x,z)} * log b (?dXZ {(x,z)} / ?dZ {z})) +
-    (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
-      ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / ?dYZ {(y, z)}))"
-    using finite_space
-    apply (auto simp: setsum_cartesian_product[symmetric] setsum_negf[symmetric]
-                      setsum_addf[symmetric] diff_minus
-      intro!: setsum_cong[OF refl])
-    apply (subst split_measure)
-    apply (simp add: If_mult_distr setsum_cases sets distribution_log_split[OF assms, of X])
-    apply (subst add_commute)
-    by (simp add: setsum_subtractf setsum_negf field_simps setsum_right_distrib[symmetric] sets_eq_Pow)
+    assume *: "0 < ?dXYZ {(fst x, fst (snd x), snd (snd x))}"
+    thus "0 < ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
+      by (auto intro!: divide_pos_pos mult_pos_pos
+           intro: distribution_order(6) distribution_mono_gt_0)
+  qed (simp_all add: setsum_cartesian_product' sum_over_space_distrib setsum_distribution finite_space)
+  also have "(\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}) = (\<Sum>z\<in>Z`space M. ?dZ {z})"
+    apply (simp add: setsum_cartesian_product')
+    apply (subst setsum_commute)
+    apply (subst (2) setsum_commute)
+    by (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric] setsum_distribution
+          intro!: setsum_cong)
+  finally show ?thesis
+    unfolding conditional_mutual_information_eq sum_over_space_distrib by simp
 qed
 
+
 definition (in prob_space)
   "conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y"
 
-abbreviation (in finite_prob_space)
-  finite_conditional_entropy ("\<H>\<^bsub>_\<^esub>'(_ | _')") where
-  "\<H>\<^bsub>b\<^esub>(X | Y) \<equiv> conditional_entropy b
+abbreviation (in finite_information_space)
+  finite_conditional_entropy ("\<H>'(_ | _')") where
+  "\<H>(X | Y) \<equiv> conditional_entropy b
     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
 
-abbreviation (in finite_prob_space)
-  finite_conditional_entropy_2 ("\<H>'(_ | _')") where
-  "\<H>(X | Y) \<equiv> \<H>\<^bsub>2\<^esub>(X | Y)"
+lemma (in finite_information_space) conditional_entropy_positive:
+  "0 \<le> \<H>(X | Y)" unfolding conditional_entropy_def using conditional_mutual_information_positive .
 
-lemma (in finite_prob_space) finite_conditional_entropy_reduce:
-  assumes "1 < b"
-  shows "\<H>\<^bsub>b\<^esub>(X | Z) =
+lemma (in finite_information_space) conditional_entropy_eq:
+  "\<H>(X | Z) =
      - (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
          joint_distribution X Z {(x, z)} *
          log b (joint_distribution X Z {(x, z)} / distribution Z {z}))"
 proof -
   have *: "\<And>x y z. (\<lambda>x. (X x, X x, Z x)) -` {(x, y, z)} = (if x = y then (\<lambda>x. (X x, Z x)) -` {(x, z)} else {})" by auto
   show ?thesis
-    unfolding finite_conditional_mutual_information_reduce[OF assms]
-      conditional_entropy_def joint_distribution_def distribution_def *
+    unfolding conditional_mutual_information_eq_sum
+      conditional_entropy_def distribution_def *
     by (auto intro!: setsum_0')
 qed
 
-lemma (in finite_prob_space) finite_mutual_information_eq_entropy_conditional_entropy:
-  assumes "1 < b" shows "\<I>\<^bsub>b\<^esub>(X ; Z) = \<H>\<^bsub>b\<^esub>(X) - \<H>\<^bsub>b\<^esub>(X | Z)" (is "mutual_information b ?X ?Z X Z = _")
-  unfolding finite_mutual_information_reduce
-    finite_entropy_reduce[OF assms]
-    finite_conditional_entropy_reduce[OF assms]
-    joint_distribution diff_minus_eq_add
+lemma (in finite_information_space) mutual_information_eq_entropy_conditional_entropy:
+  "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
+  unfolding mutual_information_eq entropy_eq conditional_entropy_eq
   using finite_space
-  apply (auto simp add: setsum_addf[symmetric] setsum_subtractf
-      setsum_Sigma[symmetric] distribution_log_split[OF assms] setsum_negf[symmetric]
-    intro!: setsum_cong[OF refl])
-  apply (simp add: setsum_negf setsum_left_distrib[symmetric])
-proof (rule disjI2)
-  let ?dX = "distribution X"
-  and ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
+  by (auto simp add: setsum_addf setsum_subtractf setsum_cartesian_product'
+      setsum_left_distrib[symmetric] setsum_addf setsum_distribution)
 
-  fix x assume "x \<in> space M"
-  have "\<And>z. (\<lambda>x. (X x, Z x)) -` {(X x, z)} \<inter> space M = (X -` {X x} \<inter> space M) \<inter> (Z -` {z} \<inter> space M)" by auto
-  thus "(\<Sum>z\<in>Z ` space M. distribution (\<lambda>x. (X x, Z x)) {(X x, z)}) = distribution X {X x}"
-    unfolding distribution_def
-    apply (subst prob_real_sum_image_fn[where e="X -` {X x} \<inter> space M" and s = "Z`space M" and f="\<lambda>z. Z -` {z} \<inter> space M"])
-    using finite_space sets_eq_Pow by auto
+lemma (in finite_information_space) conditional_entropy_less_eq_entropy:
+  "\<H>(X | Z) \<le> \<H>(X)"
+proof -
+  have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy .
+  with mutual_information_positive[of X Z] entropy_positive[of X]
+  show ?thesis by auto
 qed
 
 (* -------------Entropy of a RV with a certain event is zero---------------- *)
 
-lemma (in finite_prob_space) finite_entropy_certainty_eq_0:
-  assumes "x \<in> X ` space M" and "distribution X {x} = 1" and "b > 1"
-  shows "\<H>\<^bsub>b\<^esub>(X) = 0"
+lemma (in finite_information_space) finite_entropy_certainty_eq_0:
+  assumes "x \<in> X ` space M" and "distribution X {x} = 1"
+  shows "\<H>(X) = 0"
 proof -
   interpret X: finite_prob_space "\<lparr> space = X ` space M,
     sets = Pow (X ` space M),
-    measure = distribution X\<rparr>" by (rule finite_prob_space)
+    measure = distribution X\<rparr>" by (rule finite_prob_space_of_images)
 
   have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"
     using X.measure_compl[of "{x}"] assms by auto
@@ -694,366 +606,18 @@
 
   have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp
 
-  show ?thesis
-    unfolding finite_entropy_reduce[OF `b > 1`] by (auto simp: y fi)
+  show ?thesis unfolding entropy_eq by (auto simp: y fi)
 qed
 (* --------------- upper bound on entropy for a rv ------------------------- *)
 
-definition convex_set :: "real set \<Rightarrow> bool"
-where
-  "convex_set C \<equiv> (\<forall> x y \<mu>. x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> \<mu> * x + (1 - \<mu>) * y \<in> C)"
-
-lemma pos_is_convex:
-  shows "convex_set {0 <..}"
-unfolding convex_set_def
-proof safe
-  fix x y \<mu> :: real
-  assume asms: "\<mu> \<ge> 0" "\<mu> \<le> 1" "x > 0" "y > 0"
-  { assume "\<mu> = 0"
-    hence "\<mu> * x + (1 - \<mu>) * y = y" by simp
-    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
-  moreover
-  { assume "\<mu> = 1"
-    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
-  moreover
-  { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
-    hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
-    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms
-      apply (subst add_nonneg_pos[of "\<mu> * x" "(1 - \<mu>) * y"])
-      using real_mult_order by auto fastsimp }
-  ultimately show "\<mu> * x + (1 - \<mu>) * y > 0" using assms by blast
-qed
-
-definition convex_fun :: "(real \<Rightarrow> real) \<Rightarrow> real set \<Rightarrow> bool"
-where
-  "convex_fun f C \<equiv> (\<forall> x y \<mu>. convex_set C \<and> (x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1 
-                   \<longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y))"
-
-lemma pos_convex_function:
-  fixes f :: "real \<Rightarrow> real"
-  assumes "convex_set C"
-  assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
-  shows "convex_fun f C"
-unfolding convex_fun_def
-using assms
-proof safe
-  fix x y \<mu> :: real
-  let ?x = "\<mu> * x + (1 - \<mu>) * y"
-  assume asm: "convex_set C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
-  hence "1 - \<mu> \<ge> 0" by auto
-  hence xpos: "?x \<in> C" using asm unfolding convex_set_def by auto
-  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) 
-            \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
-    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
-      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
-  hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
-    by (auto simp add:field_simps)
-  thus "\<mu> * f x + (1 - \<mu>) * f y \<ge> f ?x" by simp
-qed
-
-lemma atMostAtLeast_subset_convex:
-  assumes "convex_set C"
-  assumes "x \<in> C" "y \<in> C" "x < y"
-  shows "{x .. y} \<subseteq> C"
-proof safe
-  fix z assume zasm: "z \<in> {x .. y}"
-  { assume asm: "x < z" "z < y"
-    let "?\<mu>" = "(y - z) / (y - x)"
-    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps)
-    hence comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C" 
-      using assms[unfolded convex_set_def] by blast
-    have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
-      by (auto simp add:field_simps)
-    also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
-      using assms unfolding add_divide_distrib by (auto simp:field_simps)
-    also have "\<dots> = z" 
-      using assms by (auto simp:field_simps)
-    finally have "z \<in> C"
-      using comb by auto } note less = this
-  show "z \<in> C" using zasm less assms
-    unfolding atLeastAtMost_iff le_less by auto
-qed
-
-lemma f''_imp_f':
-  fixes f :: "real \<Rightarrow> real"
-  assumes "convex_set C"
-  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
-  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
-  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
-  assumes "x \<in> C" "y \<in> C"
-  shows "f' x * (y - x) \<le> f y - f x"
-using assms
-proof -
-  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x"
-    hence ge: "y - x > 0" "y - x \<ge> 0" by auto
-    from asm have le: "x - y < 0" "x - y \<le> 0" by auto
-    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
-      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `y \<in> C` `x < y`],
-        THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
-      by auto
-    hence "z1 \<in> C" using atMostAtLeast_subset_convex
-      `convex_set C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
-    from z1 have z1': "f x - f y = (x - y) * f' z1"
-      by (simp add:field_simps)
-    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
-      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1`],
-        THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
-      by auto
-    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
-      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y`],
-        THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
-      by auto
-    have "f' y - (f x - f y) / (x - y) = f' y - f' z1" 
-      using asm z1' by auto
-    also have "\<dots> = (y - z1) * f'' z3" using z3 by auto
-    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
-    have A': "y - z1 \<ge> 0" using z1 by auto
-    have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
-      `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
-    hence B': "f'' z3 \<ge> 0" using assms by auto
-    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
-    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
-    from mult_right_mono_neg[OF this le(2)]
-    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
-      unfolding diff_def using real_add_mult_distrib by auto
-    hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
-    hence res: "f' y * (x - y) \<le> f x - f y" by auto
-    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
-      using asm z1 by auto
-    also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto
-    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
-    have A: "z1 - x \<ge> 0" using z1 by auto
-    have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
-      `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
-    hence B: "f'' z2 \<ge> 0" using assms by auto
-    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
-    from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
-    from mult_right_mono[OF this ge(2)]
-    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)" 
-      unfolding diff_def using real_add_mult_distrib by auto
-    hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
-    hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
-      using res by auto } note less_imp = this
-  { fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y"
-    hence"f y - f x \<ge> f' x * (y - x)"
-    unfolding neq_iff apply safe
-    using less_imp by auto } note neq_imp = this
-  moreover
-  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y"
-    hence "f y - f x \<ge> f' x * (y - x)" by auto }
-  ultimately show ?thesis using assms by blast
-qed
-
-lemma f''_ge0_imp_convex:
-  fixes f :: "real \<Rightarrow> real"
-  assumes conv: "convex_set C"
-  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
-  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
-  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
-  shows "convex_fun f C"
-using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
-
-lemma minus_log_convex:
-  fixes b :: real
-  assumes "b > 1"
-  shows "convex_fun (\<lambda> x. - log b x) {0 <..}"
-proof -
-  have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
-  hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
-    using DERIV_minus by auto
-  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
-    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
-  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
-  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
-    by auto
-  hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
-    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
-  have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
-    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
-  from f''_ge0_imp_convex[OF pos_is_convex, 
-    unfolded greaterThan_iff, OF f' f''0 f''_ge0]
-  show ?thesis by auto
-qed
-
-lemma setsum_nonneg_0:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "finite s"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
-  assumes "(\<Sum> i \<in> s. f i) = 0"
-  assumes "i \<in> s"
-  shows "f i = 0"
-proof -
-  { assume asm: "f i > 0"
-    from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
-    from setsum_nonneg[of "s - {i}" f, OF this]
-    have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
-    hence "(\<Sum> j \<in> s - {i}. f j) + f i > 0" using asm by auto
-    from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
-    have "(\<Sum> j \<in> s. f j) > 0" by auto
-    hence "False" using assms by auto }
-  thus ?thesis using assms by fastsimp
-qed
-
-lemma setsum_nonneg_leq_1:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "finite s"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
-  assumes "(\<Sum> i \<in> s. f i) = 1"
-  assumes "i \<in> s"
-  shows "f i \<le> 1"
-proof -
-  { assume asm: "f i > 1"
-    from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
-    from setsum_nonneg[of "s - {i}" f, OF this]
-    have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
-    hence "(\<Sum> j \<in> s - {i}. f j) + f i > 1" using asm by auto
-    from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
-    have "(\<Sum> j \<in> s. f j) > 1" by auto
-    hence "False" using assms by auto }
-  thus ?thesis using assms by fastsimp
-qed
-
-lemma convex_set_setsum:
-  assumes "finite s" "s \<noteq> {}"
-  assumes "convex_set C"
-  assumes "(\<Sum> i \<in> s. a i) = 1"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
-  shows "(\<Sum> j \<in> s. a j * y j) \<in> C"
-using assms
-proof (induct s arbitrary:a rule:finite_ne_induct)
-  case (singleton i) note asms = this
-  hence "a i = 1" by auto
-  thus ?case using asms by auto
-next
-  case (insert i s) note asms = this
-  { assume "a i = 1"
-    hence "(\<Sum> j \<in> s. a j) = 0"
-      using asms by auto
-    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 
-      using setsum_nonneg_0 asms by fastsimp
-    hence ?case using asms by auto }
-  moreover
-  { assume asm: "a i \<noteq> 1"
-    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
-    have fis: "finite (insert i s)" using asms by auto
-    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
-    hence "a i < 1" using asm by auto
-    hence i0: "1 - a i > 0" by auto
-    let "?a j" = "a j / (1 - a i)"
-    { fix j assume "j \<in> s"
-      hence "?a j \<ge> 0" 
-        using i0 asms divide_nonneg_pos 
-        by fastsimp } note a_nonneg = this
-    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
-    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
-    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
-    from this asms
-    have "(\<Sum>j\<in>s. ?a j * y j) \<in> C" using a_nonneg by fastsimp
-    hence "a i * y i + (1 - a i) * (\<Sum> j \<in> s. ?a j * y j) \<in> C"
-      using asms[unfolded convex_set_def, rule_format] yai ai1 by auto
-    hence "a i * y i + (\<Sum> j \<in> s. (1 - a i) * (?a j * y j)) \<in> C"
-      using mult_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j * y j" s] by auto
-    hence "a i * y i + (\<Sum> j \<in> s. a j * y j) \<in> C" using i0 by auto
-    hence ?case using setsum.insert asms by auto }
-  ultimately show ?case by auto
-qed
-
-lemma convex_fun_setsum:
-  fixes a :: "'a \<Rightarrow> real"
-  assumes "finite s" "s \<noteq> {}"
-  assumes "convex_fun f C"
-  assumes "(\<Sum> i \<in> s. a i) = 1"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
-  shows "f (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
-using assms
-proof (induct s arbitrary:a rule:finite_ne_induct)
-  case (singleton i)
-  hence ai: "a i = 1" by auto
-  thus ?case by auto
-next
-  case (insert i s) note asms = this
-  hence "convex_fun f C" by simp
-  from this[unfolded convex_fun_def, rule_format]
-  have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk>
-  \<Longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
-    by simp
-  { assume "a i = 1"
-    hence "(\<Sum> j \<in> s. a j) = 0"
-      using asms by auto
-    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 
-      using setsum_nonneg_0 asms by fastsimp
-    hence ?case using asms by auto }
-  moreover
-  { assume asm: "a i \<noteq> 1"
-    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
-    have fis: "finite (insert i s)" using asms by auto
-    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
-    hence "a i < 1" using asm by auto
-    hence i0: "1 - a i > 0" by auto
-    let "?a j" = "a j / (1 - a i)"
-    { fix j assume "j \<in> s"
-      hence "?a j \<ge> 0" 
-        using i0 asms divide_nonneg_pos 
-        by fastsimp } note a_nonneg = this
-    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
-    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
-    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
-    have "convex_set C" using asms unfolding convex_fun_def by auto
-    hence asum: "(\<Sum> j \<in> s. ?a j * y j) \<in> C"
-      using asms convex_set_setsum[OF `finite s` `s \<noteq> {}` 
-        `convex_set C` a1 a_nonneg] by auto
-    have asum_le: "f (\<Sum> j \<in> s. ?a j * y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))"
-      using a_nonneg a1 asms by blast
-    have "f (\<Sum> j \<in> insert i s. a j * y j) = f ((\<Sum> j \<in> s. a j * y j) + a i * y i)"
-      using setsum.insert[of s i "\<lambda> j. a j * y j", OF `finite s` `i \<notin> s`] asms 
-      by (auto simp only:add_commute)
-    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j) / (1 - a i) + a i * y i)"
-      using i0 by auto
-    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j / (1 - a i)) + a i * y i)"
-      unfolding divide.setsum[of "\<lambda> j. a j * y j" s "1 - a i", symmetric] by auto
-    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. ?a j * y j) + a i * y i)" by auto
-    also have "\<dots> \<le> (1 - a i) * f ((\<Sum> j \<in> s. ?a j * y j)) + a i * f (y i)"
-      using conv[of "y i" "(\<Sum> j \<in> s. ?a j * y j)" "a i", OF yai(1) asum yai(2) ai1]
-      by (auto simp only:add_commute)
-    also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
-      using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", 
-        OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
-    also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
-      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
-    also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
-    also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
-    finally have "f (\<Sum> j \<in> insert i s. a j * y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
-      by simp }
-  ultimately show ?case by auto
-qed
-
-lemma log_setsum:
-  assumes "finite s" "s \<noteq> {}"
-  assumes "b > 1"
-  assumes "(\<Sum> i \<in> s. a i) = 1"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
-  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
-  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
-proof -
-  have "convex_fun (\<lambda> x. - log b x) {0 <..}"
-    by (rule minus_log_convex[OF `b > 1`])
-  hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
-    using convex_fun_setsum assms by blast
-  thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
-qed
-
-lemma (in finite_prob_space) finite_entropy_le_card:
-  assumes "1 < b"
-  shows "\<H>\<^bsub>b\<^esub>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
+lemma (in finite_information_space) finite_entropy_le_card:
+  "\<H>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
 proof -
   interpret X: finite_prob_space "\<lparr>space = X ` space M,
                                     sets = Pow (X ` space M),
                                  measure = distribution X\<rparr>"
-    using finite_prob_space by auto
+    using finite_prob_space_of_images by auto
+
   have triv: "\<And> x. (if distribution X {x} \<noteq> 0 then distribution X {x} else 0) = distribution X {x}"
     by auto
   hence sum1: "(\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x}) = 1"
@@ -1085,7 +649,7 @@
     also have "\<dots> = (if distribution X {x} \<noteq> 0
                     then distribution X {x} * log b (inverse (distribution X {x}))
                     else 0)"
-      using log_inverse `1 < b` X.positive[of "{x}"] asm by auto
+      using log_inverse b_gt_1 X.positive[of "{x}"] asm by auto
     finally have "- distribution X {x} * log b (distribution X {x})
                  = (if distribution X {x} \<noteq> 0 
                     then distribution X {x} * log b (inverse (distribution X {x}))
@@ -1101,7 +665,7 @@
     unfolding setsum_restrict_set[OF finite_imageI[OF finite_space, of X]] by auto
   also have "\<dots> \<le> log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
                           distribution X {x} * (inverse (distribution X {x})))"
-    apply (subst log_setsum[OF _ _ `b > 1` sum1, 
+    apply (subst log_setsum[OF _ _ b_gt_1 sum1, 
      unfolded greaterThan_iff, OF _ _ _]) using pos sets_eq_Pow
       X.finite_space assms X.positive not_empty by auto
   also have "\<dots> = log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. 1)"
@@ -1110,7 +674,7 @@
     by auto
   finally have "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
                \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" by simp
-  thus ?thesis unfolding finite_entropy_reduce[OF assms] real_eq_of_nat by auto
+  thus ?thesis unfolding entropy_eq real_eq_of_nat by auto
 qed
 
 (* --------------- entropy is maximal for a uniform rv --------------------- *)
@@ -1140,34 +704,31 @@
     by (auto simp:field_simps)
 qed
 
-lemma (in finite_prob_space) finite_entropy_uniform_max:
-  assumes "b > 1"
+lemma (in finite_information_space) finite_entropy_uniform_max:
   assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
-  shows "\<H>\<^bsub>b\<^esub>(X) = log b (real (card (X ` space M)))"
+  shows "\<H>(X) = log b (real (card (X ` space M)))"
 proof -
   interpret X: finite_prob_space "\<lparr>space = X ` space M,
                                     sets = Pow (X ` space M),
                                  measure = distribution X\<rparr>"
-    using finite_prob_space by auto
+    using finite_prob_space_of_images by auto
+
   { fix x assume xasm: "x \<in> X ` space M"
     hence card_gt0: "real (card (X ` space M)) > 0"
       using card_gt_0_iff X.finite_space by auto
     from xasm have "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = distribution X {x}"
       using assms by blast
     hence "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
-         = - (\<Sum> y \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
-      by auto
-    also have "\<dots> = - real_of_nat (card (X ` space M)) * distribution X {x} * log b (distribution X {x})"
-      by auto
+         = - real (card (X ` space M)) * distribution X {x} * log b (distribution X {x})"
+      unfolding real_eq_of_nat by auto
     also have "\<dots> = - real (card (X ` space M)) * (1 / real (card (X ` space M))) * log b (1 / real (card (X ` space M)))"
-      unfolding real_eq_of_nat[symmetric]
-      by (auto simp: X.uniform_prob[simplified, OF xasm assms(2)])
+      by (auto simp: X.uniform_prob[simplified, OF xasm assms])
     also have "\<dots> = log b (real (card (X ` space M)))"
       unfolding inverse_eq_divide[symmetric]
-      using card_gt0 log_inverse `b > 1` 
+      using card_gt0 log_inverse b_gt_1
       by (auto simp add:field_simps card_gt0)
     finally have ?thesis
-      unfolding finite_entropy_reduce[OF `b > 1`] by auto }
+      unfolding entropy_eq by auto }
   moreover
   { assume "X ` space M = {}"
     hence "distribution X (X ` space M) = 0"
@@ -1176,4 +737,199 @@
   ultimately show ?thesis by auto
 qed
 
+definition "subvimage A f g \<longleftrightarrow> (\<forall>x \<in> A. f -` {f x} \<inter> A \<subseteq> g -` {g x} \<inter> A)"
+
+lemma subvimageI:
+  assumes "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
+  shows "subvimage A f g"
+  using assms unfolding subvimage_def by blast
+
+lemma subvimageE[consumes 1]:
+  assumes "subvimage A f g"
+  obtains "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
+  using assms unfolding subvimage_def by blast
+
+lemma subvimageD:
+  "\<lbrakk> subvimage A f g ; x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
+  using assms unfolding subvimage_def by blast
+
+lemma subvimage_subset:
+  "\<lbrakk> subvimage B f g ; A \<subseteq> B \<rbrakk> \<Longrightarrow> subvimage A f g"
+  unfolding subvimage_def by auto
+
+lemma subvimage_idem[intro]: "subvimage A g g"
+  by (safe intro!: subvimageI)
+
+lemma subvimage_comp_finer[intro]:
+  assumes svi: "subvimage A g h"
+  shows "subvimage A g (f \<circ> h)"
+proof (rule subvimageI, simp)
+  fix x y assume "x \<in> A" "y \<in> A" "g x = g y"
+  from svi[THEN subvimageD, OF this]
+  show "f (h x) = f (h y)" by simp
+qed
+
+lemma subvimage_comp_gran:
+  assumes svi: "subvimage A g h"
+  assumes inj: "inj_on f (g ` A)"
+  shows "subvimage A (f \<circ> g) h"
+  by (rule subvimageI) (auto intro!: subvimageD[OF svi] simp: inj_on_iff[OF inj])
+
+lemma subvimage_comp:
+  assumes svi: "subvimage (f ` A) g h"
+  shows "subvimage A (g \<circ> f) (h \<circ> f)"
+  by (rule subvimageI) (auto intro!: svi[THEN subvimageD])
+
+lemma subvimage_trans:
+  assumes fg: "subvimage A f g"
+  assumes gh: "subvimage A g h"
+  shows "subvimage A f h"
+  by (rule subvimageI) (auto intro!: fg[THEN subvimageD] gh[THEN subvimageD])
+
+lemma subvimage_translator:
+  assumes svi: "subvimage A f g"
+  shows "\<exists>h. \<forall>x \<in> A. h (f x)  = g x"
+proof (safe intro!: exI[of _ "\<lambda>x. (THE z. z \<in> (g ` (f -` {x} \<inter> A)))"])
+  fix x assume "x \<in> A"
+  show "(THE x'. x' \<in> (g ` (f -` {f x} \<inter> A))) = g x"
+    by (rule theI2[of _ "g x"])
+      (insert `x \<in> A`, auto intro!: svi[THEN subvimageD])
+qed
+
+lemma subvimage_translator_image:
+  assumes svi: "subvimage A f g"
+  shows "\<exists>h. h ` f ` A = g ` A"
+proof -
+  from subvimage_translator[OF svi]
+  obtain h where "\<And>x. x \<in> A \<Longrightarrow> h (f x) = g x" by auto
+  thus ?thesis
+    by (auto intro!: exI[of _ h]
+      simp: image_compose[symmetric] comp_def cong: image_cong)
+qed
+
+lemma subvimage_finite:
+  assumes svi: "subvimage A f g" and fin: "finite (f`A)"
+  shows "finite (g`A)"
+proof -
+  from subvimage_translator_image[OF svi]
+  obtain h where "g`A = h`f`A" by fastsimp
+  with fin show "finite (g`A)" by simp
+qed
+
+lemma subvimage_disj:
+  assumes svi: "subvimage A f g"
+  shows "f -` {x} \<inter> A \<subseteq> g -` {y} \<inter> A \<or>
+      f -` {x} \<inter> g -` {y} \<inter> A = {}" (is "?sub \<or> ?dist")
+proof (rule disjCI)
+  assume "\<not> ?dist"
+  then obtain z where "z \<in> A" and "x = f z" and "y = g z" by auto
+  thus "?sub" using svi unfolding subvimage_def by auto
+qed
+
+lemma setsum_image_split:
+  assumes svi: "subvimage A f g" and fin: "finite (f ` A)"
+  shows "(\<Sum>x\<in>f`A. h x) = (\<Sum>y\<in>g`A. \<Sum>x\<in>f`(g -` {y} \<inter> A). h x)"
+    (is "?lhs = ?rhs")
+proof -
+  have "f ` A =
+      snd ` (SIGMA x : g ` A. f ` (g -` {x} \<inter> A))"
+      (is "_ = snd ` ?SIGMA")
+    unfolding image_split_eq_Sigma[symmetric]
+    by (simp add: image_compose[symmetric] comp_def)
+  moreover
+  have snd_inj: "inj_on snd ?SIGMA"
+    unfolding image_split_eq_Sigma[symmetric]
+    by (auto intro!: inj_onI subvimageD[OF svi])
+  ultimately
+  have "(\<Sum>x\<in>f`A. h x) = (\<Sum>(x,y)\<in>?SIGMA. h y)"
+    by (auto simp: setsum_reindex intro: setsum_cong)
+  also have "... = ?rhs"
+    using subvimage_finite[OF svi fin] fin
+    apply (subst setsum_Sigma[symmetric])
+    by (auto intro!: finite_subset[of _ "f`A"])
+  finally show ?thesis .
+qed
+
+lemma (in finite_information_space) entropy_partition:
+  assumes svi: "subvimage (space M) X P"
+  shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
+proof -
+  have "(\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x})) =
+    (\<Sum>y\<in>P `space M. \<Sum>x\<in>X ` space M.
+    joint_distribution X P {(x, y)} * log b (joint_distribution X P {(x, y)}))"
+  proof (subst setsum_image_split[OF svi],
+      safe intro!: finite_imageI finite_space setsum_mono_zero_cong_left imageI)
+    fix p x assume in_space: "p \<in> space M" "x \<in> space M"
+    assume "joint_distribution X P {(X x, P p)} * log b (joint_distribution X P {(X x, P p)}) \<noteq> 0"
+    hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M \<noteq> {}" by (auto simp: distribution_def)
+    with svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
+    show "x \<in> P -` {P p}" by auto
+  next
+    fix p x assume in_space: "p \<in> space M" "x \<in> space M"
+    assume "P x = P p"
+    from this[symmetric] svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
+    have "X -` {X x} \<inter> space M \<subseteq> P -` {P p} \<inter> space M"
+      by auto
+    hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M = X -` {X x} \<inter> space M"
+      by auto
+    thus "distribution X {X x} * log b (distribution X {X x}) =
+          joint_distribution X P {(X x, P p)} *
+          log b (joint_distribution X P {(X x, P p)})"
+      by (auto simp: distribution_def)
+  qed
+  thus ?thesis
+  unfolding entropy_eq conditional_entropy_eq
+    by (simp add: setsum_cartesian_product' setsum_subtractf setsum_distribution
+      setsum_left_distrib[symmetric] setsum_commute[where B="P`space M"])
+qed
+
+corollary (in finite_information_space) entropy_data_processing:
+  "\<H>(f \<circ> X) \<le> \<H>(X)"
+  by (subst (2) entropy_partition[of _ "f \<circ> X"]) (auto intro: conditional_entropy_positive)
+
+lemma (in prob_space) distribution_cong:
+  assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
+  shows "distribution X = distribution Y"
+  unfolding distribution_def expand_fun_eq
+  using assms by (auto intro!: arg_cong[where f=prob])
+
+lemma (in prob_space) joint_distribution_cong:
+  assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
+  assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
+  shows "joint_distribution X Y = joint_distribution X' Y'"
+  unfolding distribution_def expand_fun_eq
+  using assms by (auto intro!: arg_cong[where f=prob])
+
+lemma image_cong:
+  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> X x = X' x \<rbrakk> \<Longrightarrow> X ` S = X' ` S"
+  by (auto intro!: image_eqI)
+
+lemma (in finite_information_space) mutual_information_cong:
+  assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
+  assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
+  shows "\<I>(X ; Y) = \<I>(X' ; Y')"
+proof -
+  have "X ` space M = X' ` space M" using X by (rule image_cong)
+  moreover have "Y ` space M = Y' ` space M" using Y by (rule image_cong)
+  ultimately show ?thesis
+  unfolding mutual_information_eq
+    using
+      assms[THEN distribution_cong]
+      joint_distribution_cong[OF assms]
+    by (auto intro!: setsum_cong)
+qed
+
+corollary (in finite_information_space) entropy_of_inj:
+  assumes "inj_on f (X`space M)"
+  shows "\<H>(f \<circ> X) = \<H>(X)"
+proof (rule antisym)
+  show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing .
+next
+  have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
+    by (auto intro!: mutual_information_cong simp: entropy_def the_inv_into_f_f[OF assms])
+  also have "... \<le> \<H>(f \<circ> X)"
+    using entropy_data_processing .
+  finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
+qed
+
 end
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy	Tue May 04 14:44:30 2010 +0200
@@ -25,6 +25,21 @@
   shows "nonneg (neg_part f)"
   unfolding nonneg_def neg_part_def min_def by auto
 
+lemma pos_neg_part_abs:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
+unfolding real_abs_def pos_part_def neg_part_def by auto
+
+lemma pos_part_abs:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
+unfolding pos_part_def real_abs_def by auto
+
+lemma neg_part_abs:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
+unfolding neg_part_def real_abs_def by auto
+
 lemma (in measure_space)
   assumes "f \<in> borel_measurable M"
   shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"
@@ -1273,6 +1288,22 @@
   thus "?int S" and "?I S" by auto
 qed
 
+lemma (in measure_space) integrable_abs:
+  assumes "integrable f"
+  shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
+using assms
+proof -
+  from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"
+    unfolding integrable_def by auto
+  hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"
+    using nnfis_add by auto
+  hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp
+  thus ?thesis unfolding integrable_def
+    using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]
+      ext[OF neg_part_abs[of f], of "\<lambda> y. y"]
+    using nnfis_0 by auto
+qed
+
 lemma markov_ineq:
   assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
   shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
@@ -1310,6 +1341,61 @@
     by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
 qed
 
+lemma (in measure_space) integral_0:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"
+  shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"
+proof -
+  have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto
+  moreover
+  { fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"
+    hence "\<bar> f y \<bar> > 0" by auto
+    hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"
+      using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto
+    hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
+      by auto }
+  moreover
+  { fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
+    then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto
+    hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto
+    hence "\<bar>f y\<bar> > 0"
+      using real_of_nat_Suc_gt_zero
+        positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp
+    hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }
+  ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
+    by blast
+  { fix n
+    have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using integrable_abs assms by auto
+    have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M)
+           \<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"
+      using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto
+    hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"
+      using assms unfolding nonneg_def by auto
+    have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
+      apply (subst Int_commute) unfolding Int_def
+      using borel[unfolded borel_measurable_ge_iff] by simp
+    hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>
+      {x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
+      using positive le0 unfolding atLeast_def by fastsimp }
+  moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"
+    by auto
+  moreover
+  { fix n
+    have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"
+      using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp
+    hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)
+    hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M
+         \<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }
+  ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"
+    using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]
+    unfolding o_def by (simp del: of_nat_Suc)
+  hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"
+    using LIMSEQ_const[of 0] LIMSEQ_unique by simp
+  hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"
+    using assms unfolding nonneg_def by auto
+  thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp
+qed
+
 section "Lebesgue integration on countable spaces"
 
 lemma nnfis_on_countable:
@@ -1551,10 +1637,6 @@
 
 end
 
-locale finite_measure_space = measure_space +
-  assumes finite_space: "finite (space M)"
-  and sets_eq_Pow: "sets M = Pow (space M)"
-
 lemma sigma_algebra_cong:
   fixes M :: "('a, 'b) algebra_scheme" and M' :: "('a, 'c) algebra_scheme"
   assumes *: "sigma_algebra M"
@@ -1610,7 +1692,7 @@
 lemma (in finite_measure_space) RN_deriv_finite_singleton:
   fixes v :: "'a set \<Rightarrow> real"
   assumes ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
-  and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
+  and eq_0: "\<And>x. \<lbrakk> x \<in> space M ; measure M {x} = 0 \<rbrakk> \<Longrightarrow> v {x} = 0"
   and "x \<in> space M" and "measure M {x} \<noteq> 0"
   shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
   unfolding RN_deriv_def
@@ -1621,7 +1703,7 @@
   fix a assume "a \<in> sets M"
   hence "a \<subseteq> space M" and "finite a"
     using sets_into_space finite_space by (auto intro: finite_subset)
-  have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
+  have *: "\<And>x a. x \<in> space M \<Longrightarrow> (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
     v {x} * indicator_fn a x" using eq_0 by auto
 
   from measure_space.measure_real_sum_image[OF ms_v, of a]
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Probability/Measure.thy	Tue May 04 14:44:30 2010 +0200
@@ -365,6 +365,18 @@
     by arith
 qed
 
+lemma (in measure_space) measure_mono:
+  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
+  shows "measure M a \<le> measure M b"
+proof -
+  have "b = a \<union> (b - a)" using assms by auto
+  moreover have "{} = a \<inter> (b - a)" by auto
+  ultimately have "measure M b = measure M a + measure M (b - a)"
+    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
+  moreover have "measure M (b - a) \<ge> 0" using positive assms by auto
+  ultimately show "measure M a \<le> measure M b" by auto
+qed
+
 lemma disjoint_family_Suc:
   assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
   shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
@@ -1045,4 +1057,12 @@
   qed
 qed
 
+locale finite_measure_space = measure_space +
+  assumes finite_space: "finite (space M)"
+  and sets_eq_Pow: "sets M = Pow (space M)"
+
+lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. measure M {x}) = measure M (space M)"
+  using measure_finitely_additive''[of "space M" "\<lambda>i. {i}"]
+  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
+
 end
\ No newline at end of file
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Tue May 04 14:44:30 2010 +0200
@@ -21,22 +21,23 @@
 definition
   "distribution X = (\<lambda>s. prob ((X -` s) \<inter> (space M)))"
 
-definition
-  "probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1"
+abbreviation
+  "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"
 
-definition
-  "possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0"
+(*
+definition probably :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<^sup>*" 10) where
+  "probably P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } = 1"
+definition possibly :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>\<^sup>*" 10) where
+  "possibly P \<longleftrightarrow> { x. P x } \<in> events \<and> prob { x. P x } \<noteq> 0"
+*)
 
 definition
-  "joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) -` a \<inter> space M))"
+  "conditional_expectation X M' \<equiv> SOME f. f \<in> measurable M' borel_space \<and>
+    (\<forall> g \<in> sets M'. measure_space.integral M' (\<lambda>x. f x * indicator_fn g x) =
+                    measure_space.integral M' (\<lambda>x. X x * indicator_fn g x))"
 
 definition
-  "conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and>
-    (\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) =
-              integral (\<lambda>x. X x * indicator_fn g x))"
-
-definition
-  "conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2"
+  "conditional_prob E M' \<equiv> conditional_expectation (indicator_fn E) M'"
 
 lemma positive': "positive M prob"
   unfolding positive_def using positive empty_measure by blast
@@ -389,14 +390,61 @@
 
 locale finite_prob_space = prob_space + finite_measure_space
 
-lemma (in finite_prob_space) finite_marginal_product_space_POW2:
+lemma finite_prob_space_eq:
+  "finite_prob_space M \<longleftrightarrow> finite_measure_space M \<and> measure M (space M) = 1"
+  unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def
+  by auto
+
+lemma (in prob_space) not_empty: "space M \<noteq> {}"
+  using prob_space empty_measure by auto
+
+lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. measure M {x}) = 1"
+  using prob_space sum_over_space by simp
+
+lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x"
+  unfolding distribution_def using positive sets_eq_Pow by simp
+
+lemma (in finite_prob_space) joint_distribution_restriction_fst:
+  "joint_distribution X Y A \<le> distribution X (fst ` A)"
+  unfolding distribution_def
+proof (safe intro!: measure_mono)
+  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
+  show "x \<in> X -` fst ` A"
+    by (auto intro!: image_eqI[OF _ *])
+qed (simp_all add: sets_eq_Pow)
+
+lemma (in finite_prob_space) joint_distribution_restriction_snd:
+  "joint_distribution X Y A \<le> distribution Y (snd ` A)"
+  unfolding distribution_def
+proof (safe intro!: measure_mono)
+  fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"
+  show "x \<in> Y -` snd ` A"
+    by (auto intro!: image_eqI[OF _ *])
+qed (simp_all add: sets_eq_Pow)
+
+lemma (in finite_prob_space) distribution_order:
+  shows "0 \<le> distribution X x'"
+  and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')"
+  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"
+  and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"
+  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"
+  and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"
+  and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
+  and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"
+  using positive_distribution[of X x']
+    positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"]
+    joint_distribution_restriction_fst[of X Y "{(x, y)}"]
+    joint_distribution_restriction_snd[of X Y "{(x, y)}"]
+  by auto
+
+lemma (in finite_prob_space) finite_product_measure_space:
   assumes "finite s1" "finite s2"
   shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
     (is "finite_measure_space ?M")
 proof (rule finite_Pow_additivity_sufficient)
   show "positive ?M (measure ?M)"
     unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow
-    by (simp add: joint_distribution_def)
+    by (simp add: distribution_def)
 
   show "additive ?M (measure ?M)" unfolding additive_def
   proof safe
@@ -406,7 +454,7 @@
     assume "x \<inter> y = {}"
     from additive[unfolded additive_def, rule_format, OF A B] this
     show "measure ?M (x \<union> y) = measure ?M x + measure ?M y"
-      apply (simp add: joint_distribution_def)
+      apply (simp add: distribution_def)
       apply (subst Int_Un_distrib2)
       by auto
   qed
@@ -418,11 +466,58 @@
     by simp
 qed
 
-lemma (in finite_prob_space) finite_marginal_product_space_POW:
+lemma (in finite_prob_space) finite_product_measure_space_of_images:
   shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
                                 sets = Pow (X ` space M \<times> Y ` space M),
                                 measure = joint_distribution X Y\<rparr>"
     (is "finite_measure_space ?M")
-  using finite_space by (auto intro!: finite_marginal_product_space_POW2)
+  using finite_space by (auto intro!: finite_product_measure_space)
+
+lemma (in finite_prob_space) finite_measure_space:
+  shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
+    (is "finite_measure_space ?S")
+proof (rule finite_Pow_additivity_sufficient, simp_all)
+  show "finite (X ` space M)" using finite_space by simp
+
+  show "positive ?S (distribution X)" unfolding distribution_def
+    unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto
+
+  show "additive ?S (distribution X)" unfolding additive_def distribution_def
+  proof (simp, safe)
+    fix x y
+    have x: "(X -` x) \<inter> space M \<in> sets M"
+      and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
+    assume "x \<inter> y = {}"
+    from additive[unfolded additive_def, rule_format, OF x y] this
+    have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) =
+      prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)"
+      apply (subst Int_Un_distrib2)
+      by auto
+    thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)"
+      by auto
+  qed
+qed
+
+lemma (in finite_prob_space) finite_prob_space_of_images:
+  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
+  (is "finite_prob_space ?S")
+proof (simp add: finite_prob_space_eq, safe)
+  show "finite_measure_space ?S" by (rule finite_measure_space)
+  have "X -` X ` space M \<inter> space M = space M" by auto
+  thus "distribution X (X`space M) = 1"
+    by (simp add: distribution_def prob_space)
+qed
+
+lemma (in finite_prob_space) finite_product_prob_space_of_images:
+  "finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M), 
+    measure = joint_distribution X Y\<rparr>"
+  (is "finite_prob_space ?S")
+proof (simp add: finite_prob_space_eq, safe)
+  show "finite_measure_space ?S" by (rule finite_product_measure_space_of_images)
+
+  have "X -` X ` space M \<inter> Y -` Y ` space M \<inter> space M = space M" by auto
+  thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1"
+    by (simp add: distribution_def prob_space vimage_Times comp_def)
+qed
 
 end
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue May 04 14:44:30 2010 +0200
@@ -2,10 +2,10 @@
 imports Information
 begin
 
-lemma finite_prob_spaceI:
-  "\<lbrakk> finite_measure_space M ; measure M (space M) = 1 \<rbrakk> \<Longrightarrow> finite_prob_space M"
-  unfolding finite_measure_space_def finite_measure_space_axioms_def
-    finite_prob_space_def prob_space_def prob_space_axioms_def
+lemma finite_information_spaceI:
+  "\<lbrakk> finite_measure_space M ; measure M (space M) = 1 ; 1 < b \<rbrakk> \<Longrightarrow> finite_information_space M b"
+  unfolding finite_information_space_def finite_measure_space_def finite_measure_space_axioms_def
+    finite_prob_space_def prob_space_def prob_space_axioms_def finite_information_space_axioms_def
   by auto
 
 locale finite_space =
@@ -21,8 +21,8 @@
   and measure_M[simp]: "measure M s = real (card s) / real (card S)"
   by (simp_all add: M_def)
 
-sublocale finite_space \<subseteq> finite_prob_space M
-proof (rule finite_prob_spaceI)
+sublocale finite_space \<subseteq> finite_information_space M 2
+proof (rule finite_information_spaceI)
   let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)"
 
   show "finite_measure_space M"
@@ -40,9 +40,7 @@
         by (cases "card S = 0") (simp_all add: field_simps)
     qed
   qed
-
-  show "measure M (space M) = 1" by simp
-qed
+qed simp_all
 
 lemma set_of_list_extend:
   "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
@@ -83,19 +81,6 @@
   and card_list_length: "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
   using card_finite_list_length[OF assms, of n] by auto
 
-lemma product_not_empty:
-  "A \<noteq> {} \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A \<times> B \<noteq> {}"
-  by auto
-
-lemma fst_product[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
-  by (auto intro!: image_eqI)
-
-lemma snd_product[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
-  by (auto intro!: image_eqI)
-
-lemma Ex_eq_length[simp]: "\<exists>xs. length xs = n"
-  by (rule exI[of _ "replicate n undefined"]) simp
-
 section "Define the state space"
 
 text {*
@@ -197,10 +182,10 @@
   have *: "{xs. length xs = n} \<noteq> {}"
     by (auto intro!: exI[of _ "replicate n undefined"])
   show ?thesis
-    unfolding payer_def_raw dc_crypto fst_product if_not_P[OF *] ..
+    unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
 qed
 
-lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) = (\<exists>!x \<in> A. b = f x)"
+lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
   by (unfold inj_on_def) blast
 
 lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
@@ -495,26 +480,24 @@
   show "finite dc_crypto" using finite_dc_crypto .
   show "dc_crypto \<noteq> {}"
     unfolding dc_crypto
-    apply (rule product_not_empty)
     using n_gt_3 by (auto intro: exI[of _ "replicate n True"])
 qed
 
 notation (in dining_cryptographers_space)
-  finite_mutual_information_2 ("\<I>'( _ ; _ ')")
+  finite_mutual_information ("\<I>'( _ ; _ ')")
 
 notation (in dining_cryptographers_space)
-  finite_entropy_2 ("\<H>'( _ ')")
+  finite_entropy ("\<H>'( _ ')")
 
 notation (in dining_cryptographers_space)
-  finite_conditional_entropy_2 ("\<H>'( _ | _ ')")
+  finite_conditional_entropy ("\<H>'( _ | _ ')")
 
 theorem (in dining_cryptographers_space)
   "\<I>( inversion ; payer ) = 0"
 proof -
-  have b: "1 < (2 :: real)" by simp
   have n: "0 < n" using n_gt_3 by auto
 
-  have lists: "{xs. length xs = n} \<noteq> {}" by auto
+  have lists: "{xs. length xs = n} \<noteq> {}" using Ex_list_of_length by auto
 
   have card_image_inversion:
     "real (card (inversion ` dc_crypto)) = 2^n / 2"
@@ -526,7 +509,7 @@
 
   { have "\<H>(inversion|payer) =
         - (\<Sum>x\<in>inversion`dc_crypto. (\<Sum>z\<in>Some ` {0..<n}. ?dIP {(x, z)} * log 2 (?dIP {(x, z)} / ?dP {z})))"
-      unfolding finite_conditional_entropy_reduce[OF b] joint_distribution
+      unfolding conditional_entropy_eq
       by (simp add: image_payer_dc_crypto setsum_Sigma)
     also have "... =
         - (\<Sum>x\<in>inversion`dc_crypto. (\<Sum>z\<in>Some ` {0..<n}. 2 / (real n * 2^n) * (1 - real n)))"
@@ -560,7 +543,7 @@
     finally have "\<H>(inversion|payer) = real n - 1" . }
   moreover
   { have "\<H>(inversion) = - (\<Sum>x \<in> inversion`dc_crypto. ?dI {x} * log 2 (?dI {x}))"
-      unfolding finite_entropy_reduce[OF b] by simp
+      unfolding entropy_eq by simp
     also have "... = - (\<Sum>x \<in> inversion`dc_crypto. 2 * (1 - real n) / 2^n)"
       unfolding neg_equal_iff_equal
     proof (rule setsum_cong[OF refl])
@@ -577,7 +560,7 @@
     finally have "\<H>(inversion) = real n - 1" .
   }
   ultimately show ?thesis
-    unfolding finite_mutual_information_eq_entropy_conditional_entropy[OF b]
+    unfolding mutual_information_eq_entropy_conditional_entropy
     by simp
 qed
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Product_Type.thy	Tue May 04 14:44:30 2010 +0200
@@ -990,6 +990,15 @@
 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
 by blast
 
+lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
+  by auto
+
+lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
+  by (auto intro!: image_eqI)
+
+lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
+  by (auto intro!: image_eqI)
+
 lemma insert_times_insert[simp]:
   "insert a A \<times> insert b B =
    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
@@ -999,13 +1008,20 @@
   by (auto, rule_tac p = "f x" in PairE, auto)
 
 lemma swap_inj_on:
-  "inj_on (%(i, j). (j, i)) (A \<times> B)"
-  by (unfold inj_on_def) fast
+  "inj_on (\<lambda>(i, j). (j, i)) A"
+  by (auto intro!: inj_onI)
 
 lemma swap_product:
   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   by (simp add: split_def image_def) blast
 
+lemma image_split_eq_Sigma:
+  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
+proof (safe intro!: imageI vimageI)
+  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
+  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
+    using * eq[symmetric] by auto
+qed simp_all
 
 subsubsection {* Code generator setup *}
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue May 04 14:44:30 2010 +0200
@@ -359,6 +359,10 @@
   then show "concat a \<approx> concat b" by simp
 qed
 
+lemma [quot_respect]:
+  "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+  by auto
+
 text {* Distributive lattice with bot *}
 
 lemma sub_list_not_eq:
@@ -551,6 +555,11 @@
 is
   "concat"
 
+quotient_definition
+  "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "filter"
+
 text {* Compositional Respectfullness and Preservation *}
 
 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
@@ -868,6 +877,14 @@
   then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
+text {* Raw theorems of ffilter *}
+
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
+
 text {* Lifted theorems *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -1142,6 +1159,76 @@
 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
   by (lifting concat_append)
 
+text {* ffilter *}
+
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+
+lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+
+
+section {* lemmas transferred from Finite_Set theory *}
+
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+by (induct S) auto
+
+text {* @{thm subset_empty} transferred is: *}
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+by (cases xs) (auto simp add: fsubset_finsert not_fin_fnil)
+
+text {* @{thm not_psubset_empty} transferred is: *}
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+unfolding less_fset by (auto simp add: fsubseteq_fnil)
+
+text {* @{thm card_mono} transferred is: *}
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+proof (induct xs arbitrary: ys)
+  case fempty
+  thus ?case by simp
+next
+  case (finsert x xs ys)
+  from finsert(1,3) have "xs |\<subseteq>| fdelete ys x"
+    by (auto simp add: fsubset_fin fin_fdelete)
+  from finsert(2) this have hyp: "fcard xs \<le> fcard (fdelete ys x)" by simp
+  from finsert(3) have "x |\<in>| ys" by (auto simp add: fsubset_fin)
+  from this have ys_is: "ys = finsert x (fdelete ys x)"
+    unfolding expand_fset_eq by (auto simp add: fin_fdelete)
+  from finsert(1) hyp have "fcard (finsert x xs) \<le> fcard (finsert x (fdelete ys x))"
+    by (auto simp add: fin_fdelete_ident)
+  from ys_is this show ?case by auto
+qed
+
+text {* @{thm card_seteq} transferred is: *}
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+proof (induct xs arbitrary: ys)
+  case fempty
+  thus ?case by (simp add: fcard_0)
+next
+  case (finsert x xs ys)
+  from finsert have subset: "xs |\<subseteq>| fdelete ys x"
+    by (auto simp add: fsubset_fin fin_fdelete)
+  from finsert have x: "x |\<in>| ys"
+    by (auto simp add: fsubset_fin fin_fdelete)
+  from finsert(1,4) this have "fcard (fdelete ys x) \<le> fcard xs"
+    by (auto simp add: fcard_delete)
+  from finsert(2) this subset have hyp: "xs = fdelete ys x" by auto
+  from finsert have "x |\<in>| ys"
+    by (auto simp add: fsubset_fin fin_fdelete)
+  from this hyp show ?case
+    unfolding expand_fset_eq by (auto simp add: fin_fdelete)
+qed
+
+text {* @{thm psubset_card_mono} transferred is: *}
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+unfolding less_fset linorder_not_le[symmetric]
+by (auto simp add: fcard_fseteq)
+
+
 ML {*
 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Rings.thy	Tue May 04 14:44:30 2010 +0200
@@ -684,6 +684,18 @@
 end
 
 class linordered_semiring_1 = linordered_semiring + semiring_1
+begin
+
+lemma convex_bound_le:
+  assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  shows "u * x + v * y \<le> a"
+proof-
+  from assms have "u * x + v * y \<le> u * a + v * a"
+    by (simp add: add_mono mult_left_mono)
+  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+qed
+
+end
 
 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
@@ -803,6 +815,21 @@
 end
 
 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
+begin
+
+subclass linordered_semiring_1 ..
+
+lemma convex_bound_lt:
+  assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  shows "u * x + v * y < a"
+proof -
+  from assms have "u * x + v * y < u * a + v * a"
+    by (cases "u = 0")
+       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
+  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+qed
+
+end
 
 class mult_mono1 = times + zero + ord +
   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -1108,6 +1135,7 @@
   (*previously linordered_ring*)
 begin
 
+subclass linordered_semiring_1_strict ..
 subclass linordered_ring_strict ..
 subclass ordered_comm_ring ..
 subclass idom ..
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/SEQ.thy	Tue May 04 14:44:30 2010 +0200
@@ -532,6 +532,33 @@
 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
 by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
 
+lemma convergent_const: "convergent (\<lambda>n. c)"
+by (rule convergentI, rule LIMSEQ_const)
+
+lemma convergent_add:
+  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes "convergent (\<lambda>n. X n)"
+  assumes "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n + Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ_add)
+
+lemma convergent_setsum:
+  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
+  assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+using assms
+by (induct A set: finite, simp_all add: convergent_const convergent_add)
+
+lemma (in bounded_linear) convergent:
+  assumes "convergent (\<lambda>n. X n)"
+  shows "convergent (\<lambda>n. f (X n))"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
+lemma (in bounded_bilinear) convergent:
+  assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n ** Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
 lemma convergent_minus_iff:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Tue May 04 14:44:30 2010 +0200
@@ -14,19 +14,20 @@
 structure Function_Relation : FUNCTION_RELATION =
 struct
 
-fun inst_thm ctxt rel st =
+fun inst_state_tac ctxt rel st =
   let
     val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
     val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
     val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-    val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
-  in
-    Drule.cterm_instantiate [(Rvar, rel')] st'
+  in case Term.add_vars (prop_of st') [] of
+       [v] => 
+         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+     | _ => Seq.empty
   end
 
 fun relation_tac ctxt rel i =
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN PRIMITIVE (inst_thm ctxt rel)
+  THEN inst_state_tac ctxt rel
 
 val setup =
   Method.setup @{binding relation}
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue May 04 14:44:30 2010 +0200
@@ -323,11 +323,11 @@
 
 (* prove monotonicity *)
 
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos ctxt =
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
  (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
     "  Proving monotonicity ...";
   (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
-    (map (fst o dest_Free) params) []
+    [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
@@ -340,7 +340,7 @@
 
 (* prove introduction rules *)
 
-fun prove_intrs quiet_mode coind mono fp_def k params intr_ts rec_preds_defs ctxt =
+fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
   let
     val _ = clean_message quiet_mode "  Proving the introduction rules ...";
 
@@ -354,27 +354,27 @@
 
     val rules = [refl, TrueI, notFalseI, exI, conjI];
 
-    val intrs = map_index (fn (i, intr) => rulify
-      (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
+    val intrs = map_index (fn (i, intr) =>
+      Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
        [rewrite_goals_tac rec_preds_defs,
         rtac (unfold RS iffD2) 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
-        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts
+        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
+       |> rulify
+       |> singleton (ProofContext.export ctxt ctxt')) intr_ts
 
   in (intrs, unfold) end;
 
 
 (* prove elimination rules *)
 
-fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt =
+fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
   let
     val _ = clean_message quiet_mode "  Proving the elimination rules ...";
 
-    val ([pname], ctxt') = ctxt |>
-      Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
-      Variable.variant_fixes ["P"];
+    val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
 
     fun dest_intr r =
@@ -410,7 +410,7 @@
              EVERY (map (fn prem =>
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
           |> rulify
-          |> singleton (ProofContext.export ctxt'' ctxt),
+          |> singleton (ProofContext.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
       end
 
@@ -488,16 +488,14 @@
 (* prove induction rule *)
 
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
-    fp_def rec_preds_defs ctxt =
+    fp_def rec_preds_defs ctxt ctxt''' =
   let
     val _ = clean_message quiet_mode "  Proving the induction rule ...";
     val thy = ProofContext.theory_of ctxt;
 
     (* predicates for induction rule *)
 
-    val (pnames, ctxt') = ctxt |>
-      Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
-      Variable.variant_fixes (mk_names "P" (length cs));
+    val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
     val preds = map2 (curry Free) pnames
       (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
 
@@ -592,7 +590,7 @@
             rewrite_goals_tac simp_thms',
             atac 1])])
 
-  in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end;
+  in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end;
 
 
 
@@ -689,11 +687,13 @@
       ||> Local_Theory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos lthy'';
-    val ((_, [mono']), lthy''') =
-      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+    val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
+    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
+    val (_, lthy'''') =
+      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
+        ProofContext.export lthy''' lthy'' [mono]) lthy'';
 
-  in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
+  in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
@@ -774,31 +774,30 @@
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
-    val (lthy1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
+    val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
       argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
         monos params cnames_syn lthy;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
-      params intr_ts rec_preds_defs lthy1;
+      intr_ts rec_preds_defs lthy2 lthy1;
     val elims =
       if no_elim then []
       else
         prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
-          unfold rec_preds_defs lthy1;
+          unfold rec_preds_defs lthy2 lthy1;
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl
        else if coind then
-         singleton (ProofContext.export
-           (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
+         singleton (ProofContext.export lthy2 lthy1)
            (rotate_prems ~1 (Object_Logic.rulify
              (fold_rule rec_preds_defs
                (rewrite_rule simp_thms'''
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
-           rec_preds_defs lthy1);
+           rec_preds_defs lthy2 lthy1);
 
-    val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind
+    val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
       cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
 
     val result =
@@ -809,11 +808,11 @@
        induct = induct,
        inducts = inducts};
 
-    val lthy3 = lthy2
+    val lthy4 = lthy3
       |> Local_Theory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
-  in (result, lthy3) end;
+  in (result, lthy4) end;
 
 
 (* external interfaces *)
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Wellfounded.thy	Tue May 04 14:44:30 2010 +0200
@@ -68,7 +68,7 @@
   assumes lin: "OFCLASS('a::ord, linorder_class)"
   shows "OFCLASS('a::ord, wellorder_class)"
 using lin by (rule wellorder_class.intro)
-  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
 
 lemma (in wellorder) wf:
   "wf {(x, y). x < y}"
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue May 04 14:44:30 2010 +0200
@@ -17,7 +17,7 @@
   by (auto simp del: word_uint.Rep_inject 
            simp: word_uint.Rep_inject [symmetric])
 
-lemma signed_linorder: "linorder word_sle word_sless"
+lemma signed_linorder: "class.linorder word_sle word_sless"
 proof
 qed (unfold word_sle_def word_sless_def, auto)
 
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOL/ex/Landau.thy
--- a/src/HOL/ex/Landau.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOL/ex/Landau.thy	Tue May 04 14:44:30 2010 +0200
@@ -187,7 +187,7 @@
 proof -
   interpret preorder_equiv less_eq_fun less_fun proof
   qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
-  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
     by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
 qed
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOLCF/CompactBasis.thy	Tue May 04 14:44:30 2010 +0200
@@ -237,12 +237,12 @@
   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
 
 lemma fold_pd_PDUnit:
-  assumes "ab_semigroup_idem_mult f"
+  assumes "class.ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDUnit x) = g x"
 unfolding fold_pd_def Rep_PDUnit by simp
 
 lemma fold_pd_PDPlus:
-  assumes "ab_semigroup_idem_mult f"
+  assumes "class.ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
   interpret ab_semigroup_idem_mult f by fact
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy	Tue May 04 14:44:30 2010 +0200
@@ -412,7 +412,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 
 lemma ACI_convex_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_commute)
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOLCF/LowerPD.thy	Tue May 04 14:44:30 2010 +0200
@@ -393,7 +393,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 
 lemma ACI_lower_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Tue May 04 14:44:30 2010 +0200
@@ -337,10 +337,10 @@
 (* proves a block of pattern matching equations as theorems, using unfold *)
 fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
   let
-    val tacs =
-      [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
-       asm_simp_tac (simpset_of ctxt) 1];
-    fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs));
+    val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
+    val rule = unfold_thm RS @{thm ssubst_lhs};
+    val tac = rtac rule 1 THEN asm_simp_tac ss 1;
+    fun prove_term t = Goal.prove ctxt [] [] t (K tac);
     fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
   in
     map prove_eqn eqns
diff -r 2fd4e2c76636 -r 30bd207ec222 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Tue May 04 14:38:59 2010 +0200
+++ b/src/HOLCF/UpperPD.thy	Tue May 04 14:44:30 2010 +0200
@@ -388,7 +388,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 
 lemma ACI_upper_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_commute)
diff -r 2fd4e2c76636 -r 30bd207ec222 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue May 04 14:38:59 2010 +0200
+++ b/src/Pure/Isar/class.ML	Tue May 04 14:44:30 2010 +0200
@@ -276,16 +276,16 @@
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
   let
-    val class = Sign.full_name thy bname;
+    val class = Sign.full_name thy b;
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale bname Binding.empty supexpr elems
+    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
     |> snd |> Local_Theory.exit_global
-    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
+    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)