--- 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 =", _) $
--- 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.
--- 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
--- 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)
--- 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 *}
--- 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)))
--- 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')
--- 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)
--- 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;
--- 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
--- 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");