author haftmann Thu, 04 Jun 2009 15:28:59 +0200 changeset 31456 55edadbd43d5 parent 31455 2754a0dadccc child 31457 d1cb222438d8
insert now qualified and with authentic syntax
 src/HOL/Set.thy file | annotate | diff | comparison | revisions src/HOL/Tools/hologic.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
@@ -20,7 +20,6 @@
consts
Collect       :: "('a => bool) => 'a set"              -- "comprehension"
"op :"        :: "'a => 'a set => bool"                -- "membership"
-  insert        :: "'a => 'a set => 'a set"
Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
@@ -58,19 +57,6 @@
translations
"{x. P}"      == "Collect (%x. P)"

-definition empty :: "'a set" ("{}") where
-  "empty \<equiv> {x. False}"
-
-definition UNIV :: "'a set" where
-  "UNIV \<equiv> {x. True}"
-
-syntax
-  "@Finset"     :: "args => 'a set"                       ("{(_)}")
-
-translations
-  "{x, xs}"     == "insert x {xs}"
-  "{x}"         == "insert x {}"
-
definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
"A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"

@@ -85,6 +71,22 @@
"Int"  (infixl "\<inter>" 70) and
"Un"  (infixl "\<union>" 65)

+definition empty :: "'a set" ("{}") where
+  "empty \<equiv> {x. False}"
+
+definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "insert a B \<equiv> {x. x = a} \<union> B"
+
+definition UNIV :: "'a set" where
+  "UNIV \<equiv> {x. True}"
+
+syntax
+  "@Finset"     :: "args => 'a set"                       ("{(_)}")
+
+translations
+  "{x, xs}"     == "CONST insert x {xs}"
+  "{x}"         == "CONST insert x {}"
+
syntax
"_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
@@ -408,7 +410,6 @@

defs
Pow_def:      "Pow A          == {B. B <= A}"
-  insert_def:   "insert a B     == {x. x=a} Un B"
image_def:    "f`A            == {y. EX x:A. y = f(x)}"

@@ -811,7 +812,7 @@
by blast

-subsubsection {* Augmenting a set -- insert *}
+subsubsection {* Augmenting a set -- @{const insert} *}

lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
by (unfold insert_def) blast```
```--- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
@@ -152,13 +152,13 @@
let
val sT = mk_setT T;
val empty = Const ("Set.empty", sT);
-    fun insert t u = Const ("insert", T --> sT --> sT) \$ t \$ u;
+    fun insert t u = Const ("Set.insert", T --> sT --> sT) \$ t \$ u;
in fold_rev insert ts empty end;

fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);

-fun dest_set (Const ("Orderings.bot", _)) = []
-  | dest_set (Const ("insert", _) \$ t \$ u) = t :: dest_set u
+fun dest_set (Const ("Set.empty", _)) = []
+  | dest_set (Const ("Set.insert", _) \$ t \$ u) = t :: dest_set u
| dest_set t = raise TERM ("dest_set", [t]);

fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);```