# HG changeset patch
# User haftmann
# Date 1277996082 -7200
# Node ID c5a8b612e5710c0c31670e380890bb4f2f1bea7e
# Parent  f433cb9caea45e14ff72664000c598019e248d09
qualified constants Set.member and Set.Collect

diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 01 16:54:42 2010 +0200
@@ -3302,7 +3302,7 @@
   fun reorder_bounds_tac prems i =
     let
       fun variable_of_bound (Const ("Trueprop", _) $
-                             (Const (@{const_name "op :"}, _) $
+                             (Const (@{const_name Set.member}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound (Const ("Trueprop", _) $
                              (Const ("op =", _) $
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -21,7 +21,7 @@
   | abs2list _ = [];
 
 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
-fun mk_vars (Const ("Collect",_) $ T) = abs2list T
+fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
   | mk_vars _ = [];
 
 (** abstraction of body over a tuple formed from a list of free variables.
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -2088,7 +2088,7 @@
             val (HOLThm(rens,td_th)) = norm_hthm thy hth
             val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
             val c = case concl_of th2 of
-                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
+                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
@@ -2118,7 +2118,7 @@
                           let
                               val PT = domain_type exT
                           in
-                              Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
+                              Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P
                           end
                         | _ => error "Internal error in ProofKernel.new_typedefinition"
             val tnames_string = if null tnames
@@ -2164,7 +2164,7 @@
                                     SOME (cterm_of thy t)] light_nonempty
             val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
             val c = case concl_of th2 of
-                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
+                        _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
             val tfrees = OldTerm.term_tfrees c
             val tnames = sort_strings (map fst tfrees)
@@ -2202,7 +2202,7 @@
                 let
                     val PT = type_of P'
                 in
-                    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
+                    Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P'
                 end
 
             val tnames_string = if null tnames
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -121,7 +121,7 @@
 
 val dj_cp = thm "dj_cp";
 
-fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
+fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
       Type ("fun", [_, U])])) = (T, U);
 
 fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
@@ -617,7 +617,7 @@
       |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
           Typedef.add_typedef_global false (SOME (Binding.name name'))
             (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
-            (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
+            (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
@@ -8,42 +8,36 @@
 
 subsection {* Sets as predicates *}
 
-global
-
-types 'a set = "'a => bool"
+types 'a set = "'a \<Rightarrow> bool"
 
-consts
-  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
-  "op :"        :: "'a => 'a set => bool"                -- "membership"
+definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
+  "Collect P = P"
 
-local
+definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
+  mem_def: "member x A = A x"
 
 notation
-  "op :"  ("op :") and
-  "op :"  ("(_/ : _)" [50, 51] 50)
+  member  ("op :") and
+  member  ("(_/ : _)" [50, 51] 50)
 
-defs
-  mem_def [code]: "x : S == S x"
-  Collect_def [code]: "Collect P == P"
-
-abbreviation
-  "not_mem x A == ~ (x : A)" -- "non-membership"
+abbreviation not_member where
+  "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
 
 notation
-  not_mem  ("op ~:") and
-  not_mem  ("(_/ ~: _)" [50, 51] 50)
+  not_member  ("op ~:") and
+  not_member  ("(_/ ~: _)" [50, 51] 50)
 
 notation (xsymbols)
-  "op :"  ("op \<in>") and
-  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
-  not_mem  ("op \<notin>") and
-  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
+  member      ("op \<in>") and
+  member      ("(_/ \<in> _)" [50, 51] 50) and
+  not_member  ("op \<notin>") and
+  not_member  ("(_/ \<notin> _)" [50, 51] 50)
 
 notation (HTML output)
-  "op :"  ("op \<in>") and
-  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
-  not_mem  ("op \<notin>") and
-  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
+  member      ("op \<in>") and
+  member      ("(_/ \<in> _)" [50, 51] 50) and
+  not_member  ("op \<notin>") and
+  not_member  ("(_/ \<notin> _)" [50, 51] 50)
 
 text {* Set comprehensions *}
 
@@ -312,7 +306,7 @@
         in
           case t of
             Const (@{const_syntax "op &"}, _) $
-              (Const (@{const_syntax "op :"}, _) $
+              (Const (@{const_syntax Set.member}, _) $
                 (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
             if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
           | _ => M
@@ -922,7 +916,7 @@
 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
 
 (*Would like to add these, but the existing code only searches for the
-  outer-level constant, which in this case is just "op :"; we instead need
+  outer-level constant, which in this case is just Set.member; we instead need
   to use term-nets to associate patterns with rules.  Also, if a rule fails to
   apply, then the formula should be kept.
   [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
@@ -1691,6 +1685,7 @@
 lemma vimage_code [code]: "(f -` A) x = A (f x)"
   by (simp add: vimage_def Collect_def mem_def)
 
+hide_const (open) member
 
 text {* Misc theorem and ML bindings *}
 
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -220,7 +220,7 @@
     val ihyp = Term.all T $ Abs ("z", T,
       Logic.mk_implies
         (HOLogic.mk_Trueprop (
-          Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
+          Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
           $ (HOLogic.pair_const T T $ Bound 0 $ x)
           $ R),
          HOLogic.mk_Trueprop (P_comp $ Bound 0)))
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -54,15 +54,15 @@
 fun negF AbsF = RepF
   | negF RepF = AbsF
 
-fun is_identity (Const (@{const_name "id"}, _)) = true
+fun is_identity (Const (@{const_name id}, _)) = true
   | is_identity _ = false
 
-fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+fun mk_identity ty = Const (@{const_name id}, ty --> ty)
 
 fun mk_fun_compose flag (trm1, trm2) =
   case flag of
-    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
-  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+    AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
+  | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
 let
@@ -450,7 +450,7 @@
          if ty = ty' then subtrm
          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
        end
-  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
+  | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
        let
          val subtrm = regularize_trm ctxt (t, t')
          val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
@@ -460,26 +460,26 @@
          else mk_babs $ resrel $ subtrm
        end
 
-  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+  | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
-         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
+         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+  | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
-         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
+         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
-      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
-        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
-     Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
+      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+        (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
+     Const (@{const_name Ex1}, ty') $ t') =>
        let
          val t_ = incr_boundvars (~1) t
          val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -579,7 +579,7 @@
       fun get_nparms s = if member (op =) names s then SOME nparms else
         Option.map #3 (get_clauses thy s);
 
-      fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
+      fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
             Prem ([t], Envir.beta_eta_contract u, true)
         | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
             Prem ([t, u], eq, false)
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -36,7 +36,7 @@
     fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
          let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
-           (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
+           (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
              (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
@@ -84,10 +84,10 @@
         in HOLogic.Collect_const U $
           HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
         end;
-      fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
+      fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
             Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
               mkop s T (m, p, S, mk_collect p T (head_of u))
-        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
+        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member},
             Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
               mkop s T (m, p, mk_collect p T (head_of u), S)
         | decomp _ = NONE;
@@ -271,7 +271,7 @@
            let
              val thy = Context.theory_of ctxt;
              fun factors_of t fs = case strip_abs_body t of
-                 Const (@{const_name "op :"}, _) $ u $ S =>
+                 Const (@{const_name Set.member}, _) $ u $ S =>
                    if is_Free S orelse is_Var S then
                      let val ps = HOLogic.flat_tuple_paths u
                      in (SOME ps, (S, ps) :: fs) end
@@ -281,7 +281,7 @@
              val (pfs, fs) = fold_map factors_of ts [];
              val ((h', ts'), fs') = (case rhs of
                  Abs _ => (case strip_abs_body rhs of
-                     Const (@{const_name "op :"}, _) $ u $ S =>
+                     Const (@{const_name Set.member}, _) $ u $ S =>
                        (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
                    | _ => error "member symbol on right-hand side expected")
                | _ => (strip_comb rhs, NONE))
@@ -414,7 +414,7 @@
     val {set_arities, pred_arities, to_pred_simps, ...} =
       PredSetConvData.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
-      | infer (Const (@{const_name "op :"}, _) $ t $ u) =
+      | infer (Const (@{const_name Set.member}, _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
@@ -653,7 +653,7 @@
       | Const (@{const_name "op -->"}, _) => t
       (* sets *)
       | Const (@{const_name Collect}, _) => t
-      | Const (@{const_name "op :"}, _) => t
+      | Const (@{const_name Set.member}, _) => t
       (* other optimizations *)
       | Const (@{const_name Finite_Set.card}, _) => t
       | Const (@{const_name Finite_Set.finite}, _) => t
@@ -829,7 +829,7 @@
       | Const (@{const_name "op -->"}, _) => axs
       (* sets *)
       | Const (@{const_name Collect}, T) => collect_type_axioms T axs
-      | Const (@{const_name "op :"}, T) => collect_type_axioms T axs
+      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
       (* other optimizations *)
       | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
       | Const (@{const_name Finite_Set.finite}, T) =>
@@ -2634,11 +2634,11 @@
       | Const (@{const_name Collect}, _) =>
         SOME (interpret thy model args (eta_expand t 1))
       (* 'op :' == application *)
-      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
+      | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
         SOME (interpret thy model args (t2 $ t1))
-      | Const (@{const_name "op :"}, _) $ t1 =>
+      | Const (@{const_name Set.member}, _) $ t1 =>
         SOME (interpret thy model args (eta_expand t 1))
-      | Const (@{const_name "op :"}, _) =>
+      | Const (@{const_name Set.member}, _) =>
         SOME (interpret thy model args (eta_expand t 2))
       | _ => NONE)
   end;
@@ -3050,7 +3050,7 @@
 
   fun Product_Type_fst_interpreter thy model args t =
     case t of
-      Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
+      Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
       let
         val constants_T = make_constants thy model T
         val size_U      = size_of_type thy model U
@@ -3069,7 +3069,7 @@
 
   fun Product_Type_snd_interpreter thy model args t =
     case t of
-      Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
+      Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
       let
         val size_T      = size_of_type thy model T
         val constants_U = make_constants thy model U
diff -r f433cb9caea4 -r c5a8b612e571 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Jul 01 16:54:42 2010 +0200
@@ -858,7 +858,7 @@
   val rtrancl_trans = @{thm rtrancl_trans};
 
   fun decomp (@{const Trueprop} $ t) =
-    let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
+    let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
         let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
               | decr r = (r,"r");