src/HOL/Set.thy
 changeset 37677 c5a8b612e571 parent 37387 3581483cca6c child 37767 a2b7a20d6ea3
```     1.1 --- a/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
1.2 +++ b/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
1.3 @@ -8,42 +8,36 @@
1.4
1.5  subsection {* Sets as predicates *}
1.6
1.7 -global
1.8 -
1.9 -types 'a set = "'a => bool"
1.10 +types 'a set = "'a \<Rightarrow> bool"
1.11
1.12 -consts
1.13 -  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
1.14 -  "op :"        :: "'a => 'a set => bool"                -- "membership"
1.15 +definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
1.16 +  "Collect P = P"
1.17
1.18 -local
1.19 +definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
1.20 +  mem_def: "member x A = A x"
1.21
1.22  notation
1.23 -  "op :"  ("op :") and
1.24 -  "op :"  ("(_/ : _)" [50, 51] 50)
1.25 +  member  ("op :") and
1.26 +  member  ("(_/ : _)" [50, 51] 50)
1.27
1.28 -defs
1.29 -  mem_def [code]: "x : S == S x"
1.30 -  Collect_def [code]: "Collect P == P"
1.31 -
1.32 -abbreviation
1.33 -  "not_mem x A == ~ (x : A)" -- "non-membership"
1.34 +abbreviation not_member where
1.35 +  "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
1.36
1.37  notation
1.38 -  not_mem  ("op ~:") and
1.39 -  not_mem  ("(_/ ~: _)" [50, 51] 50)
1.40 +  not_member  ("op ~:") and
1.41 +  not_member  ("(_/ ~: _)" [50, 51] 50)
1.42
1.43  notation (xsymbols)
1.44 -  "op :"  ("op \<in>") and
1.45 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
1.46 -  not_mem  ("op \<notin>") and
1.47 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
1.48 +  member      ("op \<in>") and
1.49 +  member      ("(_/ \<in> _)" [50, 51] 50) and
1.50 +  not_member  ("op \<notin>") and
1.51 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
1.52
1.53  notation (HTML output)
1.54 -  "op :"  ("op \<in>") and
1.55 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
1.56 -  not_mem  ("op \<notin>") and
1.57 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
1.58 +  member      ("op \<in>") and
1.59 +  member      ("(_/ \<in> _)" [50, 51] 50) and
1.60 +  not_member  ("op \<notin>") and
1.61 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
1.62
1.63  text {* Set comprehensions *}
1.64
1.65 @@ -312,7 +306,7 @@
1.66          in
1.67            case t of
1.68              Const (@{const_syntax "op &"}, _) \$
1.69 -              (Const (@{const_syntax "op :"}, _) \$
1.70 +              (Const (@{const_syntax Set.member}, _) \$
1.71                  (Const (@{syntax_const "_bound"}, _) \$ Free (yN, _)) \$ A) \$ P =>
1.72              if xN = yN then Syntax.const @{syntax_const "_Collect"} \$ x \$ A \$ P else M
1.73            | _ => M
1.74 @@ -922,7 +916,7 @@
1.75  lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.76
1.77  (*Would like to add these, but the existing code only searches for the
1.78 -  outer-level constant, which in this case is just "op :"; we instead need
1.79 +  outer-level constant, which in this case is just Set.member; we instead need
1.80    to use term-nets to associate patterns with rules.  Also, if a rule fails to
1.81    apply, then the formula should be kept.
1.82    [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
1.83 @@ -1691,6 +1685,7 @@
1.84  lemma vimage_code [code]: "(f -` A) x = A (f x)"
1.85    by (simp add: vimage_def Collect_def mem_def)
1.86
1.87 +hide_const (open) member
1.88
1.89  text {* Misc theorem and ML bindings *}
1.90
```