# HG changeset patch # User wenzelm # Date 1267133529 -3600 # Node ID b8c62d60195c131368e0ae8e12c212dcd0b15598 # Parent 09489d8ffece4bce4c165300eb05b466cdba6831 more antiquotations; diff -r 09489d8ffece -r b8c62d60195c src/HOL/Groups.thy --- 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; ); *} diff -r 09489d8ffece -r b8c62d60195c src/HOL/HOL.thy --- 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); diff -r 09489d8ffece -r b8c62d60195c src/HOL/Orderings.thy --- 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) => diff -r 09489d8ffece -r b8c62d60195c src/HOL/Product_Type.thy --- 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; diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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') []; diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/Datatype/datatype_aux.ML --- 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)); diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/Datatype/datatype_prop.ML --- 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))) diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/Datatype/datatype_realizer.ML --- 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 = diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/inductive.ML --- 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)) diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/inductive_codegen.ML --- 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) => diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/inductive_realizer.ML --- 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)])); diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/inductive_set.ML --- 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; diff -r 09489d8ffece -r b8c62d60195c src/HOL/Tools/simpdata.ML --- 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