clarified @{const_name} vs. @{const_abbrev};
authorwenzelm
Sat Feb 27 20:57:08 2010 +0100 (2010-02-27 ago)
changeset 35402115a5a95710a
parent 35401 bfcbab8592ba
child 35403 25a67a606782
clarified @{const_name} vs. @{const_abbrev};
src/HOL/Library/Multiset.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Rat.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Feb 27 20:56:03 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Feb 27 20:57:08 2010 +0100
     1.3 @@ -1631,9 +1631,9 @@
     1.4  
     1.5  setup {*
     1.6  let
     1.7 -  fun msetT T = Type ("Multiset.multiset", [T]);
     1.8 +  fun msetT T = Type (@{type_name multiset}, [T]);
     1.9  
    1.10 -  fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
    1.11 +  fun mk_mset T [] = Const (@{const_abbrev Mempty}, msetT T)
    1.12      | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
    1.13      | mk_mset T (x :: xs) =
    1.14            Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
    1.15 @@ -1649,7 +1649,7 @@
    1.16        rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
    1.17  
    1.18    val regroup_munion_conv =
    1.19 -      Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
    1.20 +      Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
    1.21          (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
    1.22  
    1.23    fun unfold_pwleq_tac i =
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Feb 27 20:56:03 2010 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Feb 27 20:57:08 2010 +0100
     2.3 @@ -1016,7 +1016,7 @@
     2.4                (HOLogic.mk_Trueprop (HOLogic.mk_eq
     2.5                  (supp c,
     2.6                   if null dts then HOLogic.mk_set atomT []
     2.7 -                 else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
     2.8 +                 else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
     2.9              (fn _ =>
    2.10                simp_tac (HOL_basic_ss addsimps (supp_def ::
    2.11                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
     3.1 --- a/src/HOL/Rat.thy	Sat Feb 27 20:56:03 2010 +0100
     3.2 +++ b/src/HOL/Rat.thy	Sat Feb 27 20:57:08 2010 +0100
     3.3 @@ -1188,7 +1188,7 @@
     3.4      (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     3.5      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
     3.6      (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
     3.7 -    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
     3.8 +    (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
     3.9  *}
    3.10  
    3.11  lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
     4.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:56:03 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:57:08 2010 +0100
     4.3 @@ -465,7 +465,7 @@
     4.4            (if i < length newTs then HOLogic.true_const
     4.5             else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
     4.6               Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
     4.7 -               Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
     4.8 +               Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
     4.9        end;
    4.10  
    4.11      val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
     5.1 --- a/src/HOL/Tools/Function/function_lib.ML	Sat Feb 27 20:56:03 2010 +0100
     5.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Sat Feb 27 20:57:08 2010 +0100
     5.3 @@ -168,7 +168,7 @@
     5.4  
     5.5  (* instance for unions *)
     5.6  val regroup_union_conv =
     5.7 -  regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
     5.8 +  regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}
     5.9      (map (fn t => t RS eq_reflection)
    5.10        (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
    5.11  
     6.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Feb 27 20:56:03 2010 +0100
     6.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Feb 27 20:57:08 2010 +0100
     6.3 @@ -24,7 +24,7 @@
     6.4    let
     6.5      val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
     6.6      val mlexT = (domT --> HOLogic.natT) --> relT --> relT
     6.7 -    fun mk_ms [] = Const (@{const_name Set.empty}, relT)
     6.8 +    fun mk_ms [] = Const (@{const_abbrev Set.empty}, relT)
     6.9        | mk_ms (f::fs) =
    6.10          Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
    6.11    in
     7.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:56:03 2010 +0100
     7.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:57:08 2010 +0100
     7.3 @@ -286,7 +286,7 @@
     7.4  
     7.5      val relation =
     7.6        if null ineqs
     7.7 -      then Const (@{const_name Set.empty}, fastype_of rel)
     7.8 +      then Const (@{const_abbrev Set.empty}, fastype_of rel)
     7.9        else map mk_compr ineqs
    7.10          |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
    7.11  
    7.12 @@ -321,7 +321,7 @@
    7.13    let
    7.14      val goal =
    7.15        HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
    7.16 -        Const (@{const_name Set.empty}, fastype_of c1))
    7.17 +        Const (@{const_abbrev Set.empty}, fastype_of c1))
    7.18        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    7.19    in
    7.20      case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:56:03 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:57:08 2010 +0100
     8.3 @@ -283,7 +283,7 @@
     8.4      (* bool -> typ -> typ -> (term * term) list -> term *)
     8.5      fun make_set maybe_opt T1 T2 tps =
     8.6        let
     8.7 -        val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
     8.8 +        val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
     8.9          val insert_const = Const (@{const_name insert},
    8.10                                    T1 --> (T1 --> T2) --> T1 --> T2)
    8.11          (* (term * term) list -> term *)
    8.12 @@ -313,7 +313,7 @@
    8.13          val update_const = Const (@{const_name fun_upd},
    8.14                                    (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
    8.15          (* (term * term) list -> term *)
    8.16 -        fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
    8.17 +        fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
    8.18            | aux' ((t1, t2) :: ps) =
    8.19              (case t2 of
    8.20                 Const (@{const_name None}, _) => aux' ps
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Feb 27 20:56:03 2010 +0100
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Feb 27 20:57:08 2010 +0100
     9.3 @@ -2933,7 +2933,7 @@
     9.4              "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
     9.5    in
     9.6      if k = ~1 orelse length ts < k then elems
     9.7 -      else Const (@{const_name Set.union}, setT --> setT --> setT) $ elems $ cont
     9.8 +      else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
     9.9    end;
    9.10  
    9.11  fun values_cmd print_modes param_user_modes options k raw_t state =
    10.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:56:03 2010 +0100
    10.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:57:08 2010 +0100
    10.3 @@ -265,7 +265,7 @@
    10.4    | is_eq _ = false
    10.5  
    10.6  fun mk_rel_compose (trm1, trm2) =
    10.7 -  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
    10.8 +  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
    10.9  
   10.10  fun get_relmap ctxt s =
   10.11  let
    11.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:56:03 2010 +0100
    11.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:57:08 2010 +0100
    11.3 @@ -510,7 +510,7 @@
    11.4  val setup =
    11.5    Attrib.setup @{binding ind_realizer}
    11.6      ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    11.7 -      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
    11.8 +      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
    11.9      "add realizers for inductive set";
   11.10  
   11.11  end;