--- a/NEWS Wed Dec 08 14:25:08 2010 +0100
+++ b/NEWS Wed Dec 08 16:47:57 2010 +0100
@@ -111,6 +111,17 @@
*** HOL ***
+* More canonical naming convention for some fundamental definitions:
+
+ bot_bool_eq ~> bot_bool_def
+ top_bool_eq ~> top_bool_def
+ inf_bool_eq ~> inf_bool_def
+ sup_bool_eq ~> sup_bool_def
+ bot_fun_eq ~> bot_fun_def
+ top_fun_eq ~> top_fun_def
+ inf_fun_eq ~> inf_fun_def
+ sup_fun_eq ~> sup_fun_def
+
* Quickcheck now by default uses exhaustive testing instead of random
testing. Random testing can be invoked by quickcheck[random],
exhaustive testing by quickcheck[exhaustive].
--- a/src/HOL/Complete_Lattice.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy Wed Dec 08 16:47:57 2010 +0100
@@ -44,14 +44,22 @@
lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Inf_empty:
+lemma Inf_empty [simp]:
"\<Sqinter>{} = \<top>"
by (auto intro: antisym Inf_greatest)
-lemma Sup_empty:
+lemma Sup_empty [simp]:
"\<Squnion>{} = \<bottom>"
by (auto intro: antisym Sup_least)
+lemma Inf_UNIV [simp]:
+ "\<Sqinter>UNIV = \<bottom>"
+ by (simp add: Sup_Inf Sup_empty [symmetric])
+
+lemma Sup_UNIV [simp]:
+ "\<Squnion>UNIV = \<top>"
+ by (simp add: Inf_Sup Inf_empty [symmetric])
+
lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
@@ -74,19 +82,21 @@
"\<Squnion>{a, b} = a \<squnion> b"
by (simp add: Sup_empty Sup_insert)
-lemma Inf_UNIV:
- "\<Sqinter>UNIV = bot"
- by (simp add: Sup_Inf Sup_empty [symmetric])
-
-lemma Sup_UNIV:
- "\<Squnion>UNIV = top"
- by (simp add: Inf_Sup Inf_empty [symmetric])
+lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+ by (auto intro: Inf_greatest dest: Inf_lower)
lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
by (auto intro: Sup_least dest: Sup_upper)
-lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
- by (auto intro: Inf_greatest dest: Inf_lower)
+lemma Inf_mono:
+ assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+ shows "Inf A \<le> Inf B"
+proof (rule Inf_greatest)
+ fix b assume "b \<in> B"
+ with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+ from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
+ with `a \<le> b` show "Inf A \<le> b" by auto
+qed
lemma Sup_mono:
assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
@@ -98,43 +108,39 @@
with `a \<le> b` show "a \<le> Sup B" by auto
qed
-lemma Inf_mono:
- assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
- shows "Inf A \<le> Inf B"
-proof (rule Inf_greatest)
- fix b assume "b \<in> B"
- with assms obtain a where "a \<in> A" and "a \<le> b" by blast
- from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
- with `a \<le> b` show "Inf A \<le> b" by auto
-qed
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "INFI A f = \<Sqinter> (f ` A)"
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
-definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "INFI A f = \<Sqinter> (f ` A)"
-
end
syntax
- "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
- "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
translations
+ "INF x y. B" == "INF x. INF y. B"
+ "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
+ "INF x. B" == "INF x:CONST UNIV. B"
+ "INF x:A. B" == "CONST INFI A (%x. B)"
"SUP x y. B" == "SUP x. SUP y. B"
"SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
"SUP x. B" == "SUP x:CONST UNIV. B"
"SUP x:A. B" == "CONST SUPR A (%x. B)"
- "INF x y. B" == "INF x. INF y. B"
- "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
- "INF x. B" == "INF x:CONST UNIV. B"
- "INF x:A. B" == "CONST INFI A (%x. B)"
print_translation {*
- [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"},
- Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}]
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
*} -- {* to avoid eta-contraction of body *}
context complete_lattice
@@ -158,79 +164,71 @@
lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
unfolding INFI_def by (auto simp add: le_Inf_iff)
-lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
- by (auto intro: antisym SUP_leI le_SUPI)
-
lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
by (auto intro: antisym INF_leI le_INFI)
-lemma SUP_mono:
- "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
- by (force intro!: Sup_mono simp: SUPR_def)
+lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
+ by (auto intro: antisym SUP_leI le_SUPI)
lemma INF_mono:
"(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
by (force intro!: Inf_mono simp: INFI_def)
-lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
- by (intro SUP_mono) auto
+lemma SUP_mono:
+ "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+ by (force intro!: Sup_mono simp: SUPR_def)
lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
by (intro INF_mono) auto
-lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
- by (iprover intro: SUP_leI le_SUPI order_trans antisym)
+lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
+ by (intro SUP_mono) auto
lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
by (iprover intro: INF_leI le_INFI order_trans antisym)
+lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
+ by (iprover intro: SUP_leI le_SUPI order_trans antisym)
+
end
+lemma Inf_less_iff:
+ fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+ shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
+ unfolding not_le[symmetric] le_Inf_iff by auto
+
lemma less_Sup_iff:
fixes a :: "'a\<Colon>{complete_lattice,linorder}"
shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
unfolding not_le[symmetric] Sup_le_iff by auto
-lemma Inf_less_iff:
- fixes a :: "'a\<Colon>{complete_lattice,linorder}"
- shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
- unfolding not_le[symmetric] le_Inf_iff by auto
+lemma INF_less_iff:
+ fixes a :: "'a::{complete_lattice,linorder}"
+ shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+ unfolding INFI_def Inf_less_iff by auto
lemma less_SUP_iff:
fixes a :: "'a::{complete_lattice,linorder}"
shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
unfolding SUPR_def less_Sup_iff by auto
-lemma INF_less_iff:
- fixes a :: "'a::{complete_lattice,linorder}"
- shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
- unfolding INFI_def Inf_less_iff by auto
-
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
instantiation bool :: complete_lattice
begin
definition
- Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+ "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
definition
- Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+ "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
instance proof
qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
end
-lemma Inf_empty_bool [simp]:
- "\<Sqinter>{}"
- unfolding Inf_bool_def by auto
-
-lemma not_Sup_empty_bool [simp]:
- "\<not> \<Squnion>{}"
- unfolding Sup_bool_def by auto
-
-lemma INFI_bool_eq:
+lemma INFI_bool_eq [simp]:
"INFI = Ball"
proof (rule ext)+
fix A :: "'a set"
@@ -239,7 +237,7 @@
by (auto simp add: Ball_def INFI_def Inf_bool_def)
qed
-lemma SUPR_bool_eq:
+lemma SUPR_bool_eq [simp]:
"SUPR = Bex"
proof (rule ext)+
fix A :: "'a set"
@@ -252,36 +250,226 @@
begin
definition
- Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+
+lemma Inf_apply:
+ "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
+ by (simp add: Inf_fun_def)
definition
- Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+
+lemma Sup_apply:
+ "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
+ by (simp add: Sup_fun_def)
instance proof
-qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
+qed (auto simp add: le_fun_def Inf_apply Sup_apply
intro: Inf_lower Sup_upper Inf_greatest Sup_least)
end
-lemma SUPR_fun_expand:
- fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
- shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
- by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
- simp: SUPR_def Sup_fun_def)
+lemma INFI_apply:
+ "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
+ by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
+
+lemma SUPR_apply:
+ "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
+ by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
+
+
+subsection {* Inter *}
+
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> \<Sqinter>S"
+
+notation (xsymbols)
+ Inter ("\<Inter>_" [90] 90)
+
+lemma Inter_eq:
+ "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
+proof (rule set_eqI)
+ fix x
+ have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
+ by auto
+ then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
+ by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
+qed
+
+lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
+ by (unfold Inter_eq) blast
+
+lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
+ by (simp add: Inter_eq)
+
+text {*
+ \medskip A ``destruct'' rule -- every @{term X} in @{term C}
+ contains @{term A} as an element, but @{prop "A:X"} can hold when
+ @{prop "X:C"} does not! This rule is analogous to @{text spec}.
+*}
+
+lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
+ by auto
+
+lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
+ -- {* ``Classical'' elimination rule -- does not require proving
+ @{prop "X:C"}. *}
+ by (unfold Inter_eq) blast
+
+lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
+ by blast
+
+lemma Inter_subset:
+ "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
+ by blast
+
+lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
+ by (iprover intro: InterI subsetI dest: subsetD)
+
+lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
+ by blast
+
+lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
+ by (fact Inf_empty)
+
+lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
+ by blast
+
+lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
+ by blast
+
+lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
+ by blast
+
+lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
+ by blast
+
+lemma Inter_UNIV_conv [simp,no_atp]:
+ "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
+ "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
+ by blast+
+
+lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
+ by blast
+
+
+subsection {* Intersections of families *}
+
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "INTER \<equiv> INFI"
+
+syntax
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
+
+syntax (latex output)
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
-lemma INFI_fun_expand:
- fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
- shows "(INF y:A. f y) x = (INF y:A. f y x)"
- by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
- simp: INFI_def Inf_fun_def)
+translations
+ "INT x y. B" == "INT x. INT y. B"
+ "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
+ "INT x. B" == "INT x:CONST UNIV. B"
+ "INT x:A. B" == "CONST INTER A (%x. B)"
+
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
+*} -- {* to avoid eta-contraction of body *}
+
+lemma INTER_eq_Inter_image:
+ "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
+ by (fact INFI_def)
+
+lemma Inter_def:
+ "\<Inter>S = (\<Inter>x\<in>S. x)"
+ by (simp add: INTER_eq_Inter_image image_def)
+
+lemma INTER_def:
+ "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
+ by (auto simp add: INTER_eq_Inter_image Inter_eq)
+
+lemma Inter_image_eq [simp]:
+ "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+ by (rule sym) (fact INTER_eq_Inter_image)
+
+lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
+ by (unfold INTER_def) blast
+
+lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
+ by (unfold INTER_def) blast
+
+lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
+ by auto
+
+lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
+ -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
+ by (unfold INTER_def) blast
+
+lemma INT_cong [cong]:
+ "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
+ by (simp add: INTER_def)
+
+lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
+ by blast
+
+lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
+ by blast
-lemma Inf_empty_fun:
- "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
- by (simp add: Inf_fun_def)
+lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
+ by (fact INF_leI)
+
+lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
+ by (fact le_INFI)
+
+lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
+ by blast
+
+lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
+ by blast
+
+lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
+ by (fact le_INF_iff)
+
+lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
+ by blast
+
+lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
+ by blast
+
+lemma INT_insert_distrib:
+ "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+ by blast
-lemma Sup_empty_fun:
- "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
- by (simp add: Sup_fun_def)
+lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
+ by auto
+
+lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
+ -- {* Look: it has an \emph{existential} quantifier *}
+ by blast
+
+lemma INTER_UNIV_conv[simp]:
+ "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
+ "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
+by blast+
+
+lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
+ by (auto intro: bool_induct)
+
+lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
+ by blast
+
+lemma INT_anti_mono:
+ "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
+ (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
+ -- {* The last inclusion is POSITIVE! *}
+ by (blast dest: subsetD)
+
+lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
+ by blast
subsection {* Union *}
@@ -520,200 +708,6 @@
by blast
-subsection {* Inter *}
-
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> \<Sqinter>S"
-
-notation (xsymbols)
- Inter ("\<Inter>_" [90] 90)
-
-lemma Inter_eq:
- "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
-proof (rule set_eqI)
- fix x
- have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
- by auto
- then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
-qed
-
-lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
- by (unfold Inter_eq) blast
-
-lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
- by (simp add: Inter_eq)
-
-text {*
- \medskip A ``destruct'' rule -- every @{term X} in @{term C}
- contains @{term A} as an element, but @{prop "A:X"} can hold when
- @{prop "X:C"} does not! This rule is analogous to @{text spec}.
-*}
-
-lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
- by auto
-
-lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
- -- {* ``Classical'' elimination rule -- does not require proving
- @{prop "X:C"}. *}
- by (unfold Inter_eq) blast
-
-lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
- by blast
-
-lemma Inter_subset:
- "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
- by blast
-
-lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
- by (iprover intro: InterI subsetI dest: subsetD)
-
-lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by blast
-
-lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
- by blast
-
-lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
- by blast
-
-lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
- by blast
-
-lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
- by blast
-
-lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
- by blast
-
-lemma Inter_UNIV_conv [simp,no_atp]:
- "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
- "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
- by blast+
-
-lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
- by blast
-
-
-subsection {* Intersections of families *}
-
-abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "INTER \<equiv> INFI"
-
-syntax
- "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
-
-syntax (xsymbols)
- "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
-
-syntax (latex output)
- "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
-
-translations
- "INT x y. B" == "INT x. INT y. B"
- "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
- "INT x. B" == "INT x:CONST UNIV. B"
- "INT x:A. B" == "CONST INTER A (%x. B)"
-
-print_translation {*
- [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
-*} -- {* to avoid eta-contraction of body *}
-
-lemma INTER_eq_Inter_image:
- "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (fact INFI_def)
-
-lemma Inter_def:
- "\<Inter>S = (\<Inter>x\<in>S. x)"
- by (simp add: INTER_eq_Inter_image image_def)
-
-lemma INTER_def:
- "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
- by (auto simp add: INTER_eq_Inter_image Inter_eq)
-
-lemma Inter_image_eq [simp]:
- "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by (rule sym) (fact INTER_eq_Inter_image)
-
-lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
- by (unfold INTER_def) blast
-
-lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
- by (unfold INTER_def) blast
-
-lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
- by auto
-
-lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
- -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
- by (unfold INTER_def) blast
-
-lemma INT_cong [cong]:
- "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
- by (simp add: INTER_def)
-
-lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
- by blast
-
-lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
- by blast
-
-lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
- by (fact INF_leI)
-
-lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
- by (fact le_INFI)
-
-lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
- by blast
-
-lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
- by blast
-
-lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
- by (fact le_INF_iff)
-
-lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
- by blast
-
-lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
- by blast
-
-lemma INT_insert_distrib:
- "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
- by blast
-
-lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
- by auto
-
-lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
- -- {* Look: it has an \emph{existential} quantifier *}
- by blast
-
-lemma INTER_UNIV_conv[simp]:
- "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
- "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
-by blast+
-
-lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
- by (auto intro: bool_induct)
-
-lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
- by blast
-
-lemma INT_anti_mono:
- "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
- (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
- -- {* The last inclusion is POSITIVE! *}
- by (blast dest: subsetD)
-
-lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
- by blast
-
-
subsection {* Distributive laws *}
lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
@@ -864,12 +858,18 @@
no_notation
less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
+ bot ("\<bottom>") and
+ top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>")
+ Sup ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
lemmas mem_simps =
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
--- a/src/HOL/Inductive.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Inductive.thy Wed Dec 08 16:47:57 2010 +0100
@@ -217,7 +217,8 @@
lemma coinduct3:
"[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
-apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto)
+apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
+apply (simp_all)
done
--- a/src/HOL/Lattices.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Lattices.thy Wed Dec 08 16:47:57 2010 +0100
@@ -48,8 +48,9 @@
notation
less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
- top ("\<top>") and
- bot ("\<bottom>")
+ bot ("\<bottom>") and
+ top ("\<top>")
+
class semilattice_inf = order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -587,34 +588,33 @@
begin
definition
- bool_Compl_def: "uminus = Not"
+ bool_Compl_def [simp]: "uminus = Not"
definition
- bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
+ bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
definition
- inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
+ [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
definition
- sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
+ [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
instance proof
-qed (simp_all add: inf_bool_def sup_bool_def le_bool_def
- bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto)
+qed auto
end
lemma sup_boolI1:
"P \<Longrightarrow> P \<squnion> Q"
- by (simp add: sup_bool_def)
+ by simp
lemma sup_boolI2:
"Q \<Longrightarrow> P \<squnion> Q"
- by (simp add: sup_bool_def)
+ by simp
lemma sup_boolE:
"P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: sup_bool_def)
+ by auto
subsection {* Fun as lattice *}
@@ -623,19 +623,26 @@
begin
definition
- inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+
+lemma inf_apply:
+ "(f \<sqinter> g) x = f x \<sqinter> g x"
+ by (simp add: inf_fun_def)
definition
- sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+
+lemma sup_apply:
+ "(f \<squnion> g) x = f x \<squnion> g x"
+ by (simp add: sup_fun_def)
instance proof
-qed (simp_all add: le_fun_def inf_fun_def sup_fun_def)
+qed (simp_all add: le_fun_def inf_apply sup_apply)
end
-instance "fun" :: (type, distrib_lattice) distrib_lattice
-proof
-qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1)
+instance "fun" :: (type, distrib_lattice) distrib_lattice proof
+qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
instance "fun" :: (type, bounded_lattice) bounded_lattice ..
@@ -645,6 +652,10 @@
definition
fun_Compl_def: "- A = (\<lambda>x. - A x)"
+lemma uminus_apply:
+ "(- A) x = - (A x)"
+ by (simp add: fun_Compl_def)
+
instance ..
end
@@ -655,15 +666,16 @@
definition
fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
+lemma minus_apply:
+ "(A - B) x = A x - B x"
+ by (simp add: fun_diff_def)
+
instance ..
end
-instance "fun" :: (type, boolean_algebra) boolean_algebra
-proof
-qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def
- inf_compl_bot sup_compl_top diff_eq)
-
+instance "fun" :: (type, boolean_algebra) boolean_algebra proof
+qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
no_notation
less_eq (infix "\<sqsubseteq>" 50) and
--- a/src/HOL/Library/Lattice_Syntax.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy Wed Dec 08 16:47:57 2010 +0100
@@ -7,11 +7,17 @@
begin
notation
+ bot ("\<bottom>") and
top ("\<top>") and
- bot ("\<bottom>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900)
+syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
end
--- a/src/HOL/Orderings.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Orderings.thy Wed Dec 08 16:47:57 2010 +0100
@@ -1082,14 +1082,14 @@
subsection {* Top and bottom elements *}
+class bot = preorder +
+ fixes bot :: 'a
+ assumes bot_least [simp]: "bot \<le> x"
+
class top = preorder +
fixes top :: 'a
assumes top_greatest [simp]: "x \<le> top"
-class bot = preorder +
- fixes bot :: 'a
- assumes bot_least [simp]: "bot \<le> x"
-
subsection {* Dense orders *}
@@ -1204,50 +1204,50 @@
subsection {* Order on bool *}
-instantiation bool :: "{order, top, bot}"
+instantiation bool :: "{order, bot, top}"
begin
definition
- le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+ le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
definition
- less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
+ [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
definition
- top_bool_def: "top = True"
+ [simp]: "bot \<longleftrightarrow> False"
definition
- bot_bool_def: "bot = False"
+ [simp]: "top \<longleftrightarrow> True"
instance proof
-qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
+qed auto
end
lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
- by (simp add: le_bool_def)
+ by simp
lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
- by (simp add: le_bool_def)
+ by simp
lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
- by (simp add: le_bool_def)
+ by simp
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
- by (simp add: le_bool_def)
+ by simp
lemma bot_boolE: "bot \<Longrightarrow> P"
- by (simp add: bot_bool_def)
+ by simp
lemma top_boolI: top
- by (simp add: top_bool_def)
+ by simp
lemma [code]:
"False \<le> b \<longleftrightarrow> True"
"True \<le> b \<longleftrightarrow> b"
"False < b \<longleftrightarrow> b"
"True < b \<longleftrightarrow> False"
- unfolding le_bool_def less_bool_def by simp_all
+ by simp_all
subsection {* Order on functions *}
@@ -1259,7 +1259,7 @@
le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
definition
- less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
+ "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
instance ..
@@ -1272,26 +1272,34 @@
instance "fun" :: (type, order) order proof
qed (auto simp add: le_fun_def intro: antisym ext)
+instantiation "fun" :: (type, bot) bot
+begin
+
+definition
+ "bot = (\<lambda>x. bot)"
+
+lemma bot_apply:
+ "bot x = bot"
+ by (simp add: bot_fun_def)
+
+instance proof
+qed (simp add: le_fun_def bot_apply)
+
+end
+
instantiation "fun" :: (type, top) top
begin
definition
- top_fun_def [no_atp]: "top = (\<lambda>x. top)"
+ [no_atp]: "top = (\<lambda>x. top)"
declare top_fun_def_raw [no_atp]
+lemma top_apply:
+ "top x = top"
+ by (simp add: top_fun_def)
+
instance proof
-qed (simp add: top_fun_def le_fun_def)
-
-end
-
-instantiation "fun" :: (type, bot) bot
-begin
-
-definition
- bot_fun_def: "bot = (\<lambda>x. bot)"
-
-instance proof
-qed (simp add: bot_fun_def le_fun_def)
+qed (simp add: le_fun_def top_apply)
end
--- a/src/HOL/Predicate.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Predicate.thy Wed Dec 08 16:47:57 2010 +0100
@@ -9,12 +9,18 @@
begin
notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>")
+ Sup ("\<Squnion>_" [900] 900)
+
+syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
subsection {* Predicates as (complete) lattices *}
@@ -86,12 +92,6 @@
subsubsection {* Top and bottom elements *}
-lemma top1I [intro!]: "top x"
- by (simp add: top_fun_def top_bool_def)
-
-lemma top2I [intro!]: "top x y"
- by (simp add: top_fun_def top_bool_def)
-
lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
by (simp add: bot_fun_def bot_bool_def)
@@ -104,6 +104,45 @@
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
by (auto simp add: fun_eq_iff)
+lemma top1I [intro!]: "top x"
+ by (simp add: top_fun_def top_bool_def)
+
+lemma top2I [intro!]: "top x y"
+ by (simp add: top_fun_def top_bool_def)
+
+
+subsubsection {* Binary intersection *}
+
+lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1D1: "inf A B x ==> A x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2D1: "inf A B x y ==> A x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1D2: "inf A B x ==> B x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2D2: "inf A B x y ==> B x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+ by (simp add: inf_fun_def inf_bool_def mem_def)
+
+lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
+ by (simp add: inf_fun_def inf_bool_def mem_def)
+
subsubsection {* Binary union *}
@@ -143,97 +182,64 @@
by (simp add: sup_fun_def sup_bool_def mem_def)
-subsubsection {* Binary intersection *}
+subsubsection {* Intersections of families *}
-lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
+ by (simp add: INFI_apply)
-lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
+ by (simp add: INFI_apply)
-lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
+ by (auto simp add: INFI_apply)
-lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
+ by (auto simp add: INFI_apply)
-lemma inf1D1: "inf A B x ==> A x"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
+ by (auto simp add: INFI_apply)
-lemma inf2D1: "inf A B x y ==> A x y"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
+ by (auto simp add: INFI_apply)
-lemma inf1D2: "inf A B x ==> B x"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
+ by (auto simp add: INFI_apply)
-lemma inf2D2: "inf A B x y ==> B x y"
- by (simp add: inf_fun_def inf_bool_def)
+lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
+ by (auto simp add: INFI_apply)
-lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
- by (simp add: inf_fun_def inf_bool_def mem_def)
+lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
+ by (simp add: INFI_apply fun_eq_iff)
-lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
- by (simp add: inf_fun_def inf_bool_def mem_def)
+lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
+ by (simp add: INFI_apply fun_eq_iff)
subsubsection {* Unions of families *}
lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
- by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
+ by (simp add: SUPR_apply)
lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
- by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
+ by (simp add: SUPR_apply)
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
- by (auto simp add: SUP1_iff)
+ by (auto simp add: SUPR_apply)
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
- by (auto simp add: SUP2_iff)
+ by (auto simp add: SUPR_apply)
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
- by (auto simp add: SUP1_iff)
+ by (auto simp add: SUPR_apply)
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
- by (auto simp add: SUP2_iff)
+ by (auto simp add: SUPR_apply)
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
- by (simp add: SUP1_iff fun_eq_iff)
+ by (simp add: SUPR_apply fun_eq_iff)
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
- by (simp add: SUP2_iff fun_eq_iff)
-
-
-subsubsection {* Intersections of families *}
-
-lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
- by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
-
-lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
- by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
-
-lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
- by (auto simp add: INF1_iff)
-
-lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
- by (auto simp add: INF2_iff)
-
-lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
- by (auto simp add: INF1_iff)
-
-lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
- by (auto simp add: INF2_iff)
-
-lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
- by (auto simp add: INF1_iff)
-
-lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
- by (auto simp add: INF2_iff)
-
-lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
- by (simp add: INF1_iff fun_eq_iff)
-
-lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
- by (simp add: INF2_iff fun_eq_iff)
+ by (simp add: SUPR_apply fun_eq_iff)
subsection {* Predicates as relations *}
@@ -493,8 +499,7 @@
by (simp add: minus_pred_def)
instance proof
-qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def
- fun_Compl_def fun_diff_def bool_Compl_def bool_diff_def)
+qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply)
end
@@ -514,10 +519,10 @@
by (simp add: single_def)
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
- "P \<guillemotright>= f = (SUPR {x. Predicate.eval P x} f)"
+ "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
lemma eval_bind [simp]:
- "eval (P \<guillemotright>= f) = Predicate.eval (SUPR {x. Predicate.eval P x} f)"
+ "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
by (simp add: bind_def)
lemma bind_bind:
@@ -822,7 +827,7 @@
"single x = Seq (\<lambda>u. Insert x \<bottom>)"
unfolding Seq_def by simp
-primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
+primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
"apply f Empty = Empty"
| "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
| "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
@@ -972,7 +977,7 @@
"the A = (THE x. eval A x)"
lemma the_eqI:
- "(THE x. Predicate.eval P x) = x \<Longrightarrow> Predicate.the P = x"
+ "(THE x. eval P x) = x \<Longrightarrow> the P = x"
by (simp add: the_def)
lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
@@ -1022,14 +1027,20 @@
*}
no_notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>") and
bind (infixl "\<guillemotright>=" 70)
+no_syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
--- a/src/HOL/Probability/Borel_Space.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Dec 08 16:47:57 2010 +0100
@@ -1391,7 +1391,7 @@
proof safe
fix a
have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_fun_expand[where 'c=pextreal])
+ by (auto simp: less_SUP_iff SUPR_apply)
then show "{x\<in>space M. a < ?sup x} \<in> sets M"
using assms by auto
qed
@@ -1404,7 +1404,7 @@
proof safe
fix a
have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
- by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_fun_expand)
+ by (auto simp: INF_less_iff INFI_apply)
then show "{x\<in>space M. ?inf x < a} \<in> sets M"
using assms by auto
qed
@@ -1423,11 +1423,20 @@
using assms by auto
qed
+lemma INFI_fun_expand:
+ "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
+ by (simp add: fun_eq_iff INFI_apply)
+
+lemma SUPR_fun_expand:
+ "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
+ by (simp add: fun_eq_iff SUPR_apply)
+
lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
assumes "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
using assms unfolding psuminf_def
- by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
+ by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
+
section "LIMSEQ is borel measurable"
--- a/src/HOL/Set.thy Wed Dec 08 14:25:08 2010 +0100
+++ b/src/HOL/Set.thy Wed Dec 08 16:47:57 2010 +0100
@@ -533,6 +533,36 @@
by simp
+subsubsection {* The empty set *}
+
+lemma empty_def:
+ "{} = {x. False}"
+ by (simp add: bot_fun_def bot_bool_def Collect_def)
+
+lemma empty_iff [simp]: "(c : {}) = False"
+ by (simp add: empty_def)
+
+lemma emptyE [elim!]: "a : {} ==> P"
+ by simp
+
+lemma empty_subsetI [iff]: "{} \<subseteq> A"
+ -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
+ by blast
+
+lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
+ by blast
+
+lemma equals0D: "A = {} ==> a \<notin> A"
+ -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
+ by blast
+
+lemma ball_empty [simp]: "Ball {} P = True"
+ by (simp add: Ball_def)
+
+lemma bex_empty [simp]: "Bex {} P = False"
+ by (simp add: Bex_def)
+
+
subsubsection {* The universal set -- UNIV *}
abbreviation UNIV :: "'a set" where
@@ -568,36 +598,6 @@
lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
by auto
-
-subsubsection {* The empty set *}
-
-lemma empty_def:
- "{} = {x. False}"
- by (simp add: bot_fun_def bot_bool_def Collect_def)
-
-lemma empty_iff [simp]: "(c : {}) = False"
- by (simp add: empty_def)
-
-lemma emptyE [elim!]: "a : {} ==> P"
- by simp
-
-lemma empty_subsetI [iff]: "{} \<subseteq> A"
- -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
- by blast
-
-lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
- by blast
-
-lemma equals0D: "A = {} ==> a \<notin> A"
- -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
- by blast
-
-lemma ball_empty [simp]: "Ball {} P = True"
- by (simp add: Ball_def)
-
-lemma bex_empty [simp]: "Bex {} P = False"
- by (simp add: Bex_def)
-
lemma UNIV_not_empty [iff]: "UNIV ~= {}"
by (blast elim: equalityE)
@@ -647,7 +647,41 @@
lemma Compl_eq: "- A = {x. ~ x : A}" by blast
-subsubsection {* Binary union -- Un *}
+subsubsection {* Binary intersection *}
+
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+ "op Int \<equiv> inf"
+
+notation (xsymbols)
+ inter (infixl "\<inter>" 70)
+
+notation (HTML output)
+ inter (infixl "\<inter>" 70)
+
+lemma Int_def:
+ "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
+ by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
+
+lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
+ by (unfold Int_def) blast
+
+lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
+ by simp
+
+lemma IntD1: "c : A Int B ==> c:A"
+ by simp
+
+lemma IntD2: "c : A Int B ==> c:B"
+ by simp
+
+lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
+ by simp
+
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+ by (fact mono_inf)
+
+
+subsubsection {* Binary union *}
abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
"union \<equiv> sup"
@@ -689,40 +723,6 @@
by (fact mono_sup)
-subsubsection {* Binary intersection -- Int *}
-
-abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
- "op Int \<equiv> inf"
-
-notation (xsymbols)
- inter (infixl "\<inter>" 70)
-
-notation (HTML output)
- inter (infixl "\<inter>" 70)
-
-lemma Int_def:
- "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
- by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
-
-lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
- by (unfold Int_def) blast
-
-lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
- by simp
-
-lemma IntD1: "c : A Int B ==> c:A"
- by simp
-
-lemma IntD2: "c : A Int B ==> c:B"
- by simp
-
-lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
- by simp
-
-lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- by (fact mono_inf)
-
-
subsubsection {* Set difference *}
lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"