# HG changeset patch # User haftmann # Date 1244122139 -7200 # Node ID 55edadbd43d585951f2cd0d206c9af4906dff14e # Parent 2754a0dadccc42089948f58eadd4c97c764c1872 insert now qualified and with authentic syntax diff -r 2754a0dadccc -r 55edadbd43d5 src/HOL/Set.thy --- 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 \ {x. False}" - -definition UNIV :: "'a set" where - "UNIV \ {x. True}" - -syntax - "@Finset" :: "args => 'a set" ("{(_)}") - -translations - "{x, xs}" == "insert x {xs}" - "{x}" == "insert x {}" - definition Int :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where "A Int B \ {x. x \ A \ x \ B}" @@ -85,6 +71,22 @@ "Int" (infixl "\" 70) and "Un" (infixl "\" 65) +definition empty :: "'a set" ("{}") where + "empty \ {x. False}" + +definition insert :: "'a \ 'a set \ 'a set" where + "insert a B \ {x. x = a} \ B" + +definition UNIV :: "'a set" where + "UNIV \ {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 diff -r 2754a0dadccc -r 55edadbd43d5 src/HOL/Tools/hologic.ML --- 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);