constant op @ now named append
authorhaftmann
Sat May 19 11:33:57 2007 +0200 (2007-05-19)
changeset 2302979ee75dc1e59
parent 23028 d8c4a02e992a
child 23030 c7ff1537c4bf
constant op @ now named append
NEWS
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/HOL/list.imp
src/HOL/Induct/SList.thy
src/HOL/List.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/NEWS	Sat May 19 11:33:34 2007 +0200
     1.2 +++ b/NEWS	Sat May 19 11:33:57 2007 +0200
     1.3 @@ -530,6 +530,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* constant "List.op @" now named "List.append".  Use ML antiquotations
     1.8 +@{const_name List.append} or @{term " ... @ ... "} to circumvent
     1.9 +possible incompatibilities when working on ML level.
    1.10 +
    1.11  * Constant renames due to introduction of canonical name prefixing for
    1.12    class package:
    1.13  
     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat May 19 11:33:34 2007 +0200
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat May 19 11:33:57 2007 +0200
     2.3 @@ -235,7 +235,7 @@
     2.4    REVERSE   > List.rev
     2.5    LAST      > List.last
     2.6    FRONT     > List.butlast
     2.7 -  APPEND    > "List.op @"
     2.8 +  APPEND    > List.append
     2.9    FLAT      > List.concat
    2.10    LENGTH    > Nat.size
    2.11    REPLICATE > List.replicate
     3.1 --- a/src/HOL/Import/HOL/list.imp	Sat May 19 11:33:34 2007 +0200
     3.2 +++ b/src/HOL/Import/HOL/list.imp	Sat May 19 11:33:57 2007 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4    "EXISTS" > "HOL4Compat.list_exists"
     3.5    "EVERY" > "List.list_all"
     3.6    "CONS" > "List.list.Cons"
     3.7 -  "APPEND" > "List.op @"
     3.8 +  "APPEND" > "List.append"
     3.9  
    3.10  thm_maps
    3.11    "list_size_def" > "HOL4Compat.list_size_def"
     4.1 --- a/src/HOL/Induct/SList.thy	Sat May 19 11:33:34 2007 +0200
     4.2 +++ b/src/HOL/Induct/SList.thy	Sat May 19 11:33:57 2007 +0200
     4.3 @@ -159,6 +159,10 @@
     4.4    map       :: "('a=>'b) => ('a list => 'b list)" where
     4.5    "map f xs = list_rec xs [] (%x l r. f(x)#r)"
     4.6  
     4.7 +no_syntax
     4.8 +  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
     4.9 +hide const "List.append"
    4.10 +
    4.11  definition
    4.12    append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65) where
    4.13    "xs@ys = list_rec xs ys (%x l r. x#r)"
     5.1 --- a/src/HOL/List.thy	Sat May 19 11:33:34 2007 +0200
     5.2 +++ b/src/HOL/List.thy	Sat May 19 11:33:57 2007 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  subsection{*Basic list processing functions*}
     5.5  
     5.6  consts
     5.7 -  "@" :: "'a list => 'a list => 'a list"    (infixr 65)
     5.8 +  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
     5.9    filter:: "('a => bool) => 'a list => 'a list"
    5.10    concat:: "'a list list => 'a list"
    5.11    foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
    5.12 @@ -309,7 +309,7 @@
    5.13  
    5.14  fun len (Const("List.list.Nil",_)) acc = acc
    5.15    | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
    5.16 -  | len (Const("List.op @",_) $ xs $ ys) acc = len xs (len ys acc)
    5.17 +  | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
    5.18    | len (Const("List.rev",_) $ xs) acc = len xs acc
    5.19    | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
    5.20    | len t (ts,n) = (t::ts,n);
    5.21 @@ -447,7 +447,7 @@
    5.22  
    5.23  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    5.24    (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    5.25 -  | last (Const("List.op @",_) $ _ $ ys) = last ys
    5.26 +  | last (Const("List.append",_) $ _ $ ys) = last ys
    5.27    | last t = t;
    5.28  
    5.29  fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
    5.30 @@ -455,7 +455,7 @@
    5.31  
    5.32  fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
    5.33    (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    5.34 -  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    5.35 +  | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
    5.36    | butlast xs = Const("List.list.Nil",fastype_of xs);
    5.37  
    5.38  val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
    5.39 @@ -469,7 +469,7 @@
    5.40          val lhs1 = butlast lhs and rhs1 = butlast rhs;
    5.41          val Type(_,listT::_) = eqT
    5.42          val appT = [listT,listT] ---> listT
    5.43 -        val app = Const("List.op @",appT)
    5.44 +        val app = Const("List.append",appT)
    5.45          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    5.46          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    5.47          val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
     6.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:34 2007 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:57 2007 +0200
     6.3 @@ -204,7 +204,7 @@
     6.4            val pi2 = Free ("pi2", mk_permT T);
     6.5            val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
     6.6            val cnil  = Const ("List.list.Nil", mk_permT T);
     6.7 -          val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
     6.8 +          val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
     6.9            val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
    6.10            (* nil axiom *)
    6.11            val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
     7.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat May 19 11:33:34 2007 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat May 19 11:33:57 2007 +0200
     7.3 @@ -206,7 +206,7 @@
     7.4  val fresh_def = thm "fresh_def";
     7.5  val supp_def = thm "supp_def";
     7.6  val rev_simps = thms "rev.simps";
     7.7 -val app_simps = thms "op @.simps";
     7.8 +val app_simps = thms "append.simps";
     7.9  
    7.10  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    7.11  
    7.12 @@ -402,7 +402,7 @@
    7.13                  (map (fn ((s, T), x) =>
    7.14                      let val perm = Const (s, permT --> T --> T)
    7.15                      in HOLogic.mk_eq
    7.16 -                      (perm $ (Const ("List.op @", permT --> permT --> permT) $
    7.17 +                      (perm $ (Const ("List.append", permT --> permT --> permT) $
    7.18                           pi1 $ pi2) $ Free (x, T),
    7.19                         perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
    7.20                      end)
     8.1 --- a/src/HOL/Tools/refute.ML	Sat May 19 11:33:34 2007 +0200
     8.2 +++ b/src/HOL/Tools/refute.ML	Sat May 19 11:33:57 2007 +0200
     8.3 @@ -704,7 +704,7 @@
     8.4          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
     8.5        | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
     8.6          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
     8.7 -      | Const ("List.op @", _)          => t
     8.8 +      | Const ("List.append", _)          => t
     8.9        | Const ("Lfp.lfp", _)            => t
    8.10        | Const ("Gfp.gfp", _)            => t
    8.11        | Const ("fst", _)                => t
    8.12 @@ -895,7 +895,7 @@
    8.13        | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
    8.14          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    8.15            collect_type_axioms (axs, T)
    8.16 -      | Const ("List.op @", T)          => collect_type_axioms (axs, T)
    8.17 +      | Const ("List.append", T)          => collect_type_axioms (axs, T)
    8.18        | Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
    8.19        | Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
    8.20        | Const ("fst", T)                => collect_type_axioms (axs, T)
    8.21 @@ -2727,13 +2727,13 @@
    8.22    (* theory -> model -> arguments -> Term.term ->
    8.23      (interpretation * model * arguments) option *)
    8.24  
    8.25 -  (* only an optimization: 'op @' could in principle be interpreted with *)
    8.26 +  (* only an optimization: 'append' could in principle be interpreted with *)
    8.27    (* interpreters available already (using its definition), but the code *)
    8.28    (* below is more efficient                                             *)
    8.29  
    8.30    fun List_append_interpreter thy model args t =
    8.31      case t of
    8.32 -      Const ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun",
    8.33 +      Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun",
    8.34          [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
    8.35        let
    8.36          val (i_elem, _, _) = interpret thy model
    8.37 @@ -3215,7 +3215,7 @@
    8.38       add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
    8.39       add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
    8.40       add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
    8.41 -     add_interpreter "List.op @" List_append_interpreter #>
    8.42 +     add_interpreter "List.append" List_append_interpreter #>
    8.43       add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
    8.44       add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
    8.45       add_interpreter "fst" Product_Type_fst_interpreter #>
     9.1 --- a/src/HOL/Tools/res_clause.ML	Sat May 19 11:33:34 2007 +0200
     9.2 +++ b/src/HOL/Tools/res_clause.ML	Sat May 19 11:33:57 2007 +0200
     9.3 @@ -117,7 +117,7 @@
     9.4  		   ("op :", "in"),
     9.5  		   ("op Un", "union"),
     9.6  		   ("op Int", "inter"),
     9.7 -		   ("List.op @", "append"),
     9.8 +		   ("List.append", "append"),
     9.9  		   ("ATP_Linkup.fequal", "fequal"),
    9.10  		   ("ATP_Linkup.COMBI", "COMBI"),
    9.11  		   ("ATP_Linkup.COMBK", "COMBK"),