tuned const_name antiquotations
authorhaftmann
Fri Sep 18 09:07:50 2009 +0200 (2009-09-18)
changeset 32603e08fdd615333
parent 32602 f2b741473860
child 32604 8b3e2bc91a46
tuned const_name antiquotations
src/HOL/Tools/Function/decompose.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Function/fundef_core.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/float_syntax.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
     1.1 --- a/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 09:07:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 09:07:50 2009 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4        fun prove_chain c1 c2 D =
     1.5            if is_some (Termination.get_chain D c1 c2) then D else
     1.6            let
     1.7 -            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
     1.8 +            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
     1.9                                        Const (@{const_name Set.empty}, fastype_of c1))
    1.10                         |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    1.11  
     2.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 09:07:49 2009 +0200
     2.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 09:07:50 2009 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  fun PROFILE msg = if !profile then timeap_msg msg else I
     2.5  
     2.6  
     2.7 -val acc_const_name = @{const_name "accp"}
     2.8 +val acc_const_name = @{const_name accp}
     2.9  fun mk_acc domT R =
    2.10      Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
    2.11  
     3.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 09:07:49 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 09:07:50 2009 +0200
     3.3 @@ -769,7 +769,7 @@
     3.4        val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
     3.5        val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
     3.6  
     3.7 -      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
     3.8 +      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
     3.9  
    3.10        (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
    3.11        val ihyp = Term.all domT $ Abs ("z", domT,
     4.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 09:07:49 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 09:07:50 2009 +0200
     4.3 @@ -152,7 +152,7 @@
     4.4      end
     4.5  
     4.6  fun mk_wf ctxt R (IndScheme {T, ...}) =
     4.7 -    HOLogic.Trueprop $ (Const (@{const_name "wf"}, mk_relT T --> HOLogic.boolT) $ R)
     4.8 +    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
     4.9  
    4.10  fun mk_ineqs R (IndScheme {T, cases, branches}) =
    4.11      let
     5.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 09:07:49 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 09:07:50 2009 +0200
     5.3 @@ -26,7 +26,7 @@
     5.4          val mlexT = (domT --> HOLogic.natT) --> relT --> relT
     5.5          fun mk_ms [] = Const (@{const_name Set.empty}, relT)
     5.6            | mk_ms (f::fs) = 
     5.7 -            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
     5.8 +            Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
     5.9      in
    5.10          mk_ms mfuns
    5.11      end
     6.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:49 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:50 2009 +0200
     6.3 @@ -22,7 +22,7 @@
     6.4    val description = "Rules that guide the heuristic generation of measure functions"
     6.5  );
     6.6  
     6.7 -fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
     6.8 +fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
     6.9  
    6.10  fun find_measures ctxt T =
    6.11    DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
     7.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 09:07:49 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 09:07:50 2009 +0200
     7.3 @@ -17,22 +17,22 @@
     7.4  
     7.5  (* Sum types *)
     7.6  fun mk_sumT LT RT = Type ("+", [LT, RT])
     7.7 -fun mk_sumcase TL TR T l r = Const (@{const_name "sum.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
     7.8 +fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
     7.9  
    7.10  val App = curry op $
    7.11  
    7.12  fun mk_inj ST n i = 
    7.13      access_top_down 
    7.14      { init = (ST, I : term -> term),
    7.15 -      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
    7.16 -      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i 
    7.17 +      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
    7.18 +      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i 
    7.19      |> snd
    7.20  
    7.21  fun mk_proj ST n i = 
    7.22      access_top_down 
    7.23      { init = (ST, I : term -> term),
    7.24 -      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Datatype.Projl"}, T --> LT)) o proj)),
    7.25 -      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Datatype.Projr"}, T --> RT)) o proj))} n i
    7.26 +      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
    7.27 +      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
    7.28      |> snd
    7.29  
    7.30  fun mk_sumcases T fs =
     8.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:49 2009 +0200
     8.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:50 2009 +0200
     8.3 @@ -81,7 +81,7 @@
     8.4     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
     8.5  | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
     8.6     if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
     8.7 -| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
     8.8 +| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
     8.9     if term_of x aconv y then
    8.10     NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
    8.11  | _ => Nox)
     9.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:49 2009 +0200
     9.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:50 2009 +0200
     9.3 @@ -52,18 +52,18 @@
     9.4  
     9.5  local
     9.6   fun isnum t = case t of 
     9.7 -   Const(@{const_name "HOL.zero"},_) => true
     9.8 - | Const(@{const_name "HOL.one"},_) => true
     9.9 +   Const(@{const_name HOL.zero},_) => true
    9.10 + | Const(@{const_name HOL.one},_) => true
    9.11   | @{term "Suc"}$s => isnum s
    9.12   | @{term "nat"}$s => isnum s
    9.13   | @{term "int"}$s => isnum s
    9.14 - | Const(@{const_name "HOL.uminus"},_)$s => isnum s
    9.15 - | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
    9.16 - | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
    9.17 - | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
    9.18 - | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
    9.19 - | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
    9.20 - | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
    9.21 + | Const(@{const_name HOL.uminus},_)$s => isnum s
    9.22 + | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
    9.23 + | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
    9.24 + | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
    9.25 + | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
    9.26 + | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
    9.27 + | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    9.28   | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
    9.29  
    9.30   fun ty cts t = 
    10.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 09:07:49 2009 +0200
    10.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 09:07:50 2009 +0200
    10.3 @@ -29,8 +29,8 @@
    10.4              @{const_name "op -->"}, @{const_name "op ="}] s
    10.5         then binop_conv (conv env) p 
    10.6         else atcv env p
    10.7 -  | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
    10.8 -  | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
    10.9 +  | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
   10.10 +  | Const(@{const_name Ex},_)$Abs(s,_,_) =>
   10.11      let
   10.12       val (e,p0) = Thm.dest_comb p
   10.13       val (x,p') = Thm.dest_abs (SOME s) p0
   10.14 @@ -41,8 +41,8 @@
   10.15       val (l,r) = Thm.dest_equals (cprop_of th')
   10.16      in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
   10.17         else Thm.transitive (Thm.transitive th th') (conv env r) end
   10.18 -  | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
   10.19 -  | Const(@{const_name "All"},_)$_ =>
   10.20 +  | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
   10.21 +  | Const(@{const_name All},_)$_ =>
   10.22      let
   10.23       val p = Thm.dest_arg p
   10.24       val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    11.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 09:07:49 2009 +0200
    11.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 09:07:50 2009 +0200
    11.3 @@ -456,7 +456,7 @@
    11.4  fun is_cong thm =
    11.5    case (Thm.prop_of thm)
    11.6       of (Const("==>",_)$(Const("Trueprop",_)$ _) $
    11.7 -         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
    11.8 +         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
    11.9        | _ => true;
   11.10  
   11.11  
   11.12 @@ -659,7 +659,7 @@
   11.13    end;
   11.14  
   11.15  fun restricted t = isSome (S.find_term
   11.16 -                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
   11.17 +                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
   11.18                              t)
   11.19  
   11.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
    12.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 09:07:49 2009 +0200
    12.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 09:07:50 2009 +0200
    12.3 @@ -398,7 +398,7 @@
    12.4          end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
    12.5     else raise USYN_ERR "dest_relation" "not a boolean term";
    12.6  
    12.7 -fun is_WFR (Const(@{const_name "Wellfounded.wf"},_)$_) = true
    12.8 +fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
    12.9    | is_WFR _                 = false;
   12.10  
   12.11  fun ARB ty = mk_select{Bvar=Free("v",ty),
    13.1 --- a/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:49 2009 +0200
    13.2 +++ b/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:50 2009 +0200
    13.3 @@ -27,10 +27,10 @@
    13.4  fun mk_frac str =
    13.5    let
    13.6      val {mant=i, exp = n} = Syntax.read_float str;
    13.7 -    val exp = Syntax.const @{const_name "Power.power"};
    13.8 +    val exp = Syntax.const @{const_name Power.power};
    13.9      val ten = mk_number 10;
   13.10      val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
   13.11 -  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
   13.12 +  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
   13.13  in
   13.14  
   13.15  fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
    14.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:49 2009 +0200
    14.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 18 09:07:50 2009 +0200
    14.3 @@ -74,8 +74,8 @@
    14.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    14.5            (p (fold (Logic.all o Var) vs t) f)
    14.6          end;
    14.7 -      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
    14.8 -        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
    14.9 +      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
   14.10 +        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
   14.11          | mkop _ _ _ = NONE;
   14.12        fun mk_collect p T t =
   14.13          let val U = HOLogic.dest_setT T
    15.1 --- a/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:49 2009 +0200
    15.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Sep 18 09:07:50 2009 +0200
    15.3 @@ -49,13 +49,13 @@
    15.4    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    15.5    proc = proc1, identifier = []};
    15.6  
    15.7 -fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
    15.8 -  | check (Const (@{const_name "HOL.one"}, _)) = true
    15.9 +fun check (Const (@{const_name HOL.one}, @{typ int})) = false
   15.10 +  | check (Const (@{const_name HOL.one}, _)) = true
   15.11    | check (Const (s, _)) = member (op =) [@{const_name "op ="},
   15.12 -      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
   15.13 -      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
   15.14 -      @{const_name "HOL.zero"},
   15.15 -      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
   15.16 +      @{const_name HOL.times}, @{const_name HOL.uminus},
   15.17 +      @{const_name HOL.minus}, @{const_name HOL.plus},
   15.18 +      @{const_name HOL.zero},
   15.19 +      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   15.20    | check (a $ b) = check a andalso check b
   15.21    | check _ = false;
   15.22  
    16.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Sep 18 09:07:49 2009 +0200
    16.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Sep 18 09:07:50 2009 +0200
    16.3 @@ -51,7 +51,7 @@
    16.4      atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
    16.5    | _ => [thm];
    16.6  
    16.7 -fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
    16.8 +fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
    16.9    | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   16.10    | neg_prop t = raise TERM ("neg_prop", [t]);
   16.11