--- a/NEWS Sat Dec 05 10:18:23 2009 +0100
+++ b/NEWS Sat Dec 05 20:02:21 2009 +0100
@@ -11,6 +11,25 @@
* Code generation: ML and OCaml code is decorated with signatures.
+* Complete_Lattice.thy: lemmas top_def and bot_def have been replaced
+by the more convenient lemmas Inf_empty and Sup_empty. Dropped lemmas
+Inf_insert_simp adn Sup_insert_simp, which are subsumed by Inf_insert and
+Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
+Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot respectively.
+INCOMPATIBILITY.
+
+* Finite_Set.thy and List.thy: some lemmas have been generalized from sets to lattices:
+ fun_left_comm_idem_inter ~> fun_left_comm_idem_inf
+ fun_left_comm_idem_union ~> fun_left_comm_idem_sup
+ inter_Inter_fold_inter ~> inf_Inf_fold_inf
+ union_Union_fold_union ~> sup_Sup_fold_sup
+ Inter_fold_inter ~> Inf_fold_inf
+ Union_fold_union ~> Sup_fold_sup
+ inter_INTER_fold_inter ~> inf_INFI_fold_inf
+ union_UNION_fold_union ~> sup_SUPR_fold_sup
+ INTER_fold_inter ~> INFI_fold_inf
+ UNION_fold_union ~> SUPR_fold_sup
+
*** ML ***
--- a/src/HOL/Complete_Lattice.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Complete_Lattice.thy Sat Dec 05 20:02:21 2009 +0100
@@ -7,10 +7,10 @@
begin
notation
- less_eq (infix "\<sqsubseteq>" 50) and
+ less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
top ("\<top>") and
bot ("\<bottom>")
@@ -25,7 +25,7 @@
subsection {* Abstract complete lattices *}
-class complete_lattice = lattice + bot + top + Inf + Sup +
+class complete_lattice = bounded_lattice + Inf + Sup +
assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
@@ -34,22 +34,23 @@
lemma dual_complete_lattice:
"complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (auto intro!: complete_lattice.intro dual_lattice
- bot.intro top.intro dual_preorder, unfold_locales)
- (fact bot_least top_greatest
- Sup_upper Sup_least Inf_lower Inf_greatest)+
+ by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+ (unfold_locales, (fact bot_least top_greatest
+ Sup_upper Sup_least Inf_lower Inf_greatest)+)
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
+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_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
- unfolding Sup_Inf by auto
+lemma Inf_empty:
+ "\<Sqinter>{} = \<top>"
+ by (auto intro: antisym Inf_greatest)
-lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
- unfolding Inf_Sup by auto
+lemma Sup_empty:
+ "\<Squnion>{} = \<bottom>"
+ by (auto intro: antisym Sup_least)
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)
@@ -65,37 +66,21 @@
"\<Squnion>{a} = a"
by (auto intro: antisym Sup_upper Sup_least)
-lemma Inf_insert_simp:
- "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
- by (cases "A = {}") (simp_all, simp add: Inf_insert)
-
-lemma Sup_insert_simp:
- "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
- by (cases "A = {}") (simp_all, simp add: Sup_insert)
-
lemma Inf_binary:
"\<Sqinter>{a, b} = a \<sqinter> b"
- by (auto simp add: Inf_insert_simp)
+ by (simp add: Inf_empty Inf_insert)
lemma Sup_binary:
"\<Squnion>{a, b} = a \<squnion> b"
- by (auto simp add: Sup_insert_simp)
-
-lemma bot_def:
- "bot = \<Squnion>{}"
- by (auto intro: antisym Sup_least)
+ by (simp add: Sup_empty Sup_insert)
-lemma top_def:
- "top = \<Sqinter>{}"
- by (auto intro: antisym Inf_greatest)
+lemma Inf_UNIV:
+ "\<Sqinter>UNIV = bot"
+ by (simp add: Sup_Inf Sup_empty [symmetric])
-lemma sup_bot [simp]:
- "x \<squnion> bot = x"
- using bot_least [of x] by (simp add: sup_commute sup_absorb2)
-
-lemma inf_top [simp]:
- "x \<sqinter> top = x"
- using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
+lemma Sup_UNIV:
+ "\<Squnion>UNIV = top"
+ by (simp add: Inf_Sup Inf_empty [symmetric])
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
@@ -129,16 +114,16 @@
context complete_lattice
begin
-lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
+lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
by (auto simp add: SUPR_def intro: Sup_upper)
-lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
+lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
by (auto simp add: SUPR_def intro: Sup_least)
-lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
+lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
by (auto simp add: INFI_def intro: Inf_lower)
-lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
+lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
by (auto simp add: INFI_def intro: Inf_greatest)
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
--- a/src/HOL/Finite_Set.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Finite_Set.thy Sat Dec 05 20:02:21 2009 +0100
@@ -2937,37 +2937,6 @@
end
-context complete_lattice
-begin
-
-text {*
- Coincidence on finite sets in complete lattices:
-*}
-
-lemma Inf_fin_Inf:
- assumes "finite A" and "A \<noteq> {}"
- shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
-proof -
- interpret ab_semigroup_idem_mult inf
- by (rule ab_semigroup_idem_mult_inf)
- from assms show ?thesis
- unfolding Inf_fin_def by (induct A set: finite)
- (simp_all add: Inf_insert_simp)
-qed
-
-lemma Sup_fin_Sup:
- assumes "finite A" and "A \<noteq> {}"
- shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
-proof -
- interpret ab_semigroup_idem_mult sup
- by (rule ab_semigroup_idem_mult_sup)
- from assms show ?thesis
- unfolding Sup_fin_def by (induct A set: finite)
- (simp_all add: Sup_insert_simp)
-qed
-
-end
-
subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
@@ -3345,15 +3314,15 @@
proof
qed auto
-lemma fun_left_comm_idem_inter:
- "fun_left_comm_idem op \<inter>"
+lemma (in lower_semilattice) fun_left_comm_idem_inf:
+ "fun_left_comm_idem inf"
proof
-qed auto
-
-lemma fun_left_comm_idem_union:
- "fun_left_comm_idem op \<union>"
+qed (auto simp add: inf_left_commute)
+
+lemma (in upper_semilattice) fun_left_comm_idem_sup:
+ "fun_left_comm_idem sup"
proof
-qed auto
+qed (auto simp add: sup_left_commute)
lemma union_fold_insert:
assumes "finite A"
@@ -3371,60 +3340,95 @@
from `finite A` show ?thesis by (induct A arbitrary: B) auto
qed
-lemma inter_Inter_fold_inter:
+context complete_lattice
+begin
+
+lemma inf_Inf_fold_inf:
assumes "finite A"
- shows "B \<inter> Inter A = fold (op \<inter>) B A"
+ shows "inf B (Inf A) = fold inf B A"
proof -
- interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+ interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: fold_fun_comm Int_commute)
+ (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
qed
-lemma union_Union_fold_union:
+lemma sup_Sup_fold_sup:
assumes "finite A"
- shows "B \<union> Union A = fold (op \<union>) B A"
+ shows "sup B (Sup A) = fold sup B A"
proof -
- interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+ interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: fold_fun_comm Un_commute)
+ (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
qed
-lemma Inter_fold_inter:
+lemma Inf_fold_inf:
assumes "finite A"
- shows "Inter A = fold (op \<inter>) UNIV A"
- using assms inter_Inter_fold_inter [of A UNIV] by simp
-
-lemma Union_fold_union:
+ shows "Inf A = fold inf top A"
+ using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
assumes "finite A"
- shows "Union A = fold (op \<union>) {} A"
- using assms union_Union_fold_union [of A "{}"] by simp
-
-lemma inter_INTER_fold_inter:
- assumes "finite A"
- shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold")
-proof (rule sym)
- interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
- interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
- from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
+ shows "Sup A = fold sup bot A"
+ using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
+
+lemma Inf_fin_Inf:
+ assumes "finite A" and "A \<noteq> {}"
+ shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
+proof -
+ interpret ab_semigroup_idem_mult inf
+ by (rule ab_semigroup_idem_mult_inf)
+ from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+ moreover with `finite A` have "finite B" by simp
+ ultimately show ?thesis
+ by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
+ (simp add: Inf_fold_inf)
qed
-lemma union_UNION_fold_union:
+lemma Sup_fin_Sup:
+ assumes "finite A" and "A \<noteq> {}"
+ shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
+proof -
+ interpret ab_semigroup_idem_mult sup
+ by (rule ab_semigroup_idem_mult_sup)
+ from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+ moreover with `finite A` have "finite B" by simp
+ ultimately show ?thesis
+ by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
+ (simp add: Sup_fold_sup)
+qed
+
+lemma inf_INFI_fold_inf:
assumes "finite A"
- shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold")
+ shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold")
proof (rule sym)
- interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
- interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
- from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
+ interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+ interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?inf"
+ by (induct A arbitrary: B)
+ (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
qed
-lemma INTER_fold_inter:
+lemma sup_SUPR_fold_sup:
assumes "finite A"
- shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
- using assms inter_INTER_fold_inter [of A UNIV] by simp
-
-lemma UNION_fold_union:
+ shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold")
+proof (rule sym)
+ interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+ interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?sup"
+ by (induct A arbitrary: B)
+ (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
+qed
+
+lemma INFI_fold_inf:
assumes "finite A"
- shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
- using assms union_UNION_fold_union [of A "{}"] by simp
+ shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
+ using assms inf_INFI_fold_inf [of A top] by simp
+
+lemma SUPR_fold_sup:
+ assumes "finite A"
+ shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
+ using assms sup_SUPR_fold_sup [of A bot] by simp
end
+
+end
--- a/src/HOL/Lattices.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Lattices.thy Sat Dec 05 20:02:21 2009 +0100
@@ -70,7 +70,7 @@
lemma mono_inf:
fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
- shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B"
+ shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
by (auto simp add: mono_def intro: Lattices.inf_greatest)
end
@@ -104,7 +104,7 @@
lemma mono_sup:
fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
- shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)"
+ shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
by (auto simp add: mono_def intro: Lattices.sup_least)
end
@@ -241,22 +241,22 @@
begin
lemma less_supI1:
- "x < a \<Longrightarrow> x < a \<squnion> b"
+ "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
proof -
interpret dual: lower_semilattice "op \<ge>" "op >" sup
by (fact dual_semilattice)
- assume "x < a"
- then show "x < a \<squnion> b"
+ assume "x \<sqsubset> a"
+ then show "x \<sqsubset> a \<squnion> b"
by (fact dual.less_infI1)
qed
lemma less_supI2:
- "x < b \<Longrightarrow> x < a \<squnion> b"
+ "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
proof -
interpret dual: lower_semilattice "op \<ge>" "op >" sup
by (fact dual_semilattice)
- assume "x < b"
- then show "x < a \<squnion> b"
+ assume "x \<sqsubset> b"
+ then show "x \<sqsubset> a \<squnion> b"
by (fact dual.less_infI2)
qed
@@ -294,58 +294,46 @@
end
-subsection {* Boolean algebras *}
+subsection {* Bounded lattices and boolean algebras *}
-class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
- assumes inf_compl_bot: "x \<sqinter> - x = bot"
- and sup_compl_top: "x \<squnion> - x = top"
- assumes diff_eq: "x - y = x \<sqinter> - y"
+class bounded_lattice = lattice + top + bot
begin
-lemma dual_boolean_algebra:
- "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
- by (rule boolean_algebra.intro, rule dual_distrib_lattice)
- (unfold_locales,
- auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
-
-lemma compl_inf_bot:
- "- x \<sqinter> x = bot"
- by (simp add: inf_commute inf_compl_bot)
-
-lemma compl_sup_top:
- "- x \<squnion> x = top"
- by (simp add: sup_commute sup_compl_top)
+lemma dual_bounded_lattice:
+ "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (rule bounded_lattice.intro, rule dual_lattice)
+ (unfold_locales, auto simp add: less_le_not_le)
lemma inf_bot_left [simp]:
- "bot \<sqinter> x = bot"
+ "\<bottom> \<sqinter> x = \<bottom>"
by (rule inf_absorb1) simp
lemma inf_bot_right [simp]:
- "x \<sqinter> bot = bot"
+ "x \<sqinter> \<bottom> = \<bottom>"
by (rule inf_absorb2) simp
lemma sup_top_left [simp]:
- "top \<squnion> x = top"
+ "\<top> \<squnion> x = \<top>"
by (rule sup_absorb1) simp
lemma sup_top_right [simp]:
- "x \<squnion> top = top"
+ "x \<squnion> \<top> = \<top>"
by (rule sup_absorb2) simp
lemma inf_top_left [simp]:
- "top \<sqinter> x = x"
+ "\<top> \<sqinter> x = x"
by (rule inf_absorb2) simp
lemma inf_top_right [simp]:
- "x \<sqinter> top = x"
+ "x \<sqinter> \<top> = x"
by (rule inf_absorb1) simp
lemma sup_bot_left [simp]:
- "bot \<squnion> x = x"
+ "\<bottom> \<squnion> x = x"
by (rule sup_absorb2) simp
lemma sup_bot_right [simp]:
- "x \<squnion> bot = x"
+ "x \<squnion> \<bottom> = x"
by (rule sup_absorb1) simp
lemma inf_eq_top_eq1:
@@ -354,8 +342,8 @@
proof (cases "B = \<top>")
case True with assms show ?thesis by simp
next
- case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
- then have "A \<sqinter> B < \<top>" by (rule less_infI2)
+ case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
+ then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
with assms show ?thesis by simp
qed
@@ -368,8 +356,8 @@
assumes "A \<squnion> B = \<bottom>"
shows "A = \<bottom>"
proof -
- interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
- by (rule dual_boolean_algebra)
+ interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
+ by (rule dual_bounded_lattice)
from dual.inf_eq_top_eq1 assms show ?thesis .
qed
@@ -377,14 +365,35 @@
assumes "A \<squnion> B = \<bottom>"
shows "B = \<bottom>"
proof -
- interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
- by (rule dual_boolean_algebra)
+ interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
+ by (rule dual_bounded_lattice)
from dual.inf_eq_top_eq2 assms show ?thesis .
qed
+end
+
+class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
+ assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
+ and sup_compl_top: "x \<squnion> - x = \<top>"
+ assumes diff_eq: "x - y = x \<sqinter> - y"
+begin
+
+lemma dual_boolean_algebra:
+ "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+ (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
+
+lemma compl_inf_bot:
+ "- x \<sqinter> x = \<bottom>"
+ by (simp add: inf_commute inf_compl_bot)
+
+lemma compl_sup_top:
+ "- x \<squnion> x = \<top>"
+ by (simp add: sup_commute sup_compl_top)
+
lemma compl_unique:
- assumes "x \<sqinter> y = bot"
- and "x \<squnion> y = top"
+ assumes "x \<sqinter> y = \<bottom>"
+ and "x \<squnion> y = \<top>"
shows "- x = y"
proof -
have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
@@ -393,7 +402,7 @@
by (simp add: inf_commute)
then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
by (simp add: inf_sup_distrib1)
- then have "- x \<sqinter> top = y \<sqinter> top"
+ then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
using sup_compl_top assms(2) by simp
then show "- x = y" by (simp add: inf_top_right)
qed
@@ -406,8 +415,8 @@
"- x = - y \<longleftrightarrow> x = y"
proof
assume "- x = - y"
- then have "- x \<sqinter> y = bot"
- and "- x \<squnion> y = top"
+ then have "- x \<sqinter> y = \<bottom>"
+ and "- x \<squnion> y = \<top>"
by (simp_all add: compl_inf_bot compl_sup_top)
then have "- (- x) = y" by (rule compl_unique)
then show "x = y" by simp
@@ -417,16 +426,16 @@
qed
lemma compl_bot_eq [simp]:
- "- bot = top"
+ "- \<bottom> = \<top>"
proof -
- from sup_compl_top have "bot \<squnion> - bot = top" .
+ from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
then show ?thesis by simp
qed
lemma compl_top_eq [simp]:
- "- top = bot"
+ "- \<top> = \<bottom>"
proof -
- from inf_compl_bot have "top \<sqinter> - top = bot" .
+ from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
then show ?thesis by simp
qed
@@ -437,21 +446,21 @@
by (rule inf_sup_distrib1)
also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
by (simp only: inf_commute inf_assoc inf_left_commute)
- finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
+ finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
by (simp add: inf_compl_bot)
next
have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
by (rule sup_inf_distrib2)
also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
by (simp only: sup_commute sup_assoc sup_left_commute)
- finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
+ finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
by (simp add: sup_compl_top)
qed
lemma compl_sup [simp]:
"- (x \<squnion> y) = - x \<sqinter> - y"
proof -
- interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+ interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
by (rule dual_boolean_algebra)
then show ?thesis by simp
qed
@@ -463,26 +472,26 @@
lemma (in lower_semilattice) inf_unique:
fixes f (infixl "\<triangle>" 70)
- assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
- and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
+ assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
+ and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
shows "x \<sqinter> y = x \<triangle> y"
proof (rule antisym)
- show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
+ show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
next
- have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
- show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
+ have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
+ show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
qed
lemma (in upper_semilattice) sup_unique:
fixes f (infixl "\<nabla>" 70)
- assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
- and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
+ assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
+ and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
shows "x \<squnion> y = x \<nabla> y"
proof (rule antisym)
- show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
+ show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
next
- have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
- show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
+ have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
+ show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
qed
@@ -568,6 +577,8 @@
proof
qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+instance "fun" :: (type, bounded_lattice) bounded_lattice ..
+
instantiation "fun" :: (type, uminus) uminus
begin
--- a/src/HOL/Library/List_Set.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Library/List_Set.thy Sat Dec 05 20:02:21 2009 +0100
@@ -85,50 +85,6 @@
"project P (set xs) = set (filter P xs)"
by (auto simp add: project_def)
-text {* FIXME move the following to @{text Finite_Set.thy} *}
-
-lemma fun_left_comm_idem_inf:
- "fun_left_comm_idem inf"
-proof
-qed (auto simp add: inf_left_commute)
-
-lemma fun_left_comm_idem_sup:
- "fun_left_comm_idem sup"
-proof
-qed (auto simp add: sup_left_commute)
-
-lemma inf_Inf_fold_inf:
- fixes A :: "'a::complete_lattice set"
- assumes "finite A"
- shows "inf B (Inf A) = fold inf B A"
-proof -
- interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
- from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
-qed
-
-lemma sup_Sup_fold_sup:
- fixes A :: "'a::complete_lattice set"
- assumes "finite A"
- shows "sup B (Sup A) = fold sup B A"
-proof -
- interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
- from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
-qed
-
-lemma Inf_fold_inf:
- fixes A :: "'a::complete_lattice set"
- assumes "finite A"
- shows "Inf A = fold inf top A"
- using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
-
-lemma Sup_fold_sup:
- fixes A :: "'a::complete_lattice set"
- assumes "finite A"
- shows "Sup A = fold sup bot A"
- using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-
subsection {* Functorial set operations *}
@@ -149,14 +105,6 @@
by (simp add: minus_fold_remove [of _ A] fold_set)
qed
-lemma INFI_set_fold: -- "FIXME move to List.thy"
- "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
- unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
-
-lemma SUPR_set_fold: -- "FIXME move to List.thy"
- "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
- unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
-
subsection {* Derived set operations *}
--- a/src/HOL/List.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/List.thy Sat Dec 05 20:02:21 2009 +0100
@@ -2359,15 +2359,29 @@
lemma (in complete_lattice) Inf_set_fold [code_unfold]:
"Inf (set xs) = foldl inf top xs"
- by (cases xs)
- (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
- inf_commute del: set.simps, simp add: top_def)
+proof -
+ interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_inf)
+ show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
+qed
lemma (in complete_lattice) Sup_set_fold [code_unfold]:
"Sup (set xs) = foldl sup bot xs"
- by (cases xs)
- (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
- sup_commute del: set.simps, simp add: bot_def)
+proof -
+ interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_sup)
+ show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
+qed
+
+lemma (in complete_lattice) INFI_set_fold:
+ "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
+ unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
+ by (simp add: inf_commute)
+
+lemma (in complete_lattice) SUPR_set_fold:
+ "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
+ unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
+ by (simp add: sup_commute)
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
--- a/src/HOL/Predicate.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Predicate.thy Sat Dec 05 20:02:21 2009 +0100
@@ -726,7 +726,7 @@
proof (cases "f ()")
case Empty
thus ?thesis
- unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot)
+ unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
next
case Insert
thus ?thesis