# HG changeset patch
# User huffman
# Date 1269850021 25200
# Node ID a5e7574d8214aa92308551134de90d2f2a9fd1ec
# Parent  9cdbc5ffc15c481501c4f241dd554db12dfbd0c0# Parent  7ddc33baf959c44d0693e4231230d7148eb659bb
merged

diff -r 7ddc33baf959 -r a5e7574d8214 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Mar 29 09:06:34 2010 +0200
+++ b/src/HOL/Lattices.thy	Mon Mar 29 01:07:01 2010 -0700
@@ -90,10 +90,10 @@
   by (rule order_trans) auto
 
 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-  by (blast intro: inf_greatest)
+  by (rule inf_greatest) (* FIXME: duplicate lemma *)
 
 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: order_trans le_infI1 le_infI2)
+  by (blast intro: order_trans inf_le1 inf_le2)
 
 lemma le_inf_iff [simp]:
   "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
@@ -103,6 +103,9 @@
   "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
 
+lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
+  by (fast intro: inf_greatest le_infI1 le_infI2)
+
 lemma mono_inf:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
   shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
@@ -123,11 +126,11 @@
 
 lemma le_supI:
   "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
-  by (blast intro: sup_least)
+  by (rule sup_least) (* FIXME: duplicate lemma *)
 
 lemma le_supE:
   "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: le_supI1 le_supI2 order_trans)
+  by (blast intro: order_trans sup_ge1 sup_ge2)
 
 lemma le_sup_iff [simp]:
   "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
@@ -137,6 +140,9 @@
   "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
 
+lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
+  by (fast intro: sup_least le_supI1 le_supI2)
+
 lemma mono_sup:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
   shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
@@ -345,6 +351,12 @@
   by (rule distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
+lemmas sup_inf_distrib =
+  sup_inf_distrib1 sup_inf_distrib2
+
+lemmas inf_sup_distrib =
+  inf_sup_distrib1 inf_sup_distrib2
+
 lemmas distrib =
   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
 
@@ -393,39 +405,13 @@
   "x \<squnion> \<bottom> = x"
   by (rule sup_absorb1) simp
 
-lemma inf_eq_top_eq1:
-  assumes "A \<sqinter> B = \<top>"
-  shows "A = \<top>"
-proof (cases "B = \<top>")
-  case True with assms show ?thesis by simp
-next
-  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
-
-lemma inf_eq_top_eq2:
-  assumes "A \<sqinter> B = \<top>"
-  shows "B = \<top>"
-  by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
+lemma inf_eq_top_iff [simp]:
+  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+  by (simp add: eq_iff)
 
-lemma sup_eq_bot_eq1:
-  assumes "A \<squnion> B = \<bottom>"
-  shows "A = \<bottom>"
-proof -
-  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
-
-lemma sup_eq_bot_eq2:
-  assumes "A \<squnion> B = \<bottom>"
-  shows "B = \<bottom>"
-proof -
-  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
+lemma sup_eq_bot_iff [simp]:
+  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  by (simp add: eq_iff)
 
 end
 
@@ -472,10 +458,7 @@
   "- x = - y \<longleftrightarrow> x = y"
 proof
   assume "- x = - y"
-  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 have "- (- x) = - (- y)" by (rule arg_cong)
   then show "x = y" by simp
 next
   assume "x = y"
@@ -499,18 +482,14 @@
 lemma compl_inf [simp]:
   "- (x \<sqinter> y) = - x \<squnion> - y"
 proof (rule compl_unique)
-  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
-    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) = \<bottom>"
+  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
+    by (simp only: inf_sup_distrib inf_aci)
+  then 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>"
+  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
+    by (simp only: sup_inf_distrib sup_aci)
+  then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
     by (simp add: sup_compl_top)
 qed
 
@@ -522,6 +501,21 @@
   then show ?thesis by simp
 qed
 
+lemma compl_mono:
+  "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
+proof -
+  assume "x \<sqsubseteq> y"
+  then have "x \<squnion> y = y" by (simp only: le_iff_sup)
+  then have "- (x \<squnion> y) = - y" by simp
+  then have "- x \<sqinter> - y = - y" by simp
+  then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
+  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
+qed
+
+lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
+  "- x \<le> - y \<longleftrightarrow> y \<le> x"
+by (auto dest: compl_mono)
+
 end
 
 
@@ -550,7 +544,7 @@
   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
-  
+
 
 subsection {* @{const min}/@{const max} on linear orders as
   special case of @{const inf}/@{const sup} *}
diff -r 7ddc33baf959 -r a5e7574d8214 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Mar 29 09:06:34 2010 +0200
+++ b/src/HOL/Predicate.thy	Mon Mar 29 01:07:01 2010 -0700
@@ -516,7 +516,7 @@
 
 lemma is_empty_sup:
   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
-  by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
+  by (auto simp add: is_empty_def)
 
 definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
   "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
diff -r 7ddc33baf959 -r a5e7574d8214 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Mar 29 09:06:34 2010 +0200
+++ b/src/HOL/Set.thy	Mon Mar 29 01:07:01 2010 -0700
@@ -507,7 +507,6 @@
   apply (rule Collect_mem_eq)
   done
 
-(* Due to Brian Huffman *)
 lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
 by(auto intro:set_ext)
 
@@ -1002,25 +1001,25 @@
 text {* \medskip Finite Union -- the least upper bound of two sets. *}
 
 lemma Un_upper1: "A \<subseteq> A \<union> B"
-  by blast
+  by (fact sup_ge1)
 
 lemma Un_upper2: "B \<subseteq> A \<union> B"
-  by blast
+  by (fact sup_ge2)
 
 lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
-  by blast
+  by (fact sup_least)
 
 
 text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
 
 lemma Int_lower1: "A \<inter> B \<subseteq> A"
-  by blast
+  by (fact inf_le1)
 
 lemma Int_lower2: "A \<inter> B \<subseteq> B"
-  by blast
+  by (fact inf_le2)
 
 lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
-  by blast
+  by (fact inf_greatest)
 
 
 text {* \medskip Set difference. *}
@@ -1166,34 +1165,34 @@
 text {* \medskip @{text Int} *}
 
 lemma Int_absorb [simp]: "A \<inter> A = A"
-  by blast
+  by (fact inf_idem)
 
 lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
-  by blast
+  by (fact inf_left_idem)
 
 lemma Int_commute: "A \<inter> B = B \<inter> A"
-  by blast
+  by (fact inf_commute)
 
 lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
-  by blast
+  by (fact inf_left_commute)
 
 lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
-  by blast
+  by (fact inf_assoc)
 
 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
   -- {* Intersection is an AC-operator *}
 
 lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
-  by blast
+  by (fact inf_absorb2)
 
 lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
-  by blast
+  by (fact inf_absorb1)
 
 lemma Int_empty_left [simp]: "{} \<inter> B = {}"
-  by blast
+  by (fact inf_bot_left)
 
 lemma Int_empty_right [simp]: "A \<inter> {} = {}"
-  by blast
+  by (fact inf_bot_right)
 
 lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
   by blast
@@ -1202,22 +1201,22 @@
   by blast
 
 lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
-  by blast
+  by (fact inf_top_left)
 
 lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
-  by blast
+  by (fact inf_top_right)
 
 lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
-  by blast
+  by (fact inf_sup_distrib1)
 
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
-  by blast
+  by (fact inf_sup_distrib2)
 
 lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
-  by blast
+  by (fact inf_eq_top_iff)
 
 lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
-  by blast
+  by (fact le_inf_iff)
 
 lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
   by blast
@@ -1226,40 +1225,40 @@
 text {* \medskip @{text Un}. *}
 
 lemma Un_absorb [simp]: "A \<union> A = A"
-  by blast
+  by (fact sup_idem)
 
 lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
-  by blast
+  by (fact sup_left_idem)
 
 lemma Un_commute: "A \<union> B = B \<union> A"
-  by blast
+  by (fact sup_commute)
 
 lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
-  by blast
+  by (fact sup_left_commute)
 
 lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
-  by blast
+  by (fact sup_assoc)
 
 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   -- {* Union is an AC-operator *}
 
 lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
-  by blast
+  by (fact sup_absorb2)
 
 lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
-  by blast
+  by (fact sup_absorb1)
 
 lemma Un_empty_left [simp]: "{} \<union> B = B"
-  by blast
+  by (fact sup_bot_left)
 
 lemma Un_empty_right [simp]: "A \<union> {} = A"
-  by blast
+  by (fact sup_bot_right)
 
 lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
-  by blast
+  by (fact sup_top_left)
 
 lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
-  by blast
+  by (fact sup_top_right)
 
 lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   by blast
@@ -1292,23 +1291,23 @@
   by auto
 
 lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
-  by blast
+  by (fact sup_inf_distrib1)
 
 lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
-  by blast
+  by (fact sup_inf_distrib2)
 
 lemma Un_Int_crazy:
     "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   by blast
 
 lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
-  by blast
+  by (fact le_iff_sup)
 
 lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
-  by blast
+  by (fact sup_eq_bot_iff)
 
 lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
-  by blast
+  by (fact le_sup_iff)
 
 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   by blast
@@ -1320,25 +1319,25 @@
 text {* \medskip Set complement *}
 
 lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
-  by blast
+  by (fact inf_compl_bot)
 
 lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
-  by blast
+  by (fact compl_inf_bot)
 
 lemma Compl_partition: "A \<union> -A = UNIV"
-  by blast
+  by (fact sup_compl_top)
 
 lemma Compl_partition2: "-A \<union> A = UNIV"
-  by blast
+  by (fact compl_sup_top)
 
 lemma double_complement [simp]: "- (-A) = (A::'a set)"
-  by blast
+  by (fact double_compl)
 
 lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
-  by blast
+  by (fact compl_sup)
 
 lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
-  by blast
+  by (fact compl_inf)
 
 lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   by blast
@@ -1348,16 +1347,16 @@
   by blast
 
 lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
-  by blast
+  by (fact compl_top_eq)
 
 lemma Compl_empty_eq [simp]: "-{} = UNIV"
-  by blast
+  by (fact compl_bot_eq)
 
 lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
-  by blast
+  by (fact compl_le_compl_iff)
 
 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
-  by blast
+  by (fact compl_eq_compl_iff)
 
 text {* \medskip Bounded quantifiers.
 
@@ -1531,16 +1530,16 @@
   by blast
 
 lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
-  by blast
+  by (fact sup_mono)
 
 lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
-  by blast
+  by (fact inf_mono)
 
 lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
   by blast
 
 lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
-  by blast
+  by (fact compl_mono)
 
 text {* \medskip Monotonicity of implications. *}
 
diff -r 7ddc33baf959 -r a5e7574d8214 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Mon Mar 29 09:06:34 2010 +0200
+++ b/src/HOL/SupInf.thy	Mon Mar 29 01:07:01 2010 -0700
@@ -106,10 +106,10 @@
 proof (cases "Sup X \<le> a")
   case True
   thus ?thesis
-    apply (simp add: max_def) 
+    apply (simp add: max_def)
     apply (rule Sup_eq_maximum)
-    apply (metis insertCI)
-    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
+    apply (rule insertI1)
+    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
     done
 next
   case False
@@ -177,7 +177,7 @@
   fixes S :: "real set"
   assumes fS: "finite S" and Se: "S \<noteq> {}"
   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
 
 lemma Sup_finite_gt_iff: 
   fixes S :: "real set"
@@ -331,8 +331,8 @@
   have "Inf (insert a X) \<le> Inf X"
     apply (rule Inf_greatest)
     apply (metis empty_psubset_nonempty psubset_eq x)
-    apply (rule Inf_lower_EX) 
-    apply (blast intro: elim:) 
+    apply (rule Inf_lower_EX)
+    apply (erule insertI2)
     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
     done
   moreover