src/HOL/Set.thy
changeset 41082 9ff94e7cc3b3
parent 41076 a7fba340058c
child 41107 8795cd75965e
     1.1 --- a/src/HOL/Set.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Dec 08 15:05:46 2010 +0100
     1.3 @@ -533,6 +533,36 @@
     1.4    by simp
     1.5  
     1.6  
     1.7 +subsubsection {* The empty set *}
     1.8 +
     1.9 +lemma empty_def:
    1.10 +  "{} = {x. False}"
    1.11 +  by (simp add: bot_fun_def bot_bool_def Collect_def)
    1.12 +
    1.13 +lemma empty_iff [simp]: "(c : {}) = False"
    1.14 +  by (simp add: empty_def)
    1.15 +
    1.16 +lemma emptyE [elim!]: "a : {} ==> P"
    1.17 +  by simp
    1.18 +
    1.19 +lemma empty_subsetI [iff]: "{} \<subseteq> A"
    1.20 +    -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
    1.21 +  by blast
    1.22 +
    1.23 +lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
    1.24 +  by blast
    1.25 +
    1.26 +lemma equals0D: "A = {} ==> a \<notin> A"
    1.27 +    -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
    1.28 +  by blast
    1.29 +
    1.30 +lemma ball_empty [simp]: "Ball {} P = True"
    1.31 +  by (simp add: Ball_def)
    1.32 +
    1.33 +lemma bex_empty [simp]: "Bex {} P = False"
    1.34 +  by (simp add: Bex_def)
    1.35 +
    1.36 +
    1.37  subsubsection {* The universal set -- UNIV *}
    1.38  
    1.39  abbreviation UNIV :: "'a set" where
    1.40 @@ -568,36 +598,6 @@
    1.41  lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
    1.42    by auto
    1.43  
    1.44 -
    1.45 -subsubsection {* The empty set *}
    1.46 -
    1.47 -lemma empty_def:
    1.48 -  "{} = {x. False}"
    1.49 -  by (simp add: bot_fun_def bot_bool_def Collect_def)
    1.50 -
    1.51 -lemma empty_iff [simp]: "(c : {}) = False"
    1.52 -  by (simp add: empty_def)
    1.53 -
    1.54 -lemma emptyE [elim!]: "a : {} ==> P"
    1.55 -  by simp
    1.56 -
    1.57 -lemma empty_subsetI [iff]: "{} \<subseteq> A"
    1.58 -    -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
    1.59 -  by blast
    1.60 -
    1.61 -lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
    1.62 -  by blast
    1.63 -
    1.64 -lemma equals0D: "A = {} ==> a \<notin> A"
    1.65 -    -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
    1.66 -  by blast
    1.67 -
    1.68 -lemma ball_empty [simp]: "Ball {} P = True"
    1.69 -  by (simp add: Ball_def)
    1.70 -
    1.71 -lemma bex_empty [simp]: "Bex {} P = False"
    1.72 -  by (simp add: Bex_def)
    1.73 -
    1.74  lemma UNIV_not_empty [iff]: "UNIV ~= {}"
    1.75    by (blast elim: equalityE)
    1.76  
    1.77 @@ -647,7 +647,41 @@
    1.78  lemma Compl_eq: "- A = {x. ~ x : A}" by blast
    1.79  
    1.80  
    1.81 -subsubsection {* Binary union -- Un *}
    1.82 +subsubsection {* Binary intersection *}
    1.83 +
    1.84 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.85 +  "op Int \<equiv> inf"
    1.86 +
    1.87 +notation (xsymbols)
    1.88 +  inter  (infixl "\<inter>" 70)
    1.89 +
    1.90 +notation (HTML output)
    1.91 +  inter  (infixl "\<inter>" 70)
    1.92 +
    1.93 +lemma Int_def:
    1.94 +  "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    1.95 +  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
    1.96 +
    1.97 +lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    1.98 +  by (unfold Int_def) blast
    1.99 +
   1.100 +lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
   1.101 +  by simp
   1.102 +
   1.103 +lemma IntD1: "c : A Int B ==> c:A"
   1.104 +  by simp
   1.105 +
   1.106 +lemma IntD2: "c : A Int B ==> c:B"
   1.107 +  by simp
   1.108 +
   1.109 +lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
   1.110 +  by simp
   1.111 +
   1.112 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   1.113 +  by (fact mono_inf)
   1.114 +
   1.115 +
   1.116 +subsubsection {* Binary union *}
   1.117  
   1.118  abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   1.119    "union \<equiv> sup"
   1.120 @@ -689,40 +723,6 @@
   1.121    by (fact mono_sup)
   1.122  
   1.123  
   1.124 -subsubsection {* Binary intersection -- Int *}
   1.125 -
   1.126 -abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   1.127 -  "op Int \<equiv> inf"
   1.128 -
   1.129 -notation (xsymbols)
   1.130 -  inter  (infixl "\<inter>" 70)
   1.131 -
   1.132 -notation (HTML output)
   1.133 -  inter  (infixl "\<inter>" 70)
   1.134 -
   1.135 -lemma Int_def:
   1.136 -  "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   1.137 -  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
   1.138 -
   1.139 -lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   1.140 -  by (unfold Int_def) blast
   1.141 -
   1.142 -lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
   1.143 -  by simp
   1.144 -
   1.145 -lemma IntD1: "c : A Int B ==> c:A"
   1.146 -  by simp
   1.147 -
   1.148 -lemma IntD2: "c : A Int B ==> c:B"
   1.149 -  by simp
   1.150 -
   1.151 -lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
   1.152 -  by simp
   1.153 -
   1.154 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   1.155 -  by (fact mono_inf)
   1.156 -
   1.157 -
   1.158  subsubsection {* Set difference *}
   1.159  
   1.160  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"