merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
--- a/src/HOL/Library/FuncSet.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Library/FuncSet.thy Mon Nov 19 12:29:02 2012 +0100
@@ -86,7 +86,7 @@
lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
by auto
-lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
+lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})"
apply (simp add: Pi_def, auto)
txt{*Converse direction requires Axiom of Choice to exhibit a function
picking an element from each non-empty @{term "B x"}*}
@@ -97,12 +97,31 @@
lemma Pi_empty [simp]: "Pi {} B = UNIV"
by (simp add: Pi_def)
+lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
+ by auto
+
+lemma Pi_UN:
+ fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
+ assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
+ shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
+proof (intro set_eqI iffI)
+ fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
+ then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
+ from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
+ obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+ using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
+ have "f \<in> Pi I (A k)"
+ proof (intro Pi_I)
+ fix i assume "i \<in> I"
+ from mono[OF this, of "n i" k] k[OF this] n[OF this]
+ show "f i \<in> A k i" by auto
+ qed
+ then show "f \<in> (\<Union>n. Pi I (A n))" by auto
+qed auto
+
lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
by (simp add: Pi_def)
-(*
-lemma funcset_id [simp]: "(%x. x): A -> A"
- by (simp add: Pi_def)
-*)
+
text{*Covariance of Pi-sets in their second argument*}
lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
by auto
@@ -124,6 +143,25 @@
finally show "f z \<in> B z \<times> C z" .
qed
+lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
+ by (auto simp: Pi_def)
+
+lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
+ by (auto simp: Pi_def)
+
+lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
+ by (auto simp: Pi_def)
+
+lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
+ by (auto simp: Pi_def)
+
+lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
+ apply auto
+ apply (drule_tac x=x in Pi_mem)
+ apply (simp_all split: split_if_asm)
+ apply (drule_tac x=i in Pi_mem)
+ apply (auto dest!: Pi_mem)
+ done
subsection{*Composition With a Restricted Domain: @{term compose}*}
@@ -173,6 +211,19 @@
lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
by (auto simp add: restrict_def)
+lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
+ unfolding restrict_def by (simp add: fun_eq_iff)
+
+lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
+ by (auto simp: restrict_def)
+
+lemma restrict_upd[simp]:
+ "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
+ by (auto simp: fun_eq_iff)
+
+lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
+ by (auto simp: restrict_def Pi_def)
+
subsection{*Bijections Between Sets*}
@@ -213,6 +264,9 @@
subsection{*Extensionality*}
+lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
+ unfolding extensional_def by auto
+
lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
by (simp add: extensional_def)
@@ -230,6 +284,9 @@
lemma extensional_restrict: "f \<in> extensional A \<Longrightarrow> restrict f A = f"
by(rule extensionalityI[OF restrict_extensional]) auto
+lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
+ unfolding extensional_def by auto
+
lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
by (unfold inv_into_def) (fast intro: someI2)
@@ -246,6 +303,29 @@
apply (simp add: f_inv_into_f)
done
+lemma extensional_insert[intro, simp]:
+ assumes "a \<in> extensional (insert i I)"
+ shows "a(i := b) \<in> extensional (insert i I)"
+ using assms unfolding extensional_def by auto
+
+lemma extensional_Int[simp]:
+ "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
+ unfolding extensional_def by auto
+
+lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
+ by (auto simp: extensional_def)
+
+lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
+ unfolding restrict_def extensional_def by auto
+
+lemma extensional_insert_undefined[intro, simp]:
+ "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
+ unfolding extensional_def by auto
+
+lemma extensional_insert_cancel[intro, simp]:
+ "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
+ unfolding extensional_def by auto
+
subsection{*Cardinality*}
@@ -259,156 +339,207 @@
subsection {* Extensional Function Spaces *}
-definition extensional_funcset
-where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
+definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+ "PiE S T = Pi S T \<inter> extensional S"
+
+abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
-lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
-unfolding extensional_def by auto
+syntax "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)
+
+syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
+
+syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
+
+translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
-lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
-unfolding extensional_funcset_def by simp
+abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^isub>E" 60) where
+ "A ->\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)"
+
+notation (xsymbols)
+ extensional_funcset (infixr "\<rightarrow>\<^isub>E" 60)
-lemma extensional_funcset_empty_range:
- assumes "S \<noteq> {}"
- shows "extensional_funcset S {} = {}"
-using assms unfolding extensional_funcset_def by auto
+lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
+ by (simp add: PiE_def)
+
+lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
+ unfolding PiE_def by simp
+
+lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
+ unfolding PiE_def by auto
-lemma extensional_funcset_arb:
- assumes "f \<in> extensional_funcset S T" "x \<notin> S"
- shows "f x = undefined"
-using assms
-unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
-
-lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
-unfolding extensional_funcset_def by auto
-
-lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
-unfolding extensional_def by auto
+lemma PiE_eq_empty_iff:
+ "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
+proof
+ assume "Pi\<^isub>E I F = {}"
+ show "\<exists>i\<in>I. F i = {}"
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
+ from choice[OF this] guess f ..
+ then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
+ with `Pi\<^isub>E I F = {}` show False by auto
+ qed
+qed (auto simp: PiE_def)
-lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T"
-unfolding extensional_funcset_def extensional_def by auto
+lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
+ unfolding PiE_def by auto (auto dest!: extensional_arb)
+
+lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
+ unfolding PiE_def by auto
-lemma extensional_funcset_restrict_domain:
- "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
-unfolding extensional_funcset_def extensional_def by auto
+lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
+ unfolding PiE_def extensional_def by auto
-lemma extensional_funcset_extend_domain_eq:
+lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
+ unfolding PiE_def extensional_def by auto
+
+lemma PiE_insert_eq:
assumes "x \<notin> S"
- shows
- "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
- using assms
+ shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
proof -
{
- fix f
- assume "f : extensional_funcset (insert x S) T"
- from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
- unfolding image_iff
- apply (rule_tac x="(f x, f(x := undefined))" in bexI)
- apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done
+ fix f assume "f \<in> PiE (insert x S) T"
+ with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+ by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
}
- moreover
- {
- fix f
- assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
- from this assms have "f : extensional_funcset (insert x S) T"
- by (auto intro: extensional_funcset_extend_domainI)
- }
- ultimately show ?thesis by auto
+ then show ?thesis using assms by (auto intro: PiE_fun_upd)
qed
-lemma extensional_funcset_fun_upd_restricts_rangeI: "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T - {f x})"
-unfolding extensional_funcset_def extensional_def
-apply auto
-apply (case_tac "x = xa")
-apply auto done
+lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
+ by (auto simp: PiE_def)
+
+lemma PiE_cong:
+ "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B"
+ unfolding PiE_def by (auto simp: Pi_cong)
+
+lemma PiE_E [elim]:
+ "f \<in> PiE A B \<Longrightarrow> (x \<in> A \<Longrightarrow> f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> f x = undefined \<Longrightarrow> Q) \<Longrightarrow> Q"
+by(auto simp: Pi_def PiE_def extensional_def)
+
+lemma PiE_I[intro!]: "(\<And>x. x \<in> A ==> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
+ by (simp add: PiE_def extensional_def)
+
+lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
+ by auto
+
+lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
+ by (simp add: PiE_def Pi_iff)
+
+lemma PiE_restrict[simp]: "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
+ by (simp add: extensional_restrict PiE_def)
+
+lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
+ by (auto simp: PiE_iff)
+
+lemma PiE_eq_subset:
+ assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
+ assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
+ shows "F i \<subseteq> F' i"
+proof
+ fix x assume "x \<in> F i"
+ with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
+ from choice[OF this] guess f .. note f = this
+ then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
+ then have "f \<in> Pi\<^isub>E I F'" using assms by simp
+ then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
+qed
+
+lemma PiE_eq_iff_not_empty:
+ assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
+ shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
+proof (intro iffI ballI)
+ fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
+ show "F i = F' i"
+ using PiE_eq_subset[of I F F', OF ne eq i]
+ using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
+ by auto
+qed (auto simp: PiE_def)
+
+lemma PiE_eq_iff:
+ "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
+proof (intro iffI disjCI)
+ assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
+ assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
+ then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
+ using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
+ with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
+next
+ assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
+ then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
+ using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
+qed
+
+lemma extensional_funcset_fun_upd_restricts_rangeI:
+ "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^isub>E T ==> f(x := undefined) : S \<rightarrow>\<^isub>E (T - {f x})"
+ unfolding extensional_funcset_def extensional_def
+ apply auto
+ apply (case_tac "x = xa")
+ apply auto
+ done
lemma extensional_funcset_fun_upd_extends_rangeI:
- assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
- shows "f(x := a) : extensional_funcset (insert x S) T"
+ assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T - {a})"
+ shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E T"
using assms unfolding extensional_funcset_def extensional_def by auto
subsubsection {* Injective Extensional Function Spaces *}
lemma extensional_funcset_fun_upd_inj_onI:
- assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
+ assumes "f \<in> S \<rightarrow>\<^isub>E (T - {a})" "inj_on f S"
shows "inj_on (f(x := a)) S"
using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
lemma extensional_funcset_extend_domain_inj_on_eq:
assumes "x \<notin> S"
- shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
- (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+ shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} =
+ (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
proof -
from assms show ?thesis
- apply auto
- apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
+ apply (auto del: PiE_I PiE_E)
+ apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
apply (auto simp add: image_iff inj_on_def)
apply (rule_tac x="xa x" in exI)
- apply (auto intro: extensional_funcset_mem)
+ apply (auto intro: PiE_mem del: PiE_I PiE_E)
apply (rule_tac x="xa(x := undefined)" in exI)
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
- apply (auto dest!: extensional_funcset_mem split: split_if_asm)
+ apply (auto dest!: PiE_mem split: split_if_asm)
done
qed
lemma extensional_funcset_extend_domain_inj_onI:
assumes "x \<notin> S"
- shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+ shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
proof -
from assms show ?thesis
apply (auto intro!: inj_onI)
apply (metis fun_upd_same)
- by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
+ by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
qed
subsubsection {* Cardinality *}
-lemma card_extensional_funcset:
- assumes "finite S"
- shows "card (extensional_funcset S T) = (card T) ^ (card S)"
-using assms
-proof (induct rule: finite_induct)
- case empty
- show ?case
- by (auto simp add: extensional_funcset_empty_domain)
-next
- case (insert x S)
- {
- fix g g' y y'
- assume assms: "g \<in> extensional_funcset S T"
- "g' \<in> extensional_funcset S T"
- "y \<in> T" "y' \<in> T"
- "g(x := y) = g'(x := y')"
- from this have "y = y'"
- by (metis fun_upd_same)
- have "g = g'"
- by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
- from `y = y'` `g = g'` have "y = y' & g = g'" by simp
- }
- from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
- by (auto intro: inj_onI)
- from this insert.hyps show ?case
- by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
+lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
+ by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
+
+lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)"
+proof (safe intro!: inj_onI ext)
+ fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^isub>E S T" "g \<in> Pi\<^isub>E S T"
+ assume "f(x := y) = g(x := z)"
+ then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
+ unfolding fun_eq_iff by auto
+ from this[of x] show "y = z" by simp
+ fix i from *[of i] `x \<notin> S` fg show "f i = g i"
+ by (auto split: split_if_asm simp: PiE_def extensional_def)
qed
-lemma finite_extensional_funcset:
- assumes "finite S" "finite T"
- shows "finite (extensional_funcset S T)"
-proof -
- from card_extensional_funcset[OF assms(1), of T] assms(2)
- have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
- by auto
- from this show ?thesis
- proof
- assume "card (extensional_funcset S T) \<noteq> 0"
- from this show ?thesis
- by (auto intro: card_ge_0_finite)
- next
- assume "S \<noteq> {} \<and> T = {}"
- from this show ?thesis
- by (auto simp add: extensional_funcset_empty_range)
- qed
+lemma card_PiE:
+ "finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))"
+proof (induct rule: finite_induct)
+ case empty then show ?case by auto
+next
+ case (insert x S) then show ?case
+ by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
qed
end
--- a/src/HOL/Probability/Fin_Map.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Mon Nov 19 12:29:02 2012 +0100
@@ -1284,17 +1284,16 @@
assumes "finite J"
shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
proof (rule measurable_PiM)
- show "(\<lambda>m. compose J m f)
- \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow>
- (J \<rightarrow> space M) \<inter> extensional J"
+ show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
proof safe
fix x and i
assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
with inj show "compose J x f i \<in> space M"
by (auto simp: space_PiM compose_def)
next
- fix x assume "x \<in> space (PiM (f ` J) (\<lambda>_. M))"
- show "(compose J x f) \<in> extensional J" by (rule compose_extensional)
+ fix x i assume "i \<notin> J"
+ with compose_extensional[of J x f]
+ show "compose J x f i = undefined" by (auto simp: extensional_def)
qed
next
fix S X
@@ -1303,7 +1302,7 @@
have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) = prod_emb (f ` J) (\<lambda>_. M) (f ` S) (Pi\<^isub>E (f ` S) (\<lambda>b. X (f' b)))"
using assms inv S sets_into_space[OF P]
- by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def intro: imageI)
+ by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
proof
from S show "f ` S \<subseteq> f ` J" by auto
@@ -1379,7 +1378,7 @@
assumes "\<And>i. space (M i) = UNIV"
shows "inj_on fm (space (Pi\<^isub>M J M))"
using assms
- apply (auto simp: fm_def space_PiM)
+ apply (auto simp: fm_def space_PiM PiE_def)
apply (rule comp_inj_on)
apply (rule inj_on_compose_f')
apply (rule finmap_of_inj_on_extensional_finite)
@@ -1409,7 +1408,7 @@
by (auto simp: mf_def extensional_def compose_def)
moreover
have "x \<in> extensional J" using assms sets_into_space
- by (force simp: space_PiM)
+ by (force simp: space_PiM PiE_def)
moreover
{ fix i assume "i \<in> J"
hence "mf (fm x) i = x i"
@@ -1472,13 +1471,13 @@
lemma mapmeasure_PiF:
assumes s1: "space M = space (Pi\<^isub>M J (\<lambda>_. N))"
- assumes s2: "sets M = (Pi\<^isub>M J (\<lambda>_. N))"
+ assumes s2: "sets M = sets (Pi\<^isub>M J (\<lambda>_. N))"
assumes "space N = UNIV"
assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
using assms
by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
- fm_measurable space_PiM)
+ fm_measurable space_PiM PiE_def)
lemma mapmeasure_PiM:
fixes N::"'c measure"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon Nov 19 12:29:02 2012 +0100
@@ -11,46 +11,7 @@
lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
-abbreviation
- "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
-
-syntax
- "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)
-
-syntax (xsymbols)
- "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
-
-syntax (HTML output)
- "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
-
-translations
- "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
-
-abbreviation
- funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
- (infixr "->\<^isub>E" 60) where
- "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
-
-notation (xsymbols)
- funcset_extensional (infixr "\<rightarrow>\<^isub>E" 60)
-
-lemma extensional_insert[intro, simp]:
- assumes "a \<in> extensional (insert i I)"
- shows "a(i := b) \<in> extensional (insert i I)"
- using assms unfolding extensional_def by auto
-
-lemma extensional_Int[simp]:
- "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
- unfolding extensional_def by auto
-
-lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
- by (auto simp: extensional_def)
-
-lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
- unfolding restrict_def extensional_def by auto
-
-lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
- unfolding restrict_def by (simp add: fun_eq_iff)
+subsubsection {* Merge two extensional functions *}
definition
"merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
@@ -84,9 +45,6 @@
lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
by (auto simp: extensional_def)
-lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
- by (auto simp: restrict_def Pi_def)
-
lemma restrict_merge[simp]:
"I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
"I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
@@ -97,9 +55,26 @@
lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
unfolding merge_def by auto
+lemma PiE_cancel_merge[simp]:
+ "I \<inter> J = {} \<Longrightarrow>
+ merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
+ by (auto simp: PiE_def restrict_Pi_cancel)
+
+lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
+ unfolding merge_def by (auto simp: fun_eq_iff)
+
lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
unfolding merge_def extensional_def by auto
+lemma merge_restrict[simp]:
+ "merge I J (restrict x I, y) = merge I J (x, y)"
+ "merge I J (x, restrict y J) = merge I J (x, y)"
+ unfolding merge_def by auto
+
+lemma merge_x_x_eq_restrict[simp]:
+ "merge I J (x, x) = restrict x (I \<union> J)"
+ unfolding merge_def by auto
+
lemma injective_vimage_restrict:
assumes J: "J \<subseteq> I"
and sets: "A \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" and ne: "(\<Pi>\<^isub>E i\<in>I. S i) \<noteq> {}"
@@ -113,195 +88,22 @@
proof cases
assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
- using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
+ using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
+ by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
then show "x \<in> A \<longleftrightarrow> x \<in> B"
- using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
- next
- assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
- qed
+ using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
+ by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
+ qed (insert sets, auto)
qed
-lemma extensional_insert_undefined[intro, simp]:
- assumes "a \<in> extensional (insert i I)"
- shows "a(i := undefined) \<in> extensional I"
- using assms unfolding extensional_def by auto
-
-lemma extensional_insert_cancel[intro, simp]:
- assumes "a \<in> extensional I"
- shows "a \<in> extensional (insert i I)"
- using assms unfolding extensional_def by auto
-
-lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
- unfolding merge_def by (auto simp: fun_eq_iff)
-
-lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
- by auto
-
-lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
- by auto
-
-lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
- by (auto simp: Pi_def)
-
-lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
- by (auto simp: Pi_def)
-
-lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
- by (auto simp: Pi_def)
-
-lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
- by (auto simp: Pi_def)
-
lemma restrict_vimage:
- assumes "I \<inter> J = {}"
- shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
- using assms by (auto simp: restrict_Pi_cancel)
+ "I \<inter> J = {} \<Longrightarrow>
+ (\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
+ by (auto simp: restrict_Pi_cancel PiE_def)
lemma merge_vimage:
- assumes "I \<inter> J = {}"
- shows "merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
- using assms by (auto simp: restrict_Pi_cancel)
-
-lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
- by (auto simp: restrict_def)
-
-lemma merge_restrict[simp]:
- "merge I J (restrict x I, y) = merge I J (x, y)"
- "merge I J (x, restrict y J) = merge I J (x, y)"
- unfolding merge_def by auto
-
-lemma merge_x_x_eq_restrict[simp]:
- "merge I J (x, x) = restrict x (I \<union> J)"
- unfolding merge_def by auto
-
-lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
- apply auto
- apply (drule_tac x=x in Pi_mem)
- apply (simp_all split: split_if_asm)
- apply (drule_tac x=i in Pi_mem)
- apply (auto dest!: Pi_mem)
- done
-
-lemma Pi_UN:
- fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
- assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
- shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
-proof (intro set_eqI iffI)
- fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
- then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
- from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
- obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
- using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
- have "f \<in> Pi I (A k)"
- proof (intro Pi_I)
- fix i assume "i \<in> I"
- from mono[OF this, of "n i" k] k[OF this] n[OF this]
- show "f i \<in> A k i" by auto
- qed
- then show "f \<in> (\<Union>n. Pi I (A n))" by auto
-qed auto
-
-lemma PiE_cong:
- assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
- shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
- using assms by (auto intro!: Pi_cong)
-
-lemma restrict_upd[simp]:
- "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
- by (auto simp: fun_eq_iff)
-
-lemma Pi_eq_subset:
- assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
- assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
- shows "F i \<subseteq> F' i"
-proof
- fix x assume "x \<in> F i"
- with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
- from choice[OF this] guess f .. note f = this
- then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
- then have "f \<in> Pi\<^isub>E I F'" using assms by simp
- then show "x \<in> F' i" using f `i \<in> I` by auto
-qed
-
-lemma Pi_eq_iff_not_empty:
- assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
- shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
-proof (intro iffI ballI)
- fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
- show "F i = F' i"
- using Pi_eq_subset[of I F F', OF ne eq i]
- using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
- by auto
-qed auto
-
-lemma Pi_eq_empty_iff:
- "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
-proof
- assume "Pi\<^isub>E I F = {}"
- show "\<exists>i\<in>I. F i = {}"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
- from choice[OF this] guess f ..
- then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
- with `Pi\<^isub>E I F = {}` show False by auto
- qed
-qed auto
-
-lemma Pi_eq_iff:
- "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
-proof (intro iffI disjCI)
- assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
- assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
- then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
- using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
- with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
-next
- assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
- then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
- using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
-qed
-
-lemma funset_eq_UN_fun_upd_I:
- assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
- and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
- and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
- shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
-proof safe
- fix f assume f: "f \<in> F (insert a A)"
- show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
- proof (rule UN_I[of "f(a := d)"])
- show "f(a := d) \<in> F A" using *[OF f] .
- show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
- proof (rule image_eqI[of _ _ "f a"])
- show "f a \<in> G (f(a := d))" using **[OF f] .
- qed simp
- qed
-next
- fix f x assume "f \<in> F A" "x \<in> G f"
- from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
-qed
-
-lemma extensional_funcset_insert_eq[simp]:
- assumes "a \<notin> A"
- shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
- apply (rule funset_eq_UN_fun_upd_I)
- using assms
- by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
-
-lemma finite_extensional_funcset[simp, intro]:
- assumes "finite A" "finite B"
- shows "finite (extensional A \<inter> (A \<rightarrow> B))"
- using assms by induct auto
-
-lemma finite_PiE[simp, intro]:
- assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
- shows "finite (Pi\<^isub>E A B)"
-proof -
- have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
- show ?thesis
- using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
-qed
+ "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
+ by (auto simp: restrict_Pi_cancel PiE_def)
section "Finite product spaces"
@@ -312,7 +114,7 @@
lemma prod_emb_iff:
"f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
- unfolding prod_emb_def by auto
+ unfolding prod_emb_def PiE_def by auto
lemma
shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
@@ -325,24 +127,25 @@
lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
prod_emb I M J (\<Pi>\<^isub>E i\<in>J. E i) = (\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i))"
- by (force simp: prod_emb_def Pi_iff split_if_mem2)
+ by (force simp: prod_emb_def PiE_iff split_if_mem2)
-lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
- by (auto simp: prod_emb_def Pi_iff)
+lemma prod_emb_PiE_same_index[simp]:
+ "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
+ by (auto simp: prod_emb_def PiE_iff)
lemma prod_emb_trans[simp]:
"J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
- by (auto simp add: Int_absorb1 prod_emb_def)
+ by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
lemma prod_emb_Pi:
assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
using assms space_closed
- by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
+ by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
lemma prod_emb_id:
"B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
- by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
+ by (auto simp: prod_emb_def subset_eq extensional_restrict)
lemma prod_emb_mono:
"F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
@@ -392,9 +195,9 @@
by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
next
fix A assume "A \<in> ?R"
- then obtain X where "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
+ then obtain X where A: "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
- using sets_into_space by (force simp: prod_emb_def Pi_iff)
+ by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
from X I show "A \<in> ?L" unfolding A
by (auto simp: prod_algebra_def)
qed
@@ -402,7 +205,7 @@
lemma prod_algebraI:
"finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
\<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
- by (auto simp: prod_algebra_def Pi_iff)
+ by (auto simp: prod_algebra_def)
lemma prod_algebraI_finite:
"finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
@@ -412,7 +215,7 @@
proof (safe intro!: Int_stableI)
fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
- by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
+ by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
qed
lemma prod_algebraE:
@@ -501,7 +304,7 @@
assume "I \<noteq> {}"
then obtain i where "i \<in> I" by auto
then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
- by (auto simp: prod_emb_def Pi_iff)
+ by (auto simp: prod_emb_def)
also have "\<dots> \<in> prod_algebra I M"
using `i \<in> I` by (intro prod_algebraI) auto
finally show ?thesis .
@@ -529,8 +332,7 @@
next
assume "I \<noteq> {}"
with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^isub>E i\<in>I. space (M i)). f j \<in> X j})"
- using sets_into_space[OF X(5)]
- by (auto simp: prod_emb_PiE[OF _ sets_into_space] Pi_iff split: split_if_asm) blast
+ by (auto simp: prod_emb_def)
also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
finally show "A \<in> sigma_sets ?\<Omega> ?R" .
@@ -540,11 +342,7 @@
then obtain i B where A: "A = {f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
by auto
then have "A = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. B)"
- using sets_into_space[OF A(3)]
- apply (subst prod_emb_PiE)
- apply (auto simp: Pi_iff split: split_if_asm)
- apply blast
- done
+ by (auto simp: prod_emb_def)
also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
using A by (intro sigma_sets.Basic prod_algebraI) auto
finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
@@ -585,9 +383,8 @@
proof (rule measurable_sigma_sets)
fix A assume "A \<in> prod_algebra I M"
from prod_algebraE[OF this] guess J X . note X = this
- have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
- using sets_into_space[OF X(5)] X(2-) space unfolding X(1)
- by (subst prod_emb_PiE) (auto simp: Pi_iff split: split_if_asm)
+ then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
+ using space by (auto simp: prod_emb_def del: PiE_I)
also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
finally show "f -` A \<inter> space N \<in> sets N" .
qed
@@ -654,7 +451,7 @@
assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
using fg[THEN measurable_space]
- by (auto intro!: measurable_PiM_single' simp add: space_PiM Pi_iff split: nat.split)
+ by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
lemma measurable_add_dim[measurable]:
"(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
@@ -668,7 +465,7 @@
using A j
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
-qed (auto simp: space_pair_measure space_PiM)
+qed (auto simp: space_pair_measure space_PiM PiE_def)
lemma measurable_component_update:
"x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
@@ -686,7 +483,7 @@
using A
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
-qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
+qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
lemma measurable_restrict[measurable (raw)]:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
@@ -697,7 +494,7 @@
by auto
then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
using A X by (auto intro!: measurable_sets)
-qed (insert X, auto dest: measurable_space)
+qed (insert X, auto simp add: PiE_def dest: measurable_space)
lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
by (intro measurable_restrict measurable_component_singleton) auto
@@ -762,13 +559,12 @@
next
fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
next
- fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space (PiM I M)"
- using `\<And>i. range (F i) \<subseteq> sets (M i)` sets_into_space
- by auto blast
+ fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
+ by (auto simp: PiE_def dest!: sets_into_space)
next
fix f assume "f \<in> space (PiM I M)"
with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
- show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
+ show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
next
fix i show "?F i \<subseteq> ?F (Suc i)"
using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
@@ -826,13 +622,13 @@
by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
using J E[rule_format, THEN sets_into_space]
- by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
+ by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
using J E[rule_format, THEN sets_into_space]
- by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
+ by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
(\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
using E by (subst insert) (auto intro!: setprod_cong)
@@ -844,7 +640,7 @@
finally show "?\<mu> ?p = \<dots>" .
show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
- using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
+ using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
next
show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
@@ -961,7 +757,7 @@
using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
using `finite J` `finite I` F unfolding X
- by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
+ by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times)
also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one)
also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
@@ -1034,7 +830,7 @@
show "(\<integral>\<^isup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^isub>M {i} M) = (\<integral>\<^isup>+ y. f (x(i := y i)) \<partial>Pi\<^isub>M {i} M)"
using x
by (auto intro!: positive_integral_cong arg_cong[where f=f]
- simp add: space_PiM extensional_def)
+ simp add: space_PiM extensional_def PiE_def)
qed
qed
@@ -1085,7 +881,7 @@
then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
by simp
also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
- by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
+ by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
also have "\<dots> = emeasure ?D A"
using A by (simp add: product_positive_integral_singleton emeasure_distr)
finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
@@ -1160,7 +956,7 @@
using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
unfolding comp_def .
from x I show "(\<integral> y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
- by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
+ by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
qed
finally show ?thesis .
qed
@@ -1233,7 +1029,7 @@
proof
let ?P = "sigma (space (Pi\<^isub>M I M)) P"
have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
- using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+ using E_closed by (auto simp: space_PiM P_def subset_eq)
then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
by (simp add: space_PiM)
have "sets (PiM I M) =
@@ -1281,7 +1077,7 @@
then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
- using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+ using E_closed by (auto simp: space_PiM P_def subset_eq)
then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
by (simp add: space_PiM)
have "sets (PiM I M) =
@@ -1293,18 +1089,17 @@
have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
proof (subst measurable_iff_measure_of)
show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
- from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)"
- by (auto simp: Pi_iff)
+ from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
proof
fix A assume A: "A \<in> E i"
then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
- using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
+ using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
also have "\<dots> = (\<Pi>\<^isub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
by (intro PiE_cong) (simp add: S_union)
also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j))"
using T
- apply (auto simp: Pi_iff bchoice_iff)
+ apply (auto simp: PiE_iff bchoice_iff)
apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
apply (auto simp: bij_betw_def)
done
@@ -1352,7 +1147,7 @@
using A B by (subst B.emeasure_PiM) (auto split: bool.split)
also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
using A[THEN sets_into_space] B[THEN sets_into_space]
- by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
+ by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
using A B
measurable_component_singleton[of True UNIV "bool_case M1 M2"]
--- a/src/HOL/Probability/Independent_Family.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Mon Nov 19 12:29:02 2012 +0100
@@ -867,7 +867,7 @@
then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
by (simp add: emeasure_distr X)
also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
- using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
+ using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J]
by (auto simp: emeasure_eq_measure setprod_ereal)
@@ -898,7 +898,7 @@
Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)"
from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
- using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
+ using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
by simp
also have "\<dots> = emeasure ?D ?E"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Mon Nov 19 12:29:02 2012 +0100
@@ -234,11 +234,9 @@
using w'(1) J(3)[of "Suc k"]
by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
show ?thesis
- apply (rule exI[of _ ?w])
using w' J_mono[of k "Suc k"] wk unfolding *
- apply (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM)
- apply (force simp: extensional_def)
- done
+ by (intro exI[of _ ?w])
+ (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
qed
then have "?P k (w k) (w (Suc k))"
unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
@@ -295,8 +293,8 @@
using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
{ fix n
- have "restrict w' (J n) = w n" using w(1)
- by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def space_PiM)
+ have "restrict w' (J n) = w n" using w(1)[of n]
+ by (auto simp add: fun_eq_iff space_PiM)
with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
then have "w' \<in> (\<Inter>i. A i)" by auto
@@ -391,7 +389,7 @@
lemma sets_Collect_single':
"i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
- by (simp add: space_PiM Pi_iff cong: conj_cong)
+ by (simp add: space_PiM PiE_iff cong: conj_cong)
lemma (in finite_product_prob_space) finite_measure_PiM_emb:
"(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
@@ -462,7 +460,7 @@
"(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
proof (rule measurable_PiM_single)
show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
- by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
+ by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
fix j :: nat and A assume A: "A \<in> sets M"
then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
(if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
@@ -550,7 +548,7 @@
with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
(prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
(prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
- by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib Pi_iff
+ by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
split: split_comb_seq split_comb_seq_asm)
then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^isub>M S) (?E \<times> ?F)"
by (subst emeasure_distr[OF measurable_comb_seq])
@@ -581,7 +579,7 @@
using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
(prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
- by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
+ by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
split: nat.split nat.split_asm)
then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
by (subst emeasure_distr)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Nov 19 12:29:02 2012 +0100
@@ -935,7 +935,7 @@
fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
then obtain x where "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
- using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
+ using DIM_positive by (auto simp add: set_eq_iff e2p_def
euclidean_eq[where 'a='a] eucl_less[where 'a='a])
then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
qed (auto simp: e2p_def)
@@ -953,7 +953,7 @@
let ?A = "{w \<in> space ?P. (p2e w :: 'a) $$ i \<le> x}"
assume "i < DIM('a)"
then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
- using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
+ using DIM_positive by (auto simp: space_PiM p2e_def PiE_def split: split_if_asm)
then show "?A \<in> sets ?P"
by auto
qed
@@ -966,7 +966,7 @@
let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
fix a b :: 'a
have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
- by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
+ by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff)
have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
proof cases
assume "{a..b} \<noteq> {}"
--- a/src/HOL/Probability/Projective_Family.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Mon Nov 19 12:29:02 2012 +0100
@@ -44,7 +44,7 @@
also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
using E by (simp add: K.measure_times)
also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
- using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm)
+ using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
using X `J \<subseteq> K` apply (subst emeasure_distr)
by (auto intro!: measurable_restrict_subset simp: space_PiM)
@@ -93,15 +93,10 @@
shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
proof -
have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
- proof safe
- fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
- hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
- also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
- finally show "x j \<in> space (M j)" .
- qed
+ using sets_into_space[OF A] by (auto simp: PiE_iff) blast
hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
- using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
+ using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
proof (rule emeasure_extend_measure_Pair[OF limP_def])
show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
@@ -169,7 +164,7 @@
from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
qed
from bchoice[OF this]
- show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
+ show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
qed fact
@@ -293,7 +288,7 @@
have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
have [simp]: "(K - J) \<inter> K = K - J" by auto
from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
- by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
+ by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
auto
qed
--- a/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 12:29:02 2012 +0100
@@ -428,7 +428,7 @@
also have "\<dots> = P (J i) (B i) - P' i (K' i)"
unfolding K_def P'_def
by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric]
- compact_imp_closed[OF `compact (K' _)`] space_PiM)
+ compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def)
also have "\<dots> \<le> ereal (2 powr - real i) * ?a" using K'(1)[of i] .
finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" .
qed
@@ -580,7 +580,7 @@
ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"
unfolding K_def by (auto simp: proj_space space_PiM)
hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def
- using J by (auto simp: prod_emb_def extensional_def)
+ using J by (auto simp: prod_emb_def PiE_def extensional_def)
also have "\<dots> \<subseteq> Z n" using Z' by simp
finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .
} note in_Z = this
@@ -602,7 +602,7 @@
using assms by (auto simp: f_def)
next
fix J and X::"'i \<Rightarrow> 'a set"
- show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow ((I \<rightarrow> space borel) \<inter> extensional I)"
+ show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow (I \<rightarrow>\<^isub>E space borel)"
by (auto simp: prod_emb_def)
assume JX: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> J \<rightarrow> sets borel"
hence "emb I J (Pi\<^isub>E J X) \<in> generator" using assms
@@ -645,11 +645,11 @@
interpret prob_space "P {i}" using proj_prob_space by simp
have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
by (auto simp: prod_emb_def space_PiM)
- moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
+ moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM PiE_def)
ultimately show ?thesis using `i \<in> I`
apply (subst R)
apply (subst emeasure_limB_emb_not_empty)
- apply (auto simp: limP_finite emeasure_space_1)
+ apply (auto simp: limP_finite emeasure_space_1 PiE_def)
done
qed
qed
--- a/src/HOL/ex/Birthday_Paradox.thy Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/ex/Birthday_Paradox.thy Mon Nov 19 12:29:02 2012 +0100
@@ -14,21 +14,7 @@
assumes "finite S"
assumes "\<forall>x \<in> S. finite (T x)"
shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
-proof -
- note `finite S`
- moreover
- have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
- moreover
- from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
- moreover
- have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
- moreover
- ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
- by (auto, subst card_UN_disjoint) auto
- also have "... = (SUM x:S. card (T x))"
- by (subst card_image) (auto intro: inj_onI)
- finally show ?thesis by auto
-qed
+ using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
lemma card_extensional_funcset_inj_on:
assumes "finite S" "finite T" "card S \<le> card T"
@@ -36,13 +22,13 @@
using assms
proof (induct S arbitrary: T rule: finite_induct)
case empty
- from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
+ from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
next
case (insert x S)
{ fix x
from `finite T` have "finite (T - {x})" by auto
from `finite S` this have "finite (extensional_funcset S (T - {x}))"
- by (rule finite_extensional_funcset)
+ by (rule finite_PiE)
moreover
have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
@@ -75,10 +61,10 @@
proof -
have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
- by (auto intro!: finite_extensional_funcset)
+ by (auto intro!: finite_PiE)
have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
from assms this finite subset show ?thesis
- by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
+ by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
qed
lemma setprod_upto_nat_unfold:
@@ -93,9 +79,9 @@
proof -
from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
from assms show ?thesis
- using card_extensional_funcset[OF `finite S`, of T]
+ using card_PiE[OF `finite S`, of "\<lambda>i. T"] `finite S`
card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
- by (simp add: fact_div_fact setprod_upto_nat_unfold)
+ by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
qed
end