gen_rem(s) abandoned in favour of remove / subtract
authorhaftmann
Tue Oct 10 13:59:13 2006 +0200 (2006-10-10)
changeset 20951868120282837
parent 20950 981fa0ce23ed
child 20952 070d176a8e2d
gen_rem(s) abandoned in favour of remove / subtract
NEWS
TFL/rules.ML
TFL/tfl.ML
src/FOLP/simp.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/EfficientNat.thy
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/locale.ML
src/Pure/Syntax/parser.ML
src/Pure/library.ML
src/Pure/proof_general.ML
src/Pure/type.ML
src/Sequents/prover.ML
     1.1 --- a/NEWS	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/NEWS	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -632,6 +632,14 @@
     1.4  
     1.5  * Pure/library:
     1.6  
     1.7 +gen_rem(s) abandoned in favour of remove / subtract.
     1.8 +INCOMPATIBILITY:
     1.9 +rewrite "gen_rem eq (xs, x)" to "remove (eq o swap) x xs"
    1.10 +rewrite "gen_rems eq (xs, ys)" to "subtract (eq o swap) ys xs"
    1.11 +drop "swap" if "eq" is symmetric.
    1.12 +
    1.13 +* Pure/library:
    1.14 +
    1.15  infixes ins ins_string ins_int have been abandoned in favour of insert.
    1.16  INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs"
    1.17  
     2.1 --- a/TFL/rules.ML	Tue Oct 10 13:59:12 2006 +0200
     2.2 +++ b/TFL/rules.ML	Tue Oct 10 13:59:13 2006 +0200
     2.3 @@ -763,8 +763,8 @@
     2.4                val dummy = print_thms "cntxt:" cntxt
     2.5                val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
     2.6                     sign,...} = rep_thm thm
     2.7 -              fun genl tm = let val vlist = gen_rems (op aconv)
     2.8 -                                           (add_term_frees(tm,[]), globals)
     2.9 +              fun genl tm = let val vlist = subtract (op aconv) globals
    2.10 +                                           (add_term_frees(tm,[]))
    2.11                              in fold_rev Forall vlist tm
    2.12                              end
    2.13                (*--------------------------------------------------------------
     3.1 --- a/TFL/tfl.ML	Tue Oct 10 13:59:12 2006 +0200
     3.2 +++ b/TFL/tfl.ML	Tue Oct 10 13:59:13 2006 +0200
     3.3 @@ -767,7 +767,7 @@
     3.4                of [] => (P_y, (tm,[]))
     3.5                 | _  => let
     3.6                      val imp = S.list_mk_conj cntxt ==> P_y
     3.7 -                    val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
     3.8 +                    val lvs = subtract (op aconv) globals (S.free_vars_lr imp)
     3.9                      val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
    3.10                      in (S.list_mk_forall(locals,imp), (tm,locals)) end
    3.11           end
    3.12 @@ -994,7 +994,7 @@
    3.13     fun loop ([],extras,R,ind) = (rev R, ind, extras)
    3.14       | loop ((r,ftcs)::rst, nthms, R, ind) =
    3.15          let val tcs = #1(strip_imp (concl r))
    3.16 -            val extra_tcs = gen_rems (op aconv) (ftcs, tcs)
    3.17 +            val extra_tcs = subtract (op aconv) tcs ftcs
    3.18              val extra_tc_thms = map simplify_nested_tc extra_tcs
    3.19              val (r1,ind1) = fold simplify_tc tcs (r,ind)
    3.20              val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
     4.1 --- a/src/FOLP/simp.ML	Tue Oct 10 13:59:12 2006 +0200
     4.2 +++ b/src/FOLP/simp.ML	Tue Oct 10 13:59:13 2006 +0200
     4.3 @@ -282,7 +282,7 @@
     4.4  val delete_thms = foldr delete_thm_warn;
     4.5  
     4.6  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
     4.7 -let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
     4.8 +let val congs' = fold (remove Drule.eq_thm_prop) thms congs
     4.9  in SS{auto_tac=auto_tac, congs= congs',
    4.10        cong_net= delete_thms cong_net (map mk_trans thms),
    4.11        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
     5.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 10 13:59:12 2006 +0200
     5.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 10 13:59:13 2006 +0200
     5.3 @@ -270,7 +270,7 @@
     5.4  	val cU = ctyp_of sg U
     5.5  	val tfrees = add_term_tfrees (prop_of thm,[])
     5.6  	val (rens, thm') = Thm.varifyT'
     5.7 -    (gen_rem (op = o apfst fst) (tfrees, name)) thm
     5.8 +    (remove (op = o apsnd fst) name tfrees) thm
     5.9  	val mid = 
    5.10  	    case rens of
    5.11  		[] => thm'
     6.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Oct 10 13:59:12 2006 +0200
     6.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Oct 10 13:59:13 2006 +0200
     6.3 @@ -258,7 +258,7 @@
     6.4              [] => NONE
     6.5            | thps =>
     6.6                let val (ths1, ths2) = split_list thps
     6.7 -              in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end
     6.8 +              in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
     6.9        end
    6.10    in
    6.11      case get_first mk_thms eqs of
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 10 13:59:12 2006 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 10 13:59:13 2006 +0200
     7.3 @@ -262,7 +262,7 @@
     7.4      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
     7.5      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
     7.6      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
     7.7 -    val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
     7.8 +    val rs = subtract (op = o pairself fst) xs rlzvs;
     7.9  
    7.10      fun mk_prf _ [] prf = prf
    7.11        | mk_prf rs ((prem, rprem) :: prems) prf =
     8.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 10 13:59:12 2006 +0200
     8.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 10 13:59:13 2006 +0200
     8.3 @@ -56,7 +56,7 @@
     8.4    in case Symtab.lookup tab s of
     8.5        NONE => thy
     8.6      | SOME thms =>
     8.7 -        RecCodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
     8.8 +        RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
     8.9    end handle TERM _ => (warn thm; thy);
    8.10  
    8.11  val del = Thm.declaration_attribute
     9.1 --- a/src/HOL/Tools/record_package.ML	Tue Oct 10 13:59:12 2006 +0200
     9.2 +++ b/src/HOL/Tools/record_package.ML	Tue Oct 10 13:59:13 2006 +0200
     9.3 @@ -2078,7 +2078,7 @@
     9.4        | dups => ["Duplicate parameter(s) " ^ commas dups]);
     9.5  
     9.6      val err_extra_frees =
     9.7 -      (case gen_rems (op =) (envir_names, params) of
     9.8 +      (case subtract (op =) params envir_names of
     9.9          [] => []
    9.10        | extras => ["Extra free type variable(s) " ^ commas extras]);
    9.11  
    10.1 --- a/src/Pure/Isar/locale.ML	Tue Oct 10 13:59:12 2006 +0200
    10.2 +++ b/src/Pure/Isar/locale.ML	Tue Oct 10 13:59:13 2006 +0200
    10.3 @@ -851,7 +851,7 @@
    10.4      val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
    10.5      (* compute identifiers and syntax, merge with previous ones *)
    10.6      val (ids, _) = identify true expr;
    10.7 -    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
    10.8 +    val idents = subtract (eq_fst (op =)) prev_idents ids;
    10.9      val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   10.10      (* type-instantiate elements *)
   10.11      val final_elemss = map (eval all_params tenv syntax) idents;
    11.1 --- a/src/Pure/Syntax/parser.ML	Tue Oct 10 13:59:12 2006 +0200
    11.2 +++ b/src/Pure/Syntax/parser.ML	Tue Oct 10 13:59:13 2006 +0200
    11.3 @@ -259,7 +259,7 @@
    11.4                let
    11.5                  val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
    11.6  
    11.7 -                val new_tks = gen_rems matching_tokens (start_tks, old_tks);
    11.8 +                val new_tks = subtract matching_tokens old_tks start_tks;
    11.9  
   11.10                  (*store new production*)
   11.11                  fun store [] prods is_new =
   11.12 @@ -370,7 +370,7 @@
   11.13                          |> (K (key = SOME UnknownStart)) ? AList.update (op =) (key, tk_prods')
   11.14  
   11.15                        val added_tks =
   11.16 -                        gen_rems matching_tokens (new_tks, old_tks);
   11.17 +                        subtract matching_tokens old_tks new_tks;
   11.18                      in if null added_tks then
   11.19                           (Array.update (prods, nt, (lookahead, nt_prods'));
   11.20                            process_nts nts added)
    12.1 --- a/src/Pure/library.ML	Tue Oct 10 13:59:12 2006 +0200
    12.2 +++ b/src/Pure/library.ML	Tue Oct 10 13:59:13 2006 +0200
    12.3 @@ -219,8 +219,6 @@
    12.4    val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    12.5    val \ : ''a list * ''a -> ''a list
    12.6    val \\ : ''a list * ''a list -> ''a list
    12.7 -  val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
    12.8 -  val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    12.9    val findrep: ''a list -> ''a list
   12.10    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   12.11    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   12.12 @@ -1035,12 +1033,8 @@
   12.13  (*removing an element from a list WITHOUT duplicates*)
   12.14  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   12.15    | [] \ x = [];
   12.16 -
   12.17  fun ys \\ xs = foldl (op \) (ys,xs);
   12.18  
   12.19 -(*removing an element from a list -- possibly WITH duplicates*)
   12.20 -fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   12.21 -fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
   12.22  
   12.23  (*returns the tail beginning with the first repeated element, or []*)
   12.24  fun findrep [] = []
   12.25 @@ -1079,10 +1073,10 @@
   12.26  
   12.27  fun gen_merge_lists _ xs [] = xs
   12.28    | gen_merge_lists _ [] ys = ys
   12.29 -  | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
   12.30 +  | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   12.31  
   12.32  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
   12.33 -fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
   12.34 +fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
   12.35  
   12.36  
   12.37  (** balanced trees **)
    13.1 --- a/src/Pure/proof_general.ML	Tue Oct 10 13:59:12 2006 +0200
    13.2 +++ b/src/Pure/proof_general.ML	Tue Oct 10 13:59:13 2006 +0200
    13.3 @@ -385,7 +385,7 @@
    13.4  
    13.5  fun add_master_files name files =
    13.6    let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
    13.7 -  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
    13.8 +  in masters @ subtract (op = o pairself Path.base) masters files end;
    13.9  
   13.10  fun trace_action action name =
   13.11    if action = ThyInfo.Update then
    14.1 --- a/src/Pure/type.ML	Tue Oct 10 13:59:12 2006 +0200
    14.2 +++ b/src/Pure/type.ML	Tue Oct 10 13:59:13 2006 +0200
    14.3 @@ -552,7 +552,7 @@
    14.4      (case duplicates (op =) vs of
    14.5        [] => []
    14.6      | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
    14.7 -    (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
    14.8 +    (case subtract (op =) vs (map (#1 o #1) (typ_tvars rhs')) of
    14.9        [] => []
   14.10      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   14.11      types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
    15.1 --- a/src/Sequents/prover.ML	Tue Oct 10 13:59:12 2006 +0200
    15.2 +++ b/src/Sequents/prover.ML	Tue Oct 10 13:59:13 2006 +0200
    15.3 @@ -33,14 +33,14 @@
    15.4  
    15.5  fun (Pack(safes,unsafes)) add_safes ths   = 
    15.6      let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
    15.7 -	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
    15.8 +	val ths' = subtract Drule.eq_thm_prop dups ths
    15.9      in
   15.10          Pack(sort (make_ord less) (ths'@safes), unsafes)
   15.11      end;
   15.12  
   15.13  fun (Pack(safes,unsafes)) add_unsafes ths = 
   15.14      let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
   15.15 -	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
   15.16 +	val ths' = subtract Drule.eq_thm_prop dups ths
   15.17      in
   15.18  	Pack(safes, sort (make_ord less) (ths'@unsafes))
   15.19      end;