src/HOL/Set.thy
changeset 31456 55edadbd43d5
parent 31197 c1c163ec6c44
child 31461 d54b743b52a3
     1.1 --- a/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4  consts
     1.5    Collect       :: "('a => bool) => 'a set"              -- "comprehension"
     1.6    "op :"        :: "'a => 'a set => bool"                -- "membership"
     1.7 -  insert        :: "'a => 'a set => 'a set"
     1.8    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
     1.9    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    1.10    Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
    1.11 @@ -58,19 +57,6 @@
    1.12  translations
    1.13    "{x. P}"      == "Collect (%x. P)"
    1.14  
    1.15 -definition empty :: "'a set" ("{}") where
    1.16 -  "empty \<equiv> {x. False}"
    1.17 -
    1.18 -definition UNIV :: "'a set" where
    1.19 -  "UNIV \<equiv> {x. True}"
    1.20 -
    1.21 -syntax
    1.22 -  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    1.23 -
    1.24 -translations
    1.25 -  "{x, xs}"     == "insert x {xs}"
    1.26 -  "{x}"         == "insert x {}"
    1.27 -
    1.28  definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.29    "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
    1.30  
    1.31 @@ -85,6 +71,22 @@
    1.32    "Int"  (infixl "\<inter>" 70) and
    1.33    "Un"  (infixl "\<union>" 65)
    1.34  
    1.35 +definition empty :: "'a set" ("{}") where
    1.36 +  "empty \<equiv> {x. False}"
    1.37 +
    1.38 +definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.39 +  "insert a B \<equiv> {x. x = a} \<union> B"
    1.40 +
    1.41 +definition UNIV :: "'a set" where
    1.42 +  "UNIV \<equiv> {x. True}"
    1.43 +
    1.44 +syntax
    1.45 +  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    1.46 +
    1.47 +translations
    1.48 +  "{x, xs}"     == "CONST insert x {xs}"
    1.49 +  "{x}"         == "CONST insert x {}"
    1.50 +
    1.51  syntax
    1.52    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    1.53    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
    1.54 @@ -408,7 +410,6 @@
    1.55  
    1.56  defs
    1.57    Pow_def:      "Pow A          == {B. B <= A}"
    1.58 -  insert_def:   "insert a B     == {x. x=a} Un B"
    1.59    image_def:    "f`A            == {y. EX x:A. y = f(x)}"
    1.60  
    1.61  
    1.62 @@ -811,7 +812,7 @@
    1.63  by blast
    1.64  
    1.65  
    1.66 -subsubsection {* Augmenting a set -- insert *}
    1.67 +subsubsection {* Augmenting a set -- @{const insert} *}
    1.68  
    1.69  lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
    1.70    by (unfold insert_def) blast