author haftmann Thu Jun 04 15:28:59 2009 +0200 (2009-06-04) changeset 31456 55edadbd43d5 parent 31455 2754a0dadccc child 31457 d1cb222438d8
insert now qualified and with authentic syntax
 src/HOL/Set.thy file | annotate | diff | revisions src/HOL/Tools/hologic.ML file | annotate | diff | revisions
```     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
```
```     2.1 --- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
2.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
2.3 @@ -152,13 +152,13 @@
2.4    let
2.5      val sT = mk_setT T;
2.6      val empty = Const ("Set.empty", sT);
2.7 -    fun insert t u = Const ("insert", T --> sT --> sT) \$ t \$ u;
2.8 +    fun insert t u = Const ("Set.insert", T --> sT --> sT) \$ t \$ u;
2.9    in fold_rev insert ts empty end;
2.10
2.11  fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
2.12
2.13 -fun dest_set (Const ("Orderings.bot", _)) = []
2.14 -  | dest_set (Const ("insert", _) \$ t \$ u) = t :: dest_set u
2.15 +fun dest_set (Const ("Set.empty", _)) = []
2.16 +  | dest_set (Const ("Set.insert", _) \$ t \$ u) = t :: dest_set u
2.17    | dest_set t = raise TERM ("dest_set", [t]);
2.18
2.19  fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
```