src/HOL/Complete_Lattice.thy
changeset 43831 e323be6b02a5
parent 43818 fcc5d3ffb6f5
child 43852 7411fbf0a325
     1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Jul 14 15:14:38 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Jul 14 17:14:54 2011 +0200
     1.3 @@ -76,11 +76,11 @@
     1.4  
     1.5  lemma Inf_binary:
     1.6    "\<Sqinter>{a, b} = a \<sqinter> b"
     1.7 -  by (simp add: Inf_empty Inf_insert)
     1.8 +  by (simp add: Inf_insert)
     1.9  
    1.10  lemma Sup_binary:
    1.11    "\<Squnion>{a, b} = a \<squnion> b"
    1.12 -  by (simp add: Sup_empty Sup_insert)
    1.13 +  by (simp add: Sup_insert)
    1.14  
    1.15  lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
    1.16    by (auto intro: Inf_greatest dest: Inf_lower)
    1.17 @@ -116,11 +116,11 @@
    1.18    "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
    1.19    by (rule antisym) auto
    1.20  
    1.21 -lemma not_less_bot[simp]: "\<not> (x \<sqsubset> \<bottom>)"
    1.22 -  using bot_least[of x] by (auto simp: le_less)
    1.23 +lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
    1.24 +  using bot_least [of x] by (auto simp: le_less)
    1.25  
    1.26 -lemma not_top_less[simp]: "\<not> (\<top> \<sqsubset> x)"
    1.27 -  using top_greatest[of x] by (auto simp: le_less)
    1.28 +lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
    1.29 +  using top_greatest [of x] by (auto simp: le_less)
    1.30  
    1.31  lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
    1.32    using Sup_upper[of u A] by auto
    1.33 @@ -838,25 +838,25 @@
    1.34  
    1.35  lemma UN_simps [simp]:
    1.36    "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
    1.37 -  "\<And>A B C. (\<Union>x\<in>C. A x Un B)   = ((if C={} then {} else (\<Union>x\<in>C. A x) Un B))"
    1.38 -  "\<And>A B C. (\<Union>x\<in>C. A Un B x)   = ((if C={} then {} else A Un (\<Union>x\<in>C. B x)))"
    1.39 -  "\<And>A B C. (\<Union>x\<in>C. A x Int B)  = ((\<Union>x\<in>C. A x) Int B)"
    1.40 -  "\<And>A B C. (\<Union>x\<in>C. A Int B x)  = (A Int (\<Union>x\<in>C. B x))"
    1.41 +  "\<And>A B C. (\<Union>x\<in>C. A x \<union>  B)   = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union>  B))"
    1.42 +  "\<And>A B C. (\<Union>x\<in>C. A \<union> B x)   = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
    1.43 +  "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B)  = ((\<Union>x\<in>C. A x) \<inter>B)"
    1.44 +  "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x)  = (A \<inter>(\<Union>x\<in>C. B x))"
    1.45    "\<And>A B C. (\<Union>x\<in>C. A x - B)    = ((\<Union>x\<in>C. A x) - B)"
    1.46    "\<And>A B C. (\<Union>x\<in>C. A - B x)    = (A - (\<Inter>x\<in>C. B x))"
    1.47 -  "\<And>A B. (UN x: \<Union>A. B x) = (UN y:A. UN x:y. B x)"
    1.48 -  "\<And>A B C. (UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)"
    1.49 -  "\<And>A B f. (UN x:f`A. B x)     = (UN a:A. B (f a))"
    1.50 +  "\<And>A B. (UN x: \<Union>A. B x) = (\<Union>y\<in>A. UN x:y. B x)"
    1.51 +  "\<And>A B C. (UN z: UNION A B. C z) = (\<Union>x\<in>A. UN z: B(x). C z)"
    1.52 +  "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
    1.53    by auto
    1.54  
    1.55  lemma INT_simps [simp]:
    1.56 -  "\<And>A B C. (\<Inter>x\<in>C. A x Int B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) Int B)"
    1.57 -  "\<And>A B C. (\<Inter>x\<in>C. A Int B x) = (if C={} then UNIV else A Int (\<Inter>x\<in>C. B x))"
    1.58 +  "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter>B)"
    1.59 +  "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
    1.60    "\<And>A B C. (\<Inter>x\<in>C. A x - B)   = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
    1.61    "\<And>A B C. (\<Inter>x\<in>C. A - B x)   = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
    1.62    "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
    1.63 -  "\<And>A B C. (\<Inter>x\<in>C. A x Un B)  = ((\<Inter>x\<in>C. A x) Un B)"
    1.64 -  "\<And>A B C. (\<Inter>x\<in>C. A Un B x)  = (A Un (\<Inter>x\<in>C. B x))"
    1.65 +  "\<And>A B C. (\<Inter>x\<in>C. A x \<union>  B)  = ((\<Inter>x\<in>C. A x) \<union>  B)"
    1.66 +  "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x)  = (A \<union>  (\<Inter>x\<in>C. B x))"
    1.67    "\<And>A B. (INT x: \<Union>A. B x) = (\<Inter>y\<in>A. INT x:y. B x)"
    1.68    "\<And>A B C. (INT z: UNION A B. C z) = (\<Inter>x\<in>A. INT z: B(x). C z)"
    1.69    "\<And>A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
    1.70 @@ -867,13 +867,13 @@
    1.71    "\<And>A P Q. (\<forall>x\<in>A. P | Q x) = (P | (\<forall>x\<in>A. Q x))"
    1.72    "\<And>A P Q. (\<forall>x\<in>A. P --> Q x) = (P --> (\<forall>x\<in>A. Q x))"
    1.73    "\<And>A P Q. (\<forall>x\<in>A. P x --> Q) = ((\<exists>x\<in>A. P x) --> Q)"
    1.74 -  "\<And>P. (ALL x:{}. P x) = True"
    1.75 -  "\<And>P. (ALL x:UNIV. P x) = (ALL x. P x)"
    1.76 -  "\<And>a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"
    1.77 -  "\<And>A P. (ALL x:\<Union>A. P x) = (ALL y:A. ALL x:y. P x)"
    1.78 -  "\<And>A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"
    1.79 -  "\<And>P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"
    1.80 -  "\<And>A P f. (ALL x:f`A. P x) = (\<forall>x\<in>A. P (f x))"
    1.81 +  "\<And>P. (\<forall> x\<in>{}. P x) = True"
    1.82 +  "\<And>P. (\<forall> x\<in>UNIV. P x) = (ALL x. P x)"
    1.83 +  "\<And>a B P. (\<forall> x\<in>insert a B. P x) = (P a & (\<forall> x\<in>B. P x))"
    1.84 +  "\<And>A P. (\<forall> x\<in>\<Union>A. P x) = (\<forall>y\<in>A. \<forall> x\<in>y. P x)"
    1.85 +  "\<And>A B P. (\<forall> x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall> x\<in> B a. P x)"
    1.86 +  "\<And>P Q. (\<forall> x\<in>Collect Q. P x) = (ALL x. Q x --> P x)"
    1.87 +  "\<And>A P f. (\<forall> x\<in>f`A. P x) = (\<forall>x\<in>A. P (f x))"
    1.88    "\<And>A P. (~(\<forall>x\<in>A. P x)) = (\<exists>x\<in>A. ~P x)"
    1.89    by auto
    1.90  
    1.91 @@ -894,25 +894,25 @@
    1.92  
    1.93  lemma UN_extend_simps:
    1.94    "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
    1.95 -  "\<And>A B C. (\<Union>x\<in>C. A x) Un B    = (if C={} then B else (\<Union>x\<in>C. A x Un B))"
    1.96 -  "\<And>A B C. A Un (\<Union>x\<in>C. B x)   = (if C={} then A else (\<Union>x\<in>C. A Un B x))"
    1.97 -  "\<And>A B C. ((\<Union>x\<in>C. A x) Int B) = (\<Union>x\<in>C. A x Int B)"
    1.98 -  "\<And>A B C. (A Int (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A Int B x)"
    1.99 +  "\<And>A B C. (\<Union>x\<in>C. A x) \<union>  B    = (if C={} then B else (\<Union>x\<in>C. A x \<union>  B))"
   1.100 +  "\<And>A B C. A \<union>  (\<Union>x\<in>C. B x)   = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
   1.101 +  "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter>B) = (\<Union>x\<in>C. A x \<inter> B)"
   1.102 +  "\<And>A B C. (A \<inter>(\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
   1.103    "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
   1.104    "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
   1.105 -  "\<And>A B. (UN y:A. UN x:y. B x) = (UN x: \<Union>A. B x)"
   1.106 -  "\<And>A B C. (UN  x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
   1.107 -  "\<And>A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)"
   1.108 +  "\<And>A B. (\<Union>y\<in>A. UN x:y. B x) = (UN x: \<Union>A. B x)"
   1.109 +  "\<And>A B C. (\<Union>x\<in>A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
   1.110 +  "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
   1.111    by auto
   1.112  
   1.113  lemma INT_extend_simps:
   1.114 -  "\<And>A B C. (\<Inter>x\<in>C. A x) Int B = (if C={} then B else (\<Inter>x\<in>C. A x Int B))"
   1.115 -  "\<And>A B C. A Int (\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A Int B x))"
   1.116 -  "\<And>A B C. (\<Inter>x\<in>C. A x) - B   = (if C={} then UNIV-B else (\<Inter>x\<in>C. A x - B))"
   1.117 +  "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter>B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
   1.118 +  "\<And>A B C. A \<inter>(\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
   1.119 +  "\<And>A B C. (\<Inter>x\<in>C. A x) - B   = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
   1.120    "\<And>A B C. A - (\<Union>x\<in>C. B x)   = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
   1.121    "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
   1.122 -  "\<And>A B C. ((\<Inter>x\<in>C. A x) Un B)  = (\<Inter>x\<in>C. A x Un B)"
   1.123 -  "\<And>A B C. A Un (\<Inter>x\<in>C. B x)  = (\<Inter>x\<in>C. A Un B x)"
   1.124 +  "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union>  B)  = (\<Inter>x\<in>C. A x \<union>  B)"
   1.125 +  "\<And>A B C. A \<union>  (\<Inter>x\<in>C. B x)  = (\<Inter>x\<in>C. A \<union> B x)"
   1.126    "\<And>A B. (\<Inter>y\<in>A. INT x:y. B x) = (INT x: \<Union>A. B x)"
   1.127    "\<And>A B C. (\<Inter>x\<in>A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
   1.128    "\<And>A B f. (INT a:A. B (f a))    = (INT x:f`A. B x)"