src/HOL/Set.thy
changeset 28562 4e74209f113e
parent 27824 97d2a3797ce0
child 29691 9f03b5f847cd
equal deleted inserted replaced
28561:056255ade52a 28562:4e74209f113e
   322 subsection {* Rules and definitions *}
   322 subsection {* Rules and definitions *}
   323 
   323 
   324 text {* Isomorphisms between predicates and sets. *}
   324 text {* Isomorphisms between predicates and sets. *}
   325 
   325 
   326 defs
   326 defs
   327   mem_def [code func]: "x : S == S x"
   327   mem_def [code]: "x : S == S x"
   328   Collect_def [code func]: "Collect P == P"
   328   Collect_def [code]: "Collect P == P"
   329 
   329 
   330 defs
   330 defs
   331   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   331   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   332   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   332   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   333   Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
   333   Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
  2059 
  2059 
  2060 subsection {* Inverse image of a function *}
  2060 subsection {* Inverse image of a function *}
  2061 
  2061 
  2062 constdefs
  2062 constdefs
  2063   vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
  2063   vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
  2064   [code func del]: "f -` B == {x. f x : B}"
  2064   [code del]: "f -` B == {x. f x : B}"
  2065 
  2065 
  2066 
  2066 
  2067 subsubsection {* Basic rules *}
  2067 subsubsection {* Basic rules *}
  2068 
  2068 
  2069 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
  2069 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
  2154 subsection {* Getting the Contents of a Singleton Set *}
  2154 subsection {* Getting the Contents of a Singleton Set *}
  2155 
  2155 
  2156 definition
  2156 definition
  2157   contents :: "'a set \<Rightarrow> 'a"
  2157   contents :: "'a set \<Rightarrow> 'a"
  2158 where
  2158 where
  2159   [code func del]: "contents X = (THE x. X = {x})"
  2159   [code del]: "contents X = (THE x. X = {x})"
  2160 
  2160 
  2161 lemma contents_eq [simp]: "contents {x} = x"
  2161 lemma contents_eq [simp]: "contents {x} = x"
  2162   by (simp add: contents_def)
  2162   by (simp add: contents_def)
  2163 
  2163 
  2164 
  2164 
  2187   done
  2187   done
  2188 
  2188 
  2189 
  2189 
  2190 subsection {* Rudimentary code generation *}
  2190 subsection {* Rudimentary code generation *}
  2191 
  2191 
  2192 lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
  2192 lemma empty_code [code]: "{} x \<longleftrightarrow> False"
  2193   unfolding empty_def Collect_def ..
  2193   unfolding empty_def Collect_def ..
  2194 
  2194 
  2195 lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
  2195 lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
  2196   unfolding UNIV_def Collect_def ..
  2196   unfolding UNIV_def Collect_def ..
  2197 
  2197 
  2198 lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
  2198 lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
  2199   unfolding insert_def Collect_def mem_def Un_def by auto
  2199   unfolding insert_def Collect_def mem_def Un_def by auto
  2200 
  2200 
  2201 lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
  2201 lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
  2202   unfolding Int_def Collect_def mem_def ..
  2202   unfolding Int_def Collect_def mem_def ..
  2203 
  2203 
  2204 lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
  2204 lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
  2205   unfolding Un_def Collect_def mem_def ..
  2205   unfolding Un_def Collect_def mem_def ..
  2206 
  2206 
  2207 lemma vimage_code [code func]: "(f -` A) x = A (f x)"
  2207 lemma vimage_code [code]: "(f -` A) x = A (f x)"
  2208   unfolding vimage_def Collect_def mem_def ..
  2208   unfolding vimage_def Collect_def mem_def ..
  2209 
  2209 
  2210 
  2210 
  2211 
  2211 
  2212 subsection {* Basic ML bindings *}
  2212 subsection {* Basic ML bindings *}