--- a/src/HOL/Groups.thy Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Groups.thy Thu Feb 25 22:32:09 2010 +0100
@@ -1250,7 +1250,7 @@
val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
val dest_eqI =
- fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
+ fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
);
*}
--- a/src/HOL/HOL.thy Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/HOL.thy Thu Feb 25 22:32:09 2010 +0100
@@ -846,9 +846,12 @@
setup {*
let
(*prevent substitution on bool*)
- fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
- Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
- (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
+ fun hyp_subst_tac' i thm =
+ if i <= Thm.nprems_of thm andalso
+ Term.exists_Const
+ (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false)
+ (nth (Thm.prems_of thm) (i - 1))
+ then Hypsubst.hyp_subst_tac i thm else no_tac thm;
in
Hypsubst.hypsubst_setup
#> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
@@ -1721,8 +1724,8 @@
fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
- (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const ("op =", _), [t, u]) =>
+ (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
+ | (Const (@{const_name "op ="}, _), [t, u]) =>
let
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
@@ -1731,7 +1734,7 @@
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
- | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+ | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
@@ -2050,7 +2053,7 @@
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
local
- fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+ fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
| wrong_prem (Bound _) = true
| wrong_prem _ = false;
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
--- a/src/HOL/Orderings.thy Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Orderings.thy Thu Feb 25 22:32:09 2010 +0100
@@ -657,13 +657,14 @@
fun matches_bound v t =
(case t of
- Const ("_bound", _) $ Free (v', _) => v = v'
+ Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
| _ => false);
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
fun tr' q = (q,
- fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
+ fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
+ Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
| SOME (l, g) =>
--- a/src/HOL/Product_Type.thy Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Feb 25 22:32:09 2010 +0100
@@ -448,44 +448,44 @@
*}
ML {*
-
local
- val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
- fun Pair_pat k 0 (Bound m) = (m = k)
- | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso
- m = k+i andalso Pair_pat k (i-1) t
- | Pair_pat _ _ _ = false;
- fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
- | no_args k i (t $ u) = no_args k i t andalso no_args k i u
- | no_args k i (Bound m) = m < k orelse m > k+i
- | no_args _ _ _ = true;
- fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
- | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
- | split_pat tp i _ = NONE;
+ val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta};
+ fun Pair_pat k 0 (Bound m) = (m = k)
+ | Pair_pat k i (Const (@{const_name Pair}, _) $ Bound m $ t) =
+ i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
+ | Pair_pat _ _ _ = false;
+ fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t
+ | no_args k i (t $ u) = no_args k i t andalso no_args k i u
+ | no_args k i (Bound m) = m < k orelse m > k + i
+ | no_args _ _ _ = true;
+ fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
+ | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+ | split_pat tp i _ = NONE;
fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
(K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
- fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
- | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
- (beta_term_pat k i t andalso beta_term_pat k i u)
- | beta_term_pat k i t = no_args k i t;
- fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
- | eta_term_pat _ _ _ = false;
+ fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
+ | beta_term_pat k i (t $ u) =
+ Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u)
+ | beta_term_pat k i t = no_args k i t;
+ fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
+ | eta_term_pat _ _ _ = false;
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
- | subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
- else (subst arg k i t $ subst arg k i u)
- | subst arg k i t = t;
- fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+ | subst arg k i (t $ u) =
+ if Pair_pat k i (t $ u) then incr_boundvars k arg
+ else (subst arg k i t $ subst arg k i u)
+ | subst arg k i t = t;
+ fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
- SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f))
+ SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
| NONE => NONE)
- | beta_proc _ _ = NONE;
- fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) =
+ | beta_proc _ _ = NONE;
+ fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
- SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
+ SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
- | eta_proc _ _ = NONE;
+ | eta_proc _ _ = NONE;
in
val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
@@ -565,11 +565,11 @@
ML {*
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
+ fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
| exists_p_split (Abs (_, _, t)) = exists_p_split t
| exists_p_split _ = false;
- val ss = HOL_basic_ss addsimps [thm "split_conv"];
+ val ss = HOL_basic_ss addsimps @{thms split_conv};
in
val split_conv_tac = SUBGOAL (fn (t, i) =>
if exists_p_split t then safe_full_simp_tac ss i else no_tac);
@@ -634,10 +634,11 @@
lemma internal_split_conv: "internal_split c (a, b) = c a b"
by (simp only: internal_split_def split_conv)
+use "Tools/split_rule.ML"
+setup SplitRule.setup
+
hide const internal_split
-use "Tools/split_rule.ML"
-setup SplitRule.setup
lemmas prod_caseI = prod.cases [THEN iffD2, standard]
@@ -1049,7 +1050,6 @@
"Pair" ("(_,/ _)")
setup {*
-
let
fun strip_abs_split 0 t = ([], t)
@@ -1058,16 +1058,18 @@
val s' = Codegen.new_name t s;
val v = Free (s', T)
in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
- | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
+ | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
+ (case strip_abs_split (i+1) t of
(v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
| _ => ([], u))
| strip_abs_split i t =
strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
-fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
- (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
+fun let_codegen thy defs dep thyname brack t gr =
+ (case strip_comb t of
+ (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
let
- fun dest_let (l as Const ("Let", _) $ t $ u) =
+ fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
(case strip_abs_split 1 u of
([p], u') => apfst (cons (p, t)) (dest_let u')
| _ => ([], l))
@@ -1098,7 +1100,7 @@
| _ => NONE);
fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
- (t1 as Const ("split", _), t2 :: ts) =>
+ (t1 as Const (@{const_name split}, _), t2 :: ts) =>
let
val ([p], u) = strip_abs_split 1 (t1 $ t2);
val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Feb 25 22:32:09 2010 +0100
@@ -75,7 +75,7 @@
val leafTs' = get_nonrec_types descr' sorts;
val branchTs = get_branching_types descr' sorts;
val branchT = if null branchTs then HOLogic.unitT
- else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
+ else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs;
val arities = remove (op =) 0 (get_arities descr');
val unneeded_vars =
subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
@@ -83,7 +83,7 @@
val recTs = get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
val sumT = if null leafTs then HOLogic.unitT
- else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
+ else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs;
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
val UnivT = HOLogic.mk_setT Univ_elT;
val UnivT' = Univ_elT --> HOLogic.boolT;
@@ -104,9 +104,9 @@
val Type (_, [T1, T2]) = T
in
if i <= n2 then
- Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i)
+ Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
else
- Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+ Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
end
in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
end;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Feb 25 22:32:09 2010 +0100
@@ -53,7 +53,7 @@
fun prove_casedist_thm (i, (T, t)) =
let
val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
- Abs ("z", T', Const ("True", T''))) induct_Ps;
+ Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps;
val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
Var (("P", 0), HOLogic.boolT))
val insts = take i dummyPs @ (P::(drop (i + 1) dummyPs));
@@ -200,7 +200,7 @@
val rec_unique_thms =
let
val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
- Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
+ Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
val cert = cterm_of thy1
@@ -236,7 +236,7 @@
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path
@@ -416,7 +416,7 @@
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
val (Const ("==>", _) $ tm $ _) = t;
- val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
+ val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (concl_of nchotomy') [];
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Feb 25 22:32:09 2010 +0100
@@ -120,8 +120,8 @@
fun split_conj_thm th =
((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
-val mk_conj = foldr1 (HOLogic.mk_binop "op &");
-val mk_disj = foldr1 (HOLogic.mk_binop "op |");
+val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
+val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Feb 25 22:32:09 2010 +0100
@@ -70,7 +70,7 @@
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop "op &")
+ foldr1 (HOLogic.mk_binop @{const_name "op &"})
(map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
@@ -149,7 +149,7 @@
val prems = maps (fn ((i, (_, _, constrs)), T) =>
map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)))
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Feb 25 22:32:09 2010 +0100
@@ -16,10 +16,11 @@
open Datatype_Aux;
-fun subsets i j = if i <= j then
- let val is = subsets (i+1) j
- in map (fn ks => i::ks) is @ is end
- else [[]];
+fun subsets i j =
+ if i <= j then
+ let val is = subsets (i+1) j
+ in map (fn ks => i::ks) is @ is end
+ else [[]];
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
@@ -102,7 +103,7 @@
if i mem is then SOME
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
@@ -129,8 +130,8 @@
val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
- val ivs1 = map Var (filter_out (fn (_, T) =>
- tname_of (body_type T) mem ["set", "bool"]) ivs);
+ val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *)
+ tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
val prf =
--- a/src/HOL/Tools/inductive.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Feb 25 22:32:09 2010 +0100
@@ -183,7 +183,7 @@
in
case concl_of thm of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
- | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
+ | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
@@ -300,7 +300,7 @@
else err_in_prem ctxt err_name rule prem "Non-atomic premise";
in
(case concl of
- Const ("Trueprop", _) $ t =>
+ Const (@{const_name Trueprop}, _) $ t =>
if head_of t mem cs then
(check_ind (err_in_rule ctxt err_name rule') t;
List.app check_prem (prems ~~ aprems))
--- a/src/HOL/Tools/inductive_codegen.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Feb 25 22:32:09 2010 +0100
@@ -51,12 +51,13 @@
fun thyname_of s = (case optmod of
NONE => Codegen.thyname_of_const thy s | SOME s => s);
in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
- SOME (Const ("op =", _), [t, _]) => (case head_of t of
- Const (s, _) =>
- CodegenData.put {intros = intros, graph = graph,
- eqns = eqns |> Symtab.map_default (s, [])
- (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
- | _ => (warn thm; thy))
+ SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+ (case head_of t of
+ Const (s, _) =>
+ CodegenData.put {intros = intros, graph = graph,
+ eqns = eqns |> Symtab.map_default (s, [])
+ (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
+ | _ => (warn thm; thy))
| SOME (Const (s, _), _) =>
let
val cs = fold Term.add_const_names (Thm.prems_of thm) [];
@@ -186,7 +187,7 @@
end)) (AList.lookup op = modes name)
in (case strip_comb t of
- (Const ("op =", Type (_, [T, _])), _) =>
+ (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
[Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
(if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
| (Const (name, _), args) => the_default default (mk_modes name args)
@@ -577,17 +578,20 @@
fun get_nparms s = if s mem names then SOME nparms else
Option.map #3 (get_clauses thy s);
- fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
- | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
+ fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ 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)
| dest_prem (_ $ t) =
(case strip_comb t of
- (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
- | (c as Const (s, _), ts) => (case get_nparms s of
- NONE => Sidecond t
- | SOME k =>
- let val (ts1, ts2) = chop k ts
- in Prem (ts2, list_comb (c, ts1), false) end)
- | _ => Sidecond t);
+ (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
+ | (c as Const (s, _), ts) =>
+ (case get_nparms s of
+ NONE => Sidecond t
+ | SOME k =>
+ let val (ts1, ts2) = chop k ts
+ in Prem (ts2, list_comb (c, ts1), false) end)
+ | _ => Sidecond t);
fun add_clause intr (clauses, arities) =
let
@@ -600,7 +604,7 @@
(AList.update op = (name, these (AList.lookup op = clauses name) @
[(ts2, prems)]) clauses,
AList.update op = (name, (map (fn U => (case strip_type U of
- (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
+ (Rs as _ :: _, @{typ bool}) => SOME (length Rs)
| _ => NONE)) Ts,
length Us)) arities)
end;
@@ -632,7 +636,7 @@
val (ts1, ts2) = chop k ts;
val u = list_comb (Const (s, T), ts1);
- fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1)
+ fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
| mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
val module' = if_library thyname module;
@@ -715,7 +719,7 @@
end;
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
- (Const ("Collect", _), [u]) =>
+ (Const (@{const_name Collect}, _), [u]) =>
let val (r, Ts, fs) = HOLogic.strip_psplits u
in case strip_comb r of
(Const (s, T), ts) =>
--- a/src/HOL/Tools/inductive_realizer.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Feb 25 22:32:09 2010 +0100
@@ -21,7 +21,7 @@
[name] => name
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
-val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
+val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
fun prf_of thm =
let
@@ -57,7 +57,7 @@
fun relevant_vars prop = List.foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
- (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
+ (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs
| _ => vs)
| (_, vs) => vs) [] (OldTerm.term_vars prop);
@@ -150,9 +150,10 @@
fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
| is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
- | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
- Const (s, _) => can (Inductive.the_inductive ctxt) s
- | _ => true)
+ | is_meta (Const (@{const_name Trueprop}, _) $ t) =
+ (case head_of t of
+ Const (s, _) => can (Inductive.the_inductive ctxt) s
+ | _ => true)
| is_meta _ = false;
fun fun_of ts rts args used (prem :: prems) =
@@ -174,7 +175,7 @@
(Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
end
else (case strip_type T of
- (Ts, Type ("*", [T1, T2])) =>
+ (Ts, Type (@{type_name "*"}, [T1, T2])) =>
let
val fx = Free (x, Ts ---> T1);
val fr = Free (r, Ts ---> T2);
@@ -211,8 +212,9 @@
let
val fs = map (fn (rule, (ivs, intr)) =>
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
- in if dummy then Const ("HOL.default_class.default",
- HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
+ in
+ if dummy then Const (@{const_name default},
+ HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
else fs
end) (premss ~~ dummies);
val frees = fold Term.add_frees fs [];
@@ -439,7 +441,7 @@
val r = if null Ps then Extraction.nullt
else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
(if dummy then
- [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
+ [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
else []) @
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));
--- a/src/HOL/Tools/inductive_set.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML Thu Feb 25 22:32:09 2010 +0100
@@ -33,10 +33,10 @@
val collect_mem_simproc =
Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
- fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
+ 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 ("op :", _)) $ q $ S' =>
+ (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
(case try (HOLogic.strip_ptuple ps) q of
NONE => NONE
| SOME ts =>
@@ -74,18 +74,20 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
- | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
+ fun mkop @{const_name "op &"} T x =
+ SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+ | mkop @{const_name "op |"} T x =
+ SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
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 ("op :",
+ fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
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 ("op :",
+ | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
mkop s T (m, p, mk_collect p T (head_of u), S)
| decomp _ = NONE;
@@ -263,13 +265,13 @@
fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
case prop_of thm of
- Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
(case body_type T of
- Type ("bool", []) =>
+ @{typ bool} =>
let
val thy = Context.theory_of ctxt;
fun factors_of t fs = case strip_abs_body t of
- Const ("op :", _) $ u $ S =>
+ Const (@{const_name "op :"}, _) $ 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
@@ -279,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 ("op :", _) $ u $ S =>
+ Const (@{const_name "op :"}, _) $ u $ S =>
(strip_comb S, SOME (HOLogic.flat_tuple_paths u))
| _ => error "member symbol on right-hand side expected")
| _ => (strip_comb rhs, NONE))
@@ -412,7 +414,7 @@
val {set_arities, pred_arities, to_pred_simps, ...} =
PredSetConvData.get (Context.Proof lthy);
fun infer (Abs (_, _, t)) = infer t
- | infer (Const ("op :", _) $ t $ u) =
+ | infer (Const (@{const_name "op :"}, _) $ 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/simpdata.ML Thu Feb 25 22:17:33 2010 +0100
+++ b/src/HOL/Tools/simpdata.ML Thu Feb 25 22:32:09 2010 +0100
@@ -10,11 +10,11 @@
structure Quantifier1 = Quantifier1Fun
(struct
(*abstract syntax*)
- fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
+ fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
| dest_eq _ = NONE;
- fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
+ fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
- fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
+ fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
| dest_imp _ = NONE;
val conj = HOLogic.conj
val imp = HOLogic.imp
@@ -43,9 +43,9 @@
fun mk_eq th = case concl_of th
(*expects Trueprop if not == *)
- of Const ("==",_) $ _ $ _ => th
- | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th
- | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI}
+ of Const (@{const_name "=="},_) $ _ $ _ => th
+ | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
+ | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
fun mk_eq_True r =
@@ -57,7 +57,7 @@
fun lift_meta_eq_to_obj_eq i st =
let
- fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
+ fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
| count_imp _ = 0;
val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
in if j = 0 then @{thm meta_eq_to_obj_eq}
@@ -65,7 +65,7 @@
let
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
fun mk_simp_implies Q = fold_rev (fn R => fn S =>
- Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Ps Q
+ Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps Q
val aT = TFree ("'a", HOLogic.typeS);
val x = Free ("x", aT);
val y = Free ("y", aT)
@@ -98,7 +98,7 @@
else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
in
case concl_of thm
- of Const ("Trueprop", _) $ p => (case head_of p
+ of Const (@{const_name Trueprop}, _) $ p => (case head_of p
of Const (a, _) => (case AList.lookup (op =) pairs a
of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
| NONE => [thm])
@@ -159,9 +159,12 @@
(Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
- [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
- ("All", [@{thm spec}]), ("True", []), ("False", []),
- ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
+ [(@{const_name "op -->"}, [@{thm mp}]),
+ (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ (@{const_name All}, [@{thm spec}]),
+ (@{const_name True}, []),
+ (@{const_name False}, []),
+ (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
val HOL_basic_ss =
Simplifier.global_context @{theory} empty_ss