1.1 --- a/src/HOL/Decision_Procs/Approximation.thy Thu Jul 01 16:54:42 2010 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jul 01 16:54:42 2010 +0200
1.3 @@ -3302,7 +3302,7 @@
1.4 fun reorder_bounds_tac prems i =
1.5 let
1.6 fun variable_of_bound (Const ("Trueprop", _) $
1.7 - (Const (@{const_name "op :"}, _) $
1.8 + (Const (@{const_name Set.member}, _) $
1.9 Free (name, _) $ _)) = name
1.10 | variable_of_bound (Const ("Trueprop", _) $
1.11 (Const ("op =", _) $
2.1 --- a/src/HOL/Hoare/hoare_tac.ML Thu Jul 01 16:54:42 2010 +0200
2.2 +++ b/src/HOL/Hoare/hoare_tac.ML Thu Jul 01 16:54:42 2010 +0200
2.3 @@ -21,7 +21,7 @@
2.4 | abs2list _ = [];
2.5
2.6 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
2.7 -fun mk_vars (Const ("Collect",_) $ T) = abs2list T
2.8 +fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
2.9 | mk_vars _ = [];
2.10
2.11 (** abstraction of body over a tuple formed from a list of free variables.
3.1 --- a/src/HOL/Import/proof_kernel.ML Thu Jul 01 16:54:42 2010 +0200
3.2 +++ b/src/HOL/Import/proof_kernel.ML Thu Jul 01 16:54:42 2010 +0200
3.3 @@ -2088,7 +2088,7 @@
3.4 val (HOLThm(rens,td_th)) = norm_hthm thy hth
3.5 val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
3.6 val c = case concl_of th2 of
3.7 - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
3.8 + _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
3.9 | _ => raise ERR "new_type_definition" "Bad type definition theorem"
3.10 val tfrees = OldTerm.term_tfrees c
3.11 val tnames = map fst tfrees
3.12 @@ -2118,7 +2118,7 @@
3.13 let
3.14 val PT = domain_type exT
3.15 in
3.16 - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
3.17 + Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P
3.18 end
3.19 | _ => error "Internal error in ProofKernel.new_typedefinition"
3.20 val tnames_string = if null tnames
3.21 @@ -2164,7 +2164,7 @@
3.22 SOME (cterm_of thy t)] light_nonempty
3.23 val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
3.24 val c = case concl_of th2 of
3.25 - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
3.26 + _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
3.27 | _ => raise ERR "type_introduction" "Bad type definition theorem"
3.28 val tfrees = OldTerm.term_tfrees c
3.29 val tnames = sort_strings (map fst tfrees)
3.30 @@ -2202,7 +2202,7 @@
3.31 let
3.32 val PT = type_of P'
3.33 in
3.34 - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
3.35 + Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P'
3.36 end
3.37
3.38 val tnames_string = if null tnames
4.1 --- a/src/HOL/Nominal/nominal_datatype.ML Thu Jul 01 16:54:42 2010 +0200
4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jul 01 16:54:42 2010 +0200
4.3 @@ -121,7 +121,7 @@
4.4
4.5 val dj_cp = thm "dj_cp";
4.6
4.7 -fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
4.8 +fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
4.9 Type ("fun", [_, U])])) = (T, U);
4.10
4.11 fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
4.12 @@ -617,7 +617,7 @@
4.13 |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
4.14 Typedef.add_typedef_global false (SOME (Binding.name name'))
4.15 (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
4.16 - (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
4.17 + (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
4.18 Const (cname, U --> HOLogic.boolT)) NONE
4.19 (rtac exI 1 THEN rtac CollectI 1 THEN
4.20 QUIET_BREADTH_FIRST (has_fewer_prems 1)
5.1 --- a/src/HOL/Set.thy Thu Jul 01 16:54:42 2010 +0200
5.2 +++ b/src/HOL/Set.thy Thu Jul 01 16:54:42 2010 +0200
5.3 @@ -8,42 +8,36 @@
5.4
5.5 subsection {* Sets as predicates *}
5.6
5.7 -global
5.8 +types 'a set = "'a \<Rightarrow> bool"
5.9
5.10 -types 'a set = "'a => bool"
5.11 +definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
5.12 + "Collect P = P"
5.13
5.14 -consts
5.15 - Collect :: "('a => bool) => 'a set" -- "comprehension"
5.16 - "op :" :: "'a => 'a set => bool" -- "membership"
5.17 -
5.18 -local
5.19 +definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
5.20 + mem_def: "member x A = A x"
5.21
5.22 notation
5.23 - "op :" ("op :") and
5.24 - "op :" ("(_/ : _)" [50, 51] 50)
5.25 + member ("op :") and
5.26 + member ("(_/ : _)" [50, 51] 50)
5.27
5.28 -defs
5.29 - mem_def [code]: "x : S == S x"
5.30 - Collect_def [code]: "Collect P == P"
5.31 -
5.32 -abbreviation
5.33 - "not_mem x A == ~ (x : A)" -- "non-membership"
5.34 +abbreviation not_member where
5.35 + "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
5.36
5.37 notation
5.38 - not_mem ("op ~:") and
5.39 - not_mem ("(_/ ~: _)" [50, 51] 50)
5.40 + not_member ("op ~:") and
5.41 + not_member ("(_/ ~: _)" [50, 51] 50)
5.42
5.43 notation (xsymbols)
5.44 - "op :" ("op \<in>") and
5.45 - "op :" ("(_/ \<in> _)" [50, 51] 50) and
5.46 - not_mem ("op \<notin>") and
5.47 - not_mem ("(_/ \<notin> _)" [50, 51] 50)
5.48 + member ("op \<in>") and
5.49 + member ("(_/ \<in> _)" [50, 51] 50) and
5.50 + not_member ("op \<notin>") and
5.51 + not_member ("(_/ \<notin> _)" [50, 51] 50)
5.52
5.53 notation (HTML output)
5.54 - "op :" ("op \<in>") and
5.55 - "op :" ("(_/ \<in> _)" [50, 51] 50) and
5.56 - not_mem ("op \<notin>") and
5.57 - not_mem ("(_/ \<notin> _)" [50, 51] 50)
5.58 + member ("op \<in>") and
5.59 + member ("(_/ \<in> _)" [50, 51] 50) and
5.60 + not_member ("op \<notin>") and
5.61 + not_member ("(_/ \<notin> _)" [50, 51] 50)
5.62
5.63 text {* Set comprehensions *}
5.64
5.65 @@ -312,7 +306,7 @@
5.66 in
5.67 case t of
5.68 Const (@{const_syntax "op &"}, _) $
5.69 - (Const (@{const_syntax "op :"}, _) $
5.70 + (Const (@{const_syntax Set.member}, _) $
5.71 (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
5.72 if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
5.73 | _ => M
5.74 @@ -922,7 +916,7 @@
5.75 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
5.76
5.77 (*Would like to add these, but the existing code only searches for the
5.78 - outer-level constant, which in this case is just "op :"; we instead need
5.79 + outer-level constant, which in this case is just Set.member; we instead need
5.80 to use term-nets to associate patterns with rules. Also, if a rule fails to
5.81 apply, then the formula should be kept.
5.82 [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
5.83 @@ -1691,6 +1685,7 @@
5.84 lemma vimage_code [code]: "(f -` A) x = A (f x)"
5.85 by (simp add: vimage_def Collect_def mem_def)
5.86
5.87 +hide_const (open) member
5.88
5.89 text {* Misc theorem and ML bindings *}
5.90
6.1 --- a/src/HOL/Tools/Function/induction_schema.ML Thu Jul 01 16:54:42 2010 +0200
6.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Thu Jul 01 16:54:42 2010 +0200
6.3 @@ -220,7 +220,7 @@
6.4 val ihyp = Term.all T $ Abs ("z", T,
6.5 Logic.mk_implies
6.6 (HOLogic.mk_Trueprop (
6.7 - Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
6.8 + Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
6.9 $ (HOLogic.pair_const T T $ Bound 0 $ x)
6.10 $ R),
6.11 HOLogic.mk_Trueprop (P_comp $ Bound 0)))
7.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jul 01 16:54:42 2010 +0200
7.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jul 01 16:54:42 2010 +0200
7.3 @@ -54,15 +54,15 @@
7.4 fun negF AbsF = RepF
7.5 | negF RepF = AbsF
7.6
7.7 -fun is_identity (Const (@{const_name "id"}, _)) = true
7.8 +fun is_identity (Const (@{const_name id}, _)) = true
7.9 | is_identity _ = false
7.10
7.11 -fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
7.12 +fun mk_identity ty = Const (@{const_name id}, ty --> ty)
7.13
7.14 fun mk_fun_compose flag (trm1, trm2) =
7.15 case flag of
7.16 - AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
7.17 - | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
7.18 + AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
7.19 + | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
7.20
7.21 fun get_mapfun ctxt s =
7.22 let
7.23 @@ -450,7 +450,7 @@
7.24 if ty = ty' then subtrm
7.25 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
7.26 end
7.27 - | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
7.28 + | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
7.29 let
7.30 val subtrm = regularize_trm ctxt (t, t')
7.31 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
7.32 @@ -460,26 +460,26 @@
7.33 else mk_babs $ resrel $ subtrm
7.34 end
7.35
7.36 - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
7.37 + | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
7.38 let
7.39 val subtrm = apply_subt (regularize_trm ctxt) (t, t')
7.40 in
7.41 - if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
7.42 + if ty = ty' then Const (@{const_name All}, ty) $ subtrm
7.43 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
7.44 end
7.45
7.46 - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
7.47 + | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
7.48 let
7.49 val subtrm = apply_subt (regularize_trm ctxt) (t, t')
7.50 in
7.51 - if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
7.52 + if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
7.53 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
7.54 end
7.55
7.56 - | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
7.57 - (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
7.58 - (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
7.59 - Const (@{const_name "Ex1"}, ty') $ t') =>
7.60 + | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
7.61 + (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
7.62 + (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
7.63 + Const (@{const_name Ex1}, ty') $ t') =>
7.64 let
7.65 val t_ = incr_boundvars (~1) t
7.66 val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
8.1 --- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 01 16:54:42 2010 +0200
8.2 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jul 01 16:54:42 2010 +0200
8.3 @@ -579,7 +579,7 @@
8.4 fun get_nparms s = if member (op =) names s then SOME nparms else
8.5 Option.map #3 (get_clauses thy s);
8.6
8.7 - fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
8.8 + fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
8.9 Prem ([t], Envir.beta_eta_contract u, true)
8.10 | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
8.11 Prem ([t, u], eq, false)
9.1 --- a/src/HOL/Tools/inductive_set.ML Thu Jul 01 16:54:42 2010 +0200
9.2 +++ b/src/HOL/Tools/inductive_set.ML Thu Jul 01 16:54:42 2010 +0200
9.3 @@ -36,7 +36,7 @@
9.4 fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
9.5 let val (u, _, ps) = HOLogic.strip_psplits t
9.6 in case u of
9.7 - (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
9.8 + (c as Const (@{const_name Set.member}, _)) $ q $ S' =>
9.9 (case try (HOLogic.strip_ptuple ps) q of
9.10 NONE => NONE
9.11 | SOME ts =>
9.12 @@ -84,10 +84,10 @@
9.13 in HOLogic.Collect_const U $
9.14 HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
9.15 end;
9.16 - fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
9.17 + fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
9.18 Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
9.19 mkop s T (m, p, S, mk_collect p T (head_of u))
9.20 - | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
9.21 + | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member},
9.22 Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
9.23 mkop s T (m, p, mk_collect p T (head_of u), S)
9.24 | decomp _ = NONE;
9.25 @@ -271,7 +271,7 @@
9.26 let
9.27 val thy = Context.theory_of ctxt;
9.28 fun factors_of t fs = case strip_abs_body t of
9.29 - Const (@{const_name "op :"}, _) $ u $ S =>
9.30 + Const (@{const_name Set.member}, _) $ u $ S =>
9.31 if is_Free S orelse is_Var S then
9.32 let val ps = HOLogic.flat_tuple_paths u
9.33 in (SOME ps, (S, ps) :: fs) end
9.34 @@ -281,7 +281,7 @@
9.35 val (pfs, fs) = fold_map factors_of ts [];
9.36 val ((h', ts'), fs') = (case rhs of
9.37 Abs _ => (case strip_abs_body rhs of
9.38 - Const (@{const_name "op :"}, _) $ u $ S =>
9.39 + Const (@{const_name Set.member}, _) $ u $ S =>
9.40 (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
9.41 | _ => error "member symbol on right-hand side expected")
9.42 | _ => (strip_comb rhs, NONE))
9.43 @@ -414,7 +414,7 @@
9.44 val {set_arities, pred_arities, to_pred_simps, ...} =
9.45 PredSetConvData.get (Context.Proof lthy);
9.46 fun infer (Abs (_, _, t)) = infer t
9.47 - | infer (Const (@{const_name "op :"}, _) $ t $ u) =
9.48 + | infer (Const (@{const_name Set.member}, _) $ t $ u) =
9.49 infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
9.50 | infer (t $ u) = infer t #> infer u
9.51 | infer _ = I;
10.1 --- a/src/HOL/Tools/refute.ML Thu Jul 01 16:54:42 2010 +0200
10.2 +++ b/src/HOL/Tools/refute.ML Thu Jul 01 16:54:42 2010 +0200
10.3 @@ -653,7 +653,7 @@
10.4 | Const (@{const_name "op -->"}, _) => t
10.5 (* sets *)
10.6 | Const (@{const_name Collect}, _) => t
10.7 - | Const (@{const_name "op :"}, _) => t
10.8 + | Const (@{const_name Set.member}, _) => t
10.9 (* other optimizations *)
10.10 | Const (@{const_name Finite_Set.card}, _) => t
10.11 | Const (@{const_name Finite_Set.finite}, _) => t
10.12 @@ -829,7 +829,7 @@
10.13 | Const (@{const_name "op -->"}, _) => axs
10.14 (* sets *)
10.15 | Const (@{const_name Collect}, T) => collect_type_axioms T axs
10.16 - | Const (@{const_name "op :"}, T) => collect_type_axioms T axs
10.17 + | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
10.18 (* other optimizations *)
10.19 | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
10.20 | Const (@{const_name Finite_Set.finite}, T) =>
10.21 @@ -2634,11 +2634,11 @@
10.22 | Const (@{const_name Collect}, _) =>
10.23 SOME (interpret thy model args (eta_expand t 1))
10.24 (* 'op :' == application *)
10.25 - | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
10.26 + | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
10.27 SOME (interpret thy model args (t2 $ t1))
10.28 - | Const (@{const_name "op :"}, _) $ t1 =>
10.29 + | Const (@{const_name Set.member}, _) $ t1 =>
10.30 SOME (interpret thy model args (eta_expand t 1))
10.31 - | Const (@{const_name "op :"}, _) =>
10.32 + | Const (@{const_name Set.member}, _) =>
10.33 SOME (interpret thy model args (eta_expand t 2))
10.34 | _ => NONE)
10.35 end;
10.36 @@ -3050,7 +3050,7 @@
10.37
10.38 fun Product_Type_fst_interpreter thy model args t =
10.39 case t of
10.40 - Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
10.41 + Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
10.42 let
10.43 val constants_T = make_constants thy model T
10.44 val size_U = size_of_type thy model U
10.45 @@ -3069,7 +3069,7 @@
10.46
10.47 fun Product_Type_snd_interpreter thy model args t =
10.48 case t of
10.49 - Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
10.50 + Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
10.51 let
10.52 val size_T = size_of_type thy model T
10.53 val constants_U = make_constants thy model U
11.1 --- a/src/HOL/Transitive_Closure.thy Thu Jul 01 16:54:42 2010 +0200
11.2 +++ b/src/HOL/Transitive_Closure.thy Thu Jul 01 16:54:42 2010 +0200
11.3 @@ -858,7 +858,7 @@
11.4 val rtrancl_trans = @{thm rtrancl_trans};
11.5
11.6 fun decomp (@{const Trueprop} $ t) =
11.7 - let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
11.8 + let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
11.9 let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
11.10 | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
11.11 | decr r = (r,"r");