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
```